Weak bisimilarity with infinite-state systems can be decided in polynomial time

摘要

We prove that weak bisimilarity is decidable in polynomial time between BPA and finite-state processes, and between normed BPP and finite-state processes. To the best of our knowledge, these are the first polynomial algorithms for weak bisimilarity with infinite-state systems.