Bisimilarity of One-Counter Processes Is PSPACE-Complete

A one-counter automaton is a pushdown automaton over a singleton stack alphabet. We prove that the bisimilarity of processes generated by nondeterministic one-counter automata (with no -steps) is in PSPACE. This improves the previously known decidability result (Jancar 2000), and matches the known PSPACE lower bound (Srba 2009). Moreover, we prove PTIME-completeness of regularity of one-counter processes (i.e., their finiteness up to bisimilarity).

• Type: Conference
• Year: 2010
• Where: CONCUR
• Authors: Stanislav Böhm, Stefan Göller, Petr Jancar
• Keywords: CONCUR 2010, Distributed And Parallel Computing, Nondeterministic One-counter Automata, Pushdown Automaton, Singleton Stack Alphabet