Completeness Results for Undecidable Bisimilarity Problems
| Authors | |
|---|---|
| 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 | |
| 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: |