JURDZINSKI, Martin, Nielsen MOGENS and Jiří SRBA. Undecidability of Domino Games and Hhp-Bisimilarity. Information and Computation. Netherlands: Springer-Verlag, 2003, vol. 184, No 2, p. 343-368. ISSN 0890-5401.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Undecidability of Domino Games and Hhp-Bisimilarity
Authors JURDZINSKI, Martin (616 Poland), Nielsen MOGENS (208 Denmark) and Jiří SRBA (203 Czech Republic, guarantor).
Edition Information and Computation, Netherlands, Springer-Verlag, 2003, 0890-5401.
Other information
Original language English
Type of outcome Article in a journal
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Netherlands
Confidentiality degree is not subject to a state or trade secret
WWW URL
Impact factor Impact factor: 0.851
RIV identification code RIV/00216224:14330/03:00008471
Organization unit Faculty of Informatics
Keywords in English partial order; bisimilarity; domino games
Tags bisimilarity, domino games, partial order
Changed by Changed by: Prof. Jiří Srba, Ph.D., učo 2841. Changed: 26/5/2004 13:38.
Abstract
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.
Links
GA201/03/1161, research and development projectName: Verifikace nekonečně stavových systémů
Investor: Czech Science Foundation, Verification of infinite-state systems
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
PrintDisplayed: 26/4/2024 19:31