Logics and decidability for labelled pre- and partially ordered Kripke structures (Q1328764)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Logics and decidability for labelled pre- and partially ordered Kripke structures |
scientific article |
Statements
Logics and decidability for labelled pre- and partially ordered Kripke structures (English)
0 references
3 August 1994
0 references
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.
0 references
Kripke semantics
0 references
labelled Kripke structure
0 references
trace system
0 references
completeness
0 references
decidability
0 references
propositional temporal logics
0 references
tiling problem
0 references