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

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TIME.2007.63

Stephane Demri , LSV, ENS Cachan, CNRS, INRIA, France

Regis Gascon , 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

R. Gascon and S. Demri, "The Effects of Bounding Syntactic Resources on Presburger LTL,"

*Temporal Representation and Reasoning, International Syposium on(TIME)*, Alicante, Spain, 2007, pp. 94-104.

doi:10.1109/TIME.2007.63

CITATIONS