Paper: Decidable and undecidable fragments of first-order branching temporal logics (at LICS 2002)

Authors: Ian M. Hodkinson Frank Wolter Michael Zakharyaschev

Abstract

In this paper we analyze the decision problem for fragments of first-order extensions of branching time temporal logics such as computational tree logics CTL and CTL* or Prior's Ockhamist logic of historical necessity. On the one hand, we show that the one-variable fragments of logics like first-order CTL* - such as the product of propositional CTL* with simple propositional modal logic S5, or even the one-variable bundled first-order temporal logic with sole temporal operator `some time in the future' - are undecidable. On the other hand, it is proved that by restricting applications of first-order quantifiers to state (i.e., path-independent) formulas, and applications of temporal operators and path quantifiers to formulas with at most one free variable, we can obtain decidable fragments. The same arguments show decidability of `non-local' propositional CTL*, in which truth values of propositional atoms depend on the history as well as the current time. The positive decidability results can serve as a unifying framework for devising expressive and effective time-dependent knowledge representation formalisms, e.g., temporal description or spatio-temporal logics.

BibTeX

  @InProceedings{HodkinsonWolterZakh-Decidableandundecid,
    author = 	 {Ian M. Hodkinson and Frank Wolter and Michael Zakharyaschev},
    title = 	 {Decidable and undecidable fragments of first-order branching
    temporal logics},
    booktitle =  {Proceedings of the Seventeenth Annual IEEE Symposium on Logic in Computer Science (LICS 2002)},
    year =	 {2002},
    month =	 {July}, 
    pages =      {393--402},
    location =   {Copenhagen, Denmark}, 
    publisher =	 {IEEE Computer Society Press}
  }