JANČAR, Petr, Antonín KUČERA a Richard MAYR. Deciding Bisimulation-Like Equivalences with Finite-State Processes. Theoretical Computer Science, Amsterdam, Nizozemí, 2001, roč. 258, 1-2, s. 409-433. ISSN 0304-3975.
Další formáty:   BibTeX LaTeX RIS
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 Computer hardware and architecture
Stát vydavatele Nizozemsko
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
Změnil Změnil: prof. RNDr. Antonín Kučera, Ph.D., učo 2508. Změněno: 8. 11. 2001 16:30.
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 VaVNázev: Meze algoritmické verifikovatelnosti nekonečně stavových systémů
Investor: Grantová agentura ČR, Standardní projekty
GA201/98/P046, projekt VaVNázev: Rozhodnutelné problémy v algebrách procesů
Investor: Grantová agentura ČR, Standardní projekty
MSM 143300001, záměrNá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, Výzkumné záměry
VytisknoutZobrazeno: 14. 10. 2019 21:14