|
Published Articles >> Table of Contents >> Abstract
10th International Symposium on Temporal Representation and Reasoning and Fourth International Conference on Temporal Logic
p. 91
On the Computational Complexity of Decidable Fragments of First-Order Linear Temporal Logics
Ian Hodkinson, Imperial College
Roman Kontchakov, King’s College
Agi Kurucz, King’s College
Frank Wolter, University of Liverpool
Michael Zakharyaschev, King’s College
Full Article Text:
  
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TIME.2003.1214884
Send link to a friend
| Abstract |
|
We study the complexity of some fragments of first-order temporal logic over natural numbers time. The one-variable fragment of linear first-order temporal logic even with sole temporal operator \square is EXPSPACE-complete (this solves an open problem of [10]). So are the one-variable, two-variable and monadic monodic fragments with Until and Since. If we add the operators \bigcircn, with n given in binary, the fragments become 2EXPSPACE-complete. The packed monodic fragment has the same complexity as its pure first-order part - 2EXPTIME-complete. Over any class of flows of time containing one with an infinite ascending sequence - e.g., rationals and real numbers time, and arbitrary strict linear orders - we obtain EXPSPACE lower bounds (which solves an open problem of [16]). Our results continue to hold if we restrict to models with finite first-order domains.
|
 Additional Information
|
Citation:
Ian Hodkinson, Roman Kontchakov, Agi Kurucz, Frank Wolter, Michael Zakharyaschev,
"On the Computational Complexity of Decidable Fragments of First-Order Linear Temporal Logics,"
time-ictl,
p. 91,
10th International Symposium on Temporal Representation and Reasoning and Fourth International Conference on Temporal Logic,
2003
|
|
