|
Abstract : |
Abstract. We design a general method for proving decidability of bisimulationlike 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?). 1, |