Modal Logic for Coalgebras 

Martin R¨oßiger 
Technische Universit¨at Dresden 
Institut f¨ur Algebra 
D -- 01062 Dresden, Germany 
http://www.math.tu­dresden.de/~roessig 

Abstract: Coalgebras are of growing importance in theoretical computer 
science. A major reason is that they model a great variety of dynamic 
systems. Thus, they provide an excellent opportunity for a unified 
view on these systems. As a consequence, it is significant to develop 
languages for coalgebras. Such languages could, for instance, be used 
to specify and verify systems that are modelled with coalgebras. 
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. We consider coalgebras of so­called 
Kripke­polynomial functors on the category Set. Such functors are 
inductively constructed from constant functors and the identity func­ 
tor using product, coproduct, exponentiation by a set, and the power 
set functor. Kripke­structures turn out to be a special case. 
We show how to develop a finitary modal language L F for a given 
Kripke­polynomial functor F. Models of L F are the corresponding 
F­coalgebras. In case of Kripke­structures we obtain the ``usual'' 
finitary modal logic. 

For so­called image­finite F­coalgebras, the language L F is ex­ 
pressive enough to distinguish elements up to bisimilarity, i.e. logical 
equivalence coincides with bisimilarity. This result even hold for a 
slightly restricted language. Moreover, we also give a complete 
calculus for L F in case the constants occuring in F are finite. 
The key method for this approach is to use a twofold induction 
where the ``outer'' one runs on the structure of formulas and the 
``inner'' one on the structure of the functor.