Compositionality in Logics for Coalgebras

The coalgebraic approach to modelling state-based systems allows system combinations to be modelled at the level of coalgebraic signatures using operations such as functor composition, product or coproduct. We show that this compositionality at the level of signatures can be lifted to a logical level, thereby allowing the derivation of logics for coalgebras of functor combinations from logics for coalgebras of the functors being combined. The key idea is to capture one inductive step in the definition of a language for coalgebras, using a notion of language constructor. Then, successive applications of language constructors yield languages for coalgebras, whose expressiveness w.r.t. bisimulation or some given notion of simulation follows from an expressiveness condition on the underlying language constructor. Moreover, operations on signature functors lift to (expressiveness-preserving) operations on language constructors, ultimately yielding expressive logics for combined coalgebraic types. A similar approach can be used to derive sound and complete proof systems for coalgebraic logics in a modular fashion.  

hosted by