Paper Info
Title
The Effects of Bounding Syntactic Resources on Presburger LTL
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 ℤ 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.
Year
DOI
Venue
2009
10.1093/logcom/exp037
J. Log. Comput.
Keywords
Field
DocType
quantifier-free presburger formula,satisfiability problem,presburger ltl,undecidable satisfiability,presburger constraint,atomic formula,one-counter automaton,maximal distance,bounding syntactic resources,undecidable fragment,model-checking problem
Discrete mathematics,Combinatorics,Free variables and bound variables,Boolean satisfiability problem,Satisfiability,Algorithm,Presburger arithmetic,Decidability,PSPACE,Propositional variable,Mathematics,Undecidable problem
Journal
Volume
Issue
ISSN
19
6
1530-1311
ISBN
Citations 
PageRank 
0-7695-2836-8
25
1.03
References 
Authors
32
2
Name
Order
Citations
PageRank
Stéphane Demri183260.65
Régis Gascon2765.23