| Summary: | Reactive systems \`a 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.
|
|---|