
Computer Science 2008
Model checking memoryful lineartime logics over onecounter automataAbstract: We study complexity of the modelchecking problems for LTL with registers (also known as freeze LTL) and for firstorder logic with data equality tests over onecounter automata. We consider several classes of onecounter 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 locations). 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 over deterministic onecounter automata is PSPACEcomplete with infinite and finite accepting runs. By constrast, we prove that model checking freeze LTL in which the until operator is restricted to the eventually operator over nondeterministic onecounter automata is undecidable even if only one register is used and with no propositional variable. As a corollary of our proof, this also holds for firstorder logic with data equality tests restricted to two variables. This makes a difference with the facts that several verification problems for onecounter automata are known to be decidable with relatively low complexity, and that finitary satisfiability for the two logics are decidable. Our results pave the way for modelchecking memoryful (lineartime) logics over other classes of operational models, such as reversalbounded counter machines.
