Skip Navigation



Journal of Logic and Computation Advance Access published online on July 22, 2009
Journal of Logic and Computation, doi:10.1093/logcom/exp037
This Article
Right arrow Full Text (PDF)
Right arrow References
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Demri, S.
Right arrow Articles by Gascon, R.
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

© The Author, 2009. Published by Oxford University Press. All rights reserved. For Permissions, please email: journals.permissions@oxfordjournals.org

Original Papers

The Effects of Bounding Syntactic Resources on Presburger LTL

Stéphane Demri

LSV, ENS Cachan, CNRS, INRIA Saclay, Cachan, France.
E-mail: demri{at}lsv.ens-cachan.fr

Régis Gascon

INRIA, I3S, CNRS, University of Nice Sophia Antipolis, France.
E-mail: rgascon{at}sophia.inria.fr

Received 13 February 2008.


  Abstract

LTL over Presburger constraints is the extension of LTL where the atomic formulae are quantifier-free Presburger formulae having as free variables the counters at different states of the model. This logic is known to admit undecidable satisfiability and model-checking problems. We study decidability and complexity issues for fragments of LTL with Presburger constraints obtained by restricting the syntactic resources of the formulae (the number of variables, the maximal distance between two states for which counters can be compared and, to a smaller extent, the set of Presburger constraints), while preserving the strength of the logical operators. We provide a complete picture refining known results from the literature. We show that model-checking and satisfiability problems for the fragments of LTL with difference constraints restricted to two variables and distance one and to one variable and distance two are highly undecidable, enlarging significantly the class of known undecidable fragments. On the positive side, we prove that the fragment restricted to one variable and to distance one augmented with propositional variables is PSPACE-complete. Since the atomic formulae can state quantitative properties on the counters, this extends some results about model-checking pushdown systems and one-counter automata. In order to establish the PSPACE upper bound, we show that the non-emptiness problem for Büchi one-counter automata taking values in Z and allowing zero tests and sign tests, is only NLOGSPACE-complete. Finally, we establish that model-checking one-counter automata with complete quantifier-free Presburger LTL restricted to one variable is also PSPACE-complete, whereas the satisfiability problem is undecidable.

Keywords: Linear-time temporal logic; Presburger arithmetic; Büchi automaton; one-counter automaton


Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?




Disclaimer: Please note that abstracts for content published before 1996 were created through digital scanning and may therefore not exactly replicate the text of the original print issues. All efforts have been made to ensure accuracy, but the Publisher will not be held responsible for any remaining inaccuracies. If you require any further clarification, please contact our Customer Services Department.