Title
Bisimulation equivalence and regularity for real-time one-counter automata
Abstract
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 @e-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.
Year
DOI
Venue
2014
10.1016/j.jcss.2013.11.003
J. Comput. Syst. Sci.
Keywords
Field
DocType
main result,bisimulation equivalence,real-time automaton,pushdown automaton,one-counter automaton,language equivalence,deterministic real-time one-counter automaton,bisimulation equivalent,complexity gap,real-time one-counter automaton
Discrete mathematics,Combinatorics,Two-way deterministic finite automaton,Deterministic automaton,Nondeterministic finite automaton,Deterministic pushdown automaton,DFA minimization,Timed automaton,Pushdown automaton,Mathematics,Büchi automaton
Journal
Volume
Issue
ISSN
80
4
0022-0000
Citations 
PageRank 
References 
4
0.49
33
Authors
3
Name
Order
Citations
PageRank
Stanislav Böhm1508.69
Stefan Göller214815.10
Petr Jančar331520.84