JANČAR, Petr a Jiří SRBA. Undecidability of Bisimilarity by Defender's Forcing. Journal of the ACM, New York: ACM, 2008, roč. 55/2008, č. 1, s. 1-26. ISSN 0004-5411.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Undecidability of Bisimilarity by Defender's Forcing
Název česky Nerozhodnutelnost bisimulace pomoci tlaku obránce
Autoři JANČAR, Petr (203 Česko) a Jiří SRBA (203 Česko, garant).
Vydání Journal of the ACM, New York, ACM, 2008, 0004-5411.
Další údaje
Originální jazyk angličtina
Typ výsledku Článek v odborném periodiku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Spojené státy
Utajení není předmětem státního či obchodního tajemství
Impakt faktor Impact factor: 2.339
Kód RIV RIV/00216224:14330/08:00026472
Organizační jednotka Fakulta informatiky
UT WoS 000253939800005
Klíčová slova anglicky undecidability; bisimilarity; rewrite systems
Štítky bisimilarity, rewrite systems, undecidability
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: Mgr. Jiří Srba, Ph.D., učo 2841. Změněno: 29. 9. 2008 22:32.
Anotace
tirling (1996, 1998) proved the decidability of bisimilarity on so-called normed pushdown processes. This result was substantially extended by Senizergues(1998, 2005) who showed the decidability of bisimilarity for regular (or equational) graphs of finite out-degree; this essentially coincides with weak bisimilarity of processes generated by (unnormed) pushdown automata where the epsilon-transitions can only deterministically pop the stack. The question of decidability of bisimilarity for the more general class of so called Type -1 systems, which is equivalent to weak bisimilarity on unrestricted epsilon-popping pushdown processes, was left open. This was repeatedly indicated by both Stirling and Senizergues. Here we answer the question negatively, that is, we show the undecidability of bisimilarity on Type -1 systems, even in the normed case. We achieve the result by applying a technique we call Defender's Forcing, referring to the bisimulation games. The idea is simple, yet powerful. We demonstrate its versatility by deriving further results in a uniform way. First, we classify several versions of the undecidable problems for prefix rewrite systems (or pushdown automata) as Pi^0_1-complete or Sigma^1_1-complete. Second, we solve the decidability question for weak bisimilarity on PA (Process Algebra) processes, showing that the problem is undecidable and even Sigma^1_1-complete. Third, we show Sigma^1_1-completeness of weak bisimilarity for so-called parallel pushdown (or multiset) automata, a subclass of (labeled, place/transition) Petri nets.
Anotace česky
tirling (1996, 1998) proved the decidability of bisimilarity on so-called normed pushdown processes. This result was substantially extended by Senizergues(1998, 2005) who showed the decidability of bisimilarity for regular (or equational) graphs of finite out-degree; this essentially coincides with weak bisimilarity of processes generated by (unnormed) pushdown automata where the epsilon-transitions can only deterministically pop the stack. The question of decidability of bisimilarity for the more general class of so called Type -1 systems, which is equivalent to weak bisimilarity on unrestricted epsilon-popping pushdown processes, was left open. This was repeatedly indicated by both Stirling and Senizergues. Here we answer the question negatively, that is, we show the undecidability of bisimilarity on Type -1 systems, even in the normed case. We achieve the result by applying a technique we call Defender's Forcing, referring to the bisimulation games. The idea is simple, yet powerful. We demonstrate its versatility by deriving further results in a uniform way. First, we classify several versions of the undecidable problems for prefix rewrite systems (or pushdown automata) as Pi^0_1-complete or Sigma^1_1-complete. Second, we solve the decidability question for weak bisimilarity on PA (Process Algebra) processes, showing that the problem is undecidable and even Sigma^1_1-complete. Third, we show Sigma^1_1-completeness of weak bisimilarity for so-called parallel pushdown (or multiset) automata, a subclass of (labeled, place/transition) Petri nets.
Návaznosti
MSM0021622419, záměrNázev: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Výzkumné záměry
VytisknoutZobrazeno: 3. 7. 2020 15:51