Logics and decidability for labelled pre- and partially ordered Kripke structures (Q1328764)

The paper considers some propositional temporal logics arising in computer science. Their semantics is given by ``labelled Kripke structures''. Such a structure is a set of possible worlds together with a family of binary relations, \((\to_ a)_{a\in A}\), indexed by ``labels''. The propositional language contains necessity operators corresponding to these relations, and also the \(\square\)-operator corresponding to the reflexive transitive closure of \(\bigcup \{\leftarrow_ a\): \(a\in A\}\). The system \(\Gamma\) describes pre- and partially ordered Kripke structures, and its extension \(\Gamma_ 1\) has additional axioms saying that every world has at most one successor and at most one predecessor at each label. It is stated that \(\Gamma\) and \(\Gamma_ 1\) are Kripke-complete and decidable. An important class of Kripke structures is generated by ``trace systems''; these structures are called ``frames'' [cf. \textit{W. Penczek}, Inf. Process. Lett. 43, 147-153 (1992; Zbl 0771.03006)]. It is shown that the tiling problem can be expressed in a modal propositional theory extending \(\Gamma_ 1\); this theory corresponds to some frame model.