Deciding Bisimulation-Like Equivalences with Finite-State Processes

We show that characteristic formulae for nite-state systems up to bisimulationlike equivalences (e.g., strong and weak bisimilarity) can be given in the simple branching-time temporal logic EF. Since EF is a very weak fragment of the modal -calculus, model checking with EF is decidable for many more classes of in nitestate systems. This yields a general method for proving decidability of bisimulationlike equivalences between in nite-state processes and nite-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-likeequivalences (including, e.g., strong and weak bisimilarity) is decidable between PAD and nite-state processes. On the other hand, we also demonstrate that no `reasonable' bisimulationlike equivalence is decidable between state-extended PA processes and nite-state ones. Furthermore, weak bisimilarity with nite-state processes is shown to be undecidable even for ...

• Type: Conference
• Year: 1998
• Where: ICALP
• Authors: Petr Jancar, Antonín Kucera, Richard Mayr
• Keywords: Bisimulationlike Equivalence, ICALP 1998, Nite-state Processes, Programming Languages, Weak Bisimilarity