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
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references

    Identifiers

    0 references
    0 references
    0 references
    0 references
    0 references
    0 references