Portal de Periódicos da CAPES

Bisimulation equivalence and regularity for real-time one-counter automata

2013; Elsevier BV; Volume: 80; Issue: 4 Linguagem: Inglês

10.1016/j.jcss.2013.11.003

1090-2724

Stanislav Böhm, Stefan Göller, Petr Jančar,

Software Testing and Debugging Techniques

A one-counter automaton is a pushdown automaton with a singleton stack alphabet, where stack emptiness can be tested; it is a real-time automaton if it contains no ε -transitions. We study the computational complexity of the problems of equivalence and regularity (i.e. semantic finiteness) on real-time one-counter automata. The first main result shows PSPACE -completeness of bisimulation equivalence; this closes the complexity gap between decidability [23] and PSPACE -hardness [25] . The second main result shows NL -completeness of language equivalence of deterministic real-time one-counter automata; this improves the known PSPACE upper bound (indirectly shown by Valiant and Paterson [27] ). Finally we prove P -completeness of the problem if a given one-counter automaton is bisimulation equivalent to a finite system, and NL -completeness of the problem if the language accepted by a given deterministic real-time one-counter automaton is regular. • Bisimulation equivalence is PSPACE -complete for real-time one-counter automata. • Language equivalence is NL -complete for deterministic real-time one-counter automata. • Finiteness w.r.t. bisimilarity is P -complete for real-time one-counter automata. • Regularity is NL -complete for deterministic real-time one-counter automata.