Undecidability of Domino Games and Hhp-Bisimilarity

Investor logo

Warning

This publication doesn't include Faculty of Sports Studies. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

JURDZINSKI Martin MOGENS Nielsen SRBA Jiří

Year of publication 2003
Type Article in Periodical
Magazine / Source Information and Computation
MU Faculty or unit

Faculty of Informatics

Citation
Web http://www.brics.dk/~srba/publ.html
Field Informatics
Keywords partial order; bisimilarity; domino games
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.

More info