Decidable fragments of first-order temporal logics

DOI10.1016/S0168-0072(00)00018-XMaRDI QIDQ1591203zbMATH OpenOpenAlexFDO

Authors F. Wolter, Ian Hodkinson, Michael Zakharyaschev

Publication date 28 November 2002

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s0168-0072(00)00018-x

classical decision problem decidability decidable fragments first-order temporal logic temporal databases undecidability

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Temporal logic (03B44) Undecidability and degrees of sets of sentences (03D35) Database theory (68P15) Specification and verification (program logics, model checking, etc.) (68Q60) Knowledge representation (68T30)

Review text

First-order temporal logic extends ordinary first-order logic by the binary temporal operators \({\mathcal S}\) (since) and \({\mathcal U}\) (until). The logic is interpreted using a strict linear order \((W,<)\) and for each \(w\in W\) a first-order structure \(I(w)\) where the underlying domain of the \(I(w)\) as well as the interpretations of constants are the same for each \(w\). The linear order \(W\) models the flow of time; \(I(w)\) varying with \(w\) reflects the idea that meanings of predicates may change over time. Given \(w\in W\) and a formula \(\phi\) with parameters from \(D\), one writes \(w\models \phi\) to mean that \(\phi\) is valid ``at time \(w\). One has in particular \(w\models \phi{\mathcal U}\psi\) iff there is \(v>w\) such that \(v\models \phi\) and \(u\models \psi\) for each \(w<u<v\). Likewise, \(w\models \phi{\mathcal S}\psi\) iff there is \(v<w\) such that \(v\models \phi\) and \(u\models \psi\) for each \(v<u<w\). For example, \(\diamondsuit\phi := \top{\mathcal U}\phi\) expresses that \(\phi\) holds at some later time, i.e., eventually, whereas \(\square\phi:=\neg\diamondsuit\neg\phi\) expresses that \(\phi\) holds at all later times, i.e., henceforth. Unfortunately, already the monadic fragment (only unary predicate symbols) as well as the 2-variable fragments (formulas contain at most two distinct variables) are not even recursively enumerable, i.e., there does not exist a recursive axiomatisation of the formulas that are true for some interpretation. This is proved by reduction to the recurrent tiling problem for \({\mathbf N}\times {\mathbf N}\). The situation does not change if one restricts attention to interpretation in finite domains (but over infinite time, e.g., \(W=({\mathbf N},<))\). Notice that the corresponding fragments of pure first-order logic are decidable. The contribution of the paper is that decidability of satisfiability can be regained if a) one restricts the purely first-order part to a decidable fragment and b) one allows at most one free variable in subformulas of temporal operators. For instance, the Barcan formula \(\exists x\diamondsuit\phi \Leftrightarrow\diamondsuit\exists x\phi\) belongs to this fragment. This result is all the more interesting as the considered fragments do not enjoy the finite model property, i.e., there are formulas that are satisfiable (over \((\mathbf N,<)\)) in models with infinite domain only; a case in point is the formula \(\square\exists x(P(x)\wedge\neg(\top {\mathcal S}P(x)))\) expressing that at any time \(P\) contains an element that was not there before (or in the authors' words: ``at every moment someone's starting to get old). The proof of the decidability result proceeds using finitary descriptions of models (``quasimodels) in which (the possibly infinite, see above) set of domain elements is replaced by a finite set of types, i.e., deductively closed sets of formulas in one free variable. The existence of quasimodels can be expressed in monadic second-order logic which is decidable by standard results of Büchi and Rabin.

Recommendations

Cites work

Cited in

(65)

This page was built for publication: Decidable fragments of first-order temporal logics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1591203)