Completeness Results for Undecidable Bisimilarity Problems
Jǐŕı Srba · Electronic Notes in Theoretical Computer Science · 2004
We establish Σ 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 Σ 1 1 -completeness of weak bisimilarity for Petri nets and give a negative answer to the open problem stated by Jančar (CAAP'95): “does the problem of weak bisimilarity for Petri nets belong to Δ 1 1 ?”