Bisimilarity of one-counter processes is PSPACE-complete. (English)
Gastin, Paul (ed.) et al., CONCUR 2010 ‒ concurrency theory. 21th international conference, CONCUR 2010, Paris, France, August 31 ‒ September 3, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-15374-7/pbk). Lecture Notes in Computer Science 6269, 177-191 (2010).
Summary: 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 (Jančar 2000), and matches the known PSPACE lower bound (Srba 2009). We add the PTIME-completeness result for deciding regularity (i.e. finiteness up to bisimilarity) of one-counter processes.
Start
Contact
Print
General Help
