David De Frutos Escrig ; Jeroen J. A. Keiren ; Tim A. C. Willemse - Games for Bisimulations and Abstraction

lmcs:2192 - Logical Methods in Computer Science, November 28, 2017, Volume 13, Issue 4 - https://doi.org/10.23638/LMCS-13(4:15)2017
Games for Bisimulations and AbstractionArticle

Authors: David De Frutos Escrig ; Jeroen J. A. Keiren ORCID; Tim A. C. Willemse

    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-, $\eta$- 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.


    Volume: Volume 13, Issue 4
    Published on: November 28, 2017
    Accepted on: November 8, 2017
    Submitted on: November 3, 2016
    Keywords: Computer Science - Logic in Computer Science

    3 Documents citing this article

    Consultation statistics

    This page has been seen 2105 times.
    This article's PDF has been downloaded 691 times.