HIGHLY UNDECIDABLE QUESTIONS FOR PROCESS ALGEBRAS

摘要

We show Σ_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 Π_1~1-hardness of weak ω-trace equivalence for the (sub)classes BPA (basic process algebra) and BPP (basic parallel processes).