Specifying coalgebras with modal logic (Q5941162)

We propose to use modal logic as a logic for coalgebras and discuss it in view of the work done on coalgebras as a semantics of object-oriented programming. Two approaches are taken: First, standard concepts of modal logic are applied to coalgebras. For a certain kind of functor it is shown that the logic exactly captures the notion of bisimulation and a complete calculus is given. Examples of verifications of object properties are given. Second, we discuss the relationship of this approach with the coalgebraic logic of \textit{L. S. Moss} [Coalgebraic logic, Ann Pure Appl. Logic 96, 277-317 (1999; Zbl 0969.03026)].