Games for Bisimulations and Abstraction

D. de Frutos Escrig, J.J.A. Keiren, T.A.C. Willemse

Research output: Contribution to journalArticleAcademicpeer-review

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-, delayed-, η- 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 languageEnglish
Number of pages40
JournalLogical Methods in Computer Science
Volume13
Issue number4
DOIs
Publication statusPublished - 28 Nov 2017

Fingerprint

Bisimulation
Game
Specification
Specifications
Process Algebra
Algebra
Branching
Divergence
Roots
Internal
Abstraction

Cite this

de Frutos Escrig, D. ; Keiren, J.J.A. ; Willemse, T.A.C. / Games for Bisimulations and Abstraction. In: Logical Methods in Computer Science. 2017 ; Vol. 13, No. 4.
@article{f55c71e4704f4cb1bde5088381bd4f16,
title = "Games for Bisimulations and Abstraction",
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-, delayed-, η- 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.",
author = "{de Frutos Escrig}, D. and J.J.A. Keiren and T.A.C. Willemse",
year = "2017",
month = "11",
day = "28",
doi = "10.23638/LMCS-13(4:15)2017",
language = "English",
volume = "13",
journal = "Logical Methods in Computer Science",
issn = "1860-5974",
publisher = "Technical University of Braunschweig",
number = "4",

}

Games for Bisimulations and Abstraction. / de Frutos Escrig, D. ; Keiren, J.J.A.; Willemse, T.A.C.

In: Logical Methods in Computer Science, Vol. 13, No. 4, 28.11.2017.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

T1 - Games for Bisimulations and Abstraction

AU - de Frutos Escrig, D.

AU - Keiren, J.J.A.

AU - Willemse, T.A.C.

PY - 2017/11/28

Y1 - 2017/11/28

N2 - 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-, delayed-, η- 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.

AB - 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-, delayed-, η- 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.

U2 - 10.23638/LMCS-13(4:15)2017

DO - 10.23638/LMCS-13(4:15)2017

M3 - Article

VL - 13

JO - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

SN - 1860-5974

IS - 4

ER -