Deciding Bisimulation-Like Equivalences with Finite-State Processes

Investor logo
Investor logo

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

JANČAR Petr KUČERA Antonín MAYR Richard

Year of publication 2001
Type Article in Periodical
Magazine / Source Theoretical Computer Science
MU Faculty or unit

Faculty of Informatics

Citation
Field Computer hardware and software
Keywords concurrency; infinite-state systems; bisimilarity
Description 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').
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.