Deciding Bisimulation-Like Equivalences with Finite-State Processes

JANČAR, Petr, Antonín KUČERA and Richard MAYR. Deciding Bisimulation-Like Equivalences with Finite-State Processes. Theoretical Computer Science. Amsterdam, Nizozemí, vol. 258, 1-2, p. 409-433. ISSN 0304-3975. 2001.

Basic information

• Original name: Deciding Bisimulation-Like Equivalences with Finite-State Processes
• Authors: JANČAR, Petr, Antonín KUČERA and Richard MAYR.
• Edition: Theoretical Computer Science, Amsterdam, Nizozemí, 2001, 0304-3975.

Other information

• Original language: English
• Type of outcome: Article in a journal
• Field of Study: 20206 Computer hardware and architecture
• Country of publisher: Netherlands
• Confidentiality degree: is not subject to a state or trade secret
• Impact factor: Impact factor: 0.468
• RIV identification code: RIV/00216224:14330/01:00003122
• Organization unit: Faculty of Informatics
• UT WoS: 000168502800010
• Keywords in English: concurrency; infinite-state systems; bisimilarity
• Tags: bisimilarity, concurrency, infinite-state systems

Abstract

We show that characteristic formulae for finite-state systems up to bisimulation-like equivalences (e.g., strong and weak bisimilarity) can be given in the simple branching-time temporal logic EF. Since EF is a very weak fragment of the modal mu-calculus, model checking with EF is decidable for many more classes of infinite-state systems. This yields a general method for proving decidability of bisimulation-like equivalences between infinite-state processes and finite-state ones. We apply this method to the class of PAD processes, which strictly subsumes PA and pushdown (PDA) processes, showing that a large class of bisimulation-like equivalences (including, e.g., strong and weak bisimilarity) is decidable between PAD and finite-state processes. On the other hand, we also demonstrate that no `reasonable' bisimulation-like equivalence is decidable between state-extended PA processes and finite-state ones. Furthermore, weak bisimilarity with finite-state processes is shown to be undecidable even for state-extended BPP (which are also known as `parallel pushdown processes').

Links

• GA201/97/0456, research and development project: Name: Meze algoritmické verifikovatelnosti nekonečně stavových systémů

Investor: Czech Science Foundation, Algorithmic Verification Boundaries for Infinite-State Systems

• GA201/98/P046, research and development project: Name: Rozhodnutelné problémy v algebrách procesů

Investor: Czech Science Foundation, (Un)decidable Problems in Process Algebras

• MSM 143300001, plan (intention): Name: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů

Investor: Ministry of Education, Youth and Sports of the CR, Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing