Sciweavers

Share
CORR
2008
Springer

Model checking memoryful linear-time logics over one-counter automata

8 years 3 months ago
Model checking memoryful linear-time logics over one-counter automata
We study complexity of the model-checking problems for LTL with registers (also known as freeze LTL and written LTL ) and for first-order logic with data equality tests (written FO(, <, +1)) over one-counter automata. We consider several classes of one-counter automata (mainly deterministic vs. nondeterministic) and several logical fragments (restriction on the number of registers or variables and on the use of propositional variables for control states). The logics have the ability to store a counter value and to test it later against the current counter value. We show that model checking LTL and FO(, <, +1) over deterministic one-counter automata is PSpace-complete with infinite and finite accepting runs. By constrast, we prove that model checking LTL in which the until operator U is restricted to the eventually F 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...
Stéphane Demri, Ranko Lazic, Arnaud Sangnie
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2008
Where CORR
Authors Stéphane Demri, Ranko Lazic, Arnaud Sangnier
Comments (0)
books