Undecidability of domino games and hhp-bisimilarity

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,...

Full description

Saved in:
Bibliographic Details
Published in:Information and computation 2003-08, Vol.184 (2), p.343-368
Main Authors: Jurdziński, Marcin, Nielsen, Mogens, Srba, Jiřı́
Format: Article
Language:English
Subjects:
Applied sciences
Automata. Abstract machines. Turing machines
Computer science
control theory
systems
Computer systems and distributed systems. User interface
Exact sciences and technology
Language theory and syntactical analysis
Software
Software engineering
Theoretical computing
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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 asynchronous 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.
ISSN:0890-5401
1090-2651
DOI:10.1016/S0890-5401(03)00064-6