|
| This Article | ||
| ||
| Share | ||
| Bibliographic References | ||
| Add to: | ||
| | ||
| Search | ||
| ||
17th Annual IEEE Symposium on Logic in Computer Science (LICS'02)
Decidable and Undecidable Fragments of First-Order Branching Temporal Logics
Copenhagen, Denmark
July 22-July 25
ISBN: 0-7695-1483-9
| ASCII Text | x | ||
| Ian Hodkinson, Frank Wolter, Michael Zakharyaschev, "Decidable and Undecidable Fragments of First-Order Branching Temporal Logics," Logic in Computer Science, Symposium on, pp. 393, 17th Annual IEEE Symposium on Logic in Computer Science (LICS'02), 2002. | |||
| BibTex | x | ||
| @article{ 10.1109/LICS.2002.1029847, author = {Ian Hodkinson and Frank Wolter and Michael Zakharyaschev}, title = {Decidable and Undecidable Fragments of First-Order Branching Temporal Logics}, journal ={Logic in Computer Science, Symposium on}, volume = {0}, year = {2002}, issn = {1043-6871}, pages = {393}, doi = {http://doi.ieeecomputersociety.org/10.1109/LICS.2002.1029847}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, } | |||
| RefWorks Procite/RefMan/Endnote | x | ||
| TY - CONF JO - Logic in Computer Science, Symposium on TI - Decidable and Undecidable Fragments of First-Order Branching Temporal Logics SN - 1043-6871 SP EP A1 - Ian Hodkinson, A1 - Frank Wolter, A1 - Michael Zakharyaschev, PY - 2002 KW - null VL - 0 JA - Logic in Computer Science, Symposium on ER - | |||
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.
