Deciding bisimulation-like equivalences with finite-state processes

We show that characteristic formulae for finite-state systems up to bisimul ation-like equivalences (e.g., strong and weak bismilarity) can be given in the simple branching-time temporal logic EF. Since EF is a very weak fragm ent of the modal mu -calculus, model checking with EF is decidable for many more classes of infinite state systems. This yields a general method for p roving decidability of bisimulation-like equivalences between infinite-stat e processes and finite-state ones. We apply this method to the class of PAD processes, which strictly subsumes PA and pushdown (PDA) processes, showin g that a large class of bisimulation-like equivalences (including, e.g., st rong and weak bisimilarity) is decidable between PAD and finite-state proce sses. Oa the other hand, we also demonstrate that no 'reasonable' bisimulat ion-like equivalence is decidable between state-extended PA processes and f inite-state ones. Furthermore, weak bisimilarity with finite-state processe s is shown to be undecidable even for state-extended BPP (which are also kn own as 'parallel pushdown processes'). (C) 2001 Elsevier Science B,V, All r ights reserved.