Conditional Bisimilarity for Reactive Systems

M. Hülsbusch]Mathias Hülsbuscha
B. König]Barbara Königa
S. Küpper]Sebastian Küpperb
L. Stoltenow]Lars Stoltenowa

Universität Duisburg-Essen, Germany

FernUniversität in Hagen, Germany

<concept_desc>Theory of computation Concurrency</concept_desc>
<concept_desc>Theory of computation Program reasoning</concept_desc>

[500]Theory of computation Concurrency
[500]Theory of computation Program reasoning

[Theory of computation]:
Semantics and reasoning — Program reasoning;
[Theory of computation]:
Models of computation — Concurrency

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.

§ INTRODUCTION

Behavioural equivalences, such as bisimilarity, relate system states
with the same behaviour. Here, we are in particular interested in
conditional bisimilarity, which allows us to say that two states $a,b$
are bisimilar provided that the environment satisfies a condition
$\mathcal{C}$. Work on such conditional bisimulations appears somewhat
scattered in the literature (see for instance [21, 16, 12, 4]). They
also play a role in the setting of featured transition systems for
modelling software product lines [8],
where the behaviour of many products is specified in a single
transition system. In this setting it is possible to state that two
states are bisimilar for certain products, but not for others.

We believe that conditional notions of behavioural equivalence are
worthy of further study. In practice it may easily happen that two
sub-systems are only ever used in restricted environments and it is
too much to ask that they behave equivalently under all possible
contexts. Furthermore, instead of giving a simple yes/no-answer,
bisimulation checks can answer in a more fine-grained way, specifying
conditions which ensure bisimilarity.

We state our results in a very general setting: reactive systems à
la Leifer and Milner [22], a categorical abstract framework for
rewriting, which provides a suitable framework for deriving
bisimulation congruences. In particular, this framework allows to
synthesize labelled transitions from plain reaction rules, such that
the resulting bisimilarity is automatically a congruence. Intuitively,
the label is the minimal context that has to be borrowed from the
environment in order to trigger a reduction. (Transitions labelled
with such a minimal context will be called
representative steps in the sequel. They are related to the idem pushout steps of [22].)  Here, we rely on the notion of saturated bisimilarity
introduced in [5] and we consider reactive system
rules with application conditions, generalizing [15].

Important instances of reactive systems are process calculi
with contextualization, bigraphs [19] and
double-pushout graph rewriting [9],
or in general rewriting in
adhesive categories [23]. Hence we can use our
results to reason about process calculi as well as dynamically
evolving graphs and networks for various different types of graphs
(directed or undirected graphs, node- or edge-labelled graphs, hypergraphs, etc.).

Our contributions in this paper can be summarized as follows:

* We define the notion of conditional bisimilarity, in fact we
provide three equivalent definitions: two notions are
derived from saturated bisimilarity, where a context step (or a
representative step) can be mimicked by several answering
steps. Third, we compare with the notion of conditional environment
congruence, which is based on the idea of annotating transitions
with passive environments enabling a step.

* Conditional bisimulation relations tend to
be very large — often infinite in size.
To obtain possibly substantial reductions of proof obligations in a bisimulation proof,
we propose an up-to context technique (for up-to techniques and their
history see [29]).
In particular, it can replace an infinite conditional bisimulation relation by a possibly finite
bisimulation up-to context, which provides a witness for bisimilarity.
We also view our up-to technique in a general lattice-theoretical setting
and prove the compatibility property [28], which
not only implies soundness of the technique, but also allows it to be
composed with other (compatible) up-to techniques.

* We use the notion of representative steps in order to
obtain finitely branching transition systems, further reducing proof

* We compare conditional bisimilarity with
related notions of behavioural equivalence.

* To illustrate our concepts, we
work out a small case study in the context of double-pushout graph
rewriting, where we model message passing over reliable and unreliable

The article is structured as follows: First, in
<Ref> we introduce the fundamental
ideas for reactive systems without conditions, including all
preliminary definitions and techniques developed for reactive systems
relevant to our work. In <Ref>, we consider the
refinement to conditional reactive systems, before we turn towards our
main contribution in <Ref>, which is conditional
bisimulation and its up-to variant in <Ref>.  In
<Ref> we give an alternative characterization of
conditional bisimilarity and compare to related notions of behavioural
equivalence and we conclude in <Ref>.

§ REACTIVE SYSTEMS

We denote the composition of arrows
$f \colon A \to B,\ g \colon B \to C$ by ${f;g} \colon A \to C$.
Usually written $g \circ f$, we chose $f;g$ to better match the
reading order of the diagram
$A \xrightarrow f B \xrightarrow g C = A \xrightarrow{f;g} C$.

§.§ Reactive Systems without Conditions

We now define reactive systems, which were introduced in [22]
and extended in [15] with application conditions for rules.
We initially only look at reactive systems without conditions.
Conditions and the definition of reactive systems with conditions will
be introduced later, in <Ref>.

[Reactive system rules, reaction]
Let $\catname C$ be a category with a distinguished object $\obnull$

(not necessarily initial).  A rule is a pair $(\ell,r)$ of
arrows $\ell,r \colon {\obnull \to I}$ (called left-hand side and
right-hand side).  A reactive system is a set of rules.

Let $\mathcal S$ be a reactive system and
$a, a' \colon \obnull \to J$ be arrows. We say that $a$
reduces to $a'$ ($a \leadsto a'$) whenever there exists a
rule $(\ell,r) \in \mathcal S$ with $\ell,r \colon \obnull \to I$
and an arrow $c \colon I \to J$ (the reactive context) such
that $a = \ell;c$ and $a' = r;c$.

Using a notation closer to process calculi, we could write
$C[P]\leadsto C[P']$ whenever there is a reaction rule $P\to P'$ and a
context $C[\_]$. Fixing a distinguished object $0$ means that we
consider only ground reaction rules (as opposed to the open reactive
systems investigated in [20]).

An important instance are reactive systems where the arrows are
cospans in a base category $\catname D$ with pushouts [33, 32].  A cospan is a pair of
arrows .  A cospan is
input linear if its left arrow $f_L$ is mono.

(a) at (--,0) $A$;
(x) at (-,0) $X$;
(b) at (0,) $B$;
(y) at (,0) $Y$;
(c) at (+,0) $C$;
(z) at (0,-) $Z$;

[cospanint] (a) – node[above]$f_L$ (x);
[cospanint] (b) – node[above,pos=0.7]$f_R\ $ (x);
[cospanint] (b) – node[above,pos=0.7]5pt$g_L$ (y);
[cospanint] (c) – node[above]$g_R$ (y);

[cospanint] (x) – node[below,pos=0.4]$p_L$8pt (z);
[cospanint] (y) – node[below,pos=0.4]12pt$p_R$ (z);

[cospanarr] (a) to[bend left=30] node[above,pos=0.2]$f$ (b);
[cospanarr] (b) to[bend left=30] node[above,pos=0.8]$\ g$ (c);
[cospanarr] (a) to[bend right=50] node[below]$f;g$ (c);

at (0,0) ;

Composition of cospans $f$ and $g$ is done via pushouts

(d) at (0,0) $\obnull$;
(l) at (,0) $L$;
(i) at (2*,0) $I$;
(r) at (3*,0) $R$;
(r0) at (4*,0) $\obnull$;
(g) at (1*,-1*) $G$;
(c) at (2*,-1*) $C$;
(h) at (3*,-1*) $H$;
(k) at (2*,-2*) $\obnull$;

(d) edge (l) edge (g)
(l) edge (g)
(i) edge (c)
(r) edge (h)
(r0) edge (r) edge (h);
(k) edge (g) edge (c) edge (h)
(i) edge (l) edge (r)
(c) edge (h) edge (g);

[cospanarr] (d.north east) to[bend left =10] node[above]$\ell$ (i.north west);
[cospanarr] (d.south) to[bend right=10] node[left ]$a\ $ (k.west);
[cospanarr] (i.south west) to[bend right=10,pos=0.2] node[left]$c$ (k.north west);
[cospanarr] (r0.north west) to[bend right=10] node[above]$r$ (i.north east);
[cospanarr] (r0.south) to[bend left=10] node[right]$a^\prime$ (k.east);

Double-pushout graph transformation as reactive system steps

Two cospans
are composed by taking
the pushout $(p_L, p_R)$ of $(f_R, g_L)$ as shown in
<Ref>.  The result is the cospan
, where $Z$ is the pushout object of $f_R,\; g_L$.  For
adhesive categories [23] (see
), the composition of input linear
cospans again yields an  linear cospan (by applying <cit.> to the cospan composition
diagram).  Given an  category $\catname D$,
$\ILC(\catname D)$ is the category where the objects are the objects
of $\catname D$, the arrows $f\colon A\rightarrow C$ are
linear cospans $f\colon A \rightarrow B \leftarrow C$
of $\catname D$ and composition is performed via pushouts as
described above.  We see an arrow $f \colon A \to C$ of
$\ILC(\catname D)$ as an object $B$ of $\catname D$ equipped with
two interfaces $A,C$ and corresponding arrows $f_L,f_R$ to relate
the interfaces to $B$, and composition glues the inner objects of
two cospans via their common interface.  Input linearity is useful
since we rely on adhesive categories where pushouts along monos are
well-behaved. In particular, they always exist and form Van Kampen
squares (see Appendix <ref>),
the latter being a requirement for borrowed context
diagrams (<Ref>).

In this article, as a running example we consider the category $\catname\Graphfin$,
which has finite graphs (we use directed multigraphs with node and edge labels) as objects and
total graph morphisms (functions that map nodes and edges of one graph to another, with the edge map being consistent to the node map) as arrows.

In $\catname\Graphfin$, monos are

exactly the injective graph morphisms.  We then use reactive systems
over $\ILC(\catname\Graphfin)$ (input-linear cospans of graphs),
i.e. we rewrite graphs with interfaces.  If the distinguished object
$0$ is the empty graph (the initial object of $\catname\Graphfin$),
such reactive systems  [33] with the

well-known double pushout (DPO) graph transformation
approach [11, 17] when used with injective matches.  As
shown in <Ref>, a DPO rewrite step $G \Rightarrow H$
can be expressed as a reactive system reaction $a \leadsto a'$ where
the pushouts of the DPO step are obtained from cospan compositions
$\ell;c$ and $r;c$.

§.§ Deriving Bisimulation Congruences

The reduction relation $\leadsto$ generates an unlabelled transition
system, where the states are the reactive agents (in our example, graphs).
Note that bisimilarity on this transition system only checks whether any reaction is possible: for two bisimilar agents, it is not required that the same rule is used in their reactions, or even that the reaction is applied at the same position.

A disadvantage of bisimilarity on $\leadsto$ is that it usually is not a
congruence: it is easy to construct an example where neither $a$ nor
$b$ can perform a step since no complete left-hand side is
present (hence $a$ would be bisimilar to $b$). However, by adding a suitable context $f$, $a;f$ could contain a
full left-hand side and can reduce, whereas $b;f$ can not.

Therefore, to check whether two components can be exchanged, they have
to be combined with every possible context and bisimilarity has to be
shown for each.

In order to obtain a congruence, we can resort to defining
bisimulation on labelled transitions, using as labels the additional
contexts that allow an agent to react [22, 15].

[Context step (without conditions) [15]]

[use as bounding box] (-0.1-0.21,0.45) rectangle (2*+0.1,--0.2);

(tlempty) at (0,0) $\obnull$;
(i) at (1*,0) $I$;
(trempty) at (2*,0) $\obnull$;
(j) at (0,-) $J$;
(k) at (1*,-) $K$;
[->] (tlempty) – node[above]$\ell$ (i);
[->] (trempty) – node[above]$r$ (i);
[->] (trempty) – node[below,pos=0.3]$a^\prime$ (k);

[->] (tlempty) – node[left]$a$ (j);
[->] (i) – node[left]$c$ (k);

[->] (j) – node[above,pos=0.45]$f$ (k);

Let $\mathcal S$ be a reactive system and $a \colon \obnull \to J,\ f \colon J \to K,\ a' \colon \obnull \to K$ be arrows.
We write $a \nccstep{f} a'$ whenever $a;f \leadsto a'$ (i.e. there exists a rule $(\ell,r) \in \mathcal S$
and an arrow $c$ such that $a;f = \ell;c,\allowbreak\ a' = r;c$).
Such steps are called context steps.

Intuitively we have to find a context $f$ for the arrow $a$ (which we
want to rewrite) such that we obtain the left-hand side $\ell$ plus
some additional context $c$.
The name context step stems from the fact that $a$ might not be
able to do a reaction
on its own, but requires an additional context $f$. This can be seen in the
following example:

[Context step (without conditions)]
Consider the following reactive system over $\ILC(\catname\Graphfin)$,
i.e. all arrows (such as $\ell, r, \dots$) are input-linear cospans of graphs that represent graphs with interfaces.
We model a network of nodes that pass messages (represented by $m$-loops) over
communication channels (represented by $\chanLabel$-edges).
The transmission of a message from the left node to the right node can be represented with the following rule:

[gedge/.append style=font=]
(#2) at (0,0) [draw,roundbox,minimum width=2cm, minimum height=1.25cm] ;
[anchor=west] at (-1cm,-0.35) $\scriptstyle{#1}$;

(#1) at (0,0.15cm) [draw,roundbox,minimum width=2cm, minimum height=0.95cm] ;

[gn] (l) at (-0.35,0.05) ;
[gn] (r) at (0.35,0.05) ;

[gedge] (l) to node[above]$\chanLabel$ (r);

[gedge] (l.120) to[loop,out=120+30,in=120-30,distance=0.3cm] node[left]$m\mkern-5mu$ (l.90);
[gedge] (r.90) to[loop,out=60+30,in=60-30,distance=0.3cm] node[right]$\mkern-2mu m$ (r.60);
(leftnull) at (0,0.15cm) [draw,roundbox,minimum width=0.5cm, minimum height=0.95cm] ;

(rightnull) at (0,0.15cm) [draw,roundbox,minimum width=0.5cm, minimum height=0.95cm] ;

[inner xsep=0cm,anchor=east] at (-2.4,0) $P = \bigg($;
[inner xsep=0cm,anchor=west] at (8.4,0) $\bigg)$;
[cospanint] (leftnull) – (leftbox);
[cospanint] (ifbox) – (leftbox);
[cospanint] (ifbox) – (rightbox);
[cospanint] (rightnull) – (rightbox);

[cospanarr] (-2,0.7) to[bend left=20] node[above,overlay]$\ell$ (3-0.25,0.85);
[cospanarr] (8,0.7) to[bend right=20] node[above,overlay]$r$ node[above] (3+0.25,0.85);

at (0,0.8) $L$;
at (3,0.8) $I$;
at (6,0.8) $R$;

All graph morphisms are induced by edge labels and position of nodes,
i.e. the left node is always mapped to the left node.

We can observe that a channel by itself
($a = {\emptyset \rightarrow \inlinechan{chan} \leftarrow \inlinechan{}}$)
cannot do a reaction, since there is no message to be transferred.
However, if a message on the left node is borrowed
we obtain $a;f$ (<Ref>),
to which the example rule can be applied (<Ref>).
As a result, we obtain the context step
$a \nccstep{f} a'$ or
${(\emptyset \rightarrow \inlinechan{chan} \leftarrow \inlinechan{})}
\nccstep{(\inlinechan{} \rightarrow \loopOnArrow{\inlinechan{msgleft}} \leftarrow \inlinechan{})}
{(\emptyset \rightarrow \inlinechan{chan,msgright} \leftarrow \inlinechan{})}$.

(#2) at ($(\boxSxp,\boxSyp)!.5!(-\boxSxm,-\boxSym)$) [draw,roundbox,minimum width=cm, minimum height=cm] ;
[anchor=west] at (-,-0.3) $\scriptstyle{#1}$;

[cospanint] (#1) edge (#2);

[cospanarr] (#1.#6) to[#7] node[#5]$#4$ (#3.#6);

[gn] (l) at (0,0.05) ;
[gn] (r) at (0.5,0.05) ;

[gedge] (l) to node[above]$\chanLabel$ (r);

[gedge] (l.120) to[loop,out=120+30,in=120-30,distance=0.3cm] node[left]$m\mkern-5mu$ (l.90);
[gedge] (r.90) to[loop,out=60+30,in=60-30,distance=0.3cm] node[right]$\mkern-2mu m$ (r.60);

at ($(2*\gridx,2*\gridy - \boxSym - 0.6)$) ;
at ($(2*\gridx,0*\gridy + \boxSyp + 0.6)$) ;

at ($(boxnull)!0.5!(Gp)$) ;
at ($(L)!0.5!(C)$) ;
at ($(G)!0.5!(F)$) ;
at ($(Gp)!0.5!(K)$) ;

[gedge/.append style=font=, cospanarr/.append style=font=,y=1.00cm]
[cospanarr] (boxnull.south west) to[bend right=12] node[left]$a$ (N0.north west);
[cospanarr] (N0.south east) to[bend right=10] node[below]$f$ (N0r.south west);
[cospanarr] (boxnull.east) to[bend left=25] node[above right]$a;f$ (N0r.north);

A channel $a$ together with borrowed context $f$, resulting in $a;f$.

[gedge/.append style=font=, cospanarr/.append style=font=,y=1.00cm]

(boxnull) at ($(\boxSxp,0)!.25!(-\boxSxm,0) + (0,\boxSyp)!.5!(0,-\boxSym) + (0*\gridx,0)$) [draw,roundbox,minimum width=0.5*cm, minimum height=cm] ;
(boxnullr) at ($(\boxSxp,0)!.75!(-\boxSxm,0) + (0,\boxSyp)!.5!(0,-\boxSym) + (4*\gridx,0)$) [draw,roundbox,minimum width=0.5*cm, minimum height=cm] ;
[anchor=west] at ($(-\boxSxm,-0.3) + (0*\gridx,0) + (\boxW*0.5,0)$) $\scriptstyle{\obnull}$;
[anchor=west] at ($(-\boxSxm,-0.3) + (4*\gridx,0)$) $\scriptstyle{\obnull}$;

[cospanarr] (boxnull.north east) to[bend left=10] node[above]$\ell$ (I.north west);
[cospanarr] (boxnullr.north west) to[bend right=10] node[above]$r$ (I.north east);
[cospanarr] (boxnull.south) to[bend right=25] node[below left]$a;f$ (K.west);
[cospanarr] (boxnullr.south) to[bend left=25] node[below right]$a'$ (K.east);
[cospanarr] (I.south east) to[bend left=12,pos=0.3] node[right]$c$ (K.north east);

$a;f$ can now do a reaction to $a' = r;c$.

Visualization of the context step described in <Ref>.

A bisimulation relation over $\rightarrow_C$ is called saturated
bisimulation, as it checks all contexts. Consequently, saturated
bisimilarity $\simC$ (${\sim_{S\mkern-2mu AT}}$ in [15]) is
a congruence [5, 15], i.e., it is closed under
contextualization. In other words $a \mathrel{\simC} b$ implies $a;c \mathrel{\simC} b;c$
for all contexts $c$.

§.§ Representative Squares

Checking bisimilarity of context steps is impractical
because the transition system is generally infinitely branching:
usually, $f$ can be chosen from an infinite set of possible
contexts, which all have to be checked.  Most of these contexts are
larger than necessary, that is, they contain elements that do not
actively participate in the reduction.  (In
<Ref>, contexts can be arbitrarily large, as

long as they have an $m$-loop on the left node.)  An improvement
would be to check only the minimal contexts from which all
other context steps can be derived.

When checking which contexts are required to make a rule applicable,

in the reaction diagram (<Ref>) the arrows $a, \ell$ are
given and we need to check for possible values of $f$ (which generate
matching $c, a'$).  To derive a set of contexts $f$ which is as small
as possible — preferably finite — [3, 15] introduced the
notion of representative squares, which describe a way to represent
all possible squares that close a pair $a,\ell$ by a smaller set of
squares (the so-called representative squares).  We can then limit
bisimilarity checking to just the steps using representative squares,
which, if this smaller set is indeed finite, leads to a finitely
branching transition system.

(a) at (0,0) $A$;
(b) at (-,0) $B$;
(c) at (0,-+) $C$;
(ds) at (-,-+) $D'$;
[->] (a) – node[above]$\alpha_1$ (b);
[->] (a) – node[left]$\alpha_2$ (c);

[->] (b) – node[right]$\delta_1$ (ds);
[->] (c) – node[below]$\delta_2$ (ds);

at (+1,-0.5*) $\rightarrow$;

(a) at (0,0) $A$;
(b) at (-,0) $B$;
(c) at (0,-+) $C$;
(d) at (--,-++) $D$;
(ds) at (,-) $D'$;
[->] (a) – node[above]$\alpha_1$ (b);
[->] (a) – node[left]$\alpha_2$ (c);
[->] (b) – node[left,pos=0.25]$\beta_1$ (d);
[->] (c) – node[above,pos=0.3]$\beta_2$ (d);

[->] (d.center)+(5pt,-5pt) – (ds);
at ($(d.center)+(12pt,-4pt)$) $\gamma$;
[->] (b) – node[right]$\delta_1$ (ds);
[->] (c) – node[below]$\delta_2$ (ds);

Every commuting square of the category (left) can be reduced to a representative square in $\kappa$ and an arrow $\gamma$ which extends the representative square to the original square (right).

[Representative squares [3]]
A class $\kappa$ of commuting squares in a category $\catname C$ is representative if $\kappa$ satisfies the following condition:
for each commuting square $(\alpha_1, \alpha_2, \delta_1, \delta_2)$ in $\catname C$
there exists a commuting square $(\alpha_1, \alpha_2, \beta_1, \beta_2)$ in $\kappa$ and an arrow $\gamma$,
such that $\delta_1 = \beta_1;\gamma,\ \delta_2 = \beta_2;\gamma$.
This situation is depicted in <Ref>.

For two arrows $\alpha_1 \colon A \to B,\ \alpha_2 \colon A \to C$,
we define $\kappa(\alpha_1,\alpha_2)$ as the set of pairs of arrows $(\beta_1,\beta_2)$ which,
together with $\alpha_1,\alpha_2$, form representative squares in $\kappa$.

The original paper on reactive systems [22] used the (more restrictive)
notion of idem pushouts  of representative
squares. Unfortunately, the universal property of idem pushouts leads
to complications, in particular for cospan categories, where one has
to resort to the theory of bicategories in order to be able to express
this requirement. For the purposes of this paper, we stick to the
simpler notion of representative squares, in order to keep our
results independent of the concrete class of squares chosen.

The question arises which constructions yield suitable classes of representative squares, ideally with finite $\kappa(\alpha_1,\alpha_2)$, in order to represent all possible contexts $\delta_1,\delta_2$ with a finite set of representative contexts $\beta_1,\beta_2$.
Pushouts can be used when they exist [15], however, they do not exist for $\ILC(\catname\Graphfin)$.

For cospan categories over adhesive categories, borrowed context
diagrams — initially introduced as an extension of DPO
rewriting [10] — can be used as representative squares. Before
we can introduce such diagrams, we first need the notion of jointly

[Jointly epi]
A pair of arrows $f \colon B \to D,\ g \colon C \to D$ is
jointly epi (JE) if for each pair of arrows
$d_1, d_2 \colon D \to E$ the following holds: if $f;d_1 = f;d_2$
and $g;d_1 = g;d_2$, then $d_1 = d_2$.

In $\catname\Graphfin$ jointly epi equals jointly surjective, meaning
that each node or edge of $D$ is required to have a preimage under $f$
or $g$ or both (it contains only images of $B$ or $C$).

This criterion is similar to, but weaker than a pushout:
For jointly epi graph morphisms $d_1 \colon B \to D,\ d_2 \colon C \to D$,
there are no restrictions on which elements of $B,C$ can be merged in $D$.
However, in a pushout constructed from morphisms $a_1 \colon A \to B,\ a_2 \colon A \to C$,
elements in $D$ can (and must) only be merged if they have a common preimage in $A$.
(Hence every pushout generates a pair of jointly epi arrows, but not vice versa.)

[Borrowed context diagram [15]]
A commuting diagram in the category $\ILC(\catname C)$, where
$\catname C$ is adhesive, is a borrowed context diagram
whenever it has the form of the diagram shown in <Ref>,
and the four squares in the base category $\catname C$ are pushout
(PO), pullback (PB) or jointly epi (JE) as indicated. In particular
$L\rightarrowtail G^+$, $G\rightarrowtail G^+$ must be jointly epi.

<Ref> shows a more concrete version of
<Ref>, where graphs and their overlaps are depicted by
Venn diagrams (assuming that all morphisms are injective). Because of
the two pushout squares, this diagram can be interpreted as
composition of cospans $a;f = \ell;c = D \rightarrow G^+ \leftarrow K$
with extra conditions on the top left and the bottom right square.
The top left square fixes an overlap $G^+$ of $L$ and $G$, while $D$
is contained in the intersection of $L$ and $G$ (shown as a hatched
area). Being jointly epi ensures that it really is an overlap and does
not contain unrelated elements.

The top right pushout corresponds to the left
pushout of a DPO rewriting diagram. It contains a total match of $L$
in $G^+$.  Then, the bottom left pushout gives us the minimal borrowed
context $F$ such that applying the rule becomes possible.

The bottom right pullback ensures that the interface $K$ is as large
as possible.

will discuss an example of a borrowed context diagram below
(<Ref>).  For additional examples, we refer to [10].

[use as bounding box] (-0.7,0.8) rectangle (2*+0.7,-2*-0.87);

(d) at (0,0) $D$;
(l) at (,0) $L$;
(i) at (,0) $I$;
(g) at (0,-) $G$;
(gp) at (,-) $\mkern-3mu G^+\mkern-5mu$;
(c) at (,-) $C$;
(j) at (0,-) $J$;
(f) at (,-) $F$;
(k) at (,-) $K$;

at (0.5*,-0.5*) ;
at (1.5*,-0.5*) ;
at (0.5*,-1.5*) ;
at (1.5*,-1.5*) ;

(d) edge (l) edge (g)
(l) edge (gp)
(g) edge (gp)
(i) edge (c)
(j) edge (f);
(j) edge (g)
(k) edge (f) edge (c)
(f) edge (gp)
(i) edge (l)
(c) edge (gp);

[cospanarr] (d.north east) to[bend left =10] node[above]$\ell$ (i.north west);
[cospanarr] (d.south west) to[bend right=10] node[left ]$a$ (j.north west);
[cospanarr] (i.south east) to[bend left =10] node[right]$c$ (k.north east);
[cospanarr] (j.south east) to[bend right=10] node[below]$f$ (k.south west);

Structure of a borrowed context diagram.
The inner, lighter arrows are morphisms of the base category $\catname C$,
while the outer arrows are morphisms of $\ILC(\catname C)$.

((0.05,0) ellipse[x radius=0.53, y radius=0.24]
((0.05,0) ellipse[x radius=0.65, y radius=0.36]
((0.6,0.14) circle[radius=0.28]
((0.6,0.14) circle[radius=0.4]
(-,-) rectangle (,)

ịn 0,1,...,20
[black!40, line width=0.7pt] (0, -1cm + 0.3pt + *̣2pt) – +(1cm,1cm);

[vennfill] ;

[vennfill] ;

[vennfill] ;

[vennfill] ;

[cospanint] (#1) edge (#2);

at ($(boxnull)!0.5!(Gp)$) ;
at ($(L)!0.5!(C)$) ;
at ($(G)!0.5!(F)$) ;
at ($(Gp)!0.5!(K)$) ;

Borrowed context diagrams represented as Venn diagrams.
The outer circles represent graphs $L,G$, and
the area between the inner and outer circles represents their interfaces $I,J$.

Borrowed context diagrams

For cospan categories over adhesive categories, borrowed context
diagrams form a representative class of
squares [3]. Furthermore, for some categories (such as
$\catname\Graphfin$), there are — up to isomorphism — only finitely
many jointly epi squares for a given span of monos and hence only
finitely many borrowed context diagrams given $a,\ell$ (since pushout
complements along monos in adhesive categories are unique up to

This motivates the following finiteness assumption that we will refer
to in this paper: given $a,\ell$, we require that $\kappa(a,\ell)$
is finite. (Fin)

§.§ Representative Steps

It is possible to define a reaction relation based on representative squares.
By requiring that the left square is representative, we ensure that the contexts $\hat f$ are not larger than necessary:

[Representative step (without conditions) [15]]
Let  $a' \colon \obnull \to K$ be arrows.
We write $a \ncrstep{\hat f} a'$ if a context step $a \nccstep{\hat f} a'$ is possible
(i.e. $a;\hat f \leadsto a'$, i.e. for some rule $(\ell,r)$ and some arrow $\hat c$ we have $a;\hat f = \ell;\hat c$ and $r;\hat c = a'$)and additionally $\kappa(a,\ell) \ni (\hat f,\hat c)$ (i.e. the arrows $(a,\ell,\hat f,\hat c)$ form a representative square).
Such steps are called representative steps.

<Ref> imply that every context step
$a \nccstep{f} a'$ (left diagram)
can be reduced to a representative step
$a \ncrstep{\hat f} r;\hat c$ (right diagram), a fact used in the

0pt plus 1filll

(a) at (0,0) $\obnull$;
(b) at (-+,0) $I$;
(c) at (0,-+-) $J$;
(ds) at (-+,-+-) $K$;
[->] (a) – node[above]$\ell$ (b);
[->] (a) – node[left]$a$ (c);

[->] (b) – node[right,pos=0.4]$c$ (ds);
[->] (c) – node[above]$f$ (ds);

(r0) at (-+ ,0) $\obnull$;
[->] (r0) – node[above]$r$ (b);
[->] (r0) – node[right]$a'$ (ds);

at (4.5,-0.45*) $\rightarrow$;

(a) at (0,0) $\obnull$;
(b) at (-,0) $I$;
(c) at (0,-+) $J$;
(d) at (--,-++) $K'$;
(ds) at (,-) $K$;
[->] (a) – node[above]$\ell$ (b);
[->] (a) – node[left]$a$ (c);
[->] (b) – node[left,pos=0.3]$\hat c$ (d);
[->] (c) – node[above,pos=0.3]$\hat f$ (d);

[->] (d.center)+(5pt,-5pt) – (ds);
at ($(d.center)+(12pt,-3pt)$) $\hat g$;
[->] (b) to[bend left=15] node[right,pos=0.4]$c$ (ds);
[->] (c) – node[below]$f$ (ds);

(r0) at (-+ ,0) $\obnull$;
[->] (r0) – node[above]$r$ (b);
[->] (r0) – node[right]$a'$ (ds);

0pt plus 1filll

For this, we construct the representative square $(a,\ell,\hat f,\hat c) \in \kappa$ (which, according to <Ref>, always exists) from the square $(a,\ell,f,c)$ describing the context step.
We obtain arrows $\hat f, \hat c$ and an arrow $\hat g$ which completes $\hat f, \hat c$ to $f,c$ (i.e. $\hat f ; \hat g = f,\ \hat c ; \hat g = c$).

[Representative steps]
Reconsider the reactive system described in Example <ref>,
i.e., a message $m$ can be transferred along a channel $\chanLabel$.
One possible context step allows a channel $\inlinechan{chan}$ to borrow a message $\inlinechan{msgleft}$ (depicted in <Ref>) and do a transfer:
${(\emptyset \rightarrow \inlinechan{chan} \leftarrow \inlinechan{})}
\nccstep{(\inlinechan{} \rightarrow \loopOnArrow{\inlinechan{msgleft}} \leftarrow \inlinechan{})}
{(\emptyset \rightarrow \inlinechan{chan,msgright} \leftarrow \inlinechan{})}$.

Another possible context step is to borrow an additional message on the right node, i.e.
${(\emptyset \rightarrow \inlinechan{chan} \leftarrow \inlinechan{})}
\nccstep{(\inlinechan{} \rightarrow \loopOnArrow{\inlinechan{msgleft,msgright}} \leftarrow \inlinechan{})}
{(\emptyset \rightarrow \inlinechan{chan,msgright=2} \leftarrow \inlinechan{})}$
(depicted in ).
Clearly, this is a valid context step, but the right message is not required by the rule, and we do not want to consider such steps in our analysis (by adding yet more messages, we obtain infinitely many context steps).

(#2) at ($(\boxSxp,\boxSyp)!.5!(-\boxSxm,-\boxSym)$) [draw,roundbox,minimum width=cm, minimum height=cm] ;
at (-0.35,-0.25) $\scriptstyle{#1}$;

[cospanint] (#1) edge (#2);

[cospanarr] (#1.#6) to[#7] node[#5]$#4$ (#3.#6);

[gn] (l) at (0,0) ;
[gn] (r) at (0.5,0) ;

[gedge] (l) to node[below]$\chanLabel$ (r);

[gedge] (l.150) to[loop,out=135+30,in=135-30,distance=0.3cm] node[left]$m\mkern-5mu$ (l.120);
[gedge] (r.60) to[loop,out=45+30,in=45-30,distance=0.3cm] node[right]$\mkern-2mu m$ (r.30);

at ($(boxnull)!0.5!(Gp)$) ;
at ($(L)!0.5!(C)$) ;
at ($(G)!0.5!(F)$) ;
at ($(Gp)!0.5!(K)$) ;

[gedge/.append style=font=, cospanarr/.append style=font=]
11 G^+Gp
[cospanarr] (boxnull.north east) to[bend left=10] node[above]$\ell$ (I.north west);
[cospanarr] (boxnull.south west) to[bend right=12] node[left]$a$ (J.north west);
[cospanarr] (J.south east) to[bend right=10] node[below]$f$ (K.south west);
[cospanarr] (I.south east) to[bend left=12] node[right]$c$ (K.north east);

Borrowed context diagram for a channel  a message on the left node

[gedge/.append style=font=, cospanarr/.append style=font=]
11 G^+Gp
[cospanarr] (boxnull.north east) to[bend left=10] node[above]$\ell$ (I.north west);
[cospanarr] (boxnull.south west) to[bend right=12] node[left]$a$ (J.north west);
[cospanarr] (J.south east) to[bend right=10] node[below]$f$ (K.south west);
[cospanarr] (I.south east) to[bend left=12] node[right]$c$ (K.north east);

Commuting diagram for a channel additionally borrowing a message on the right, which is not needed for the reaction

Diagrams for the two steps described in <Ref>.

However, the second context step is not a representative step
(assuming that representative squares correspond to borrowed context
We try to construct a borrowed context diagram: First we fill in the graphs given by $a$, $f$ and $\ell$,
then we construct the bottom left pushout, we obtain $G^+ = \inlinechan{chan,msgleft,msgright}$ as depicted in <Ref>.
Then however the top left square is not jointly epi, since neither $L = \inlinechan{chan,msgleft}$ (from $\ell$) nor $G = \inlinechan{chan}$ (from $a$) provide a preimage for the right $m$-loop $\inlinechan{msgright}$.

On the other hand, the first context step is representative, since there $G^+ = \inlinechan{chan,msgleft}$ does not contain the problematic right $m$-loop and it is possible to complete the borrowed context diagram as shown in <Ref>.
(To obtain the result of the context step, the right-hand side $a'$ is constructed just as for context steps (see <Ref>), which is not depicted here.)

In a semi-saturated bisimulation, $\rightarrow_R$-steps are
answered by $\rightarrow_C$-steps (for every  and step
$a \ncrstep{f} a'$ there is $b \nccstep{f} b'$ such that
$(a',b') \in R$ and vice versa).  The resulting bisimilarity $\simR$ is
identical [15] to saturated bisimilarity (i.e.
$\simR = \simC$) and therefore also a congruence. Whenever
(Fin) holds, $\sim_R$ is amenable to mechanization, since
we have to consider only finitely many $\rightarrow_R$-steps
($\rightarrow_R$ is finitely branching).

Note that answering $\rightarrow_R$-steps with $\rightarrow_R$-steps gives a different, finer notion of behavioural equivalence than answering $\rightarrow_R$-steps with $\rightarrow_C$-steps.
As an example, consider the reactive system with two rules:
$\inlinerr{a,b} \Rightarrow \inlinerr{a,b}$ and $\inlinerr{c}
\Rightarrow \inlinerr{c}$, where the single node is in the rule interface.
Both rules replace the graphs with themselves,
hence, any rewriting step does not change the graph at all.

By exhaustive enumeration of all representative steps, it is easy to see that $\inlinerr{a,c}, \inlinerr{c}$ are semi-saturated bisimilar.
It is important to keep in mind that the answering step does not need to use the same rule.
For example, a step $\inlinerr{a,c} \ncrstep{\loopOnArrow{\inlinerr{b}}} \inlinerr{a,b,c}$ (using the first rule) can be answered by a step $\inlinerr{c} \nccstep{\loopOnArrow{\inlinerr{b}}} \inlinerr{b,c}$ (using the second rule).
Because the resulting graphs both contain a $c$-loop, they are also bisimilar, since any subsequent steps (using either rule) can always be answered by applying the second rule.

However, the step $\inlinerr{c} \nccstep{\loopOnArrow{\inlinerr{b}}} \inlinerr{b,c}$ is not a representative step, because it borrows more than what is necessary to apply the second rule.
There is also no other representative step that originates from $\inlinerr{c}$ and borrows exactly $\inlinerr{b}$.
Hence, under a notion of bisimulation where $\rightarrow_R$-steps are answered by $\rightarrow_R$-steps, $\inlinerr{a,c},\inlinerr{c}$ are not bisimilar.

§ CONDITIONS FOR REACTIVE SYSTEMS

The reactive systems defined so far cannot represent rules where a
certain component is required to be absent: whenever a reaction
$a \leadsto a'$ is possible, a reaction $a;c \leadsto a';c$ (with
additional context $c$) is also possible, with no method to prevent
this.  Restricting rule applications can be useful, e.g. to model
access to a shared resource, which may only be accessed if no other
entity is currently using it.

For graph transformation systems, application conditions with a
first-order logic flavour have been studied extensively (e.g. in [14, 18]) and generalized to reactive systems in [3]. If we interpret such conditions in
$\ILC(\catname\Graphfin)$, we obtain a logic that subsumes
first-order logic (for more details on expressiveness
see [3]).

In this section, we summarize the definitions from [3] and
define shifting of conditions as partial evaluation.  We then
summarize the changes that are necessary to extend reactive systems
with conditions. We illustrate the concepts of this chapter
with various examples. An example for conditional reactive systems will be
discussed later (<Ref>).  For an additional example, we refer to [3].

§.§ Conditions and Satisfaction

[Condition [3]]
Let $\catname C$ be a category and $A$ be an object of $\catname C$.
The set of conditions over $A$ is defined inductively as:

* $\condtrue_A \defeq (A, \forall, \emptyset)$ and
$\condfalse_A \defeq (A, \exists, \emptyset)$ are conditions over $A$ (base case)

* $\mathcal{A} = (A, \mathcal{Q}, S)$ is a condition over $A$,

* $A = \Ro(\mathcal{A})$ is the root object of $\mathcal A$,

* $\mathcal{Q} \in \{\forall, \exists\}$ is a quantifier and

* $S$ is a finite set of pairs $(h, \mathcal{A}^\prime)$, where
$h \colon A \to A'$ is an arrow and
$\mathcal A'$ is a condition over $A'$.

Note that conditions can be represented as finite trees.

[Satisfaction [3]]
Let $\mathcal A$ be a condition over $A$. For an arrow $a \colon A \to B$ and a condition $\mathcal A$  we define the satisfaction relation $a \models \mathcal A$ as follows:

* $a \models (A, \forall, S)$ iff for every pair $(h, \mathcal{A}^\prime) \in S$ and every arrow $g \colon \Ro(\mathcal{A}^\prime) \to B$ we have: if $a = h;g$, then $g \models \mathcal{A}^\prime$.

* $a \models (A, \exists, S)$ iff there exists a pair $(h, \mathcal{A}^\prime) \in S$ and an arrow $g \colon \Ro(\mathcal{A}^\prime) \to B$ such that $a = h;g$ and $g \models \mathcal{A}^\prime$.

From the above it follows that
$\condtrue_A$ is satisfied by every arrow with domain $A$, and
$\condfalse_A$ is satisfied by no arrow.

We write $\mathcal A \models \mathcal B$ ($\mathcal{A}$ implies $\mathcal{B}$) if for every arrow $c$ with $\dom(c) = \Ro(\mathcal A) = \Ro(\mathcal B)$ we have: if $c \models \mathcal A$, then $c \models \mathcal B$.
Two conditions are equivalent ($\mathcal A \equiv \mathcal B$) if $\mathcal A \models \mathcal B$ and $\mathcal B \models \mathcal A$.

With satisfaction defined in this way,
universal conditions implicitly implement conjunction, i.e.,
$(A, \forall, \{ (f_1, \mathcal A_1), (f_2, \mathcal A_2), \dots \})$
can be understood as
$\forall(f_1, \mathcal A_1) \land \forall(f_2, \mathcal A_2) \land \dots$
[4]
(with a meaning analogous to the conditions of [14, 18]);
similarly, existential conditions implement disjunction
($\exists(f_1, \mathcal A_1) \lor \exists(f_2, \mathcal A_2) \land \dots$).

Based on this, we can define negation of conditions, and conjunctions and disjunctions of arbitrarily quantified conditions such as $\exists(\dots) \land \exists(\dots)$ (note the flipped logical connective):

Consider the following Boolean operations:

* $\neg(A, \forall, S) \defeq (A, \exists, \{ (h, \neg\mathcal{A}^\prime) \mid (h, \mathcal{A}^\prime) \in S \})$, $\neg(A, \exists, S) \defeq (A, \forall, \{ (h, \neg\mathcal{A}^\prime) \mid (h, \mathcal{A}^\prime) \in S \})$

* $\mathcal{A} \lor \mathcal{B} \defeq (A, \exists, \{ (\id_A, \mathcal{A}), (\id_A, \mathcal{B}) \})$ for two conditions $\mathcal{A}, \mathcal{B}$ over $A$

* $\mathcal{A} \land \mathcal{B} \defeq (A, \forall, \{ (\id_A, \mathcal{A}), (\id_A, \mathcal{B}) \})$ for two conditions $\mathcal{A}, \mathcal{B}$ over $A$

[2]
These operations satisfy the standard laws of propositional logic, i.e.
$a \models \neg\mathcal A$ if and only if $a \notmodels \mathcal A$;
$a \models \mathcal A \lor \mathcal B$ if and only if $a \models \mathcal A \;\lor\; a \models \mathcal B$,
analogously for $\mathcal A \land \mathcal B$.
Conjunction and disjunction can be extended in the obvious way to arbitrary, rather than binary, conjunctions and disjunctions.

[Examples of conditions]

* $\mathcal{A}_{node}$ recognizes graphs that contain at least one node:

\[
\mathcal{A}_{node}
\Big( \emptyset, \exists, \Big\{
( \emptyset \rightarrow \gn \leftarrow \gn,~ \condtrue_{\gn} )
\Big\} \Big)
\]

The condition is checked as follows: any arrow that satisfies the condition
must be decomposable into two arrows, the first of which is given in the condition and contributes the required node,
and the second optionally provides additional elements.
Since the output interface is not empty, the second arrow is free to connect edges to the required node,
i.e. the condition matches both isolated and non-isolated nodes.

* The condition $\mathcal{A}_{iso}$ recognizes graphs that contain an isolated node:

\[
\mathcal{A}_{iso}
\Big( \emptyset, \exists, \Big\{
( \emptyset \rightarrow \gn \leftarrow \emptyset,~ \condtrue_\emptyset )
\Big\} \Big)
% =
% \Big( \emptyset, \exists, \Big\{
% \big( \emptyset \rightarrow \gn \leftarrow \emptyset,~ (\emptyset, \forall, \emptyset) \big)
% \Big\} \Big)
\]

As the outer interface of $h = \emptyset \rightarrow \gn \leftarrow \emptyset$ is empty, $h;g$ has to contain an isolated node ($g$ can only connect an edge to the node provided by $h$ if it is contained in the interface).

* $\mathcal{A}_{ab}$ recognizes the graphs where
for all occurrences of an $a$-edge, there also exists a $b$-edge in the opposite direction:

\[ \begin{aligned}
\mathcal{A}_{ab} =
\Big( \emptyset, \forall, \Big\{ (
\emptyset
\ &\rightarrow\ %
\begin{tikzpicture}[baseline=-0.5ex]
\node[gn] (l) at (0,0) {};
\node[gn] (r) at (0.6,0) {};
\draw[gedge] (l) to node[below]{$a$} (r);
\end{tikzpicture}
\ \leftarrow\ %
\AabInterface,
\ \mathcal{A}^\prime
) \Big\} \Big) \\
\mathcal{A}^\prime =
\Big(
\AabInterface,
\exists,
\Big\{ (
\AabInterface
\ &\rightarrow\ %
\begin{tikzpicture}[baseline=-0.5ex]
\node[gn] (l) at (0,0) {};
\node[gn] (r) at (0.6,0) {};
\draw[gedge] (r) to node[below]{$b$} (l);
\end{tikzpicture}
\ \leftarrow\ %
\AabInterface,
\condtrue_{\text{\textbullet\,\textbullet}}%cheat
) \Big\} \Big)
\end{aligned} \]

Note that in the examples above, the root object of the condition is empty, since we only consider isolated conditions.
When using conditions in a transformation rule, we would use the interface of the rule instead.
This ensures that the condition is evaluated at the same position where the rule is applied, and not in any other position.

§.§ Shifting as Partial Evaluation of Conditions

When evaluating conditions, it is sometimes known that a given context
is guaranteed to be present. In this case, a condition can be
rewritten, using representative squares, under the assumption that
this context is provided by the environment. This operation is known
as shift [18]:

[Shift of a condition [3]]
Given a fixed class of representative squares $\kappa$,
the shift of a condition $\mathcal A = (A, \mathcal Q, S)$ along an arrow
$c \colon A \to B$ is inductively defined as follows:

\[
\mathcal{A}_{\downarrow c} \defeq \Big( B, \mathcal Q, \Big\{
( \beta, \mathcal{A}^\prime_{\downarrow\alpha} ) \:\Big|\: (h, \mathcal{A}^\prime) \in S,\ (\alpha,\beta) \in \kappa(h, c)
\Big\} \Big)
\]

The shift operation can be understood as a partial evaluation of
$\mathcal A$ under the assumption that $c$ is already present.
It satisfies
$ c;d \models \mathcal{A} \iff d \models \mathcal{A}_{\downarrow c} $.

(z) at (-1*,0) $Z$;
(a) at (0,0) $A$;
(b) at (1*,0) $B$;
(x) at (2*,0) $X$;
[->,fancydotted] (z) – node[above]$a$ (a);
[->] (a) – node[above]$c$ (b);
[->] (b) – node[above]$d$ (x);
[condtri,dart tip angle=60,shape border rotate=90] at (a.south) $\mathcal A\vphantom{{}_{\downarrow}}\mkern3mu$;
[condtri,dart tip angle=60,shape border rotate=90] at (b.south) $\mkern-5mu\mathcal A_{\downarrow c}\mkern-6mu$;
at (0,-1.4) ;

The typical case, which we will encounter throughout the rest of this paper,
is that a condition on the context of some arrow $a$ is given,
this arrow is then placed into some environment $c$ (which might not fully satisfy the condition, but possibly parts of it),
and we are interested in a condition that an additional context $d$ has to satisfy.
(For instance, if $\mathcal A$ requires the existence of two elements and $c$ already provides one of them,
then $d$ only needs to add the other one, which is reflected in $\mathcal A_{\downarrow c}$.)

The representation of the shifted condition may differ depending on the class of representative squares chosen.
However, no matter which class is chosen, the resulting conditions are equivalent to each other.
Furthermore, if we assume that (Fin) holds,
shifting a finite condition will again result in a finite condition.

Representative squares as well as shift play a major role in the
diagrammatic proofs.
The shift operation satisfies a few equivalences that we will use in the proofs of our theorems:

\begin{align*}
(\mathcal{A} \lor \mathcal{B})_{\downarrow c} &\equiv \mathcal{A}_{\downarrow c} \lor \mathcal{B}_{\downarrow c} &
\mathcal{A}_{\downarrow\id} &\equiv \mathcal{A} &
\mathcal{A} \models \mathcal{B} &\implies \mathcal{A}_{\downarrow c} \models \mathcal{B}_{\downarrow c} \\
(\mathcal{A} \land \mathcal{B})_{\downarrow c} &\equiv \mathcal{A}_{\downarrow c} \land \mathcal{B}_{\downarrow c} &
\condtrue_{\downarrow c} &\equiv \condtrue &
\mathcal{A}_{\downarrow c_1;c_2} &\equiv (\mathcal{A}_{\downarrow c_1})_{\downarrow c_2} \\
\neg(\mathcal{A}_{\downarrow c}) &\equiv (\neg\mathcal{A})_{\downarrow c} &
\condfalse_{\downarrow c} &\equiv \condfalse
\end{align*}

[Simplifying conditions by shifting]

Let the following condition $\mathcal A_{nb}$ be given, which
requires that the interface node does not have a $b$-loop attached:

\[ \mathcal{A}_{nb}
= \Big( \gn, \forall, \Big\{ ( \gn \rightarrow \mbrloop \leftarrow \gn ,~ \condfalse ) \Big\}
\Big) \]

Furthermore let the cospan $c = \gn \rightarrow \mbrloop \leftarrow \gn$.
We now compute the result of the shift $\mathcal{A}_{nb\downarrow c}$,
i.e., the condition $\mathcal{A}_{nb}$ under the assumption that $c$ is already given.
We expect the resulting condition to be equivalent to $\condfalse$, since the presence of the $b$-loop in $c$ already violates $\mathcal{A}_{nb}$.
We will show that this is indeed the case.
By <Ref> we have:

\begin{align*}
\mathcal{A}_{nb\downarrow c}
\big( \gn, \forall, \big\{ ( \beta, \mathcal{A}^\prime_{\downarrow\alpha} ) \;\big|\; (h, \mathcal{A}^\prime) \in S,~ (\alpha,\beta) \in \kappa(h,c) \big\} \big) \\
\big( \gn, \forall, \big\{
( \beta, \mathcal{A}^\prime_{\downarrow\alpha})
\;\big|\;
\mathcal{A}^\prime = \condfalse,~
h = \gn \rightarrow \smash\mbrloop \leftarrow \gn ,~
(\alpha,\beta) \in \kappa(h,c)
\big\} \big)
\intertext{
We can obtain possible $\alpha,\beta$ by enumerating the borrowed context diagrams where $h,c$ are already given.
As seen in \Cref{shift-ex-bcds}, there are two possible choices for the jointly epi square in the top left:
the $b$-loops of $h$ and $c$ can be mapped to two different loops in the center graph (\Cref{shift-ex-bcd-disjoint})
or they can be mapped to a single loop (\Cref{shift-ex-bcd-overlap}).
The remaining pushout and pullback squares are then uniquely determined.
We therefore obtain:}
&= \big( \gn, \forall, \big\{
\big( \gn \rightarrow \smash\mbrloop \leftarrow \gn, (\condfalse)_{\downarrow\alpha_1} \big),
\big( \gn \rightarrow \gn \leftarrow \gn, (\condfalse)_{\downarrow\alpha_2} \big)
\\ & \hspace{100pt}\hspace{45pt} \big|\;
\alpha_1 = \gn \rightarrow \smash\mbrloop \leftarrow \gn,\ %
\alpha_2 = \gn \rightarrow \gn \leftarrow \gn
\big\} \big)
\intertext{Shifting $\condfalse$ along any arrow $\alpha_i$ again results in $\condfalse$:}
&= \big( \gn, \forall, \big\{ ( \gn \rightarrow \smash\mbrloop \leftarrow \gn, \condfalse ), ( \gn \rightarrow \gn \leftarrow \gn, \condfalse ) \big\} \big)
\end{align*}

Furthermore, since $\gn \rightarrow \gn \leftarrow \gn$ is an identity cospan,
the condition is equivalent to ,
which is the expected result.

(#2) at ($(\boxSxp,\boxSyp)!.5!(-\boxSxm,-\boxSym)$) [draw,roundbox,minimum width=cm, minimum height=cm] ;

[cospanint] (#1) edge (#2);

[cospanarr] (#1.#6) to[#7] node[#5]$#4$ (#3.#6);

[gedge] (l.150) to[loop,out=135+30,in=135-30,distance=0.3cm] node[left]$m\mkern-5mu$ (l.120);
[gedge] (r.60) to[loop,out=45+30,in=45-30,distance=0.3cm] node[right]$\mkern-2mu m$ (r.30);

at ($(boxnull)!0.5!(Gp)$) ;
at ($(L)!0.5!(C)$) ;
at ($(G)!0.5!(F)$) ;
at ($(Gp)!0.5!(K)$) ;

[gedge/.append style=font=, cospanarr/.append style=font=]
11 G^+Gp
[cospanarr] (boxnull.north east) to[bend left=10] node[above]$h$ (I.north west);
[cospanarr] (boxnull.south west) to[bend right=12] node[left]$c$ (J.north west);
[cospanarr] (J.south east) to[bend right=10] node[below]$\beta_1$ (K.south west);
[cospanarr] (I.south east) to[bend left=12] node[right]$\alpha_1$ (K.north east);

$b$-loops of $h$ and $c$ are kept separate in the center graph.

[gedge/.append style=font=, cospanarr/.append style=font=]
11 G^+Gp
[cospanarr] (boxnull.north east) to[bend left=10] node[above]$h$ (I.north west);
[cospanarr] (boxnull.south west) to[bend right=12] node[left]$c$ (J.north west);
[cospanarr] (J.south east) to[bend right=10] node[below]$\beta_2$ (K.south west);
[cospanarr] (I.south east) to[bend left=12] node[right]$\alpha_2$ (K.north east);

$b$-loops of $h$ and $c$ are mapped to a single loop.

Borrowed context diagrams for $h,c$ as given in <Ref>.

§.§ Conditional Reactive Systems

We now extend reactive systems with application conditions:

[Conditional reactive system [3]]
A rule with condition is a triple $(\ell,r,\mathcal R)$
where $\ell, r \colon \obnull \to I$ are arrows
and $\mathcal R$ is a condition with root object $I$.
A conditional reactive system is a set of rules with conditions.

As the root object $I$ of the condition is the codomain of the rule arrow,
it is also the domain of the reactive context,
which has to satisfy the rule condition in order to be able to apply the rule:

Let $a, a'$ be arrows of a conditional reactive system with rules $\mathcal S$.We say that $a$ reduces to $a'$ ($a \leadsto a'$)
whenever there exists a rule $(\ell,r,\mathcal R) \in \mathcal S$ with $\ell,r \colon \obnull \to I$
and a reactive context $c \colon I \to J$
such that $a = \ell;c$, $a' = r;c$ and additionally $c \models \mathcal R$.

In order to define a bisimulation for conditional reactive systems that is also a congruence,
it is necessary to enrich labels with conditions derived from
the application conditions. Since we can not assume that the full
context is present, the application condition might refer to currently
unknown parts of the context and this has to be suitably integrated
into the label.

[Context/representative step with conditions [15]]

[use as bounding box] (-0.33,1) rectangle (2*+0.1,--1);

(tlempty) at (0,0) $\obnull$;
(i) at (1*,0) $I$;
(trempty) at (2*,0) $\obnull$;
(j) at (0,-) $J$;
(k) at (1*,-) $K$;
[->] (tlempty) – node[above]$\ell$ (i);
[->] (trempty) – node[above]$r$ (i);
[->] (trempty) – node[below,pos=0.4]$a^\prime$ (k);

[->] (tlempty) – node[left]$a$ (j);
[->] (i) – node[left]$c$ (k);

[->] (j) – node[above]$f$ (k);
[condtri,dart tip angle=50,shape border rotate=270] at (i.north) $\mathcal R$;
[condtri,dart tip angle=50,shape border rotate=90] at (k.south) $\mkern-3mu\mathcal A$;

(pcdst) at (2*,-1.3*) ;
[->,fancydotted] (k) – node[below]$d$ (pcdst);

Let $\mathcal S$ be a conditional reactive system, let
$a \colon \obnull \to J,\ f \colon J \to K,\ a' \colon \obnull \to K$
be arrows and $\mathcal A$ be a condition over $K$.  We
write $a \cstep{f}{\mathcal A} a'$ whenever there exists a rule
and an arrow $c$ such that
$a;f = \ell;c,\ a' = r;c$ (i.e. the reaction is
conditions) and furthermore
$\mathcal A \models \mathcal{R}_{\downarrow c}$ (a condition on an additional context $d$ as explained below).
Such steps are called context steps.

We write $a \rstep{f}{\mathcal A} a'$ whenever
$a \cstep{f}{\mathcal A} a'$, $\kappa(a,\ell) \ni (f,c)$ and
$\mathcal A = \mathcal{R}_{\downarrow c}$.  Such steps are called
representative steps.

Conditions are represented graphically in the form of “arrowhead
shapes” depicted next to the root object.  Intuitively
$a \cstep{f}{\mathcal A} a'$ means that $a$ can make a step to $a'$
when borrowing $f$, if the yet unknown context $d$ beyond $f$ satisfies
condition $\mathcal{A}$ (since this context $d$ does not directly
participate in the reduction, we call it passive context).

The intuition behind this requirement is that $\mathcal A$ should
allow only the contexts that are allowed by the rule condition
$\mathcal R$ (thereby checking that the rule can actually be
Since $\mathcal A$ is a condition over an additional context $d$ that is
beyond the reaction context $c$, and $c$ might partially satisfy
$\mathcal R$, we shift $\mathcal R$ over $c$ to obtain a condition that
only requires the parts of $\mathcal R$ that are still missing.
For context steps, $\mathcal A$ may also be stronger, hence $\models$.

In the case of a representative step, we
require that a context step is possible, the borrowed context is
minimal, and the condition on the passive context is not stronger than

In the proofs, we will make extensive use of the following construction
to obtain a representative step for a given context step:

<Ref> imply,
analogously to <Ref>,
that every context step $a \cstep{f}{\mathcal A} a'$ (left diagram)
can be reduced to a representative step  (right diagram),
with $\mathcal R$ being the condition of the rule $(\ell,r,\mathcal R)$ that enables the given context step.

(tlempty) at (0,0) $\obnull$;
(i) at (2.5,0) $I$;
(trempty) at (4.7,0) $\obnull$;
(j) at (0,-2.5) $J$;
(k) at (2.5, -2.5) $K$;
[->] (tlempty) – node[above]$\ell$ (i);
[->] (trempty) – node[above]$r$ (i);
[->] (trempty) to[bend left=5] node[right]$a'$ (k);

[->] (tlempty) – node[left]$a$ (j);
[->] (i) to[bend left=5] node[right]$c$ (k);

[->] (j) – node[below]$f$ (k);

[condtri,shape border rotate=270] at (i.north) $\mathcal{R}$;
[condtri,shape border rotate=90] at (k.south) $\mkern-3mu\mathcal{A}$;

at (5.75,-1.5) $\rightarrow$;

(tlempty) at (0,0) $\obnull$;
(i) at (2.5,0) $I$;
(trempty) at (4.7,0) $\obnull$;
(j) at (0,-2.4) $J$;
(kp) at (1.95,-1.95) $\hat K$;
(k) at (2.9, -2.9) $K$;
[->] (tlempty) – node[above]$\ell$ (i);
[->] (trempty) – node[above]$r$ (i);
[->] (trempty) to[bend left=5] node[right]$a'$ (k.40);

[->] (tlempty) – node[left]$a$ (j);
[->] (i.300) to[bend left=5] node[right]$c$ (k);

[->] (j) – node[below]$f$ (k);

[->] (i) – node[left]$\hat c$ (kp);
[->] (j) – node[above]$\hat f$ (kp);
[->] (kp) – node[right,pos=0.1]9pt$\hat g$ (k);

[condtri,shape border rotate=270] at (i.north) $\mathcal R$;
[condtri,shape border rotate=90] at (k.south) $\mathcal A$;

[rotate around=-55:(kp.center),condtri,shape border rotate=0,scale=0.7] at (kp.west)
25$\mathcal{R}_{\downarrow \hat c}$

We will also make use of the following context-step-rewriting lemma:

A context step $a;d \cstep{f}{\mathcal{A}} a^\prime$ is equivalent
to a step $a \cstep{d;f}{\mathcal{A}} a^\prime$.  In particular,
$a;d \cstep{f}{\mathcal{A}} a^\prime$  if and only if
$a \cstep{d;f}{\mathcal{A}} a^\prime$.

According to <Ref>, for a step
$a;d \cstep{f}{\mathcal{A}} a^\prime$ there exists a rule
$(\ell,r,\mathcal{R})$ such that
$(a;d);f = \ell;c,\ a^\prime = r;c,\ \mathcal{A} \models
\mathcal{R}_{\downarrow c}$ for some arrow $c$.  Since composition
is associative, we rewrite this to $a;(d;f) = \ell;c$, which
immediately results in the definition of
$a \cstep{d;f}{\mathcal A} a^\prime$.

We now extend (semi-)saturated bisimilarity to rules with conditions:

[(Semi-)Saturated bisimilarity [15]]
Let $\mathcal{S}$ be a conditional reactive system.
A saturated bisimulation is a relation $R$,
relating arrows $a,b \colon \obnull \to J$, such that: for
all $(a,b) \in R$ and for every context step
$a \cstep{f}{\mathcal A} a^\prime$ there exist answering moves
$b \cstep{f}{\mathcal{B}_i} b_i^\prime$, $i\in I$, such that
$(a^\prime, b_i^\prime) \in R$ and
$\mathcal{A} \models \bigvee_{i \in I} {\mathcal{B}_i}$, where $I$
is a finite index set;
and, vice versa, for every context step
$b \cstep{f}{\mathcal B} b'$ there exist answering moves
$a \cstep{f}{\mathcal A_j} a_j^\prime$, $j \in J$, such that
$(a_j^\prime, b') \in R$ and
$\mathcal B \models \bigvee_{j \in J} {\mathcal A_j}$.

Two arrows $a, b$ are called saturated bisimilar
($(a, b) \in \simC$) whenever there exists a saturated bisimulation
$R$ with $(a, b) \in R$.  Similarly, for semi-saturated
bisimilarity we require that $\rightarrow_R$-steps of $a$ can be
answered by $\rightarrow_C$-steps of $b$,
and vice versa for $\rightarrow_R$-steps of $b$.
Saturated and semi-saturated bisimilarity agree and both are
congruences [15].

§ CONDITIONAL BISIMILARITY

We will now introduce our new results on conditional bisimilarity: as
stated earlier, our motivation is to extend the notion of saturated
bisimilarity, which is often too strict, since it requires that two system
states behave identically in all possible contexts. However, sometimes
it is enough to ensure behavioural equivalence only in specific

Hence we now replace standard bisimilarity, which is a binary
relation, by a ternary relation — called conditional relation — with
tuples of the form $(a,b,\mathcal{C})$.
Then, a conditional bisimulation is a conditional relation, where a tuple $(a,b,\mathcal C)$ can
be read as: $a,b$
are bisimilar in all contexts satisfying $\mathcal{C}$.

§.§ Definition, Properties and Examples

[Conditional relation]
A conditional relation is a set of triples
$(a,b,\mathcal C)$, where $a,b \colon \obnull \to J$ are arrows with
identical target and $\mathcal C$ is a condition over $J$.

Note that for a triple $(a,b,\mathcal C)$,
the root object of the condition $\mathcal C$ is not the source of $a$
(as is the case for satisfaction), but the target $\codom(a)$.  This
is because we do not state a condition on the arrows $a,b$ themselves,
but on the context in which they are embedded ($a;f$ resp. $b;f$ for
some context $f$), so the condition is over $\dom(f) = \codom(a) = \codom(b)$.

[Closure under contextualization, $u(R)$, conditional congruence]

If $R$ is a conditional relation, then:

* $R$ is reflexive if
$(a,a,\mathcal C) \in R$ for all $a, \mathcal C$ with $\codom(a)=\Ro(\mathcal C)$

* $R$ is symmetric if
$(a,b,\mathcal C)\in R$ implies $(b,a,\mathcal C)\in R$

* $R$ is transitive if
$(a,b,\mathcal C) \in R$ and $(b,c,\mathcal C) \in R$ implies
$(a,c,\mathcal C) \in R$

* $R$ is closed under contextualization if
$(a,b,\mathcal C) \in R$ implies $(a;d, b;d, \mathcal C_{\downarrow d}) \in R$

* $R$ is a conditional congruence if
it is an equivalence (reflexive, symmetric, transitive) and closed under contextualization

For a conditional relation $R$, $u(R)$ is its closure under contextualization, that is,

Closure under contextualization means that whenever $a,b$ are
related under a context satisfying $\mathcal{C}$, then they are
still related when we contextualize under $d$, where however the
condition has to be shifted since we commit to the fact that the
context is of the form $d;c$ for some additional context $c$.

We will now introduce one of the central definitions of this paper. Here,
given a conditional reactive system we will describe when two arrows
$a,b$ are bisimilar in all contexts that satisfy a condition

[Conditional bisimulation]
We fix a conditional reactive system.
A conditional bisimulation $R$ is a conditional relation such that the following holds:
for each triple $(a,b,\mathcal{C}) \in R$ and each context step $a \cstep{f}{\mathcal A} a^\prime$,
there are answering steps $b \cstep{f}{\mathcal{B}_i} b_i^\prime$,
$i\in I$
(where $I$ is possibly infinite),
and conditions $\mathcal{C}_i^\prime$
such that $(a^\prime, b_i^\prime, \mathcal{C}_i^\prime) \in R$
and $\mathcal{A} \land \mathcal{C}_{\downarrow f} \models \bigvee_{i \in I} \left( \mathcal{C}_i^\prime \land \mathcal{B}_i \right)$;
and vice versa[For each triple $(a,b,\mathcal{C}) \in R$ and each context step $b \cstep{f}{\mathcal B} b'$,
there are answering steps $a \cstep{f}{\mathcal{A}_j} a_j^\prime$
and conditions $\mathcal{C}_j^\prime$
such that $(a_j', b', \mathcal{C}_j^\prime) \in R$
and $\mathcal{B} \land \mathcal{C}_{\downarrow f} \models \bigvee_{j \in J} \left( \mathcal{C}_j^\prime \land \mathcal{A}_j \right)$].
Two arrows are conditionally bisimilar  ($(a, b, \mathcal{C})
\in \csimC$) whenever a conditional bisimulation $R$ with $(a, b,
\mathcal{C}) \in R$ exists.[Note that since conditional
bisimulations are closed under union, $\csimC$ is itself a
conditional bisimulation.]

(tlempty) at (0,0) $\obnull$;
(i) at (1*,0) $I$;
(trempty) at (2*,0) $\obnull$;
(j) at (0,-1*) $J$;
(k) at (1*,-1*) $K$;
(blempty) at (0,-2*) $\obnull$;
(ii) at (1*,-2*) $I_i$;
(brempty) at (2*,-2*) $\obnull$;
[->] (tlempty) – node[above]$\ell$ (i);
[->] (trempty) – node[above]$r$ (i);
[->] (trempty) – node[below,pos=0.25]$a^\prime$ (k.30);
[->] (blempty) – node[above]$\ell_i$ (ii);
[->] (brempty) – node[above]$r_i$ (ii);
[->] (brempty) – node[above,pos=0.25]$b_i^\prime$ (k.-30);

[->] (tlempty) – node[left]$a$ (j);
[->] (blempty) – node[left]$b$ (j);
[->] (i) – node[left]$c$ (k);
[->] (ii) – node[left]$e_i$ (k);

[->] (j) – node[above]$f$ (k);

[condtri,dart tip angle=60,shape border rotate=270] at (i.north) $\mathcal{R}$;
[condtri,dart tip angle=60,shape border rotate=0] at (j.west) $\kern 0.5mm \mathcal{C}$;
[condtri,dart tip angle=60,shape border rotate=90] at (ii.south) $\kern -0.5mm\mathcal{R}_i\kern -0.5mm$;
[rotate around=5:(k.center),condtri,shape border rotate=180] at (k.east) -3pt0pt[0.5][0.2]$\mathcal{C}_i^\prime$;
[rotate around=-20:(k.center),condtri,shape border rotate=270,scale=0.9] at (k.80) $\mathcal{A}$;
[rotate around=20:(k.center),condtri,shape border rotate=90,scale=0.9] at (k.-80) 0pt[1.8pt][1.5pt]$\mathcal{B}_i$;

(pcdst) at (2.25*,-1.4*) ;
[->,fancydotted] (k.-10) – node[above,pos=0.85]$d$ (pcdst);

A context step $a \protect\cstep{f}{\mathcal A} a'$ (top half) and a single answer step $b \protect\cstep{f}{\mathcal B_i} b_i^\prime$ (bottom half) in conditional bisimulation

The situation for one answer step is depicted in <Ref>.
Since the definition is rather complex, we will discuss its various
aspects in the following remarks.

In <Ref>, the implication $\mathcal A \land \mathcal C_{\downarrow f} \models \bigvee_{i \in I} (\mathcal C_i^\prime \land \mathcal B_i)$
is to be understood as follows:
For every step, we have a borrowed context $f$ and an additional passive context $d$ (as explained below <Ref>).
The condition $\mathcal C$ from the triple refers to the full context of $a$ (i.e. both the borrowed context $f$ and the passive context $d$, hence $f;d \models \mathcal C$ or equivalently $d \models \mathcal C_{\downarrow f}$),
while $\mathcal A$, coming from the context step, only refers to the passive context $d$ (hence $d \models \mathcal A$).

Every environment $d$ that is valid for the context step of $a$
(i.e. which satisfies $\mathcal A \land \mathcal C_{\downarrow f}$)
must also be valid for some answering step of $b$, i.e. satisfies at least one $\mathcal B_i$.
Depending on the context, different answering steps may be chosen, and the resulting pair $a',b'_i$ might only be conditionally bisimilar for some contexts, which is indicated by the condition $\mathcal C_i^\prime$.

As for saturated bisimilarity,
we need to allow several answering moves for a single
step of $a$: the answering step taken by $b$ might depend on the
context, using different rules for contexts satisfying different
conditions $\mathcal{B}_i$. We just have to ensure that all answering
step conditions taken together (disjunction on the right-hand side) fully cover the conditions under which the
step of $a$ is feasible (left-hand side).
As an example for this, consider the following example (originally presented in <cit.>).
Assume three rules:

\[\bgroup%
\renewcommand{\arraystretch}{1.5}%
\setlength{\arraycolsep}{0.3pt}%
\begin{array}{rlrccclr} % x.|R|=... | L | ... | R | ... | text...
1.\ &  R_A   &{}= \big(
\emptyset \rightarrow & \inlinechan{chan=a}  & \leftarrow \inlinechan{},\  %
\emptyset \rightarrow & \inlinechan{} & \leftarrow \inlinechan{},
\condtrue_{\mathifnodessubscript} \big)
&\text{(unconditionally delete an $a$-edge)} \\
2.\ & R_{B1} &{}= \big(
\emptyset \rightarrow & \inlinechan{chan=b}  & \leftarrow \inlinechan{},\  %
\emptyset \rightarrow & \inlinechan{} & \leftarrow \inlinechan{},\ %
\mathcal A_q \big)
&\text{\parbox[t]{61.5mm}{(delete a $b$-edge if the context satisfies some condition $\mathcal A_q$)}} \\
3.\ & R_{B2} &{}= \big(
\emptyset \rightarrow & \inlinechan{chan=b}  & \leftarrow \inlinechan{},\  %
\emptyset \rightarrow & \inlinechan{} & \leftarrow \inlinechan{},\ %
\neg\mathcal A_q \big)
&\text{\parbox[t]{61.5mm}{(delete a $b$-edge in contexts not satisfying $\mathcal A_q$)}}
\end{array}\egroup\]

(Hence rules 2 and 3 together allow a $b$-edge to be deleted in any context, since every context satisfies either $\mathcal A_q$ or $\neg\mathcal A_q$.
The condition $\mathcal A_q$ can be chosen arbitrarily, as long as it
is not equivalent to $\condtrue$ or $\condfalse$.)
Then, an $a$-edge is conditionally bisimilar to a $b$-edge under $\condtrue$ (all contexts):
a step that deletes the $a$-edge can be answered by deleting the $b$-edge,
but depending on the context that the step happens in, a different rule has to be chosen:
two answering steps with $\mathcal B_1 = \mathcal A_q,\ \mathcal B_2 = \neg\mathcal A_q$ are required, and together they cover $\condtrue$.
(The other direction — deleting the $b$-edge using either rule 2 or 3 being answered by deleting the $a$-edge using rule 1 — does not require multiple answering steps in this example.)

The definition explicitly permits an infinite index set $I$ for the
answering steps (this is in contrast to saturated bisimilarity, cf.  <Ref>, which required finite $I$). If we do not
consider conditional bisimilarity and the finiteness assumption
(Fin) holds, it does not make a difference whether we
consider finite or infinite index sets, since there are only
finitely many possible answering steps [15]. However, in
the presence of conditions, it might make a difference.

Since the logic does not support infinite disjunctions,
$\mathcal A \land \mathcal C_{\downarrow f} \models \bigvee_{i \in
I} {\mathcal C_i' \land \mathcal B_i}$ means that for every $d$
with $d \models \mathcal A \land \mathcal C_{\downarrow f}$, there
exists $i \in I$ such that
$d \models \mathcal C_i' \land \mathcal B_i$.

In many practical applications, it may be useful to restrict to a
variant of the definition that permits only finitely many answering
steps.  Our theorems are valid for either variant (finite or
infinite), except for the proof of <Ref> which in its
current version requires $I$ to be infinite.

𝒜_U ∄n
[Message passing over unreliable channels]
We now work in the category of input-linear cospans of graphs, i.e.,

We extend our previous example (cf. <Ref>) of networked
nodes, introducing different types of channels.
A channel can be reliable or unreliable, indicated by an $\relLabel$-edge or $\unrelLabel$-edge respectively.
Sending a message over a reliable channel always succeeds (rule $P_R$), while an unreliable channel only transmits a message if there is no noise (indicated by a parallel $\noiseLabel$-edge) in the environment that disturbs the transmission (rule $P_U$).
The reactive system has the following rules with application conditions, where condition $\AUneN$ states that the unreliable channel must not have an $\noiseLabel$-edge in parallel:

[gedge/.append style=font=]
[anchor=center] (#2) at (0,0) [draw,roundbox,minimum width=2cm, minimum height=1.25cm] ;
[anchor=west] at (-1cm,-0.35) $\scriptstyle{#1}$;

[gn] (l) at (-0.35,0.05) ;
[gn] (r) at (0.35,0.05) ;

[gedge] (l) to node[below]$#1$ (r);

[gedge] (l.120) to[loop,out=120+30,in=120-30,distance=0.3cm] node[left]$m\mkern-5mu$ (l.90);
[gedge] (r.90) to[loop,out=60+30,in=60-30,distance=0.3cm] node[right]$\mkern-2mu m$ (r.60);
(leftnull) at (0,0) [draw,roundbox,minimum width=0.5cm, minimum height=1.25cm] ;

(rightnull) at (0,0) [draw,roundbox,minimum width=0.5cm, minimum height=1.25cm] ;

[inner xsep=0cm,anchor=east] at (-2.4,-0.125) $P_{#3} = \Bigg($;
[inner xsep=0cm,anchor=west] at (8.4,-0.125) $, #4 \Bigg)$;
[cospanint] (leftnull) – (leftbox);
[cospanint] (ifbox) – (leftbox);
[cospanint] (ifbox) – (rightbox);
[cospanint] (rightnull) – (rightbox);

[cospanarr] (-2,0.7) to[bend left=20] node[below,pos=0.65]$\ell$ (3-0.25,0.85);
[cospanarr] (8,0.7) to[bend right=20] node[below,pos=0.65]$r$ node[above] (3+0.25,0.85);

at (0,0.8) $L$;
at (3,0.8) $I$;
at (6,0.8) $R$;

[inner xsep=0cm,anchor=east] at (-2.4,-0.125) $\AUneN = \Big($;
[inner xsep=0cm,anchor=west] at (-2.4,-0.125) $U_0, \forall, \Big\{ \Big( $;

[gn] (l) at (-0.35,0.05) ;
[gn] (r) at (0.35,0.05) ;

[gedge] (l.45) to[bend left=10] node[above]$\noiseLabel$ (r.135);

[cospanint] (leftbox)  – (ifbox);
[cospanint] (rightbox) – (ifbox);
[inner xsep=0cm,anchor=west] at (7.5,-0.125) $, \condfalse_{U_0} \Big) \Big\} \Big) $;

Hence the application condition $\AUneN$ says that the
context must not be decomposable into
$U_0\rightarrow U_N\leftarrow U_0$ and some other cospan, which
is only the case if the $\unrelLabel$-edge in the interface of $P_U$ has no parallel $\noiseLabel$-edge. In other words:
there is no noise.

We compare the behaviour of a reliable channel
($r \defeq \emptyset \rightarrow \inlinechan{reliable} \leftarrow \inlinechan{}$)
to that of an unreliable channel
($u \defeq \emptyset \rightarrow \inlinechan{unreliable} \leftarrow \inlinechan{}$).
It is easy to see that they are not saturated bisimilar: $r$ can do
a step by borrowing a message on the left
($f \defeq \inlinechan{} \rightarrow \inlinechan{msgleft} \leftarrow \inlinechan{}$) without further
restrictions (i.e. using an environment condition
$\mathcal A = \condtrue$). But $u$ is unable to answer this step,
because the corresponding rule is only applicable if no $\noiseLabel$-edge is

However, $r$ and $u$ are conditionally bisimilar under the
assumption that no $\noiseLabel$-edge is present between the two nodes
($\mathcal C = \AIneN$, where $\AIneN \defeq \big( \inlinechan{}, \forall, \big\{ (
{\inlinechan{} \rightarrow \inlinechan{noise} \leftarrow \inlinechan{}},
\allowbreak\condfalse_{\mathifnodessubscript} ) \big\} \big)$),
i.e. there exists a conditional bisimulation that contains
$(r, u, \AIneN)$.  A direct proof is hard, since the
proof involves checking infinitely many context steps, since messages
accumulate on the right-hand side.  However, in
<Ref> we will use an argument based on
representative steps to construct a proof.

It holds that $(a,b,\mathcal C')\in \csimC$,
$\mathcal C \models \mathcal C'$ implies
$(a,b,\mathcal{C})\in \csimC$. (This is due to the fact that
$\mathcal C \models \mathcal C'$ implies
$\mathcal C_{\downarrow f}\models \mathcal C'_{\downarrow f}$ which,
in <Ref>, implies
$\mathcal A \land \mathcal C_{\downarrow f}\models \mathcal A \land
\mathcal C'_{\downarrow f}$ for any condition $\mathcal A$ and arrow

Our motivation for introducing the notion of conditional bisimilarity
was to check whether two systems are behaviourally equivalent when
they are put into a context that satisfies some condition
$\mathcal C$.  It is not immediately obvious that our definition can
be used for this purpose, since all context steps are checked, not
just the ones that actually satisfy $\mathcal C$.

Hence we now show that our definition is sound, i.e. if two systems
are conditionally bisimilar, then they show identical behaviour under
all contexts that satisfy $\mathcal C$.

Let $R$ be a conditional bisimulation. Then
$ R^\prime = \{ (a;d, b;d) \mid (a,b,\mathcal{C}) \in R \allowbreak\land d \models \mathcal{C} \} $
is a bisimulation for the reaction relation

To prove that $R'$ is a bisimulation, we need to show that
if $a;d \mathrel{R^\prime} b;d$ and $a;d \leadsto a^\prime$, then there exists $b^\prime$ such that $b;d \leadsto b^\prime$ and $a^\prime \mathrel{R^\prime} b^\prime$;
and vice versa.
Equivalently, if $a;d$ can do a step, then $b;d$ can answer this step (and vice versa) and the result is again contained in the bisimulation $R'$.
We show only one direction ($a;d$ answered by $b;d$), the other one can be done analogously.

Now let some $(a;d, b;d) \in R^\prime$ be given, for which there must exist a triple $(a, b, \mathcal{C}) \in R$.
Consider a step $a;d \leadsto a^\prime$. This step is due to some rule $(\ell, r, \mathcal{R})$, shown graphically in <Ref>.

(tlempty) at (0,0) $\obnull$;
(i) at (1*,0) $I$;
(trempty) at (2*,0) $\obnull$;
(j) at (0,-1*) $J$;
(k) at (1*,-1*) $K$;
[->] (tlempty) – node[above]$\ell$ (i);
[->] (trempty) – node[above]$r$ (i);
[->] (trempty) – node[below,pos=0.4]$a^\prime$ (k);

[->] (tlempty) – node[left]$a$ (j);
[->] (i) – node[left]$c$ (k);

[->] (j) – node[above]$d$ (k);

[condtri,dart tip angle=60,shape border rotate=270] at (i.north) $\mathcal{R}$;
[condtri,dart tip angle=60,shape border rotate=0] at (j.west) $\kern 0.5mm \mathcal{C}$;

(ii) at (1*,-2*) $\phantom{I_i}$;
[condtri,dart tip angle=60,shape border rotate=90,draw=none] at (ii.south) $\kern -0.5mm\phantom{\mathcal{R}_i}\kern -0.5mm$;

A reaction $a;d \leadsto a'$ for some context $d$ that satisfies $\mathcal C$.

(tlempty) at (0,0) $\obnull$;
(i) at (1*,0) $I$;
(trempty) at (2*,0) $\obnull$;
(j) at (0,-1*) $J$;
(k) at (1*,-1*) $K$;
(blempty) at (0,-2*) $\obnull$;
(ii) at (1*,-2*) $I_i$;
(brempty) at (2*,-2*) $\obnull$;
[->] (tlempty) – node[above]$\ell$ (i);
[->] (trempty) – node[above]$r$ (i);
[->] (trempty) – node[below,pos=0.4]$a^\prime$ (k);
[->] (blempty) – node[above]$\ell_i$ (ii);
[->] (brempty) – node[above]$r_i$ (ii);
[->] (brempty) – node[above,pos=0.4]$b_i^\prime$ (k);

[->] (tlempty) – node[left]$a$ (j);
[->] (blempty) – node[left]$b$ (j);
[->] (i) – node[left]$c$ (k);
[->] (ii) – node[left]$e_i$ (k);

[->] (j) – node[above]$d$ (k);

[condtri,dart tip angle=60,shape border rotate=270] at (i.north) $\mathcal{R}$;
[condtri,dart tip angle=60,shape border rotate=0] at (j.west) $\kern 0.5mm \mathcal{C}$;
[condtri,dart tip angle=60,shape border rotate=90] at (ii.south) $\kern -0.5mm\mathcal{R}_i\kern -0.5mm$;

The same step, together with answering steps provided by the conditional bisimulation.

The steps considered in the proof of <Ref>

We have $c \models \mathcal R$ (otherwise the rule would not be applicable and therefore the step $a;d \leadsto a'$ would not be possible)
and $d \models \mathcal C$ (follows from the given $(a;d, b;d) \in R^\prime$ by construction of $R'$).
To make them usable for the answering steps, we transform $\mathcal R, \mathcal C$ to be conditions over $K$.
Trivially $d = d;\id_K$, so using <Ref> we rewrite $d;\id_K \models \mathcal{C}$ to $\id_K \models \mathcal{C}_{\downarrow d}$.
Analogously, we rewrite $c;\id_K \models \mathcal{R}$ to $\id_K \models \mathcal{R}_{\downarrow c}$.

We set $\mathcal{A} \defeq \mathcal{R}_{\downarrow c}$ and interpret this diagram as $a \cstep{d}{\mathcal{A}} a^\prime$.
Since $R$ is a conditional bisimulation and $(a,b,\mathcal{C}) \in R$, $b$ can answer the step of $a$, using one of possibly several rules $(\ell_i, r_i, \mathcal{R}_i)$ depending on the given context $d$.
Setting $\mathcal{B}_i \defeq \mathcal{R}_{i \downarrow e_i}$, we get steps $b \cstep{d}{\mathcal{B}_i} b_i^\prime$ and we extend the diagram as shown in <Ref>.

Generally, not every answering step that is possible for our given triple $(a,b,\mathcal{C})$ is a suitable answering step for the given context $d$.
But since $R$ is a conditional bisimulation, we know that $\mathcal{R}_{\downarrow c} \land \mathcal{C}_{\downarrow d} \models \bigvee_{i \in I} \left( \mathcal{C}_i^\prime \land \mathcal{B}_i \right)$.
Previously we derived $\id_K \models \mathcal{R}_{\downarrow c} \land \mathcal{C}_{\downarrow d}$.
Therefore, $\id_K$ also satisfies $\bigvee_{i \in I} \left( \mathcal{C}_i^\prime \land \mathcal{B}_i \right)$, that is, $\id_K$ satisfies $\mathcal{C}_i^\prime \land \mathcal{B}_i = \mathcal{C}_i^\prime \land \mathcal{R}_{i \downarrow e_i}$ for some $i$. From now on, we only consider answering steps for which this is indeed the case.

Using <Ref> we rewrite $\id_K \models \mathcal{R}_{i \downarrow e_i}$ to $e_i;\id_K = e_i \models \mathcal{R}_i$, which means that the rule $(\ell_i, r_i, \mathcal{R}_i)$ can actually be applied, that is, $b;d \leadsto b_i^\prime = r_i;e_i$. So $b$ has a suitable answering step.

To show that $R'$ is a bisimulation, we only have to show that $(a^\prime, b_i^\prime) \in R'$.
As $R$ is a conditional bisimulation, for the given answering step we know that $(a^\prime, b_i^\prime, \mathcal{C}_i^\prime) \in R$.
Previously we had $\id_K \models \mathcal{C}_i^\prime$, therefore, the requested pair $(a^\prime;\id_K, b_i^\prime;\id_K) = (a^\prime, b_i^\prime)$ is added during the construction of $R'$.

Note that the converse of <Ref> (if $R'$ is a bisimulation, then $R$ is a conditional bisimulation) does not hold.
Consider the following counterexample:

\[\bgroup%
\renewcommand{\arraystretch}{1.5}%
\setlength{\arraycolsep}{0.1em}%
\begin{array}{rlccccclccccl}
R_1    &= \big( & \inlinenlg{} & \rightarrow & \inlinenlg{a,x,fw} & \leftarrow & \inlinenlg{x,fw}&,
\                 \inlinenlg{} & \rightarrow & \inlinenlg{e,x,fw} & \leftarrow & \inlinenlg{x,fw}&,\  \condtrue_X \big) \\
R_2    &= \big( & \inlinenlg{} & \rightarrow & \inlinenlg{b,fw}   & \leftarrow & \inlinenlg{fw}&,
\                 \inlinenlg{} & \rightarrow & \inlinenlg{e,fw}   & \leftarrow & \inlinenlg{fw}&,\  \mathcal A_{\exists X} \big) \\
\mathcal A_{\exists X} &= \mathrlap{\Big(
\inlinenlg{}, \exists, \big\{ (
\inlinenlg{} \rightarrow \inlinenlg{x} \leftarrow \inlinenlg{x},\  \condtrue_X
) \big\}
\Big)}
\end{array}\egroup\]

Here $X = \inlinenlg{x}$. In this case, an $a$-loop can be replaced with an $e$-loop if an $x$-loop is present, ensured by requiring (and retaining) it in the rule $R_1$.
A $b$-loop can also be replaced with an $e$-loop, also if an $x$-loop is present, this time ensured by an application condition.

Now consider the conditional relation
$R = \{ (\inlinenlg{a}, \inlinenlg{b}, \condtrue) \} \cup \{ (G,G,\condtrue) \mid \text{$G$ is}\allowbreak\text{a graph} \}$[
The reflexive triples $(G,G,\condtrue)$ are needed because
$\inlinenlg{a}, \inlinenlg{b}$ can both be transformed to $\inlinenlg{e}$ in the presence of $\inlinenlg{x}$ and we require
that the resulting (identical) graphs are related.]
(all graphs are seen as cospans with empty interfaces)
and the accompanying relation
$R' = \{ (a;d, b;d) \mid (a,b,\mathcal C) \in R \land d \models \mathcal C \}$.

Clearly, the graphs $\inlinenlg{a}$ and $\inlinenlg{b}$ are bisimilar under all contexts,
and therefore $R'$ is a bisimulation:
either the context contains an $x$-loop, then they both reduce to a graph that contains $\inlinenlg{e,x}$ and possibly further context (both steps reach the same graph),
or the context does not contain an $x$-loop, in which case neither rule is applicable.

However, $R$ is not a conditional bisimulation, the violating triple being $(\inlinenlg{a},\inlinenlg{b},\condtrue)$:
the step $\inlinenlg{b} \cstep{\id}{\mathcal A_{\exists X}} \inlinenlg{e}$ cannot be answered by $\inlinenlg{a}$,
since in $R_1$, the $x$-loop is directly participating in the
reaction, but $\mathcal A_{\exists X}$ only guarantees its existence
in a passive environment (i.e. it is not participating in the reaction).
($\inlinenlg{a}$ could only do a step by borrowing $\inlinenlg{x}$, but this does not constitute a valid answering step for the step of $\inlinenlg{b}$ where $\id$ (i.e. no additional elements) has been borrowed.)

Next, we will show that conditional bisimilarity $\csimC$ is a conditional congruence.
This is an important plausibility check, since reactive systems have
been introduced with the express purpose to define and reason about
bisimulation congruences.

Conditional bisimilarity $\csimC$ is a conditional congruence.

We show that $\csimC$ is:

reflexive We prove that $R = \{(a,a,\mathcal{C})\mid \codom(a) =
\Ro(\mathcal{C})\}$ is a conditional bisimulation.

Any context step $a \cstep{f}{\mathcal A} a'$ can be trivially
answered by the exact same step, setting
$\mathcal B_1 \defeq \mathcal A,\ \mathcal C_1^\prime \defeq
\mathcal C_{\downarrow f},\ b_1^\prime \defeq a'$, where
$I = \{1\}$, and we have
$(a',b'_1,\mathcal{C}'_1) = (a', a', \mathcal C_{\downarrow f}) \in

Let $R$ be a conditional bisimulation.
It is easily seen that $R^{-1}$, due to the symmetric nature of the definition, is also a conditional bisimulation.
Then, $R \subseteq \csimC$ implies $R^{-1} \subseteq \csimC$,
which proves symmetry of $\csimC$.

transitive Let $R_1, R_2$ be conditional bisimulations that are
closed under condition strengthening, i.e.
$(a,b,\mathcal C')\in R_i$ and $\mathcal C \models \mathcal C'$
implies $(a,b,\mathcal C) \in R_i$.  We show that
$R_1R_2 \defeq \{ (a,c,\mathcal D) \mid \text{there exists $b$ such that }
(a,b,\mathcal D) \in R_1 \,\text{ and }\, (b,c,\mathcal D) \in R_2 \}$
is a conditional bisimulation.

Then, since $\csimC$ is a conditional bisimulation closed under
condition strengthening (<Ref>),
$(a,b,\mathcal D) \in \csimC, (b,c,\mathcal D) \in \csimC$ implies
$(a,c,\mathcal D) \in \csimC\csimC$ and, since we show that
$\csimC\csimC$ is a conditional bisimulation,
$a,c$ are conditionally bisimilar under $\mathcal D$, which proves
transitivity of $\csimC$.

Consider a triple $(a,c,\mathcal D) \in R_1R_2$,
which by construction of $R_1R_2$ results from some $(a,b,\mathcal D) \in R_1,\ (b,c,\mathcal D) \in R_2$.
Also consider a step
$a \cstep{f}{\mathcal A} a'$.
Then, $R_1R_2$ fulfills the requirements of a conditional bisimulation:

* Answering steps $c \cstep{f}{\mathcal C_{i,j}} c_{i,j}^\prime$:
Since $(a,b,\mathcal D) \in R_1$ and $R_1$ is a conditional bisimulation,
we know that there exist answering steps
$b \cstep{f}{\mathcal B_i} b_i^\prime$ such that for all $i \in I$,
$(a', b_i^\prime, \mathcal D_i^\prime) \in R_1$ and
$\mathcal A \land \mathcal D_{\downarrow f} \models \bigvee_{i \in I} \left( \mathcal D_i^\prime \land \mathcal B_i \right)$.

Additionally, since $(b,c,\mathcal D) \in R_2$, for each
$b \cstep{f}{\mathcal B_i} b_i^\prime$ there exist answering steps
$c \cstep{f}{\mathcal C_{i,j}} c_{i,j}^\prime$ such that for all $j \in J_i$ we have
$(b_i^\prime, c_{i,j}^\prime, \mathcal D_{i,j}^\prime) \in R_2$ and
$\mathcal B_i \land \mathcal D_{\downarrow f} \models \bigvee_{j \in J_i} \big( \mathcal D_{i,j}^\prime \land \mathcal C_{i,j} \big)$.

We now collect all answering steps $c \cstep{f}{\mathcal C_{i,j}} c_{i,j}^\prime$
and use them as answering steps for the original step $a \cstep{f}{\mathcal A} a'$.

* $(a', c_{i,j}', \mathcal D_{i,j}^\prime) \in R_1R_2$:
Since $(a', b_i^\prime, \mathcal D_i^\prime) \in R_1$, and $R_1$ is closed
under condition strengthening, and
$\mathcal D_{i,j}^\prime \land \mathcal D_i^\prime \models \mathcal D_i^\prime$,
we also have $(a',\ b_i^\prime,\ \mathcal D_{i,j}^\prime \land
\mathcal D_i^\prime) \in R_1$ for all $j\in J_i$.
Similarly, we obtain $(b_i^\prime,\ c_{i,j}^\prime,\ \mathcal D_{i,j}^\prime \land \mathcal D_i^\prime) \in R_2$.
By construction of $R_1R_2$ we then also have $(a',\ c_{i,j}^\prime,\ \mathcal D_{i,j}^\prime \land \mathcal D_i^\prime) \in R_1R_2$.

* $\mathcal A \land \mathcal D_{\downarrow f} \models \bigvee_{i \in I} \left( \mathcal D_i^\prime \land \mathcal C_i^\prime \right)$:
We now rewrite

\begin{align*}
\mathcal A \land \mathcal D_{\downarrow f} &\models \bigvee\nolimits_{i \in I} \left( \mathcal D_i^\prime \land \mathcal B_i \right)
&&\text{(given from $(a,b,\mathcal D) \in R_1$)} \\
\mathcal A \land \mathcal D_{\downarrow f} &\models \bigvee\nolimits_{i \in I} \left( \mathcal D_i^\prime \land \mathcal B_i \right) \land \mathcal D_{\downarrow f}
&&\text{(since $\mathcal D_{\downarrow f}$ is given on the left already)}
\\
\mathcal A \land \mathcal D_{\downarrow f} &\models \bigvee\nolimits_{i \in I} \left( \mathcal D_i^\prime \land \mathcal B_i \land \mathcal D_{\downarrow f} \right)
\intertext{From $(b,c,\mathcal D) \in R_2$ we know $\mathcal B_i \land \mathcal D_{\downarrow f} \models \bigvee_{j \in J_i} \big( \mathcal D_{i,j}^\prime \land \mathcal C_{i,j} \big)$, therefore this also implies:}
\mathcal A \land \mathcal D_{\downarrow f} &\models \mathrlap{\bigvee\nolimits_{i \in I} \Big( \mathcal D_i^\prime \land \bigvee\nolimits_{j \in J_i} \big( \mathcal D_{i,j}^\prime \land \mathcal C_{i,j} \big) \Big)}
\\
\mathcal A \land \mathcal D_{\downarrow f} &\models \mathrlap{\bigvee\nolimits_{i \in I,\, j \in J_i} \big( \mathcal D_i^\prime \land \mathcal D_{i,j}^\prime \land \mathcal C_{i,j} \big)}
\end{align*}

Observe that this implication is of the required form for the previously
derived tuples $(a',\ c_{i,j}^\prime,\ \mathcal D_{i,j}^\prime \land \mathcal D_i^\prime) \in R_1R_2$.

In case $I$ is infinite, the same idea can be applied, but we need to slightly change the notation to prevent the creation of infinite disjunctions:

\begin{align*}
c \models (\mathcal A \land \mathcal D_{\downarrow f}) &\implies \exists i \in I \colon c \models ( \mathcal D_i' \land \mathcal B_i)
&&\text{(since $(a,b,\mathcal D) \in R_1$)} \\
c \models (\mathcal A \land \mathcal D_{\downarrow f}) &\implies \mathrlap{\exists i \in I \colon c \models ( \mathcal D_i' \land \mathcal B_i ) \land c \models \mathcal D_{\downarrow f} }
&&\text{($\mathcal D_{\downarrow f}$ on left)}
\\
c \models (\mathcal A \land \mathcal D_{\downarrow f}) &\implies \exists i \in I \colon c \models ( \mathcal D_i' \land \mathcal B_i \land \mathcal D_{\downarrow f} )
\intertext{From $(b,c,\mathcal D) \in R_2$ we know $c \models (\mathcal B_i \land \mathcal D_{\downarrow f}) \implies \exists j \in J_i \colon ( \mathcal D_{i,j}^\prime \land \mathcal C_{i,j} )$, therefore this also implies:}
c \models (\mathcal A \land \mathcal D_{\downarrow f}) &\implies \mathrlap{\exists i \in I \colon c \models \mathcal D_i' \land \exists j \in J_i \colon c \models ( \mathcal D_{i,j}^\prime \land \mathcal C_{i,j} ) }
\\
c \models (\mathcal A \land \mathcal D_{\downarrow f}) &\implies \mathrlap{\exists i \in I, j \in J_i \colon c \models (\mathcal D_i' \land \mathcal D_{i,j}^\prime \land \mathcal C_{i,j} ) }
\end{align*}

Symmetrically, steps $c \cstep{f}{\mathcal C} c'$ can be answered by $a$.
Therefore, $R_1R_2$ is a conditional bisimulation.

closed under contextualization
We show that $u(R) = \left\{ (a;d, b;d, \mathcal{C}_{\downarrow d}) \mid (a,b,\mathcal C) \in R \right\}$ is a conditional bisimulation, assuming $R$ is a conditional bisimulation.

Consider a triple $(a;d, b;d, \mathcal{C}_{\downarrow d}) \in u(R)$
and a step $a;d \cstep{f}{\mathcal A} a'$.
This step is due to some rule $(\ell, r, \mathcal R)$.
We have to show that there exist answering steps $b;d \cstep{f}{\mathcal{B}_i} b_i^\prime$
such that $(a', b_i^\prime, \mathcal{C}_i^\prime) \in u(R)$
and $\mathcal A \land (\mathcal{C}_{\downarrow d})_{\downarrow f} \models \bigvee_{i \in I} \left( \mathcal{C}_i^\prime \land \mathcal{B}_i \right)$.

According to <Ref>, the given step can be rewritten to $a \cstep{d;f}{\mathcal A} a'$.

By construction of $u(R)$, for the given triple $(a;d, b;d, \mathcal{C}_{\downarrow d}) \in u(R)$ there must exist a triple $(a,b,\mathcal C) \in R$.
As $R$ is a conditional bisimulation, the step $a \cstep{d;f}{\mathcal A} a'$
has answering steps $b \cstep{d;f}{\mathcal B_i} b_i^\prime$
such that $(a', b_i^\prime, \mathcal{C}_i^\prime) \in R$
and $\mathcal A \land \mathcal{C}_{\downarrow d;f} \models \bigvee_{i \in I} \left( \mathcal{C}_i^\prime \land \mathcal{B}_i \right)$.

However, we are not interested in answering steps for the context $d;f$, but rather for the original step $a;d \cstep{f}{\mathcal A} a'$.

* Answering steps $b;d \cstep{f}{\mathcal{B}_i} b_i^\prime$:
According to <Ref>,
the answering steps $b \cstep{d;f}{\mathcal B_i} b_i^\prime$
can be rewritten to $b;d \cstep{f}{\mathcal B_i} b_i^\prime$.

* $(a^\prime, b_i^\prime, \mathcal{C}_i^\prime) \in u(R)$:
Since $(a', b_i^\prime, \mathcal{C}_i^\prime) \in R$,
we have $(a';\id,\ b_i^\prime;\id,\ \mathcal{C}_{i \downarrow \id}^\prime) = (a', b_i^\prime, \mathcal{C}_i^\prime) \in u(R)$.

* $\mathcal{A} \land (\mathcal{C}_{\downarrow d})_{\downarrow f} \models \bigvee_{i \in I} \left( \mathcal{C}_i^\prime \land \mathcal{B}_i \right)$:
The implication to be shown is identical to the one that we obtained above,
except for $(\mathcal{C}_{\downarrow d})_{\downarrow f}$, which, however, is
equivalent to $\mathcal C_{\downarrow d;f}$.

Answering steps for $b;d \cstep{f}{\mathcal B} b'$ can be derived analogously.

§.§ Alternative Characterization using Fixpoint Theory

Behavioural equivalences can be characterized as fixpoints of certain functions on complete lattices [28].
Before we provide definitions that characterize conditional bisimulation relations as fixpoints, we provide a quick summary of fixpoint theory.
We do not rely on this characterization in the proofs in this section.
However, we will use the theory and the alternative definitions for the proofs of up-to techniques in <Ref>.

A complete lattice is a partially ordered set $(L,
\sqsubseteq)$ where each subset $Y\subseteq L$ has an infimum,
denoted by $\bigsqcap Y$ and a supremum, denoted by $\bigsqcup Y$.
In this paper, the type of lattices that we consider
contain relations ordered by inclusion,
i.e. the elements of the lattice are relations
and thus the functions we consider map relations to relations.

A function $f \colon L \to L$ is monotone if for all $l_1, l_2 \in L$,
$l_1 \sqsubseteq l_2$ implies $f(l_1) \sqsubseteq f(l_2)$,
idempotent if $f \circ f = f$,
and extensive if $l \sqsubseteq f(l)$ for all $l \in L$.
When $f$ is monotone, extensive and idempotent it is called an (upper) closure.
In this case, $f(L) = \{ f(l) \mid l \in L \}$ is a complete lattice.

Given some behavioural equivalence, we define a monotone function
$f \colon L \to L$ in such a way that its greatest fixpoint $\nu f$
equals the behavioural equivalence.  Behavioural equivalence can
then be checked by establishing whether some given element of the
lattice $l \in L$ (for instance a relation consisting of a single
pair) is under the fixpoint, i.e., if $l \sqsubseteq \nu f$.
By Tarski's Theorem [34],
$\nu f = \bigsqcup \{ x \mid x \sqsubseteq f(x) \}$, i.e., the
greatest fixpoint is the supremum of all post-fixpoints. Hence for
showing that $l\sqsubseteq \nu f$, it is sufficient to prove that
$l$ is under some post-fixpoint $l'$, i.e.,
$l \sqsubseteq l'\sqsubseteq f(l')$.

Using these preliminaries, we can now give an alternative characterization
of conditional bisimulation using fixpoint theory:

Consider the complete lattice $\Condrel$, which is the set of all conditional relations ordered by set inclusion.
Then, conditional bisimulations can also be seen as post-fixpoints of $f_C$
(i.e. $R$ is a conditional bisimulation if and only if $R \subseteq f_C(R)$),
and conditional bisimilarity as the greatest fixpoint of $f_C$
(i.e. $\csimC = \nu f_C$),
where the monotone function $f_C \colon \Condrel \to \Condrel$ is
the conditional bisimulation function
defined by

\begin{align*}
f_C(R) \defeq \big\{ (a,b,\mathcal C) \;\big|\; &
\text{for each
$a \cstep{f}{\mathcal A} a'$
there exist
$b \cstep{f}{\mathcal B_i} b_i'$
conditions $\mathcal C_i'$
} \\& \text{%
such that
$(a', b_i', \mathcal C_i') \in R$
$\mathcal A \land \mathcal C_{\downarrow f} \models
{\textstyle\bigvee\nolimits_{i \in I}} (\mathcal C_i' \land
\mathcal B_i)$,
} \\& \text{%
and vice versa (for each $\smash{b \cstep{f}{\mathcal B} b'}$\dots)%
\big\}
\end{align*}

The correctness of this characterization (i.e. that “$f_C$ is the right function”) can be seen by
expanding the definition of $f_C$ on the right-hand side of $(a,b,\mathcal C) \in R \implies (a,b,\mathcal C) \in f_C(R)$,
which results in exactly the definition of a conditional
bisimulation relation.

§.§ Representative Conditional Bisimulations

Checking whether two arrows are conditionally bisimilar, or whether a
given relation is a conditional bisimulation, can be hard in
practice, since we have to check all possible context steps, of which
there are typically infinitely many.

For saturated bisimilarity, we used representative steps instead of context
steps (cf. <Ref>) to reduce the number of contexts to
be checked.
In this section, we extend our definition of conditional bisimulation to use
representative steps and prove that the resulting bisimilarity is identical to
the one previously defined.

[Representative conditional bisimulation]
We fix a conditional reactive system.
A representative conditional bisimulation $R$ is a conditional relation such that the following holds:
for each triple $(a,b,\mathcal{C}) \in R$ and each representative step $a \rstep{f}{\mathcal A} a^\prime$,
there are answering context steps $b \cstep{f}{\mathcal{B}_i} b_i^\prime$ and conditions $\mathcal{C}_i^\prime$
such that $(a^\prime, b_i^\prime, \mathcal{C}_i^\prime) \in R$
and $\mathcal{A} \land \mathcal{C}_{\downarrow f} \models \bigvee_{i \in I} \left( \mathcal{C}_i^\prime \land \mathcal{B}_i \right)$;
and vice versa.
Two arrows are representative conditionally bisimilar under $\mathcal C$ ($(a, b, \mathcal{C}) \in \csimR$) whenever a representative conditional bisimulation $R$ with $(a, b, \mathcal{C}) \in R$ exists.

Analogously to <Ref>, we can define
representative conditional bisimulations as post-fixpoints of $f_R$,
and representative conditional bisimilarity as the greatest fixpoint
of $f_R$, where $f_R$ is defined on $\Condrel$ as follows:

\begin{align*}
f_R(R) \defeq \big\{ (a,b,\mathcal C) \;\big|\; &
\text{for each
$a \rstep{f}{\mathcal A} a'$
there exist
$b \cstep{f}{\mathcal B_i} b_i'$
conditions $\mathcal C_i'$
} \\& \text{%
such that
$(a', b_i', \mathcal C_i') \in R$
$\mathcal A \land \mathcal C_{\downarrow f} \models {\textstyle\bigvee\nolimits_{i \in I}} (\mathcal C_i' \land \mathcal B_i)$,
} \\& \text{%
and vice versa (for each $\smash{b \rstep{f}{\mathcal B} b'}$\dots)%
\big\}
\end{align*}

It is easy to see that $f_C \subseteq f_R$:
Their definitions differ only in the type of steps which are checked.
A triple that satisfies the requirements for all context steps (is in $f_C(R)$)
naturally satisfies them for all representative steps (is in $f_R(R)$),
since every representative step is also a context step.

To show that the two conditional bisimilarities using context and representative steps are equivalent (<Ref>) and for the proofs of <Ref>, we need the following two lemmas:

Given a context step $a \cstep{f}{\mathcal A} a^\prime$, the borrowed context $f$ can be extended by an additional context $c'$, that is:

Representative conditional bisimilarity is closed under contextualization, that is,
$(a,b,\mathcal{C}) \in \csimR$ implies $(a;d, b;d, \mathcal{C}_{\downarrow d}) \in \csimR$.

We show that $u(R) = \left\{ (a;d, b;d, \mathcal{C}_{\downarrow d}) \mid (a,b,\mathcal C) \in R \right\}$ is a representative conditional bisimulation, assuming $R$ is a representative conditional bisimulation.

Consider a triple $(a;d, b;d, \mathcal{C}_{\downarrow d}) \in u(R)$
and a step $a;d \rstep{f}{\mathcal A} a'$.
This step is due to some rule $(\ell, r, \mathcal R)$.
We have to show that there exist answering steps $b;d \cstep{f}{\mathcal{B}_i} b_i^\prime$
such that $(a', b_i^\prime, \mathcal{C}_i^\prime) \in u(R)$
and $\mathcal A \land (\mathcal{C}_{\downarrow d})_{\downarrow f} \models \bigvee_{i \in I} \left( \mathcal{C}_i^\prime \land \mathcal{B}_i \right)$.

The representative step is of course also a context step ($a;d \cstep{f}{\mathcal A} a'$),
which, according to <Ref>, can be rewritten to $a \cstep{d;f}{\mathcal A} a'$.
As a result, the step is not necessarily a representative one anymore. However we can find a matching representative step (see also <Ref>):

(tlempty) at (0,0) $\obnull$;
(i) at (2.5,0) $I$;
(trempty) at (4.7,0) $\obnull$;
(j) at (0,-2.5) $J$;
(k) at (2.5, -2.5) $K$;
[inner sep=2pt] (ki) at ($(j)!0.5!(k)$) ;
[->] (tlempty) – node[above]$\ell$ (i);
[->] (trempty) – node[above]$r$ (i);
[->] (trempty) to[bend left=5] node[right]$a'$ (k);

[->] (tlempty) – node[left]$a$ (j);
[->] (i) to[bend left=5] node[right]$c$ (k);

[->] (j) – node[below]$d$ (ki);
[->] (ki) – node[below]$f$ (k);

[condtri,shape border rotate=270] at (i.north) $\mathcal{R}$;
[condtri,shape border rotate=90] at (k.south) $\mkern-3mu\mathcal{A}$;

at (5.75,-1.5) $\rightarrow$;

(tlempty) at (0,0) $\obnull$;
(i) at (2.5,0) $I$;
(trempty) at (4.7,0) $\obnull$;
(j) at (0,-2.4) $J$;
(kp) at (1.95,-1.95) $\hat K$;
(k) at (2.9, -2.9) $K$;
[inner sep=2pt] (ki) at ($(j)!0.5!(k)$) ;
[->] (tlempty) – node[above]$\ell$ (i);
[->] (trempty) – node[above]$r$ (i);
[->] (trempty) to[bend left=5] node[right]$a'$ (k.40);

[->] (tlempty) – node[left]$a$ (j);
[->] (i.300) to[bend left=5] node[right]$c$ (k);

[->] (j) – node[below]$d$ (ki);
[->] (ki) – node[below]$f$ (k);

[->] (i) – node[left]$\hat c$ (kp);
[->] (j) – node[above]$\hat f$ (kp);
[->] (kp) – node[right,pos=0.1]9pt$\hat g$ (k);

[condtri,shape border rotate=270] at (i.north) $\mathcal R$;
[condtri,shape border rotate=90] at (k.south) $\mathcal A$;

[rotate around=-55:(kp.center),condtri,shape border rotate=0,scale=0.7] at (kp.west)
25$\mathcal{R}_{\downarrow \hat c}$

Note that $\hat f;\hat g = d;f,\ \hat c;\hat g = c$.
Variables with a hat (e.g. $\hat c$) refer to the representative step,
but otherwise play the same role than their unhatted counterparts (e.g. $c$), which refer to the original step.
The result is a representative step
$a \rstep{\hat f}{\mathcal{R}_{\downarrow \hat c}} r;\hat c$.

By construction of $u(R)$, for the given triple $(a;d, b;d, \mathcal{C}_{\downarrow d}) \in u(R)$ there must exist a triple $(a,b,\mathcal C) \in R$.
As $R$ is a representative conditional bisimulation, the step $a \rstep{\hat f}{\mathcal{R}_{\downarrow \hat c}} r;\hat c$
has answering steps $b \cstep{\hat f}{\hat{\mathcal{B}_i}} \hat{b_i^\prime}$
such that $(r;\hat c, \hat{b_i^\prime}, \hat{\mathcal{C}_i^\prime}) \in R$
and $\mathcal{R}_{\downarrow \hat c} \land \mathcal{C}_{\downarrow \hat f} \models \bigvee_{i \in I} \left( \hat{\mathcal{C}_i^\prime} \land \hat{\mathcal{B}_i}\right)$.

However we are not interested in answering steps for the representative context $\hat f$, but rather for the original step $a;d \rstep{f}{\mathcal A} a'$, that is, we need answering steps of $b;d$ using context $f$.
So we need
(1) answering steps $b;d \cstep{f}{\mathcal{B}_i} b_i^\prime$
(2) such that $(a^\prime, b_i^\prime, \mathcal{C}_i^\prime) \in u(R)$
and (3) $\mathcal A \land (\mathcal{C}_{\downarrow d})_{\downarrow f} \models \bigvee_{i \in I} \left( \mathcal{C}_i^\prime \land \mathcal{B}_i \right)$.

* Answering steps $b;d \cstep{f}{\mathcal{B}_i} b_i^\prime$:
<Ref> and $b \cstep{\hat f}{\hat{\mathcal{B}_i}} \hat{b_i^\prime}$
imply that steps $b \cstep{\hat f;\hat g}{{\hat{\mathcal{B}_i}}_{\downarrow \hat g}} \hat{b_i^\prime};\hat g$ are possible.
Since $d;f = \hat f;\hat g$, these are equivalent to $b \cstep{d;f}{{\hat{\mathcal{B}_i}}_{\downarrow \hat g}} \hat{b_i^\prime};\hat g$.
We set $b_i^\prime \defeq \hat{b_i^\prime};\hat g,\ \mathcal{B}_i \defeq {\hat{\mathcal{B}_i}}_{\downarrow \hat g}$
and get steps $b \cstep{d;f}{\mathcal{B}_i} b_i^\prime$,
which, according to <Ref>, are equivalent to steps $b;d \cstep{f}{\mathcal{B}_i} b_i^\prime$.

* $(a^\prime, b_i^\prime, \mathcal{C}_i^\prime) \in u(R)$:
Set $\mathcal{C}_i^\prime \defeq \hat{\mathcal{C}_i^\prime}_{\downarrow \hat g}$.
By construction of $u(R)$, $(r;\hat c,\ \hat{b_i^\prime},\ \hat{\mathcal{C}_i^\prime}) \in R$ implies $(r;\hat c;\hat g,\ \hat{b_i^\prime};\hat g,\ \hat{\mathcal{C}_i^\prime}_{\downarrow \hat g}) = (a^\prime, b_i^\prime, \mathcal{C}_i^\prime) \in u(R)$.

* $\mathcal{A} \land (\mathcal{C}_{\downarrow d})_{\downarrow f} \models \bigvee_{i \in I} \left( \mathcal{C}_i^\prime \land \mathcal{B}_i \right)$:
Above, we already showed $\mathcal{R}_{\downarrow \hat c} \land \mathcal{C}_{\downarrow \hat f} \models \bigvee_{i \in I} \left( \hat{\mathcal{C}_i^\prime} \land \hat{\mathcal{B}_i} \right)$.
By shifting both sides with $\hat g$ and applying the rules of <Ref>, we get:

\begin{align*}
\mathcal{R}_{\downarrow \hat c} \land \mathcal{C}_{\downarrow \hat f}
&\models \bigvee\nolimits_{i \in I} \left( \hat{\mathcal{C}_i} \land \hat{\mathcal{B}_i} \right)
\\ \Rightarrow
\left( \mathcal{R}_{\downarrow \hat c} \land \mathcal{C}_{\downarrow \hat f} \right)_{\downarrow \hat g}
&\models \left( \bigvee\nolimits_{i \in I} \big( \hat{\mathcal{C}_i^\prime} \land \hat{\mathcal{B}_i} \big) \right)_{\downarrow \hat g}
\\ \Leftrightarrow
\mathcal{R}_{\downarrow \hat c;\hat g} \land \mathcal{C}_{\downarrow \hat f;\hat g}
&\models \bigvee\nolimits_{i \in I} \left( {\hat{\mathcal{C}_i^\prime}}_{\downarrow \hat g} \land {\hat{\mathcal{B}_i}}_{\downarrow \hat g} \right)
\end{align*}

By substituting $\hat c;\hat g = c,\   \hat f;\hat g = d;f,\   \mathcal{C}_i^\prime = {\hat{\mathcal{C}_i^\prime}}_{\downarrow \hat g},\   \mathcal{B}_i = {\hat{\mathcal{B}_i}}_{\downarrow \hat g}$, we obtain
$\mathcal{R}_{\downarrow c} \land \mathcal{C}_{\downarrow d;f}
\models \bigvee_{i \in I} \left( \mathcal{C}_i^\prime \land \mathcal{B}_i \right)$.
Since $\mathcal{A} \models \mathcal{R}_{\downarrow c}$, we have $\mathcal{A} \land \mathcal{C}_{\downarrow d;f} \models \mathcal{R}_{\downarrow c} \land \mathcal{C}_{\downarrow d;f} \models \bigvee_{i \in I} \left( \mathcal{C}_i^\prime \land \mathcal{B}_i \right)$, which was to be shown.

Analogously, answering steps for $b;d \rstep{f}{\mathcal B} b'$ can be constructed.

The following theorem is based on a proof strategy similar to

Conditional bisimilarity and representative conditional bisimilarity , that is, $\csimC = \csimR$.

$\csimC \subseteq \csimR$
Consider a triple $(a, b, \mathcal C) \in \csimC$.
By <Ref>, for each step $a \cstep{f}{\mathcal A} a^\prime$
there exist answering steps of $b$ with the requirements listed there;
symmetrically, each step $b \cstep{f}{\mathcal B} b^\prime$ can be answered by $a$.
To show that $(a, b, \mathcal C) \in \csimR$, the same statement has to be shown for each representative step $a \rstep{f}{\mathcal{A}} a^\prime$
(and $b \rstep{f}{\mathcal{B}} b^\prime$).
Since it already holds for all context steps, which are a superset of representative steps (every $\rightarrow_R$ step is also a $\rightarrow_C$ step), <Ref> is trivially satisfied.

$\csimC \supseteq \csimR$
By definition of $\csimC$, if a conditional relation $R$ is a conditional bisimulation, then $R \subseteq \csimC$.
We show that $R = \csimR$ is a conditional bisimulation, i.e. that it satisfies the requirements of <Ref>.

Consider a triple $(a, b, \mathcal C) \in \Relname$ and a context step $a \cstep{f}{\mathcal A} a'$.
This step is due to some rule $(\ell, r, \mathcal R)$.
According to <Ref>, this context step can be reduced to a representative step
$a \rstep{\hat f}{\mathcal{R}_{\downarrow \hat c}} r;\hat c$,
and there exists $\hat g$ such that $\hat f ; \hat g = f,\ \hat c ; \hat g = c$.
Again, all variables with a hat (e.g. $\hat c$) refer to the representative step,
but otherwise take the same role as their unhatted counterparts.

Since $\Relname$ is the representative conditional bisimilarity,
$\Relname$ is a representative conditional bisimulation.
Together with $(a, b, \mathcal C) \in \Relname$, this means that
for the aforementioned step there exist answering steps $b \cstep{\hat f}{\hat{\mathcal{B}_i}} \hat{b_i^\prime}$ and conditions $\hat{\mathcal{C}_i^\prime}$,
such that $(r;\hat c,\ \hat{b_i^\prime},\ \hat{\mathcal{C}_i^\prime}) \in \Relname$ and
$\mathcal{R}_{\downarrow \hat c} \land \mathcal{C}_{\downarrow \hat f}
\models \bigvee_{i \in I} \big( \hat{\mathcal{C}_i^\prime} \land \hat{\mathcal{B}_i} \big)$.

However we are not interested in answering steps for the representative step, but rather for the original step $a \cstep{f}{\mathcal A} a'$,
that is, we need answering steps of $b$ using context $f$.
So we need
(1) answering steps $b \cstep{f}{\mathcal{B}_i} b_i^\prime$
(2) such that $(a^\prime, b_i^\prime, \mathcal{C}_i^\prime) \in \Relname$
and (3) $\mathcal{A} \land \mathcal{C}_{\downarrow f} \models \bigvee_{i \in I} \left( \mathcal{C}_i^\prime \land \mathcal{B}_i \right)$.
Analogously to the proof of <Ref>, we have:

* Answering steps:
Having steps $b \cstep{\hat f}{\hat{\mathcal B_i}} \hat{b_i^\prime}$
implies that steps  are possible (<Ref>).
Rewritten as $b \cstep{f}{\mathcal B_i} b_i^\prime$ (where $\mathcal B_i \defeq {\hat{\mathcal B_i}}_{\downarrow \hat g},\ b_i^\prime \defeq \hat{b_i^\prime};\hat g$), we get the desired answering steps for the original step.

* $(a', b_i', \mathcal C_i') \in R$:
Since $\Relname$ is the representative conditional bisimilarity, by <Ref> we know that $\Relname$ is closed under contextualization.
$(r;\hat c,\ \hat{b_i^\prime},\ \hat{\mathcal{C}_i^\prime}) \in \Relname$ implies
$(r;\hat c;\hat g,\ \hat{b_i^\prime};\hat g,\ \hat{\mathcal C_i^\prime}_{\downarrow \hat g}) = (a^\prime, b_i^\prime, \mathcal C_i^\prime) \in \Relname$,
i.e. the original target $a^\prime$ is conditionally bisimilar to the targets $\hat{b_i^\prime};\hat{g}$ of the answering steps.

* $\mathcal{A} \land \mathcal{C}_{\downarrow f} \models \bigvee_{i \in I} \left( \mathcal{C}_i^\prime \land \mathcal{B}_i \right)$:
Using the rules of <Ref> we get:

\begin{align*}
\mathcal R_{\downarrow \hat c} \land \mathcal C_{\downarrow \hat f}
& \models \bigvee \left( \hat{\mathcal C_i^\prime} \land \hat{\mathcal B_i} \right)
\\ \Rightarrow
(\mathcal R_{\downarrow \hat c})_{\downarrow \hat g} \land (\mathcal{C}_{\downarrow \hat{f}})_{\downarrow \hat g}
& \models \bigvee \left( \hat{\mathcal C_i^\prime}_{\downarrow \hat g} \land \hat{\mathcal B_i}_{\downarrow \hat g} \right)
\\ \Leftrightarrow
\mathcal R_{\downarrow \hat c ;\hat g} \land \mathcal{C}_{\downarrow \hat{f};\hat{g}}
& \models \bigvee \left( \hat{\mathcal C_i^\prime}_{\downarrow \hat g} \land \hat{\mathcal B_i}_{\downarrow \hat g} \right)
\\ \Leftrightarrow
\mathcal R_{\downarrow c} \land \mathcal C_{\downarrow f}
& \models \bigvee \left( \mathcal C_i^\prime \land \mathcal{B}_i \right)
\end{align*}

Since $\mathcal A \models \mathcal R_{\downarrow c}$,
we have $
\mathcal A \land \mathcal C_{\downarrow f}
\models \mathcal R_{\downarrow c} \land \mathcal C_{\downarrow f}
\models \bigvee \left( \mathcal{C}_i^\prime \land \mathcal{B}_i \right)
$, which is the required condition for the triple $(a, b, \mathcal C)$.

Analogously, we can construct answering steps for $b \cstep{f}{\mathcal B} b'$.
We have therefore shown that $\Relname = \csimR$ is a conditional bisimulation and therefore $\csimR \subseteq \csimC$.

We now discuss the notion of representative condition bisimulation in
two examples.

[Message passing over unreliable channels, continued]
Consider the reactive system of <Ref>.  There
exists a representative conditional bisimulation $R$ such that

$(\emptyset \rightarrow \inlinechan{reliable} \leftarrow \inlinechan{},\ %
\emptyset \rightarrow \inlinechan{unreliable} \leftarrow \inlinechan{},\ \AIneN) \in R$
(where $\AIneN$ requires that no $\noiseLabel$-edge exists).

We consider the representative steps that are possible from either
$\inlinechan{reliable}$ or $\inlinechan{unreliable}$ and only explain the most interesting cases
(cf. <Ref>).

* The graph $\inlinechan{reliable}$ can do a step using rule $P_R$ by borrowing a message on
the left node, that is, $f = \inlinechan{} \rightarrow \inlinechan{msgleft} \leftarrow \inlinechan{}$,
reacting to $\inlinechan{reliable,msgright}$.  No further restrictions on the environment are
necessary, so $\mathcal A = \condtrue$.  The graph $\inlinechan{unreliable}$ can answer this step
using $P_U$ and reacts to $\inlinechan{unreliable,msgright}$, but only if no noise is present
(environment satisfies $\mathcal B_i = \AIneN$).  We evaluate
the implication
$\mathcal A \land \mathcal C_{\downarrow f}
\equiv {\condtrue} \land {\AIneN}_{\downarrow f}
\equiv \AIneN
\models
\bigvee_{i \in I} \left( \mathcal{C}_i^\prime \land \AIneN \right)
\equiv \bigvee_{i \in I} \left( \mathcal{C}_i^\prime \land \mathcal{B}_i \right)$,
$\mathcal{C}_i^\prime = \AIneN$. (Note that
${\AIneN}_{\downarrow f} \equiv \AIneN$ since $\AIneN$ forbids
the existence of an $\noiseLabel$-edge between the two interface nodes and $f$
is unrelated, providing an $m$-loop on the left-hand node.)  We now
$(\emptyset \rightarrow \inlinechan{reliable,msgright} \leftarrow \inlinechan{},\ %
\emptyset \rightarrow \inlinechan{unreliable,msgright} \leftarrow \inlinechan{},\ \AIneN) \in R$.

* Symmetrically, $\inlinechan{unreliable}$ can do a step using $P_U$ by borrowing a message on the left node, reacting to $\inlinechan{unreliable,msgright}$ in an environment without noise ($\mathcal A = \AIneN$).
$\inlinechan{reliable}$ can answer this step under any condition $\mathcal B_i$. Then,
the implication is satisfied if we set $\mathcal C_i^\prime = \AIneN$,
so we require again $(\emptyset \rightarrow \inlinechan{reliable,msgright} \leftarrow \inlinechan{},\ %
\emptyset \rightarrow \inlinechan{unreliable,msgright} \leftarrow \inlinechan{},\ \AIneN) \in R$.

* There are additional representative steps that differ in how
much of the left-hand side is borrowed, but can be proven
analogously to the two previously discussed steps.

[gedge/.append style=font=]

/in 0/,3.5/
[gn] (u1) at (-0.35,0) ;
[gn] (u2) at (0.35,0) ;
at (-0.35cm-8pt,0pt) $1$;
at (0.35cm+8pt,0pt) $2$;
[gedge] (u1) – node[below]$\chanlabel$ (u2);

at (1.75,0) $R$;

/in 0/,3.5/
[gn] (u1) at (-0.35,0) ;
[gn] (u2) at (0.35,0) ;
at (-0.35cm-8pt,0pt) $1$;
at (0.35cm+8pt,0pt) $2$;
[gedge] (u1) – node[below]$\chanlabel$ (u2);
[gedge] (u2) to[loop,out=45+90,in=45+20,distance=0.4cm] node[right] $m$ (u2);

at (1.75,-2.75) $R$;

/in 0/,3.5/
[gn] (u1) at (-0.35,0) ;
[gn] (u2) at (0.35,0) ;
at (-0.35cm-8pt,0pt) $1$;
at (0.35cm+8pt,0pt) $2$;
[gedge] (u1) – node[below]$\chanlabel$ (u2);
[gedge] (u2) to[loop,out=45+90,in=45+20,distance=0.4cm] node[right] $m$ (u2);
[gedge] (u2) to[loop,out=45+90+180+10,in=45+180+50,distance=0.4cm] node[right]$m$ (u2);

at (1.75,-5.5) $R$;

in 0,-2.75
[->] (0,-0.6) to (0,-2.25);
at (0.2,-2.1) $C$;
[->] (3.5,-0.6) to (3.5,-2.25);
at (3.5+0.2,-2.1) $C$;

in 0,-2.75
/in 0.7/,4.2/ℬ_i
[gn] (n1) at (-0.25,0) ;
[gn] (n2) at (0.25,0) ;
at (-0.35cm-6pt,0pt) $1$;
at (0.25cm+6pt,0pt) $2$;
[gedge] (n1) to[loop,out=45+90,in=45,distance=0.4cm] node[right] $m$ (n1);
[anchor=west] at (0.5cm,0pt) $, \condlabel$;

[->] (0,-5.5-0.5) to (0,-5.5-1.25);
[->] (3.5,-5.5-0.5) to (3.5,-5.5-1.25);
at (0.2,-5.5-1.1) $C$;
at (3.5+0.2,-5.5-1.1) $C$;
at (0,-5.5-1.5) $\vdots$;
at (3.5,-5.5-1.5) $\vdots$;

Showing conditional bisimilarity may require an infinite number of steps

[gedge/.append style=font=]
at (3.5,-5.5-1.5) $\phantom\vdots$;

/in 0/,3.5/
[gn] (u1) at (-0.35,0) ;
[gn] (u2) at (0.35,0) ;
at (-0.35cm-8pt,0pt) $1$;
at (0.35cm+8pt,0pt) $2$;
[gedge] (u1) – node[below]$\chanlabel$ (u2);

at (1.75,0) $R$;

/in 0/,3.5/
[gn] (u1) at (-0.35,0) ;
[gn] (u2) at (0.35,0) ;
at (-0.35cm-8pt,0pt) $1$;
at (0.35cm+8pt,0pt) $2$;
[gedge] (u1) – node[below]$\chanlabel$ (u2);
[gedge,thick,dash pattern=on 1.25pt off 1.75pt,black!75] (u2) to[loop,out=35+90,in=45,distance=0.5cm] node[right]$\color{black!75}\ m$ (u2);

at (1.75,-3) $R$;

[->] (0,-0.6) to (0,-2.25);
at (0.2,-2.1) $C$;
[->] (3.5,-0.6) to (3.5,-2.25);
at (3.5+0.2,-2.1) $C$;

/in 0.7/,4.2/ℬ_i
[gn] (n1) at (-0.25,0) ;
[gn] (n2) at (0.25,0) ;
at (-0.35cm-6pt,0pt) $1$;
at (0.25cm+6pt,0pt) $2$;
[gedge] (n1) to[loop,out=45+90,in=45,distance=0.4cm] node[right] $m$ (n1);
[anchor=west] at (0.5cm,0pt) $, \condlabel$;

Removing unrelated context (dotted edge) before relating the pair would allow stopping after a single step

Showing conditional bisimilarity of two types of channels using the rules

This means we have to add the pair

to $R$ and to continue adding pairs
until we obtain a bisimulation: with every step, a new triple with an
additional $m$-loop on the right node is added to the relation,
therefore, the smallest conditional bisimulation has infinite size.
This is visualized in <Ref>.

However, except for the additional $m$-loop on the right node, which
does not affect rule application, this pair is identical to the
initial one and we can hence use a similar argument.  In
<Ref> we show how to make this formal, using up-to
technique.  In summary, we conclude that $\inlinechan{reliable}$ is
conditionally bisimilar to $\inlinechan{unreliable}$ under the
condition $\AIneN$.

[Unreliable channel vs. no channel]
For <Ref>, it can also be
shown that under the condition $\neg\AIneN$, the unreliable
channel $\emptyset \rightarrow \inlinechan{unreliable} \leftarrow \inlinechan{}$ is conditionally bisimilar
to not having a channel between the two nodes ($\emptyset \rightarrow \inlinechan{} \leftarrow \inlinechan{}$).

In this case, $\inlinechan{unreliable}$ can still do a reaction under $\AIneN$.
Then, $\inlinechan{}$ can answer with an empty set of steps. The implication $\AIneN \land \mathcal C_{\downarrow f} \models \bigvee_{i \in I} \left( \mathcal C_i^\prime \land \mathcal B_i \right)$
is then simplified to $\AIneN \land \neg \AIneN \models
\condfalse$, which is easily seen to be valid.

§ UP-TO TECHNIQUES FOR PROVING CONDITIONAL BISIMILARITY

Our optimizations so far involved replacing context steps by
representative steps, which ensure finite branching and thus greatly
reduce the proof obligations for a single step. However, it can still
happen very easily that the smallest possible bisimulation is of
infinite size, in which case automated proving of conditional
bisimilarity becomes impossible. For instance, in
<Ref>, the least conditional bisimulation
relating the two cospans $u,r$ (representing (un)reliable channels)
under $\AIneN$
contains infinitely many triples $(u;m^n,\, r;m^n,\, \AIneN)$
for any number $n$ of messages on the right node
($m = \inlinechan{} \rightarrow \inlinechan{msgright} \leftarrow \inlinechan{}$).

On the other hand, conditional bisimilarity is closed under contextualization,
hence if $u,r$ are related, we can conclude that $u;m$ and $r;m$ must be
related as well. Intuitively the relation $R = \{(u,r,\AIneN)\}$
is a sufficient witness, since after one step we reach the triple
$(u;m,\, r;m,\, \AIneN)$, from which we can “peel off” a common context $m$ to
obtain a triple already contained in $R$
(visualized in <Ref>).

This is an instance of an up-to technique, which can be used to
obtain smaller witness relations by identifying and removing redundant
elements from a bisimulation relation.  Instead of requiring the
redundant triple $(u;m,\, r;m,\, \AIneN)$ to be contained in the relation, it is
sufficient to say that up to the passive context $m$, the triple is
represented by $(u,r,\AIneN)$, which is already contained in the
relation.  In particular, this specific up-to technique is known as
up-to context [28], a well-known proof
technique for process calculi.
[Stated in the language of
process algebra, a symmetric relation $R$ is a bisimulation up-to context,
if whenever $(P,Q)\in R$ and $P \xrightarrow{a} P'$,
then $Q \xrightarrow{a} Q'$, where $P' = C[P'']$, $Q' = C[Q'']$ and
$(P'',Q'')\in R$.]

Note that in general, a bisimulation up-to context is not a
bisimulation relation.  However, it can be converted into a
bisimulation by closing it under all contexts.

In this section, we show how to adapt this concept to conditional
bisimilarity and in particular discuss how to deal with the conditions
in a conditional bisimulation .

§.§ Up-To Techniques and Fixpoint Theory

As in <Ref>, we will provide definitions and proofs
that are based on fixpoint theory. Hence, we first introduce the
remaining preliminary concepts for implementing up-to techniques using
fixpoint theory, again mostly following [28].

In <Ref> we already explained that to show that
some element $l$ of the lattice is contained in behavioural equivalence
($l \sqsubseteq \nu f$), it is sufficient to prove that $l$ is under some
post-fixpoint $l'$ ($l \sqsubseteq l' \sqsubseteq f(l')$).
The idea of using up-to techniques is now to define a monotone
function $u$ (the up-to function) and check if
$l \sqsubseteq \nu(f \circ u)$ by showing that $l$ is a
post-fixpoint of $f\circ u$.  Typically, the characteristics
of $u$ should make it easier to prove $l \sqsubseteq f(u(l))$
than proving $l \sqsubseteq f(l)$.  This is clearly the case when
$u$ is extensive, since extensiveness of $u$ and monotonicity of $f$
implies $f(l) \sqsubseteq f(u(l))$ and thus obtaining
$l \sqsubseteq f(u(l))$ is easier than obtaining
$l \sqsubseteq f(l)$.

Naturally, for the up-to technique to be useful, it also has to be shown that $\nu(f \circ u) \sqsubseteq \nu f$:

[sound up-to function]

Let $L$ be a complete lattice and let $f \colon L \to L$ be a monotone
function. A sound up-to function for $f$ is any monotone
function $u \colon L \to L$ such that
$\nu (f \circ u) \sqsubseteq \nu f$.

Instead of soundness, we will use the stronger notion of compatibility:

[$f$-compatibility of $u$]

Let $L$ be a complete lattice and let $f \colon L \to L$ be a monotone
function. A monotone function $u \colon L \to L$ is $f$-compatible if
$u \circ f \sqsubseteq f \circ u$.

Compatibility has several advantages over soundness: First,
compatibility implies soundness, second, $f$-compatible up-to
techniques can be combined with each other to obtain more powerful
proof techniques, and third, it implies that the up-to function
preserves the greatest fixpoint (a kind of congruence

Let $f \colon L \to L$ be a monotone function and let $u \colon L \to L$ be an
$f$-compatible closure.
Then $\nu f = \nu (f\circ u)$.

$\nu (f \circ u) \sqsubseteq \nu f$ by <cit.>.
$\nu f \sqsubseteq \nu (f \circ u)$ because $u$ is a closure and therefore extensive.

Note that the first inclusion is sufficient to show soundness, but we will later also use the second one to simplify some of the proofs.

This lemma gives rise to the following proof rule:
to show that $l$ is in the behavioural equivalence ($l \sqsubseteq \nu f$),
it is sufficient to show that $l$ is a post-fixpoint of $f \circ u$
(i.e., ), which implies
$l \sqsubseteq \nu(f \circ u) = \nu f$.

If $u_1, u_2$ are $f$-compatible, then $u_1 \circ u_2$ is also $f$-compatible.

Let $f \colon L \to L$ be a monotone function and
let $u \colon L \to L$ be an $f$-compatible closure.
Then $u(\nu f) = \nu f$.

$\nu f \sqsubseteq u(\nu f)$ holds because $u$ is a closure and
therefore extensive.

Since $u$ is $f$-compatible, <cit.> guarantees
$u(\nu f) \sqsubseteq \nu f$.

We will also need the following (straightforward) result.

Let $f \colon L \to L$ be a monotone function,
let $u \colon L \to L$ be an $f$-compatible closure,
and let $l \in L$.
Then, $l \sqsubseteq f(u(l)) \iff u(l) \sqsubseteq f(u(l))$.

$l \sqsubseteq f(u(l)) \Rightarrow u(l) \sqsubseteq f(u(l))$
Since $u$ is monotone, $l \sqsubseteq f(u(l))$ implies $u(l) \sqsubseteq u(f(u(l)))$.
By $f$-compatibility of $u$ ($u \circ f \sqsubseteq f \circ u$),
then also $u(l) \sqsubseteq f(u(u(l)))$,
which by idempotence of $u$ is equivalent to $u(l) \sqsubseteq f(u(l))$.

$l \sqsubseteq f(u(l)) \Leftarrow u(l) \sqsubseteq f(u(l))$
$u$ is extensive, therefore $l \sqsubseteq u(l)$.
Combined, we obtain $l \sqsubseteq u(l) \sqsubseteq f(u(l))$
and hence our desired result.

§.§ Conditional Bisimilarity Up-To Context

We start our investigation of conditional bisimilarity up-to context with the idea of a relation that can be extended to a conditional bisimulation.
To show, using such a conditional bisimulation up-to context $R$, that
a pair of arrows is conditionally bisimilar, it is not in general
necessary to find this pair in $R$, but one can instead extend a pair in $R$ to the pair under review.
As this extension might provide parts of the context that the original condition referred to, it is necessary to shift the associated condition over the extension.

[Conditional bisimulation up-to context (CBUC)]
A conditional relation $R$ is a conditional bisimulation
up-to context if the following holds:
for each triple $(a,b,\mathcal{C}) \in R$ and each context step
$a \cstep{f}{\mathcal A} a^\prime$, there are  steps
$b \cstep{f}{\mathcal{B}_i} b_i^\prime$, $i\in I$, and conditions
$\mathcal{C}_i^\dprime$ such that for each $i\in I$ there exists
$(a_i^\dprime, b_i^\dprime, \mathcal{C}_i^\dprime) \in R$ with
$b_i^\prime = b_i^\dprime;j_i$ for some
arrow $j_i$  and additionally
vice versa for steps $b \cstep{f}{\mathcal B} b'$.

The situation for one answer step is depicted in <Ref>.
The weakest possible $\mathcal A, \mathcal B_i$ can be derived from the rule
conditions as $\mathcal A = \mathcal R_{\downarrow c},\ \mathcal B_i
= {\mathcal R_i}_{\downarrow e_i}$.

(tlempty) at (0,0) $\obnull$;
(i) at (1*,0) $I$;
(trempty) at (2*,0) $\obnull$;
(j) at (0,-1*) $J$;
(k) at (1*,-1*) $K$;
(jp) at (2*,-1*) $J'$;
(blempty) at (0,-2*) $\obnull$;
(ii) at (1*,-2*) $I_i$;
(brempty) at (2*,-2*) $\obnull$;
[->] (tlempty) – node[above]$\ell$ (i);
[->] (trempty) – node[above]$r$ (i);
[->] (trempty) – node[below,pos=0.25]$a^\prime$ (k.30);
[->] (blempty) – node[above]$\ell_i$ (ii);
[->] (brempty) – node[above]$r_i$ (ii);
[->] (brempty) – node[above,pos=0.25]$b_i^\prime$ (k.-30);

[->] (tlempty) – node[left]$a$ (j);
[->] (blempty) – node[left]$b$ (j);
[->] (i) – node[left]$c$ (k);
[->] (ii) – node[left]$e_i$ (k);
[->] (trempty) – node[right]$a_i^\dprime$ (jp);
[->] (brempty) – node[right]$b_i^\dprime$ (jp);

[->] (j) – node[above]$f$ (k);
[->] (jp) – node[above]$j_i$ (k);

[condtri,dart tip angle=60,shape border rotate=270] at (i.north) $\mathcal{R}$;
[condtri,dart tip angle=60,shape border rotate=0] at (j.west) $\kern 0.5mm \mathcal{C}$;
[condtri,dart tip angle=60,shape border rotate=90] at (ii.south) $\kern -0.5mm\mathcal{R}_i\kern -0.5mm$;
[condtri,dart tip angle=60,shape border rotate=180] at (jp.east) $\kern -1mm \mathcal{C}_i^\dprime$;
[rotate around=-20:(k.center),condtri,shape border rotate=270,scale=0.9] at (k.80) $\mathcal{A}$;
[rotate around=20:(k.center),condtri,shape border rotate=90,scale=0.9] at (k.-80) 0pt[1.8pt][1.5pt]$\mathcal{B}_i$;

A single answer step in conditional bisimulation up-to context

Compared to a regular conditional bisimulation, which directly relates
the results of the answering steps
$(a^\prime, b_i^\prime, \mathcal{C}_i^\prime)$, in a CBUC it is
sufficient to relate some pair
$(a_i^\dprime, b_i^\dprime, \mathcal{C}_i^\dprime)$, where
$a_i^\dprime, b_i^\dprime$ are obtained from $a^\prime, b_i^\prime$ by
removing an identical context $j_i$.
(The conditional bisimilarity of the actual successors
$a^\prime, b_i^\prime$ can then be derived by contextualizing the relation, i.e.,
we use <Ref> and refer to a triple in $u(R)$ that is contextualized under $j_i$.)

A CBUC can also be defined based on the closure under contextualization $u$ (see <Ref>,
note that $u$ is easily seen to be a closure[Monotonicity: trivial.
Extensiveness: $(a,b,\mathcal C) \in R$ implies $(a;\id,b;\id,\mathcal C_{\downarrow \id}) = (a,b,\mathcal C) \in u(R)$.
$u \subseteq u \circ u$ by extensiveness and monotonicity,
$u \circ u \subseteq u$ because subsequent contextualization first under $d_1$ then $d_2$ can also be done in a single step of $d_1;d_2$.
A conditional relation $R$ is a CBUC if and only if
$R \subseteq f_C(u(R))$
(i.e. $R$ is a post-fixpoint of $f_C \circ u$).
This can be seen by expanding the definitions of $f_C$ and $u$ on the right-hand side of $(a,b,\mathcal C) \in R \implies (a,b,\mathcal C) \in f_C(u(R))$,
which results in exactly the definition of a CBUC.

We now show that this up-to technique is useful or sound (<Ref>),
that is, all
elements recognized as bisimilar by the up-to technique are actually
bisimilar [31, 28].
In fact, we prove the stronger result that the technique is $f_C$-compatible,
which (as outlined in <Ref>) not only implies soundness,
but also makes it possible to combine our technique with other $f_C$-compatible
up-to techniques.

Let $R$ be a conditional relation. Then it holds that
$u(f_C(R)) \subseteq f_C(R)$. This implies that $u(f_C(R)) \subseteq
f_C(u(R))$, i.e., $u$ is $f_C$-compatible.

We show that $(a,b,\mathcal C) \in u(f_C(R))$ implies $(a,b,\mathcal C) \in f_C(R)$.

Within this proof, we use the following notation:
Given arrows $x,d$, $\pfeilohne{x}{d}$ indicates an arrow such that $x = \pfeilohne{x}{d} ; d$.
Given a condition $\mathcal C$, $\conditionohne{\mathcal C}{d}$ is a condition such that $\mathcal C = (\conditionohne{\mathcal C}{d})_{\downarrow d}$.

* Since $(a,b,\mathcal C) \in u(f_C(R))$,
by definition of $u$ this means that

there exist $d, \pfeilohne{a}{d}, \pfeilohne{b}{d}, \conditionohne{\mathcal C}{d}$
such that $a = \pfeilohne{a}{d};d,\ b = \pfeilohne{b}{d};d,\ \mathcal C = (\conditionohne{\mathcal C}{d})_{\downarrow d}$, and
$(\pfeilohne{a}{d}, \pfeilohne{b}{d}, \conditionohne{\mathcal C}{d}) \in f_C(R)$

* This means that

for all steps $\pfeilohne{a}{d} \cstep{f}{\mathcal A} a'$
there exist answering steps $\pfeilohne{b}{d} \cstep{f}{\mathcal B_i} b_i'$
and conditions $\mathcal C_i'$
such that
$(a', b_i', \mathcal C_i') \in R$
$\mathcal A \land (\conditionohne{\mathcal C}{d})_{\downarrow f}
\models \bigvee\nolimits_{i \in I} (\mathcal C_i' \land \mathcal B_i)$;
vice versa for steps of $\pfeilohne{b}{d}$

* Some of the borrowed contexts $f$ for which this statement holds are of the shape $f = d;f'$, therefore, we also know that

for all steps $\pfeilohne{a}{d} \cstep{d;f'}{\mathcal A} a'$
there exist answering steps $\pfeilohne{b}{d} \cstep{d;f'}{\mathcal B_i} b_i'$
and conditions $\mathcal C_i'$
such that
$(a', b_i', \mathcal C_i') \in R$
$\mathcal A \land (\conditionohne{\mathcal C}{d})_{\downarrow d;f'}
\models \bigvee\nolimits_{i \in I} (\mathcal C_i' \land \mathcal B_i)$;
vice versa for steps of $\pfeilohne{b}{d}$

* Applying <Ref> to this statement, we obtain:

for all steps $\pfeilohne{a}{d};d \cstep{f'}{\mathcal A} a'$
there exist answering steps $\pfeilohne{b}{d};d \cstep{f'}{\mathcal B_i} b_i'$
and conditions $\mathcal C_i'$
such that
$(a', b_i', \mathcal C_i') \in R$
$\mathcal A \land ((\conditionohne{\mathcal C}{d})_{\downarrow d})_{\downarrow f'}
\models \bigvee\nolimits_{i \in I} (\mathcal C_i' \land \mathcal B_i)$;
vice versa for steps of $\pfeilohne{b}{d};d$

* Applying the equalities for the variables annotated with $\pfeilohne{}{d}$ and $\conditionohne{}{d}$, we get:

for all steps $a \cstep{f'}{\mathcal A} a'$
there exist answering steps $b \cstep{f'}{\mathcal B_i} b_i'$
and conditions $\mathcal C_i'$
such that
$(a', b_i', \mathcal C_i') \in R$
$\mathcal A \land (\mathcal C)_{\downarrow f'}
\models \bigvee\nolimits_{i \in I} (\mathcal C_i' \land \mathcal B_i)$;
vice versa for steps of $b$

This is exactly the definition of $(a,b,\mathcal C) \in f_C(R)$.
Therefore, $u(f_C(R)) \subseteq f_C(R)$.

Since $R\subseteq u(R)$ due to extensiveness of $u$, we can infer
$f_C(R) \subseteq f_C(u(R))$ since $f_C$ is monotone. Combined, this
gives us $f_C$-compatibility of $u$.

Note the stronger result ($u(f_C(R)) \subseteq f_C(R)$ instead of just $u(f_C(R)) \subseteq f_C(u(R))$)
can intuitively be explained as follows:
since $f_C$ quantifies over all context steps
and the size of the borrowed context $f$ is not bounded,
this means the successor triples are already closed under contextualization.

From compatibility, we obtain as a corollary that this up-to technique is useful or sound, that is, all
elements recognized as bisimilar by the up-to technique are actually
bisimilar (see <Ref> and [31, 28]).

A conditional relation $R$ satisfies Definition <ref>
(i.e. it is a CBUC) if and only if
its closure under contextualization $u(R)$
is a conditional bisimulation.

$R$ satisfying <Ref> is, by <Ref>,