Undecidability of Weak Bisimilarity for PA-Processes

We prove that the problem whether two PA-processes are weakly bisimilar is undecidable. We combine several proof techniques to provide a reduction from Post's correspondence problem to our problem: existential quantification technique, masking technique and deadlock elimination technique