Reference Coalgebraic semantics of modal logics: An overview [kupke-pattinson-modal-2011]

Abstract

  • September 2, 2011
  • Clemens Kupke, Dirk Pattinson

Coalgebras can be seen as a natural abstraction of Kripke frames. In the same sense, coalgebraic logics are generalised modal logics. In this paper, we give an overview of the basic tools, techniques and results that connect coalgebras and modal logic. We argue that coalgebras unify the semantics of a large range of different modal logics (such as probabilistic, graded, relational, conditional) and discuss unifying approaches to reasoning at this level of generality. We review languages defined in terms of the so-called cover modality, languages induced by predicate liftings as well as their common categorical abstraction, and present (abstract) results on completeness, expressiveness and complexity in these settings, both for basic languages as well as a number of extensions, such as hybrid languages and fixpoints. 

 @article
{Kupke_Pattinson_2011, series={CMCS Tenth Anniversary Meeting}, title={Coalgebraic semantics of modal logics: An overview}, volume={412}, ISSN={0304-3975}, DOI={10.1016/j.tcs.2011.04.023}, number={38}, journal={Theoretical Computer Science}, author={Kupke, Clemens and Pattinson, Dirk}, year={2011}, month={Sept}, pages={5070–5094}, collection={CMCS Tenth Anniversary Meeting} }

Backlinks

Modal logics and coalgebra [lcc-003G]

Let T: X \to \Delta (X) be a (discrete) stochastic dynamical system. Then for each \epsilon , we obtain an operator \diamond _\epsilon : P(X) \to P(X), where \diamond _\epsilon (\phi )(x) if P_{x' \sim Tx}(\phi (x')) \geq \epsilon . But where do these come from?

Clearly, one step is to take a property of distributions on X ("the probability of \phi is at least \epsilon ) and pull it back to a property of points in X via the map P(T): P(X) \leftarrow P(\Delta (X)), given by the contravariant powerset functor. The other step involves building a map [0,1] \times PX \to P(\Delta (X)). This is a sort of distributive law-type deal between the functor [0,1] and \Delta (X) (and P).

Conceptually, defining a modal logic means giving P(X) some sort of algebra structure, which is naturally dual to the coalgebra structure of X - and this is logical, since P is contravariant. The question is the relationship between the functor (or monad) of the algebra and the functor (or comonad) of the coalgebra.

For example, consider T: X \to X^A, a transition system with input alphabet A. Note that P(X^A) = 2^{X^A}. There is a natural evaluation map X^A \times A \to X, which induces (2^{X^A})^A = 2^{X^A \times A} \leftarrow 2^X, which is then mated to a map 2^X \times A \to 2^{X^A}, or in other words P(X) \times A \to P(X^A), taking \phi , a to the proposition "f(a) satisfies \phi ". Applying this to T gives you the modality \diamond _a(\phi ), meaning "if the next input is a, then \phi will hold after the next step".

There is a duality between coalgebraic modal logic in this sense (expressing subsets of the state space) and categorical universal algebra (which reasons about equations, i.e equivalence relations on, or quotients of, the algebra in question).

One can ask how to apply this idea to the dynamical systems of Categorical Systems Theory, which are not directly coalgebras, and where, crucially, the set of input/output trajectories (which is the cofree coalgebra) is much more complicated, and problematic to define in general.

Read: Modal Logics are Coalgebraic, Coalgebraic semantics of modal logics: An overview.