|
Published Articles >> Table of Contents >> Abstract
17th Annual IEEE Symposium on Logic in Computer Science (LICS'02)
p. 393
Decidable and Undecidable Fragments of First-Order Branching Temporal Logics
Ian Hodkinson, Imperial College
Frank Wolter, Universität Leipzig
Michael Zakharyaschev, King’s College
Full Article Text:
  
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2002.1029847
Send link to a friend
| 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 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.
|
 Additional Information
|
Citation:
Ian Hodkinson, Frank Wolter, Michael Zakharyaschev,
"Decidable and Undecidable Fragments of First-Order Branching Temporal Logics,"
lics,
p. 393,
17th Annual IEEE Symposium on Logic in Computer Science (LICS'02),
2002
|
|
