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

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-ti...

Full description

Saved in:
Bibliographic Details
Published in:Journal of computer and system sciences 2014-06, Vol.80 (4), p.720-743
Main Authors: Bohm, Stanislav, Goller, Stefan, Jancar, Petr
Format: Article
Language:English
Subjects:
Automation
Bisimulation equivalence
Complexity
Equivalence
Language equivalence
Mathematical analysis
One-counter automaton
Real time
Regularity
Semantics
Stacks
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0022-0000
1090-2724
DOI:10.1016/j.jcss.2013.11.003