Reference Modal Logics are Coalgebraic [cirsea-etal-modal-logic]

  • January 1, 2011
  • Corina Cîrstea, Alexander Kurz, Dirk Pattinson, Lutz Schröder, Yde Venema
  • 10.1093/comjnl/bxp004

Abstract

  • January 1, 2011
  • Corina Cîrstea, Alexander Kurz, Dirk Pattinson, Lutz Schröder, Yde Venema

Applications of modal logics are abundant in computer science, and a large number of structurally different modal logics have been successfully employed in a diverse spectrum of application contexts. Coalgebraic semantics, on the other hand, provides a uniform and encompassing view on the large variety of specific logics used in particular domains. The coalgebraic approach is generic and compositional: tools and techniques simultaneously apply to a large class of application areas and can, moreover, be combined in a modular way. In particular, this facilitates a pick-and-choose approach to domain-specific formalisms, applicable across the entire scope of application areas, leading to generic software tools that are easier to design, to implement and to maintain. This paper substantiates the authors’ firm belief that the systematic exploitation of the coalgebraic nature of modal logic will not only have impact on the field of modal logic itself but also lead to significant progress in a number of areas within computer science, such as knowledge representation and concurrency/mobility. 

 @article
{Cîrstea_Kurz_Pattinson_Schröder_Venema_2011, title={Modal Logics are Coalgebraic}, volume={54}, ISSN={0010-4620}, DOI={10.1093/comjnl/bxp004}, number={1}, journal={The Computer Journal}, author={Cîrstea, Corina and Kurz, Alexander and Pattinson, Dirk and Schröder, Lutz and Venema, Yde}, year={2011}, month={Jan}, pages={31–41} }

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.