Completeness Results for Undecidable Bisimilarity Problems

Investor logo

Warning

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

SRBA Jiří

Year of publication 2004
Type Article in Proceedings
Conference Proccedings of the 5th International Workshop on Verification of Infinite-State Systems (INFINITY'03)
MU Faculty or unit

Faculty of Informatics

Citation
Web http://www.brics.dk/~srba/publ.html
Field Informatics
Keywords high undecidability; bisimilarity
Description We establish Sigma_1^1-completeness (in the analytical hierarchy) of weak bisimilarity checking for infinite-state processes generated by pushdown automata and parallel pushdown automata. The results imply Sigma_1^1-completeness of weak bisimilarity for Petri nets and give a negative answer to the open problem stated by Jancar (CAAP'95): ``does the problem of weak bisimilarity for Petri nets belong to Delta_1^1 ?''
Related projects:

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