Coalgebras and Modal Logic
Martin Rößiger · Electronic Notes in Theoretical Computer Science · 2000
Coalgebras are of growing importance in theoretical computer science. To develop languages for them is significant for the specification and verification of systems. Modal logic has proved to be suitable for this purpose. So far, most approaches have presented a language to describe only deterministic coalgebras. The present paper introduces a generalization that also covers non-deterministic systems. Models for our modal language are F-coalgebras where the functor F is inductively constructed from constant sets and the identity functor using product, coproduct, exponentiation, and the power set functor. Thus, Kripke-structures constitute a special case. First we introduce a language that is based on a multisorted modal setting: here the sorts are given by the subfunctors of F. Then we consider a restricted language that still has the same expressiveness. It turns out that, for the case of Kripke-structures, the obtained language is equivalent to the “usual” modal logic for these structures. Hence this approach actually constitutes a bridge between modal languages for coalgebras and the modal logic for Kripke-structures. A well-known result from modal logic can be transfered to our setting: for so-called image-finite coalgebras bisimilarity coincides with logical equivalence. Finally, we present a sound and complete deduction calculus in case the constants in F are finite.