Deciding Bisimulation-Like Equivalences with Finite-State Processes

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

Základní údaje

• Originální název: Deciding Bisimulation-Like Equivalences with Finite-State Processes
• Autoři: JANČAR, Petr, Antonín KUČERA a Richard MAYR.
• Vydání: Theoretical Computer Science, Amsterdam, Nizozemí, 2001, 0304-3975.

Další údaje

• Originální jazyk: angličtina
• Typ výsledku: Článek v odborném periodiku
• Obor: 20206 Computer hardware and architecture
• Stát vydavatele: Nizozemské království
• Utajení: není předmětem státního či obchodního tajemství
• Impakt faktor: Impact factor: 0.468
• Kód RIV: RIV/00216224:14330/01:00003122
• Organizační jednotka: Fakulta informatiky
• UT WoS: 000168502800010
• Klíčová slova anglicky: concurrency; infinite-state systems; bisimilarity
• Štítky: bisimilarity, concurrency, infinite-state systems

Anotace

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').

Návaznosti

• GA201/97/0456, projekt VaV: Název: Meze algoritmické verifikovatelnosti nekonečně stavových systémů

Investor: Grantová agentura ČR, Meze algoritmické verifikovatelnosti nekonečně stavových systémů

• GA201/98/P046, projekt VaV: Název: Rozhodnutelné problémy v algebrách procesů

Investor: Grantová agentura ČR, Rozhodnutelné problémy v algebrách procesů

• MSM 143300001, záměr: Název: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů

Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Nesekvenční modely výpočtů -- kvantové a souběžné distribuované modely výpočetních procesů