Publication details

Completeness Results for Undecidable Bisimilarity Problems

Investor logo


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

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.

More info