loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
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
Stephane Demri, LSV, ENS Cachan, CNRS, INRIA, France
Regis Gascon, LSV, ENS Cachan, CNRS, INRIA, France
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.