Abstract
Weak bisimulations are typically used in process algebras where silent steps are used to abstract from internal behaviours. They facilitate relating implementations to specifications. When an implementation fails to conform to its specification, pinpointing the root cause can be challenging. In this paper we provide a generic characterisation of branching-, delay-, η- and weak-bisimulation as a game between Spoiler and Duplicator, offering an operational understanding of the relations. We show how such games can be used to assist in diagnosing non-conformance between implementation and specification. Moreover, we show how these games can be extended to distinguish divergences.
| Original language | English |
|---|---|
| Article number | 15 |
| Number of pages | 40 |
| Journal | Logical Methods in Computer Science |
| Volume | 13 |
| Issue number | 4 |
| DOIs | |
| Publication status | Published - 22 Nov 2017 |
Keywords
- Abstraction
- Behavioural equivalences
- Bisimulation games
- Branching bisimulation
- Divergence
Fingerprint Dive into the research topics of 'Games for bisimulations and abstraction'. Together they form a unique fingerprint.
Cite this
de Frutos Escrig, D., Keiren, J. J. A., & Willemse, T. A. C. (2017). Games for bisimulations and abstraction. Logical Methods in Computer Science, 13(4), [15]. https://doi.org/10.23638/LMCS-13(4:15)2017