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.