Final coalgebras and the Hennessy-Milner property (Q2576941)

In recent years it has turned out that many notions in theoretical computer science can be modeled by category theory or logic (the latter being in some sense equivalent, since a particular logical theory can be considered in many cases to be a ``presentation'' of some category [cf., e.g., \textit{M. Makkai} and \textit{G. E. Reyes}, First order categorical logic. Lect. Notes Math. 611. Berlin: Springer (1977; Zbl 0357.18002)]. In particular coalgebras of functors \(T : \mathbf{Set} {\rightarrow} \text\textbf{Set}\) on the category of sets are useful in modelling notions associated with data structures, transition systems and process algebras. The notion of \textit{final} coalgebra is particularly useful since its members represent all possible behaviours of processes. The paper under review attempts to answer the following question: When can logic be used to construct a final object in the category of coalgebras of some functor \(T : \mathbf{Set} {\rightarrow} \text\textbf{Set}\)? More precisely the author claims to prove that a final \(T\)-coalgebra exists if there exists a logic with the property of having a set of formulas that differentiates coalgebraic elements up to bisimilarity. Conversely, the existence of a final coalgebra implies the existence of a logical system with this property, provided that the bisimilarity relation between coalgebraic states is transitive, This property holds in any process-algebraic context for which bisimilarity means observational (or behavioural) indistinguishability. Section 2 reviews the basic theory of coalgebras and bisimulations to be considered. Section 3 discusses the construction of simple coalgebras by the theory of congruences and explains their relation to to coinductive coalgebras. Section 4 formulates the notion of a logic for coalgebras and gives the main result characterizing the existence of final coalgebras. Section 5 gives a formulation for the case that bisimilarity is not transitive.