A finite model construction for coalgebraic modal logic (Q2643335)

This paper extends previous results in the theory of coalgebraic modal logic. In particular, the paper presents a proof that coalgebraic modal logic has the finite model property, a weak completeness result, and a variety of decidability and complexity results. The coalgebraic approach to modal logic aims at providing a generic framework for describing reactive systems that can be specified in terms of state sets and transition functions. The approach goes back to work by \textit{J. Rutten} [Universal coalgebra: A theory of systems. Technical report CS-R 9652, CWI, Amsterdam (1996); see also Theor. Comput. Sci. 249, No. 1, 3--80 (2000; Zbl 0951.68038)], who showed that coalgebras can be used to generalize concepts discussed in the context of transition systems, and \textit{L. Moss} [Ann. Pure Appl. Logic 96, No. 1--3, 277--317 (1999); erratum ibid. 99, No. 1--3, 241--259 (1999; Zbl 0969.03026)], who proposed to use modal logics to formulate bisimulation-invariant properties of coalgebraically modelled systems. In the paper under review, coalgebraic modal logic is based on the semantic approach proposed by \textit{D. Pattinson} [Theor. Comput. Sci. 309, No. 1--3, 177--193 (2003; Zbl 1052.03009)], which employs predicate liftings to define the semantic interpretation of modal operators. The key notion is that of a \(T\)-coalgebra, where \(T\) is a set functor (called signature functor) that describes the data structure of observational states in a reactive system. A \(T\)-coalgebra, then, is defined by a set of states \(X\) and a map that assigns to each state the data observations after a possible one-step transition in the system. Interestingly, a variety of systems can be formulated in that framework, such as Kripke frames and Kripke models, multigraphs (as discussed in the context of graded modal logic), probabilistic transition systems (for probabilistic modal logic), reactive probabilistic automata, and linear automata. The semantics of a modality \(\square\) is determined by a predicate lifting, which in turn is defined in category-theoretical terms as a natural transformation. Given a fixed \(T\)-coalgebra \(C\) with state set \(X\), the component of the predicate lifting at \(X\) is a map from the powerset of \(X\) into the powerset of \(TX\). Then, a formula \(\square\phi\) is satisfied at state \(x\) if and only if the data observation after a one-step transition in \(x\) is contained in the lifting of the set of states in which \(\phi\) holds true. The paper explores proof systems of coalgebraic modal logic that consist of so-called one-step derivation rules (furthermore proof systems are assumed to be closed with respect to propositional reasoning and to the rule of replacement of equivalents). These one-step rules allow as premise only propositional logic formulae and as conclusion only disjunctive clauses (disjunctions of literals) over rank 1 formulae of the form \(\square p\), where \(p\) is a propositional variable. Based on the concepts of one-step soundness and one-step completeness, which fit in the semantic interpretation of modal connectives via predicate liftings, Schröder then shows that each coalgebraic modal logic admits a one-step complete axiomatization (Theorem 18) and that each one-step complete axiomatization is weakly complete (Corollary 31; note that, in general, coalgebraic modal logics do not have the compactness property and hence do not admit a strongly complete axiomatization). The second result is obtained via a Lindenbaum construction on Hintikka sets, which associates a finite model to a consistent formula. This construction gives rise to the mentioned result that every satisfiable formula of a coalgebraic modal logic is satisfiable in a finite \(T\)-coalgebra. Based on these results, Schröder presents some methods on how decision problems in coalgebraic modal logic (and their complexities) can be reduced to ``one-step'' counterparts. These reductions provide nice, but not very tight, upper complexity bounds for such decision problems (Schröder refers to better new results in a final remark). The results obtained by Schröder go significantly beyond results by \textit{D. Pattinson} [loc. cit.] and by \textit{M. Rößiger} [Coalgebras, clone theory, and modal logic. Diss. Univ. Dresden (2000)]. Rößiger's contribution considered Kripke-polynomial functors only. Pattinson presented the first weak completeness result in coalgebraic modal logic, and he established a finite model property result, but only for the special case that the underlying signature functor preserves finiteness. A closer examination of the relationship between Schröder's results and the modular construction of coalgebraic modal logics discussed by \textit{C. Cîrstea} and \textit{D. Pattinson} [Theor. Comput. Sci. 388, No. 1--3, 83--108 (2007; Zbl 1126.03020)] can be found in [\textit{L. Schröder} and \textit{D. Pattinson}, Lect. Notes Comput. Sci. 4596, 459--471 (2007; Zbl 1126.03028)].