Mathias Hülsbusch ; Barbara König ; Sebastian Küpper ; Lars Stoltenow - Conditional Bisimilarity for Reactive Systems

lmcs:6937 - Logical Methods in Computer Science, January 12, 2022, Volume 18, Issue 1 -
Conditional Bisimilarity for Reactive Systems

Authors: Mathias Hülsbusch ; Barbara König ; Sebastian Küpper ; Lars Stoltenow

    Reactive systems à la Leifer and Milner, an abstract categorical framework for rewriting, provide a suitable framework for deriving bisimulation congruences. This is done by synthesizing interactions with the environment in order to obtain a compositional semantics. We enrich the notion of reactive systems by conditions on two levels: first, as in earlier work, we consider rules enriched with application conditions and second, we investigate the notion of conditional bisimilarity. Conditional bisimilarity allows us to say that two system states are bisimilar provided that the environment satisfies a given condition. We present several equivalent definitions of conditional bisimilarity, including one that is useful for concrete proofs and that employs an up-to-context technique, and we compare with related behavioural equivalences. We consider examples based on DPO graph rewriting, an instantiation of reactive systems.

    Volume: Volume 18, Issue 1
    Published on: January 12, 2022
    Accepted on: October 29, 2021
    Submitted on: November 30, 2020
    Keywords: Computer Science - Logic in Computer Science


    Consultation statistics

    This page has been seen 464 times.
    This article's PDF has been downloaded 478 times.