Highly Undecidable Questions for Process Algebras

• Authors: JANCAR Petr; SRBA Jiří
• Year of publication: 2004
• Type: Article in Proceedings
• Conference: Proceedings of 3rd IFIP International Conference on Theoretical Computer Science (TCS'04)
• MU Faculty or unit: Faculty of Informatics
• Web: http://www.brics.dk/~srba/publ.html
• Field: Informatics
• Keywords: high undecidability; process rewrite systems; completeness
• Description: We show Sigma^1_1-completeness of weak bisimilarity for PA (process algebra), and of weak simulation preorder/equivalence for PDA (pushdown automata), PA and PN (Petri nets). We also show Pi^1_1-hardness of weak omega-trace equivalence for the (sub)classes BPA (basic process algebra) and BPP (basic parallel processes).

Related projects

• Verification of infinite-state systems
• Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing