Sciweavers

Share
FOSSACS
2008
Springer

Model Checking Freeze LTL over One-Counter Automata

8 years 3 months ago
Model Checking Freeze LTL over One-Counter Automata
We study complexity issues related to the model-checking problem for LTL with registers (a.k.a. freeze LTL) over one-counter automata. We consider several classes of one-counter automata (mainly deterministic vs. nondeterministic) and several syntactic fragments (restriction on the number of registers and on the use of propositional variables for control locations). The logic has the ability to store a counter value and to test it later against the current counter value. ducing a non-trivial abstraction on counter values, we show that model checking LTL with registers over deterministic one-counter automata is PSPACEcomplete with infinite accepting runs. By constrast, we prove that model checking LTL with registers over nondeterministic one-counter automata is 1 1 -complete [resp. 0 1 -complete] in the infinitary [resp. finitary] case even if only one register is used and with no propositional variable. This makes a difference with the facts that several verification problems for one-c...
Stéphane Demri, Ranko Lazic, Arnaud Sangnie
Added 26 Oct 2010
Updated 26 Oct 2010
Type Conference
Year 2008
Where FOSSACS
Authors Stéphane Demri, Ranko Lazic, Arnaud Sangnier
Comments (0)
books