Weak Bisimilarity between Finite-State Systems and BPA or normed BPP is Decidable in Polynomial Time

• Authors: KUČERA Antonín; MAYR Richard
• Year of publication: 2002
• Type: Article in Periodical
• Magazine / Source: Theoretical Computer Science
• MU Faculty or unit: Faculty of Informatics
• Field: Computer hardware and software
• Keywords: concurrency; infinite-state systems; bisimilarity
• Description: We prove that weak bisimilarity is decidable in polynomial time between finite-state systems and several classes of infinite-state systems: context-free processes (BPA) and normed Basic Parallel Processes (normed BPP). To the best of our knowledge, these are the first polynomial algorithms for weak bisimilarity problems involving infinite-state systems.

Related projects

• Infinite state concurrent systems - models and verification
• Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing