Modal logic and the approximation induction principle (Q2883116)

Hennessy Milner Logic, HML, is given through formulas NEWLINE\[NEWLINE \phi ::= \top \mid \bigwedge_{i\in I}\phi_i \mid \langle a \rangle \phi \mid \neg \phi, NEWLINE\]NEWLINE where \(I\) is an arbitrary index set; this logic is modified by replacing negation through a box operator \([a]\) and by adding disjunctions indexed by an arbitrary index set \(I\), yielding a logic HML\({}^+\). These logics are interpreted in a canonic way through a labelled transition system. Define for a sublogic \(\mathcal{O}\) an equivalence relation \(\sim_\mathcal{O}\) on the states of an labelled transition system through the satisfaction od exactly the same formulas in \(\mathcal{O}\). Conditions are investigated under which \(\sim_\mathcal{O}\) and \(\sim_{\mathcal{O}_{\text{FIN}}}\) resp. \(\sim_\mathcal{O}\) and \(\sim_{\mathcal{O}_{\text{FDP}}}\) coincide for image finite transition systems, where \(\mathcal{O}_{\text{FIN}}\) and \(\mathcal{O}_{\text{FDP}}\) are all formulas in \(\mathcal{O}\) that do not contain infinite conjunctions resp. are of finite depth. Since \(\mathcal{O}\) can be interpreted as a modal characterization of trace semantics, this yields a compactness result for these semantics. The results are compared to earlier results due to \textit{R. Goldblatt} and \textit{M. Hollenberg} [CSLI Lecture Notes 53, 189--216 (1995)] for modally saturated processes.NEWLINENEWLINE The second part of the paper introduces and discusses the approximation induction principle: Given projection operators, this principle states that two processes are equal if and only if they are equal up to any finite depth. Soundness of this principle is investigated in terms of HML-formulas of finite depth, and a simulation preorder is defined. Some complexity results are derived through sophisticated combinatorial arguments. They help constructing algorithmically a labelled transition system for which the simulation preorder stabilizes.NEWLINENEWLINEThe paper utilizes and extends the results given by \textit{R. J. van Glabbeek} [Lect. Notes Comput. Sci. 247, 336--347 (1987; Zbl 0612.68025); CONCUR, LNCS 715, 66--81 (1993)] on modal characterizations for process semantics. Upper bounds are given for the number of iterations for the computation of preorders. Previous results hinted at by \textit{L. Aceto} et al. [Inf. Comput. 111, No. 1, 1--52 (1994; Zbl 0822.68059)] are formally established.