Deciding Bisimilarity between BPA and BPP Processes

Investor logo

Warning

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

JANČAR Petr KUČERA Antonín MOLLER Faron

Year of publication 2003
Type Article in Proceedings
Conference Proceedings of 14th International Conference on Concurrency Theory (CONCUR 2003)
MU Faculty or unit

Faculty of Informatics

Citation
Field Informatics
Keywords verification; bisimilarity; infinite-state systems
Description We identify a necessary condition for when a given BPP process can be expressed as a BPA process. We provide an effective procedure for testing if this condition holds of a given BPP, and in the positive case we provide an effective construction for a particular form of one-counter automaton which is bisimilar to the given BPP. This in turn provides the mechanism to decide bisimilarity between a given BPP process and a given BPA process.
Related projects:

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

More info