Deciding Bisimulation-Like Equivalences with Finite-State Processes
| Autoři | |
|---|---|
| Rok publikování | 2001 |
| Druh | Článek v odborném periodiku |
| Časopis / Zdroj | Theoretical Computer Science |
| Fakulta / Pracoviště MU | |
| Citace | |
| Obor | Počítačový hardware a software |
| Klíčová slova | concurrency; infinite-state systems; bisimilarity |
| Popis | We show that characteristic formulae for finite-state systems up to bisimulation-like 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 mu-calculus, model checking with EF is decidable for many more classes of infinite-state systems. This yields 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'). |
| Související projekty: |