loading...
Decidable and Undecidable Fragments of First-Order Branching Temporal Logics
Copenhagen, Denmark July 22-July 25
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2002.102984717th Annual IEEE Symposium on Logic i ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Ian Hodkinson, Imperial College
Frank Wolter, Universität Leipzig
Michael Zakharyaschev, King?s College
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.
Citation:
Ian Hodkinson, Frank Wolter, Michael Zakharyaschev, "Decidable and Undecidable Fragments of First-Order Branching Temporal Logics," lics, pp.393, 17th Annual IEEE Symposium on Logic in Computer Science (LICS'02), 2002
Usage of this product signifies your acceptance of the Terms of Use.