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í, 2001, vol. 258, 1-2, p. 409-433. ISSN 0304-3975.

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

Language

English

Type of outcome

Článek v odborném periodiku

Field of Study

20206 Computer hardware and architecture

Country of publisher

Netherlands

Confidentiality degree

není předmětem státního či obchodního tajemství

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

V originále

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