Undecidability of Domino Games and Hhp-Bisimilarity

J 2003

Undecidability of Domino Games and Hhp-Bisimilarity

JURDZINSKI, Martin; Nielsen MOGENS a Jiří SRBA

Základní údaje

Originální název

Undecidability of Domino Games and Hhp-Bisimilarity

Autoři

JURDZINSKI, Martin; Nielsen MOGENS a Jiří SRBA

Vydání

Information and Computation, Netherlands, Springer-Verlag, 2003, 0890-5401

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Nizozemské království

Utajení

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

Odkazy

URL

Impakt faktor

Impact factor: 0.851

Označené pro přenos do RIV

Ano

Kód RIV

RIV/00216224:14330/03:00008471

Organizační jednotka

Fakulta informatiky

Klíčová slova anglicky

partial order; bisimilarity; domino games

Štítky

Změněno: 26. 5. 2004 13:38, Prof. Jiří Srba, Ph.D.

Anotace

V originále

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 VaV

Název: Verifikace nekonečně stavových systémů

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

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ů

Citovat

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.

@article{492122,
   author = {Jurdzinski, Martin and Mogens, Nielsen and Srba, Jiří},
   article_location = {Netherlands},
   article_number = {2},
   keywords = {partial order; bisimilarity; domino games},
   language = {eng},
   issn = {0890-5401},
   journal = {Information and Computation},
   title = {Undecidability of Domino Games and Hhp-Bisimilarity},
   url = {http://www.brics.dk/~srba/publ.html},
   volume = {184},
   year = {2003}
}

TY  - JOUR
ID  - 492122
AU  - Jurdzinski, Martin - Mogens, Nielsen - Srba, Jiří
PY  - 2003
TI  - Undecidability of Domino Games and Hhp-Bisimilarity
JF  - Information and Computation
VL  - 184
IS  - 2
SP  - 343-368
EP  - 343-368
PB  - Springer-Verlag
SN  - 08905401
KW  - partial order
KW  - bisimilarity
KW  - domino games
UR  - http://www.brics.dk/~srba/publ.html
N2  - 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.
ER  -

JURDZINSKI, Martin; Nielsen MOGENS a Jiří SRBA. Undecidability of Domino Games and Hhp-Bisimilarity. \textit{Information and Computation}. Netherlands: Springer-Verlag, 2003, roč.~184, č.~2, s.~343-368. ISSN~0890-5401.

Přehled o publikaci