2010 | OriginalPaper | Chapter
Bisimilarity of One-Counter Processes Is PSPACE-Complete
Authors : Stanislav Böhm, Stefan Göller, Petr Jančar
Published in: CONCUR 2010 - Concurrency Theory
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.