We design a general method for proving decidability of bisimulation-like equivalences between infinite-state processes and finite-state ones. We apply this method to the class of PAD processes, which strictly subsumes PA and pushdown (PDA) processes, showing that a large class of bisimulation-like equivalences (including e.g. strong and weak bisimilarity) is decidable between PAD and finite-state processes. On the other hand, we also demonstrate that no 'reasonable' bisimulation-like equivalence is decidable between state-extended PA processes and finite-state ones. Furthermore, weak bisimilarity with finite-state processes is shown to be undecidable even for state-extended BPP (which are also known as 'parallel pushdown processes').
CITATION STYLE
Jančar, P., Kučera, A., & Mayr, R. (1998). Deciding bisimulation-like equivalences with finite-state processes. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1443 LNCS, pp. 200–211). Springer Verlag. https://doi.org/10.1007/bfb0055053
Mendeley helps you to discover research relevant for your work.