JURDZINSKI, Martin, Nielsen MOGENS a Jiří SRBA. Undecidability of Domino Games and Hhp-Bisimilarity. Information and Computation, Netherlands: Springer-Verlag, 2003, roč. 184, č. 2, s. 343-368. ISSN 0890-5401.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Undecidability of Domino Games and Hhp-Bisimilarity
Autoři JURDZINSKI, Martin (616 Polsko), Nielsen MOGENS (208 Dánsko) a Jiří SRBA (203 Česko, garant).
Vydání Information and Computation, Netherlands, Springer-Verlag, 2003, 0890-5401.
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 Nizozemsko
Utajení není předmětem státního či obchodního tajemství
WWW URL
Impakt faktor Impact factor: 0.851
Kód RIV RIV/00216224:14330/03:00008471
Organizační jednotka Fakulta informatiky
Klíčová slova anglicky partial order; bisimilarity; domino games
Štítky bisimilarity, domino games, partial order
Změnil Změnil: Mgr. Jiří Srba, Ph.D., učo 2841. Změněno: 26. 5. 2004 13:38.
Anotace
History preserving bisimilarity (hp-bisimilarity) and hereditary history preserving bisimilarity (hhp-bisimilarity) are behavioural equivalences taking into account causal relationships between events of concurrent systems. Their prominent feature is that they are preserved under action refinement, an operation important for the top-down design of concurrent systems. It is shown that, in contrast to hp-bisimilarity, checking hhp-bisimilarity for finite labelled asyn\-chro\-nous transition systems is undecidable, by a reduction from the halting problem of 2-counter machines. To make the proof more transparent a novel intermediate problem of checking domino bisimilarity for origin constrained tiling systems is introduced and shown undecidable. It is also shown that the unlabelled domino bisimilarity problem is undecidable, which implies undecidability of hhp-bisimilarity for unlabelled finite asynchronous systems. Moreover, it is argued that the undecidability of hhp-bisimilarity holds for finite elementary net systems and 1-safe Petri nets.
Návaznosti
GA201/03/1161, projekt VaVNázev: Verifikace nekonečně stavových systémů
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: 5. 8. 2020 16:38