The Community for Technology Leaders
Temporal Representation and Reasoning, International Syposium on (2007)
Alicante, Spain
June 28, 2007 to June 30, 2007
ISSN: 1530-1311
ISBN: 0-7695-2836-8
pp: 94-104
Regis Gascon , LSV, ENS Cachan, CNRS, INRIA, France
Stephane Demri , LSV, ENS Cachan, CNRS, INRIA, France
ABSTRACT
We study decidability and complexity issues for fragments of LTL with Presburger constraints by restricting the syntactic resources of the formulae (the class of constraints, the number of variables and the distance between two states for which counters can be compared) while preserving the strength of the logical operators. We provide a complete picture refining known results from the literature, in some cases pushing forward the known decidability limits. By way of example, we show that model-checking formulae from LTL with quantifier-free Presburger arithmetic over one-counter automata is only PSPACE-complete. In order to establish the PSPACE upper bound, we show that the nonemptiness problem for Buchi one-counter automata taking values in \mathbb{Z} and allowing zero tests and sign tests, is only NLOGSPACE-complete.
INDEX TERMS
null
CITATION
Regis Gascon, Stephane Demri, "The Effects of Bounding Syntactic Resources on Presburger LTL", Temporal Representation and Reasoning, International Syposium on, vol. 00, no. , pp. 94-104, 2007, doi:10.1109/TIME.2007.63
90 ms
(Ver )