Coalgebraic modal logic of finite rank
This paper studies coalgebras from the perspective of finite observations. We introduce the notion of finite step equivalence and a corresponding category with finite step equivalence-preserving morphisms. This category always has a final object, which generalises the canonical model construction from Kripke models to coalgebras. We then turn to logics whose formulae are invariant under finite step equivalence, which we call logics of rank $omega$. For these logics, we use topological methods and give a characterisation of compact logics and definable classes of models.
|Specifying and Verifying and Reasoning about Programs (acm F.3.1), Software/Program Verification (acm D.2.4)|
|Modal logic (including the logic of norms) (msc 03B45)|
|Software (theme 1)|
|Software Engineering [SEN]|
Kurz, A, & Pattinson, D. (2002). Coalgebraic modal logic of finite rank. Software Engineering [SEN]. CWI.