14th International Symposium on Temporal Representation and Reasoning (TIME'07) The Effects of Bounding Syntactic Resources on Presburger LTL Alicante, Spain June 28-June 30 ISBN: 0-7695-2836-8
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TIME.2007.63
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.
Citation:
Stephane Demri, Regis Gascon, "The Effects of Bounding Syntactic Resources on Presburger LTL," time, pp.94-104, 14th International Symposium on Temporal Representation and Reasoning (TIME'07), 2007 Usage of this product signifies your acceptance of the Terms of Use. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||