# Bisimulation maps in presheaf categories

Harsh Beohar  Universität Duisburg-Essen
Duisburg, Germany  Sebastian Küpper  FernUniversität in Hagen
Hagen, Germany

###### Abstract

The category of presheaves on a (small) category is a suitable semantic
universe to study behaviour of various dynamical systems. In particular,
presheaves can be used to record the executions of a system and their
morphisms correspond to simulation maps for various kinds of state-based
systems. In this paper, we introduce a notion of bisimulation maps between
presheaves (or executions) to capture well known behavioural equivalences in
an abstract way. We demonstrate the versatility of this framework by working
out the characterisations for standard bisimulation, $\forall$-fair
bisimulation, and branching bisimulation.

###### keywords:

Presheaves, $\forall$-fair bisimulation, Branching bisimulation.

††volume: MFPS††journal: Electronic Notes in Theoretical Computer Science

Functor====¿ Map—-¿ EmbeddingC-+-¿ MonoC—¿ Epi—-¿¿ Openo—¿¿ Closedtriangle—¿
Iso===== AllMap….¿ AllEmbeddingC.+.¿ AllMonoC…¿ AllEpi….¿¿ AllOpeno…¿¿
AllClosedtriangle…¿ ExistMapdashdashdash¿ ExistEmbeddingCdash+dash¿
ExistMonoCdashdash¿ ExistEpidashdashdash¿¿ ExistOpenodashdash¿¿

††thanks: Email<EMAIL_ADDRESS>Email:
<EMAIL_ADDRESS>
##  1 Introduction

The importance of formal semantics should not be underestimated, especially
when aimning to design _reliable_ dynamical systems in heterogeneous
environments. Therefore, a variety of state based modelling frameworks at
different levels of abstraction have been proposed; to quote Goguen [16]: _one
person’s syntax is another person’s semantics_. Diversity in algorithms can be
desirable; however, as argued in [16, 1, 34], the proliferation of semantic
theories indicates our scattered understanding of concurrent systems. Thus, we
seek a framework that provides semantic structure describing the behaviour of
a dynamical system and its refinement independently of syntax.

This goal is shared to an extent by the theory of coalgebras [29]. In [6], we
abandoned state-based modelling in favour of describing behaviour as the set
of executions (inspired by [10, 28]) because the branching structure of a
state in the presence of invisible actions is described by the set of
executions (not states). This situation further escalates when one is
interested in infinite executions (e.g. fairness properties [17, 25]) or dense
executions which are omnipresent in hybrid systems (e.g. [12]). The point is
not that executions are inexpressible in a coalgebra, but rather that we need
a semantic framework where they are treated as first-class citizens just as
states are in a coalgebraic framework. Thus, our hypothesis is that behaviour
of a system is given solely by its executions.

We anticipate presheaves to be the “right” semantic structure to study
executions without fixing a kind of dynamical system. Note that we are _not_
the first in proposing presheaves as the mathematical universe to studying
behaviour. Winskel and his colleagues [34, 8, 19, 23, 15] have already
employed presheaves (among other things) by giving a denotational semantics of
process-algebraic terms supported by characterisations of strong bisimulation
and weak bisimulation relations using open maps in the context of transition
systems. For a more modern treatment, Hirschowitz and his colleagues [13, 14,
20] advocated game semantics using (pre)sheaves.

The novelty of our work lies in refining the notion of open maps (which we
christened _bisimulation maps_) in a presheaf category and using it to
characterise $\forall$-fair bisimulation [24, 18] and branching bisimulation
[33] relations. In addition, the prospect of having to specify notions of time
and observation (which was absent in the earlier works on presheaf semantics)
leads to a clearer modelling, so explicitly highlighting these two dimensions
of system modelling is at the core of our contribution (cf. Section 2). This
distinction was in turn essential to capture branching bisimulation in the
presence of invisible actions $\tau$.

Interestingly, unlike open maps, bisimulation maps are always retracts in the
category of presheaves (in turn, they are surjective at the level of
executions). As a slogan, presheaf maps are refinement maps, while
bisimulation maps (which are special presheaf maps) are complete refinement
maps (Section 3). By moving to a finer notion, we are still able to capture
functional bisimulations without fairness. However, in the context of
fairness, we can show (Theorem 4.10) that the behavioural equivalence induced
by a bisimulation map coincides with $\forall$-fair bisimulation relation.
Note that our $\forall$-fair bisimulations are equivalence relations by
definition in contrast to the existing definition [24, 18] (see the dicussion
after Theorem 4.10 on Page 4.10). This is an improvement with respect to the
previous characterisation of $\exists$-fair bisimulation [24, 18] (called
_extended bisimulation_ in [17]) obtained by Hildebrandt [19] using open maps,
since any $\forall$-fair bisimulation relation is strictly finer than an
$\exists$-fair bisimulation relation [18] and our correspondence does not
impose any restrictions on the fairness predicates. These restrictions,
originally from [17], asserted that fairness predicates on infinite executions
are closed under the removal and the addition of finite prefixes.

Another practical aspect of the theory of presheaves is that it guides us in
finding the right semantic categories once a notion of time and observation is
fixed. Moreover, we can apply concepts (like, e.g., essential geometric
morphism [27]) that transform a dynamical system from one observation space
$\mathcal{O}$ to another space $\mathcal{O}^{\prime}$. This way we can
transform (see Section 5) a presheaf of executions (induced by a given
transition system) into a presheaf of minimal executions (i.e., executions in
which trailing $\tau$-transitions are chopped off). This property is specific
to branching bisimulation, which may be the reason why this construction was
not discussed in [15] (their objective was to capture weak bisimulation).

#### Organisation of the paper.

In Section 2, we introduce our mathematical framework to model behaviour of a
dynamical system with a special focus on the aspects of time and observation.
Then, we introduce the notion of bisimulation maps in presheaves on an
arbitrary (small) category in Section 3. Turning our attention towards the
first major example, we characterise $\forall$-fair bisimulation relations in
Section 4. The case of invisible actions in Section 5 is based on a change of
observation space. We first outline an obvious (but ultimately failed) attempt
to capture branching bisimulation, before giving the correct (yet intuitive)
construction that characterises branching bisimulation.

##  2 Our universe of discourse

The objective of this section is to describe our semantic framework in which
one can model behaviour of a dynamical system. By _behaviour_ of a dynamical
system, we understand some _phenomena that evolve over time_. Our aim is to
formalise this intuition. We begin by modelling time as a small category
$\mathbf{T}$, whose objects are points in time and arrows describe passing of
time.

###### Notation

An object $C$ (an arrow $f$) of a category $\mathbf{C}$ will be denoted by the
predicate $C\in\mathbf{C}$ ($f\in\mathbf{C}$). Moreover, the codomain and
domain of an arrow $f\in\mathbf{C}$ are denoted as $\text{cod}(f)$ and
$\text{dom}(f)$, respectively.

Invariably, dynamical systems come with a notion of observation. For instance,
a letter from a fixed alphabet may denote the assignment of model variables in
a computer program/controller. We assume that a system under study has a
display unit together with the existence of a hypothetical ‘observer’
$\mathcal{O}$ who is watching/measuring behaviour of the system using this
display unit over time. In addition, our observer $\mathcal{O}$ can remember
its observations over time, i.e., earlier observations can be deduced from the
later observations. Mathematically, this amounts to saying that $\mathcal{O}$
is a contravariant functor $\mathbf{T}\rTo\mathbf{Set}$.

######  Proposition 2.1.

Let $\mathbf{C}$ be a small category. Then, the collection of functors of type
${\mathbf{C}}^{\text{op}}\rTo\mathbf{Set}$ (i.e., presheaves on a category
$\mathbf{C}$) and natural transformations between them form a category
$\mathbf{PSh}(\mathbf{C})$.

###### Notation 1

Given a presheaf $F\in\mathbf{PSh}(\mathbf{C})$, we follow [27] in writing
$x\cdot f$ to denote the restriction of $x\in FC$ along $C^{\prime}\rTo^{f}C$,
i.e., $Ff(x)=x\cdot f$. In case $\mathbf{C}$ is a poset (viewed as a category)
$\mathbf{C}$, we write $x\cdot C^{\prime}$ to denote the restriction of $x\in
FC$ along $C^{\prime}\preceq C$. Note that we use calligraphic letters for
specific presheaves, whereas arbitrary ones are denoted by capital letters as
above.

######  Example 2.2.

In this example, we fix the notion of time $\mathbf{T}$ and observation
$\mathcal{O}$ associated with a (labelled) transition system. For time
$\mathbf{T}$ we take the set of natural numbers ${\rm Nature}$ viewed as a
category (arrows are the less-than-equal-to relations). For the given alphabet
$A$, we now define a presheaf $\mathcal{A}\in\mathbf{PSh}({\rm Nature})$:

$\mathcal{A}(n)=\\{\sigma\in{A}^{\star}\mid|\sigma|=n\\}\qquad\text{(for every
$n\in{\rm Nature}$),}$

together with the action on $\mathcal{A}$ given by $\sigma\cdot n=\sigma|_{n}$
(for every $\sigma\in\mathcal{A}(n^{\prime})$ and $n\leq n^{\prime}$). In
other words, $\mathcal{A}(n)$ is the set of those finite words
$\sigma\in{A}^{\star}$ whose length is $n$ (denoted by $|\sigma|=n$), while
the action $\\_\cdot n$ simply maps a word $\sigma$ of length $n^{\prime}$ to
its unique prefix of length $n$ (denoted by $\sigma|_{n}$). Note that
$\mathcal{A}(0)$ is a singleton set containing the empty word which we denote
by $\varepsilon$.

######  Remark 2.3.

In modelling some dynamical systems, like, e.g., those arising from control
theory [28], $\mathcal{O}$ may have even more structure in that global
observations can be constructed by gluing the local observations (smaller
neighbourhoods). In such situations, the category of sheaves
$\mathbf{Sh}(\mathbf{C},J)$ equipped with a Grothendieck topology $J$ on
$\mathbf{C}$ is more suitable (cf. [30]) for semantic purposes. Moreover,
sheaves equipped with discrete Grothendieck topology are exactly presheaves
(cf. [27]), so our mathematical universe is actually the category of sheaves
(rather than presheaves). But due to the discrete nature of dynamical systems
considered in this paper, we restrict ourselves to presheaves. Nevertheless,
we will state our definitions so that they are applicable on sheaves (see,
e.g., Remark 3.2).

Once a notion of time $\mathbf{T}$ and an observation
$\mathcal{O}\in\mathbf{PSh}(\mathbf{T})$ is fixed, then a system essentially
describes the _runs_ (also known as _trajectories_ or _executions_) of the
system and the observation associated with each run. To answer both, we
envisage that a dynamical system is nothing but an object in the slice
category $\mathbf{PSh}(\mathbf{C})/\mathcal{O}$. In other words, a dynamical
system corresponds to a presheaf $F$ modelling the runs of the system and a
natural transformation $F\rTo^{\alpha}\mathcal{O}$ modelling the observation
associated with each run of the system. More importantly, a _system
homomorphism_ $\varphi$ between two systems $(F,\alpha)$ and $(G,\beta)$,
denoted $(F,\alpha)\rTo^{\varphi}(G,\beta)$, is a natural transformation
$F\rTo^{\varphi}G$ preserving the observations, i.e.,
$\beta\circ\varphi=\alpha$. Intuitively, a system homomorphism
$(F,\alpha)\rTo^{\varphi}(G,\beta)$ says that the system $(F,\alpha)$ is a
_refinement_ of $(G,\beta)$ (i.e., every observable behaviour of $F$ is also
part of the observable behaviour of $G$).

###  2.1 Refining our framework by unifying time and observation

Although the slice category $\mathbf{PSh}(\mathbf{T})/\mathcal{O}$ is close to
our system theoretic intuition, its presentation can be further simplified.
Recall the _category of elements_ of a presheaf
$F\in\mathbf{PSh}(\mathbf{C})$, denoted $\mathbb{E}_{\mathbf{C}}(F)$ (we drop
the subscript $\mathbf{C}$ whenever clear from the context), has as objects
the tuples $(x,C)$ with $C\in\mathbf{C},x\in FC$ and as arrows
$(x,C)\rTo^{f}(x^{\prime},C^{\prime})$ the morphism
$C\rTo^{f}C^{\prime}\in\mathbf{C}$ such that $x^{\prime}\cdot f=x$.

######  Theorem 2.4 ([27, Exercise III.8(a)]).

For a presheaf $F$ over a small category $\mathbf{C}$, there is an equivalence
of categories $\mathbf{PSh}(\mathbf{C})/F\cong\mathbf{PSh}(\mathbb{E}(F))$.

Note that a similar result also holds in the setting of sheaves (cf. [27,
Exercise III.8(b)]).

In other words, time can be made inherent with observation and, thus, we can
work in a simpler setting without worrying about the bookkeeping associated
with slice categories. To see this, recall Example 2.2 and the poset of finite
words ${A}^{\star}$ (a.k.a. free monoid) generated by a set $A$, which is
ordered by the prefix relation $\preceq\
\subseteq{A}^{\star}\times{A}^{\star}$. Notice that the categories
$\mathbb{E}(\mathcal{A})$ and ${A}^{\star}$ are isomorphic: since the length
of a word is redundant in the objects of $\mathbb{E}(\mathcal{A})$ dropping
the length results in the elements of ${A}^{\star}$. Thus, we obtain

######  Corollary 2.5.

There is an equivalence of categories $\mathbf{PSh}({\rm
Nature})/\mathcal{A}\cong\mathbf{PSh}({A}^{\star})$.

As a result, the category of presheaves on ${A}^{\star}$ can serve as the
semantic universe to study behaviour of a transition system (cf. Example 2.6).
More generally, by giving the semantics to a ‘syntactic’ category of a
computational model $\mathbf{M}$, we mean identifying the notion of time
$\mathbf{T}$ and observation $\mathcal{O}\in\mathbf{PSh}(\mathbf{T})$ together
with a faithful functor
$\mathbf{M}\rTo^{\llbracket\\_\rrbracket}\mathbf{PSh}(\mathbb{E}_{\mathbf{T}}(\mathcal{O}))$,
called the _semantics_ functor. By interpreting an arrow $M\rTo^{f}M^{\prime}$
in $\mathbf{M}$ as _$M$ is an implementation of $M^{\prime}$ witnessed by
$f$_, then faithfulness of $\llbracket\\_\rrbracket$ asserts: if an
implementation is witnessed by two semantically same morphisms $\llbracket
f\rrbracket=\llbracket g\rrbracket$, then $f=g$ must be the same
syntactically.

######  Example 2.6.

Consider a transition system $(X,A,\rightarrow)$ where $X$ is the set of
states, $A$ is the set of actions, and $\rightarrow\subseteq X\times A\times
X$ is the transition relation111Transition systems without initial states are
standard in process algebraic literature (see [3]).. Then the collection of
transition systems together with simulation functions form a category denoted
$\mathbf{LTS}$. Note that a _simulation function_ is a function $X\rTo^{f}Y$
satisfying:

$\forall_{x,x^{\prime}\in X,a\in A}\ x$ (1)

As usual, we write $x$ to denote $(x,a,x^{\prime})\in\rightarrow$. Let
$\downarrow\sigma=\\{\sigma^{\prime}\in{A}^{\star}\mid\sigma^{\prime}\preceq\sigma\\}$
be the prefixes of $\sigma$. Next, define a presheaf $\llbracket
X\rrbracket\in\mathbf{PSh}({A}^{\star})$ which records all the executions
whose trace is $\sigma$ at $\llbracket X\rrbracket(\sigma)$:

$\displaystyle\llbracket X\rrbracket(\sigma)=$ $\displaystyle\
\left\\{\downarrow\sigma\rTo^{p}X\mid\forall_{\sigma^{\prime},a}\
\big{(}\sigma^{\prime}a\preceq\sigma\implies p(\sigma^{\prime})\right\\},$
$\displaystyle p\cdot\sigma^{\prime}=$ $\displaystyle\
p_{\downarrow\sigma^{\prime}}\quad\text{\big{(}for any
$\sigma^{\prime}\preceq\sigma$ and $p\in\llbracket
X\rrbracket(\sigma)$\big{)}}.$

Moreover, any function $X\rTo^{f}Y$ induces a family of maps $\llbracket
f\rrbracket_{\sigma}(p)=f\circ p$ (for each $\sigma\in{A}^{\star}$).

Thus, we obtain the following result; wherein, the result that presheaf maps
encode simulation maps is well known from the early work of Joyal et al. in
[23].

######  Proposition 2.11.

The map $\llbracket\\_\rrbracket$ defined in Example 2.6 is a faithful
functor. Moreover,

  * •

if $\llbracket f\rrbracket$ is a presheaf map for any $f\in\mathbf{LTS}$, then
$f$ is a simulation function.

  * •

if a function $f$ between the underlying state spaces induces a presheaf map
$\llbracket f\rrbracket$, then $f$ is a simulation map.

As a result, the category of transition systems $\mathbf{LTS}$ has presheaf
semantics on ${A}^{\star}$. In the subsequent sections, we will show the
applicability of our semantic framework by giving presheaf semantics to
different computational models; namely, transition systems with fairness
predicates and invisible transitions.

##  3 Bisimulation maps: towards complete refinement

Consider a category of computational models $\mathbf{M}$ together with its
semantics over a presheaf category $\mathbf{PSh}(\mathbf{C})$, i.e.,
$\mathbf{M}\rTo^{\llbracket\\_\rrbracket}\mathbf{PSh}(\mathbf{C})$. As
mentioned earlier, an arrow between any two images of the semantics functor as
a refinement map from the modelling point of view. In particular, we interpret
$\llbracket M\rrbracket\rTo^{\llbracket f\rrbracket}\llbracket
M^{\prime}\rrbracket$ (induced by an arrow $M\rTo^{f}M^{\prime}\in\mathbf{M}$)
as the information that $\llbracket M\rrbracket$ is an implementation of
$\llbracket M^{\prime}\rrbracket$ witnessed by the refinement map $\llbracket
f\rrbracket$. Note that this is a straightforward generalisation of
Proposition 2.11 since simulation maps encode the refinement of behaviour in
the case of labelled transition systems. Therefore, to study bisimulation maps
at the level of presheaves (executions), we will restrict ourselves to those
presheaf morphisms that represent ‘complete’ refinement of behaviour in the
following sense. Theorem 3.3 expresses this in a more formal manner.

  * •

Every observable behaviour in $\llbracket M^{\prime}\rrbracket$ is also
observable in $\llbracket M\rrbracket$ (thus, $\llbracket M\rrbracket$ is a
refinement of $\llbracket M^{\prime}\rrbracket$).

  * •

Moreover, every observable behaviour in $\llbracket M\rrbracket$ can be
retracted onto an observable behaviour in $\llbracket M^{\prime}\rrbracket$.

One possibility is to use the open maps of Joyal et al. [23], which gave a
unified definition of functional bisimulations over the range of computational
models. In particular, when invoked in a presheaf category, open maps
correspond to natural transformations whose naturality squares are the weak-
pullback squares in $\mathbf{Set}$ (see [8, Proposition 2.3]). Nevertheless,
an open map falls short in capturing the complete refinement point of view
since an arbitrary open map may not even be a surjective map at the level of
executions; i.e., our implementation may not even implement or cover all the
behaviour present in the specification.

In [5], open maps [23] were refined to embedding-open maps in the setting of
concrete categories. An important difference to the classical definition of
open maps is that the parametric notion of path extensions can be replaced by
embeddings (see [2, Definition 8.6(2)] for a formal definition). Moreover,
embedding-open maps are always retracts under some mild restrictions on
concrete categories (cf. [5]). Now, if a category is concrete over itself,
then an embedding corresponds to simply a monomorphism. Consequently, we
propose the following definition of an embedding-open map, which we simply
call a _bisimulation_ map.

######  Definition 3.1.

A map $F\rTo^{f}G\in\mathbf{PSh}(\mathbf{C})$ is a _bisimulation_ if, and only
if, for every commutative square depicted in (LABEL:eq:bisim-presheaf) with a
mono $P\rMono^{g}Q$ and maps $m,n$ in $\mathbf{PSh}(\mathbf{C})$, there is a
map $Q\rTo^{k}F\in\mathbf{PSh}(\mathbf{C})$ such that the two triangles
commute, i.e., $k\circ g=m$ and $f\circ k=n$.

Intuitively, (LABEL:eq:bisim-presheaf) states that every extension of
behaviour observable in $G$ can be reflected as an extension observable in $F$
through the witnesser $f$.

######  Remark 3.2.

It is interesting to note that a similar definition for sheaves can be derived
from the definition of embedding-open maps as given in [5]. First, note that
$\mathbf{Sh}(\mathbf{C},J)$ is concrete over $\mathbf{PSh}(\mathbf{C})$ due to
the forgetful functor $\mathfrak{i}$, which is fully faithful. Moreover,
embeddings in this concrete category are actually monomorphisms. This is
because any mono is a regular mono in $\mathbf{Sh}(\mathbf{C},J)$ and the
faithful functor $\mathfrak{i}$ preserves regular monos (since $\mathfrak{i}$
is right adjoint to the associated sheaf functor $\mathfrak{a}$ [27]). Lastly,
every regular mono is an embedding whenever the faithful functor preserves
regular monos [2, Proposition 8.7.3]. Thus, we have the exact same definition
of bisimulation maps in $\mathbf{Sh}(\mathbf{C},J)$.

######  Theorem 3.3.

Every bisimulation map in a (pre)sheaf category is a retract.

We end this section by capturing functional bisimulations in terms of
bisimulation maps whose proof can be extracted from the proof of Theorem 4.5.
Note that a similar theorem was proven earlier in the seminal paper [23] for
functional bisimulation; however, the difference is that we use bisimulation
maps (not open maps) in our characterisation.

######  Theorem 3.4.

Given a simulation function $X\rTo^{f}Y$, then $\llbracket f\rrbracket$ is a
bisimulation map in $\mathbf{PSh}({A}^{\star})$ if, and only if, the function
$f$ is a surjection satisfying:

$\forall_{x\in X,y\in Y}\ \big{(}f(x)$ (2)

##  4 The case of fairness

When considering infinite, rather than finite, behaviour of systems, it is
common to take fairness into account. There are various notions of fairness
[18] but the general idea for fair (bi)simulation is to demand that fair
executions are matched by fair executions, in addition to classical
(bi)simulation properties. In this section, we give a presheaf semantics to
fair transition systems and outline how $\forall$-fair bisimulation can be
captured via bisimulation maps.

Let ${A}^{\omega}=\\{\sigma\mid{\rm Nature}\rTo^{\sigma}A\\}$ be the set of
infinite words generated from $A$ and fix
${A}^{\infty}={A}^{\star}\cup{A}^{\omega}$, which is ordered by the prefix
relation $\preceq$. The object of study are _fair transition system_ s
$(X,A,\rightarrow,\text{Fair}_{X})$, where $(X,A,\rightarrow)$ is a transition
system and $\text{Fair}_{X}$ is a fairness predicate on infinite executions.
An _infinite execution_ is a function
$\downarrow\sigma\rTo^{p}X\cup\\{\Omega\\}$ whose domain is the history of an
infinite word $\sigma\in{A}^{\omega}$ such that $p(\sigma)=\Omega$ and
$\forall_{\sigma^{\prime},a}\ (\sigma^{\prime}a\prec\sigma\implies
p(\sigma^{\prime})$. Here, $\Omega$ is the _chaos_ state which the system
enters once it has executed an infinite execution. Let
$\text{FExec}(X)=\text{Fair}_{X}\cup\text{Exec}(X)$ be the set of all fair
executions ordered by the prefix relation $\preceq$, i.e., $p\preceq
p^{\prime}\iff p^{\prime}|_{\text{dom}(p)}=p$ (for
$p,p^{\prime}\in\text{FExec}(X)$). The set of (finite) executions
$\text{Exec}(X)$ is defined as earlier, i.e.,
$\text{Exec}(X)=\\{\downarrow\sigma\rTo^{p}X\mid\sigma\in{A}^{\star}\wedge\forall_{\sigma^{\prime}a\in\downarrow\sigma}\
p(\sigma^{\prime})$.

######  Definition 4.3.

A chaos preserving extension
$X\cup\\{\Omega\\}\rTo^{f_{\Omega}}Y\cup\\{\Omega\\}$ (i.e.,
$f_{\Omega}(x)=f(x)$ for $x\in X$ and $f_{\Omega}(\Omega)=\Omega$) of a
function $X\rTo^{f}Y$ is a _fair simulation_ between
$(X,A,\rightarrow,\text{Fair}_{X}),(Y,A,\rightarrow,\text{Fair}_{Y})$ if, and
only if, $f$ satisfies (1) and $\forall_{p\in\text{Fair}_{X}}\ f_{\Omega}\circ
p\in\text{Fair}_{Y}$. Henceforth, we do not distinguish between $f_{\Omega}$
and $f$.

Note that an infinite, but fair, execution can be seen as the limit of a
monotonically increasing sequence of finite executions in $\text{FExec}(X)$.
Since this limiting sequence is part of behaviour, we should reflect it. Thus,
we say a _fair bisimulation_ $X\cup\\{\Omega\\}\rTo^{f}Y\cup\\{\Omega\\}$ is a
surjective fair simulation $f$ satisfying (2) and the following condition for
any increasing sequence of finite executions $(p_{i})_{i\in{\rm Nature}}$ in
$X$:

$\bigsqcup_{i\in{\rm Nature}}f\circ p_{i}\approx f\circ\bigsqcup_{i\in{\rm
Nature}}p_{i}.$ (3)

Here, $\approx$ is the Kleene equality used to equate the partially defined
terms above.

To the best of our knowledge, the above notion of fair bisimulation is novel;
however, below we will establish its connection with the literature after
characterising it in terms of presheaf morphisms. So let $\mathbf{FTS}$ be the
category of fair transition systems and fair simulation between them. In
addition,

  * •

Time: Since infinite executions are allowed in a fair transition system, we
take $\mathbf{T}={\rm Nature}\cup\\{\infty\\}$ to be the category of natural
numbers extended by a number representing infinity (i.e., $\forall_{n\in{\rm
Nature}}\ n\leq\infty$).

  * •

Observation: Using the definition of $\mathcal{A}$ in Example 2.2, we define:
$\mathcal{O}(\infty)={A}^{\omega}$ and $\mathcal{O}(n)=\mathcal{A}(n)$ (for
$n\in{\rm Nature}$).

Clearly, the categories $\mathbb{E}(\mathcal{O})$ and ${A}^{\infty}$ are
isomorphic and by applying Theorem 2.4 we obtain
$\mathbf{PSh}(\mathbb{E}(\mathcal{O}))\cong\mathbf{PSh}({A}^{\infty})$. So, we
take the category $\mathbf{PSh}({A}^{\infty})$ as the semantic universe to
study fair transition systems. Just as in Example 2.6, for a given fair
transition system $(X,A,\rightarrow,\text{Fair}_{X})$, we define a presheaf

$\llbracket
X\rrbracket(\sigma)=\left\\{p\in\text{FExec}(X)\mid\max\text{dom}(p)=\sigma\right\\}\quad(\text{for
each $\sigma\in{A}^{\infty}$}),$

and the action is given by restricting the domain of an execution. Moreover,
for any fair simulation function $f$, we let $\llbracket
f\rrbracket_{\sigma}=f\circ\\_$ (for each $\sigma\in{A}^{\infty}$); thus,
resulting in a presheaf semantics to fair transition systems.

######  Proposition 4.4.

The above map
$\mathbf{FTS}\rTo^{\llbracket\\_\rrbracket}\mathbf{PSh}({A}^{\infty})$ is a
faithful functor.

Invoking the bisimulation map definition between any two presheaves generated
by fair transition systems results in the characterisation of fair
bisimulation.

######  Theorem 4.5.

A fair simulation function $f$ is a fair bisimulation if, and only if, the
underlying map $\llbracket f\rrbracket$ is a bisimulation map in
$\mathbf{PSh}({A}^{\infty})$.

Remark 2. It should be noted that fair bisimulation maps are stronger than the
open maps studied by Hildebrandt [19] in $\mathbf{PSh}({A}^{\infty})$ to
characterise the extended bisimulation of Hennessy and Stirling [17] for
pointed systems, i.e. systems with explicitly initial states. To demonstrate
this, recall that an $\text{Inf}_{\bot}$-open map of Hildebrandt [19,
Proposition 25] is a fair simulation function (not necessarily surjective)
$X\cup\\{\Omega\\}\rTo^{f}Y\cup\\{\Omega\\}$ satisfying (2) and the property:

$\forall_{x\in X,q\in\text{FExec}(Y)}\
\big{(}q(\varepsilon)=f(x)\implies\exists_{p\in\text{FExec}(X)}\
(p(\varepsilon)=x\land f\circ p=q)\big{)}.$ (4)

Consider the two systems drawn on the right with a function $f$ between the
states depicted by dashed lines.

$x$$x^{\prime}$$y$$a$$a$$a$$a$

In the left system, the infinite executions visiting $x^{\prime}$ infinitely
often are considered fair, whereas the only infinite execution in the right
system is fair. Clearly, $f$ is a fair simulation satisfying (4). But $f$ is
_not_ a fair bisimulation because the sequence of finite executions
$(p_{i})_{i\in{\rm Nature}}$ formed by unfolding the self-loop on $x$ has a
fair execution $\bigsqcup_{i\in{\rm Nature}}f\circ p_{i}$ (looping on $y$) as
the limit in the right system. Yet, $(p_{i})_{i\in{\rm Nature}}$ has no limit,
thus, violating (3).

######  Remark 4.6.

In [19], (separated) presheaves with sup topology are used because an
increasing sequence of finite executions induced by a fair transition system
has at most one limit point. Unlike [19], we are not interested in one-to-one
semantic representation of our syntactical models, so we work with arbitrary
presheaves. This is because the choice whether the semantic universe should be
(separated) presheaves or sheaves depends on observations, i.e., how
$\mathcal{O}$ is modelled. This is also why we do _not_ require our semantic
functor $\llbracket\\_\rrbracket$ to be full.

Next, we relate fair bisimulation maps with $\forall$-fair bisimulation
relations.

######  Definition 4.7.

A _$\forall$ -fair bisimulation_ on $(X,A,\rightarrow,\text{Fair}_{X})$ is an
equivalence relation $\mathcal{R}\subseteq X\times X$ satisfying the following
transfer properties:

  1. (1)

$\forall_{x,y,x^{\prime},a}\ \big{(}(x$, and

  2. (2)

$\forall_{p,q}\ \big{(}(p=_{\mathcal{R}}q\land p\in\text{Fair}_{X})\implies
q\in\text{Fair}_{X}\big{)}$.

Here, $p=_{\mathcal{R}}q$ is an abbreviation for
$\text{dom}(q)=\text{dom}(p)\land\forall_{\sigma\in\text{dom}(p)\cap{A}^{\star}}\
p(\sigma)\mathcal{R}q(\sigma)$.

######  Theorem 4.10.

Two states $x$ and $x^{\prime}$ are related by a $\forall$-fair bisimulation
relation if, and only if, there is a fair bisimulation function $f$ such that
$f(x)=f(x^{\prime})$.

The requirement of equivalence relations in the above definition may look
superfluous at first glance. This is because, traditionally (i.e., when
fairness predicates are empty sets), a strong bisimulation relation by
definition is not necessarily an equivalence relation on the set of states.
Moreover, _bisimilarity_ which is defined as the union of all strong
bisimulation relations turns out to be both an equivalence relation and a
strong bisimulation relation. However, such closure results do not hold in
general for $\forall$-fair bisimulation relations. $\forall$-fair bisimulation
relations are not closed under union and the relational composition (even if
we relax Definition 4.7 by replacing ‘an equivalence relation’ for ‘a
symmetric relation’)222This is how $\forall$-fair bisimulation relations are
defined in [24] on the states of Kripke structures. In regards to the above
closure properties, we are only aware of [21] who showed that $\forall$-fair
simulation relations are not closed under union.. Thus, $\forall$-fair
bisimilarity may, in general, neither be an equivalence relation nor a
$\forall$-fair bisimulation; in other words, $\forall$-fair bisimilarity is
not a coinductive definition (like how strong bisimilarity is). Nevertheless,
we deemed all $\forall$-fair bisimulation relations to be equivalences
because: first, the main use of a $\forall$-fair bisimulation relation is to
equate two systems that have the same behaviour sensitive to fair executions;
second, the mathematics tells us that the kernel of a (fair bisimulation)
function is an equivalence relation.

##  5 The case of invisible actions

The behaviour of a specification and its implementation is often spread over
different levels of abstraction. The standard process algebraic way to relate
the behaviour of an implementation with its specification is by delineating
the effect of actions in lower levels of abstraction as invisible. For
instance, removing a message from a buffer is considered unobservable in a
rendezvous between communicating processes. This is made formal by
reinterpreting the notion of (bi)simulation functions in the presence of the
invisible action $\tau$.

###  5.1 Branching bisimulation

###### Notation 3

Henceforth, $\tau\not\in A$ will denote the invisible action and
$A_{\tau}=A\cup\\{\tau\\}$. Furthermore, $\text{Exec}(X,\sigma)$ is the set of
executions $p$ having trace $\sigma$, i.e., $\max\text{dom}(p)=\sigma$ and
$\ext@arrow 0359\arrowfill@\relbar\relbar\twoheadrightarrow{}{}{}\subseteq
X\times{A}^{\star}\times X$ is the _weak reachability_ relation on
$(X,A_{\tau},\rightarrow)$ given as the smallest relation satisfying the
following conditions:

$\frac{}{x\ext@arrow
0359\arrowfill@\relbar\relbar\twoheadrightarrow{}{\varepsilon}{}x}\qquad\frac{x\step\tau
x^{\prime}}{x\ext@arrow
0359\arrowfill@\relbar\relbar\twoheadrightarrow{}{\varepsilon}{}x^{\prime}}\qquad\frac{x\ext@arrow
0359\arrowfill@\relbar\relbar\twoheadrightarrow{}{\varepsilon}{}x^{\prime}\wedge
x^{\prime}\ext@arrow
0359\arrowfill@\relbar\relbar\twoheadrightarrow{}{\varepsilon}{}x^{\prime\prime}}{x\ext@arrow
0359\arrowfill@\relbar\relbar\twoheadrightarrow{}{\varepsilon}{}x^{\prime\prime}}\qquad\frac{x\ext@arrow
0359\arrowfill@\relbar\relbar\twoheadrightarrow{}{\sigma}{}x^{\prime}\land
x^{\prime}\step ax^{\prime\prime}}{x\ext@arrow
0359\arrowfill@\relbar\relbar\twoheadrightarrow{}{\sigma
a}{}x^{\prime\prime}}.$

######  Definition 5.3.

A _branching simulation_ function $f$ between systems
$(X,A_{\tau},\rightarrow)$ and $(Y,A_{\tau},\rightarrow)$ is a function
$X\rTo^{f}Y$ satisfying the following properties:

  1. (1)

Simulation of observable transitions, i.e., $\forall_{x,x^{\prime}\in X,a\in
A}\ x$, and

  2. (2)

(Possible) simulation of invisible transitions, i.e.,
$\forall_{x,x^{\prime}\in X}\ x$.

  3. (3)

Stuttering of $\tau$-transitions, i.e., for any $x_{1},x_{2},x_{3}$ we have

$\big{(}x_{1}\ext@arrow
0359\arrowfill@\relbar\relbar\twoheadrightarrow{}{\varepsilon}{}x_{2}\ext@arrow
0359\arrowfill@\relbar\relbar\twoheadrightarrow{}{\varepsilon}{}x_{3}\land
f(x_{1})=f(x_{3})\big{)}\implies f(x_{1})=f(x_{2}).$ (5)

A _branching bisimulation_ $f$ is a branching simulation surjection $f$
satisfying the ‘weak’ reflection of transitions, i.e., for any $x\in X,y\in
Y$, and $a\in A_{\tau}$ we have

$f(x)$ (6)

######  Definition 5.10.

Given a labelled transition system $(X,A_{\tau},\rightarrow)$, then a
symmetric relation $\mathcal{R}\subseteq X\times X$ is a _branching
bisimulation_ [33] if, and only if, the following transfer property is
satisfied

$\forall_{x_{1},x_{2},y_{1},a\in A_{\tau}}\Big{(}(x_{1}$

Two states $x,x^{\prime}\in X$ are branching bisimilar if there exists a
branching bisimulation $\mathcal{R}$ such that $x\mathcal{R}x^{\prime}$.

We work with branching bisimulation functions (not relations) because of the
following result (Theorem 5.13), which is similar in spirit to Lemma 2.7
proved by Caucal in [9]. The difference is that Caucal’s branching
bisimulation functions (which he calls _reduction_ in [9]) do not respect the
stuttering of invisible steps (5). Nevertheless, we are still able to obtain
the following correspondence since the largest branching bisimulation relation
satisfies the so-called _stuttering lemma_ of [33]. In particular, any
reduction $X\rTo^{f}Y$ in the sense of Caucal can be extended to a branching
bisimulation function by composing it with the quotient map
$Y\rTo^{q}Y/\mathcal{R}$, where $\mathcal{R}\subseteq Y\times Y$ is the
largest branching bisimulation relation on $Y$.

######  Theorem 5.13.

Two states $x,x^{\prime}\in X$ of a transition system
$(X,A_{\tau},\rightarrow)$ are branching bisimilar if, and only if, there are
a transition system $(Y,A_{\tau},\rightarrow)$ and a branching bisimulation
function $X\rTo^{f}Y$ such that $fx=fx^{\prime}$.

###  5.2 The setup

Our first step towards the characterisation of branching bisimulation is the
presheaf representation of executions induced by a transition system with
invisible actions. Since a transition system evolves in a step-based manner,
it is sufficient to model the time by the set of natural numbers ${\rm
Nature}$. The only difference, when compared to the strong case (cf. Example
2.2), is in the notion of observation. Instead of recording words from
${A}^{\star}$, our hypothetical ‘observer’ now records words from
${A}^{\star}_{\tau}$. So, consider a presheaf ${{\rm
Nature}}^{\text{op}}\rTo^{\mathcal{A}_{\tau}}\mathbf{Set}$ in the spirit of
$\mathcal{A}$ as defined in Example 2.2. Recall that the slice category
$\mathbf{PSh}({\rm Nature})/\mathcal{A}_{\tau}$ is equivalent to the category
of presheaves on the category of elements $\mathbb{E}(\mathcal{A}_{\tau})$,
which is isomorphic to the category ${A}^{\star}_{\tau}$. Thus, for a given
transition system $(X,A_{\tau},\rightarrow)$, we define a presheaf
$F_{X}\in\mathbf{PSh}({A}^{\star}_{\tau})$ as follows:

$F_{X}(\sigma)=\text{Exec}(X,\sigma),\quad\text{(for every
$\sigma\in{A}^{\star}_{\tau}$)}.$ (7)

The action on $F_{X}$ is given by the restriction of the domain of an
execution.

Incidentally, a branching simulation function $X\rTo^{f}Y$ between
$(X,A_{\tau},\rightarrow)$ and $(Y,A_{\tau},\rightarrow)$ does _not_ induce a
system homomorphism between the underlying dynamical systems (presheaves)
$F_{X}$ and $F_{Y}$ because a branching simulation function does not
necessarily preserve the length of the executions. For example, a sequence of
transitions $\bullet$ may get mapped to a transition $\bullet$.

Thus, we need a procedure that transforms a given presheaf on
${A}^{\star}_{\tau}$ to a presheaf on ${A}^{\star}$. It turns out that there
already is a general result in category theory for this purpose, which we
explain next. In particular, recall the cocompletion of a category
$\mathbf{C}$ through the Yoneda embedding
$\mathbf{C}\rTo^{\mathbb{Y}_{\mathbf{C}}}\mathbf{PSh}(\mathbf{C})$.

######  Theorem 5.17 (see [27]).

For any functor $\mathbf{C}\rTo^{h}\mathbf{D}$, when $\mathbf{C}$ is small and
$\mathbf{D}$ is cocomplete, there is a colimit preserving functor
$\mathbf{PSh}(\mathbf{C})\rTo^{L_{h}}\mathbf{D}$ satisfying
$L_{h}\circ\mathbb{Y}_{\mathbf{C}}\cong h$. Moreover, $L_{h}$ has a right
adjoint $R_{h}$ given by: $R_{h}D(C)=\mathbf{D}(hC,D)$, for each
$C\in\mathbf{C},D\in\mathbf{D}$.

Using the language of Kan extensions, $L_{h}$ is the left Kan extension of $h$
along the Yoneda embedding $\mathbb{Y}_{\mathbf{C}}$. Moreover, using the
notion of a coend [26], we have:

$L_{h}F\cong\int^{C\in\mathbf{C}}FC\odot hC,$

where $\mathbf{D}\rTo^{S\odot\\_}\mathbf{D}$ is the copower functor given by
$S\odot D=\coprod_{s\in S}D$ (taking $S$ disjoint copies of $D$). If we
replace $\mathbf{C}\rTo^{h}\mathbf{D}$ in the above diagram by a map
$\mathbf{C}\rTo^{h}\mathbf{D}\rTo^{\mathbb{Y}_{\mathbf{D}}}\mathbf{PSh}(\mathbf{D})$,
then we obtain the so-called _essential geometric morphism_ [27] between
$\mathbf{PSh}(\mathbf{C})\rTo\mathbf{PSh}(\mathbf{D})$. In full, this means
that the composition functor $h^{*}$ not only has a right adjoint $\Pi_{h}$,
but also a left adjoint $\Sigma_{h}$ (see, for instance, [27] for a formal
definition of a geometric morphism). Below, the composition functor $h^{*}$,
its left adjoint $\Sigma_{h}$, and its right adjoint $\Pi_{h}$ are given by
(up to isomorphism)
$R_{\mathbb{Y}_{\mathbf{D}}h},L_{\mathbb{Y}_{\mathbf{D}}h}$, and
$R_{h^{*}\mathbb{Y}_{\mathbf{D}}}$, respectively.

######  Corollary 5.18 (see [27]).

Given a functor $\mathbf{C}\rTo^{h}\mathbf{D}$ between small categories, then
the inverse image functor
$\mathbf{PSh}(\mathbf{D})\rTo^{h^{*}}\mathbf{PSh}(\mathbf{C})$ given by
$h^{*}G=G\circ{h}^{\text{op}}$ (for each $G\in\mathbf{PSh}(\mathbf{D})$) has
both left and right adjoints:

$\Sigma_{h}\dashv h^{*}\dashv\Pi_{h}.$

So, in principle, there are two ways to land in $\mathbf{PSh}({A}^{\star})$
from $\mathbf{PSh}({A}^{\star}_{\tau})$ whenever there is a functor between
${A}^{\star}_{\tau}\rTo{A}^{\star}$. Nevertheless, since our aim is to
characterise branching bisimulation functions, we will choose the left adjoint
(over the right adjoint) of the composition functor for this task. This is
because to reflect (recall (6)) an observable transition – say, of the form
$\bullet$ –, we only need _minimal_ executions which are of the form
$\bullet\ext@arrow
0359\arrowfill@\relbar\relbar\twoheadrightarrow{}{}{}\bullet$ (cf. Definition
5.23). In particular, we will show (cf. Theorem 5.25) that the left adjoint
$\Sigma_{h}$ (induced by a suitable $h$) transforms a presheaf of executions
into a presheaf of minimal executions (or those executions in which trailing
$\tau$-transitions are chopped off).

###  5.3 An obvious, but failed attempt

There is an evident functor ${A}^{\star}_{\tau}\rTo^{h}{A}^{\star}$ which
treats the letter $\tau$ as an empty word. It is then natural to investigate
whether the bisimulation maps in $\mathbf{PSh}({A}^{\star})$ between any two
induced presheaves $\Sigma_{h}F_{X},\Sigma_{h}F_{Y}$ characterise the
branching bisimulation map. Unfortunately, the answer is no! We explain this
extensively, as this lays the formal foundation for the desired
characterisation given in the next subsection.

So, consider the hiding function $A_{\tau}\rTo^{h}{A}^{\star}$ which treats
$\tau$ as the unit of ${A}^{\star}$ (i.e., $h(\tau)=\varepsilon$) and treats
an action $a\in A$ as observable (i.e., $h(a)=a$ when $a\in A$). This lifts to
an order-preserving function ${A}^{\star}_{\tau}\rTo^{h}{A}^{\star}$ (denoted
again as $h$ by abuse of notation). Thus, we have a functor
${A}^{\star}_{\tau}\rTo^{h}{A}^{\star}$.

######  Proposition 5.21.

The categories ${A}^{\star}_{\tau},{A}^{\star}$ have binary products.

######  Remark 5.22.

It is worthwhile noting that $h$ does not generally preserve finite limits (or
infimum $\sqcap$ in this case). Consider the words $a\tau
b,ab\in{A}^{\star}_{\tau}$. Then, $h(a\tau b\sqcap ab)=h(a)=a$; however,
$h(a\tau b)\sqcap h(ab)=ab\sqcap ab=ab$.

Furthermore, $S\odot X\cong S\times X$ (for any two sets $S,X$) and the
(co)limit in any presheaf category is computed point-wise. Thus, using these
observations, we calculate $\Sigma_{h}F$ (for
$F\in\mathbf{PSh}({A}^{\star}_{\tau})$) at $\varrho\in{A}^{\star}$ as follows:

$\Sigma_{h}F(\varrho)\cong\int^{\sigma\in{A}^{\star}_{\tau}}F(\sigma)\times\mathbb{Y}_{{A}^{\star}}(h(\sigma))(\varrho)\
\cong\ \varinjlim_{\sigma\in{{A}^{\star}_{\tau}}^{\text{op}},\varrho\preceq
h(\sigma)}F(\sigma).$ (8)

Note that the reason for the last isomorphism is that every colimit can be
encoded as a coend (see [26, p. 224–225] for a dual statement). In addition,
(8) is the colimit of ${{A}^{\star}_{\tau}}^{\text{op}}\rTo^{F}\mathbf{Set}$
when $\varrho=\varepsilon$. Notice that ${{A}^{\star}_{\tau}}^{\text{op}}$ is
directed; thus, the colimit of the filtered diagram is
$\coprod_{\varepsilon\preceq h(\sigma)}F\sigma/{\sim}$, where $\sim\
\subseteq\coprod_{\varepsilon\preceq
h(\sigma)}F(\sigma)\times\coprod_{\varepsilon\preceq h(\sigma)}F(\sigma)$ is
the equivalence relation defined as follows:

$(\sigma,p)\sim(\sigma^{\prime},p^{\prime})\iff\exists_{\sigma^{\prime\prime}}\
\left(\sigma^{\prime\prime}\preceq\sigma\land\sigma^{\prime\prime}\preceq\sigma^{\prime}\land
p\cdot\sigma^{\prime\prime}=p^{\prime}\cdot\sigma^{\prime\prime}\right).$ (9)

It turns out that from a system theoretic viewpoint, the set
$\varinjlim_{\varepsilon\preceq h(\sigma)}F_{X}(\sigma)$ is nothing but the
set of minimal executions whose observable trace is an empty observation.
Theorem 5.25 states this result in full generality.

######  Definition 5.23.

Given a transition system $(X,A_{\tau},\rightarrow)$ and a word
$\varrho\in{A}^{\star}$, we say an execution $p$ has an _observable trace_
$\varrho$ if $h(\max\text{dom}(p))=\varrho$. Furthermore,
$\text{MExec}(X,\varrho)$ is the set of all _minimal executions_ w.r.t. the
prefix order $\preceq$ on executions whose observable trace is $\varrho$.
Formally, $p\preceq p^{\prime}\iff p^{\prime}|_{\text{dom}(p)}=p$ and

$\text{MExec}(X,\varrho)=\Big{\\{}p\mid\ \downarrow
p\cap\\{q\in\text{Exec}(X)\mid
h(\max\text{dom}(q))=\varrho\\}=\\{p\\}\Big{\\}}.$

Before we prove Theorem 5.25, we need a category theoretic result (which is
probably folklore; see [26, Exercise IV.2.7] for a dual statement), namely,
that the colimit of a diagram can be decomposed into the coproducts of the
colimits of diagrams with smaller shapes under certain restrictions.

######  Lemma 5.24.

Given a set $J$ and a small category $\mathbf{C}=\coprod_{j\in
J}\mathbf{C}_{j}$ with injections $\iota_{j}$, then for any functor $F$ from
$\mathbf{C}$ to a cocomplete category $\mathbf{D}$, we have
$\varinjlim_{\mathbf{C}}F\cong\coprod_{j\in
J}\varinjlim_{\mathbf{C}_{j}}F\circ\iota_{j}.$

######  Theorem 5.25.

For a given transition system $(X,A_{\tau},\rightarrow)$ and
$\varrho\in{A}^{\star}$, we have
$\Sigma_{h}F_{X}(\varrho)\cong\text{MExec}(X,\varrho).$

Next, we explore the action of the presheaf $\Sigma_{h}F_{X}$ from a system
theoretic viewpoint. Firstly, it is defined by the universal property of the
colimit. Let $\varrho^{\prime}\preceq\varrho$ and let $\sigma$ be a minimal
word such that $h(\sigma)=\varrho$. Then, there is a unique minimal word
$\sigma_{\varrho^{\prime}}=\bigsqcap\\{\sigma^{\prime}\preceq\sigma\mid
h(\sigma^{\prime})=\varrho^{\prime}\\}$. Note that this infimum exists since
the history of a word in ${A}^{\star}_{\tau}$ is a finite totally ordered set
of words. Therefore, the family of arrows depicted by the dotted arrows in
(LABEL:eq:sigma_h-action) forms a cone, where
$A_{\tau,\varrho}^{\star}=\\{\sigma\in{A}^{\star}_{\tau}\mid\varrho\preceq
h(\sigma)\\}$ is a sub-forest of ${A}^{\star}_{\tau}$. Thus, the universal
property of the colimit gives a map
$\Sigma_{h}F_{X}\varrho\rTo\Sigma_{h}F_{Y}\varrho^{\prime}$, which we denote
by $\Sigma_{h}(\varrho,\varrho^{\prime})$.

Secondly, for any $\varrho^{\prime}\preceq\varrho$ with
$\varrho,\varrho^{\prime}\in{A}^{\star}$, we define a map:

$\text{MExec}(X,\varrho)\rTo^{\text{mpast}(\varrho,\varrho^{\prime})}\text{MExec}(X,\varrho^{\prime})\quad\text{given
by}\quad p\mapsto p|_{\downarrow\sigma_{\varrho^{\prime}}}\ ,$

where $\sigma=\max\text{dom}(p)$. Now we can establish that the isomorphism in
Theorem 5.25 is natural in $\varrho\in{A}^{\star}$.

######  Theorem 5.26.

For any $\varrho,\varrho^{\prime}\in{A}^{\star}$ with
$\varrho^{\prime}\preceq\varrho$, the square in (LABEL:eq:naturality-mexec)
commutes.

Now that we know what $\Sigma_{h}$ does to a presheaf, we use the category
$\mathbf{PSh}({A}^{\star})$ as our semantic universe to handle invisible
actions. Thus, for a given $(X,A_{\tau},\rightarrow)$, we let $\llbracket
X\rrbracket=\Sigma_{h}F_{X}$. In addition, for a branching simulation function
$X\rTo^{f}Y$, we use the isomorphic view of minimal executions and let
$\llbracket f\rrbracket_{\varrho}(p)=p_{f}$ (for each
$\varrho\in{A}^{\star}$), where $p_{f}$ is an execution defined inductively
using the following rules.

  * •

If $\text{dom}(p)=\varepsilon$ then $\text{dom}(p_{f})=\varepsilon$ and
$p_{f}(\varepsilon)=f(p(\varepsilon))$.

  * •

If $p$, $p_{f}$, $\text{last}(q)=f(\text{last}(p^{\prime}))$, and $a\in A$
then $p^{\prime}_{f}=q$.

  * •

If $p$ and $f(\text{last}(p))=f(\text{last}(p^{\prime}))$ then
$p^{\prime}_{f}=p_{f}$.

  * •

If $p$, $f(\text{last}(p))\neq f(\text{last}(p^{\prime}))$, $p_{f}$ then
$p^{\prime}_{f}=q$.

Here, $p$; the function $\text{last}(p)$ returns the last visited state by the
execution $p$, i.e., $\text{last}(p)=p(\max\text{dom}(p))$.

######  Lemma 5.33.

For a given branching simulation function $X\rTo^{f}Y$ and a minimal execution
$p\in\text{MExec}(X,\varrho)$, we have $p_{f}\in\text{MExec}(Y,\varrho)$.

Next let $\mathbf{LTS}_{\tau}$ be the category of transition systems with
possible invisible steps, which comprises of transition systems as objects and
morphisms are the collection of identity functions and branching simulation
functions. Thus, we can now give a presheaf semantics for the category
$\mathbf{LTS}_{\tau}$.

######  Theorem 5.34.

The mapping
$\mathbf{LTS}_{\tau}\rTo^{\llbracket\\_\rrbracket}\mathbf{PSh}({A}^{\star})$
is a faithful functor.

Finally, we can invoke the bisimulation maps in $\mathbf{PSh}({A}^{\star})$
but the characterisation of branching bisimulation functions fails to hold.
The mismatch is in the reflection (6) of invisible steps (not with the
reflection of observable transitions), which we explain next in the following
example.

######  Example 5.35.

Consider the two transition systems and the branching simulation $f$ depicted
below with dashed lines. Note that $f$ is _not_ a branching bisimulation
function (even though it is surjective) because it fails to reflect the
transition $y_{1}$.

$x_{1}$$x_{2}$$x_{3}$$y_{1}$$y_{3}$$y_{2}$$a$$\tau$$a$

Yet $\llbracket f\rrbracket$ is a bisimulation map in
$\mathbf{PSh}({A}^{\star})$. For this consider a given commutative square
(LABEL:eq:bisim-presheaf) in $\mathbf{PSh}({A}^{\star})$. The crucial case in
defining the functions $k_{\varrho}$ is when $\varrho\in\\{\varepsilon,a\\}$.

  * •

Let $q\in Q(\varepsilon)$. If $n_{\varepsilon}(q)=\varepsilon_{y_{i}}$ then we
let $k_{\varepsilon}(q)=\varepsilon_{x_{i}}$ (for $i\in\\{1,2,3\\}$).

  * •

Let $q\in Q(a)$. Then, $n_{a}(q)$ is the minimal execution witnessing $y_{1}$
since there are no other minimal executions in $\text{MExec}(Y,a)$. Thus, we
let $k_{a}(q)$ to be the minimal execution witnessing the transition $x_{1}$.

###  5.4 Characterisation of branching bisimulation

Unfortunately, all the information related to silent transitions is lost by
transforming a presheaf using the functor $\Sigma_{h}$ because all the
executions with empty observations get fused into their corresponding empty
(minimal) executions. In retrospect, the problem lies in our specification of
observation since our hypothetical ‘observer’ $\mathcal{O}$ is unable to
differentiate between _empty observation due to no system move_ and _empty
observation due to zero or more system moves_. Therefore, to model this latter
observation, we introduce a constant $\bar{\tau}$ which can be observed
anytime after $0$. So for this section, we define $\mathcal{O}$ in the next
page as follows:

$\displaystyle\mathcal{O}(0)=\mathcal{A}_{\tau}(0)\quad\text{and}\quad\mathcal{O}(n)=\mathcal{A}_{\tau}(n)\cup\\{\bar{\tau}\\}\quad(\text{for
every $n>0$});$ $\displaystyle\sigma\cdot
m=\begin{cases}\sigma|_{m},&\text{if}\ \sigma\neq\bar{\tau}\\\
\varepsilon,&\text{if}\ m=0\land\sigma=\bar{\tau}\\\ \bar{\tau},&\text{if}\
m>0\land\sigma=\bar{\tau}.\end{cases}\qquad\Big{(}\text{for any $m\leq n$ and
$\sigma\in\mathcal{O}(n)$}\Big{)}.$

Put differently, $\bar{\tau}$ is ‘really’ a constant observation over time
except at $0$. The introduction of $\bar{\tau}$ is new and inspired from the
constant $\eta$ [4] which can be viewed as an _empty observation due to at
least one system move_.

######  Proposition 5.39.

The above mapping ${{\rm Nature}}^{\text{op}}\rTo^{\mathcal{O}}\mathbf{Set}$
is a presheaf.

Moreover, the categories $\mathbf{PSh}({\rm Nature})/\mathcal{O}$ and
$\mathbf{PSh}(\mathbb{E}(\mathcal{O}))$ are equivalent (Theorem 2.4). So,
consider the category of elements $\mathbb{E}(\mathcal{O})$ whose objects are
tuples $(n,\sigma)$ (for $n\in{\rm Nature},\sigma\in\mathcal{O}(n)$) and whose
arrows are given by the rule:

$(n,\sigma)$

Just as the category $\mathbb{E}(\mathcal{A}_{\tau})$ has a simpler
description in terms of ${A}^{\star}_{\tau}$, we simplify
$\mathbb{E}(\mathcal{O})$ by defining a set
$A_{\tau\bar{\tau}}^{\star}={A}^{\star}_{\tau}\cup\\{(n,\bar{\tau})\mid
n>0\\}$ ordered by the smallest relation $\preceq\subseteq
A_{\tau\bar{\tau}}^{\star}\times A_{\tau\bar{\tau}}^{\star}$ satisfying the
following rules:

$\frac{(|\sigma|,\sigma)\step{}(|\sigma^{\prime}|,\sigma^{\prime})\in\mathbb{E}(\mathcal{A}_{\tau})}{\sigma\preceq\sigma^{\prime}}\quad\frac{(m,\bar{\tau})\step{}(n,\bar{\tau})\in\mathbb{E}(\mathcal{O})}{(m,\bar{\tau})\preceq(n,\bar{\tau})}\quad\frac{n>0}{\varepsilon\preceq(n,\bar{\tau})}.$

Note that the leftmost rule is concerned with the elements of
${A}^{\star}_{\tau}$. Thus, the slice category $\mathbf{PSh}({\rm
Nature})/\mathcal{O}$ is equivalent to the category
$\mathbf{PSh}(A_{\tau\bar{\tau}}^{\star})$ since $\mathbb{E}(\mathcal{O})\cong
A_{\tau\bar{\tau}}^{\star}$. Using the presheaf $F_{X}$ (cf. (7)) induced by a
given transition system $(X,A_{\tau},\rightarrow)$, define a presheaf
$\bar{F}_{X}\in\mathbf{PSh}(A_{\tau\bar{\tau}}^{\star})$ as follows:

$\bar{F}_{X}(\sigma)=\begin{cases}F_{X}(\sigma),&\text{if}\
\sigma\in{A}^{\star}_{\tau}\\\ \coprod_{n\in{\rm
Nature}}F_{X}(\tau^{n}),&\text{otherwise}\end{cases},\ \text{where}\
\begin{array}[]{l}\tau^{0}=\\{\varepsilon\\}\\\
\tau^{n+1}=\tau^{n}\cup\prod_{n+1}\\{\tau\\}\end{array}.$

The executions based on invisible steps are seen _stretchable in time_ by
$\mathcal{O}$, i.e., a system may perform invisible executions of length
independent of time instants. This is encoded in the second clause of
$\bar{F}_{X}$. To complete the definition of $\bar{F}_{X}$ as a presheaf, we
define, for any $p\in\bar{F}_{X}(\sigma)$ and $\sigma^{\prime}\preceq\sigma$
in $A_{\tau\bar{\tau}}^{\star}$, the action of $\bar{F}_{X}$ as:

$p\cdot\sigma^{\prime}=\begin{cases}p|_{\downarrow\sigma^{\prime}},&\text{if}\
\sigma\in{A}^{\star}_{\tau}\land\sigma^{\prime}\in{A}^{\star}_{\tau}\\\
p|_{\\{\varepsilon\\}},&\text{if}\
\sigma\not\in{A}^{\star}_{\tau}\land\sigma^{\prime}=\varepsilon\\\
p,&\text{if}\
\sigma\not\in{A}^{\star}_{\tau}\land\sigma^{\prime}\not\in{A}^{\star}_{\tau}.\end{cases}$

Notice how the above formulation closely follows the three defining clauses of
$\mathcal{O}$.

######  Proposition 5.43.

The mapping $\bar{F}_{X}$ defined above is a contravariant functor.

To characterise branching bisimulation, define a structure
$A_{\bar{\tau}}^{\star}$ similar to ${A}^{\star}$ and a structure preserving
map $A_{\tau\bar{\tau}}^{\star}\rTo A_{\bar{\tau}}^{\star}$ similar to $h$
(Section 5.3). To this end, our semantic category for branching bisimulation
will be $A_{\bar{\tau}}^{\star}={A}^{\star}\cup\\{\bar{\tau}\\}$ ordered by
the relation $\preceq\subseteq A_{\bar{\tau}}^{\star}\times
A_{\bar{\tau}}^{\star}$ consisting of prefix relation and the pairs
$(\varepsilon,\bar{\tau}),(\bar{\tau},\bar{\tau})$. We consider
$A_{\tau\bar{\tau}}^{\star}\rTo^{\bar{h}}A_{\bar{\tau}}^{\star}$ given by:
$\bar{h}(\sigma)=h(\sigma)$, if $\sigma\in{A}^{\star}_{\tau}$; and
$\bar{h}(n,\bar{\tau})=\bar{\tau}$ (for all $n\in{\rm Nature}$).

Next, we aim to compute the presheaf $\Sigma_{\bar{h}}\bar{F}_{X}$ at
$\varrho\in A_{\bar{\tau}}^{\star}$. At this stage, we can take the advantage
of similarity between the structures
${A}^{\star}_{\tau},A_{\tau\bar{\tau}}^{\star}$ and
${A}^{\star},A_{\bar{\tau}}^{\star}$ to compute the colimits, similar to (8)
where ${{A}^{\star}_{\tau}}^{\text{op}}$ is replaced by
${A_{\tau\bar{\tau}}^{\star}}^{\text{op}}$ as the indexing category. In lieu
of Theorems 5.25 and 5.26, we obtain

######  Theorem 5.44.

For a given transition system $(X,A_{\tau},\rightarrow)$, we find that
$\Sigma_{\bar{h}}\bar{F}_{X}(\bar{\tau})\cong\coprod_{n\in{\rm
Nature}}\text{Exec}(X,\tau^{n})$ and
$\Sigma_{\bar{h}}\bar{F}_{X}(\varrho)\cong\text{MExec}(X,\varrho)$ (for any
$\varrho\neq\bar{\tau}$). Moreover, the above isomorphisms are natural in
$\varrho\in A_{\bar{\tau}}^{\star}$. I.e., for any
$\varrho^{\prime}\preceq\varrho$ with
$\varrho,\varrho^{\prime}\in{A}^{\star}$, the square in (LABEL:eq:naturality-
mexec) and the following square commute.

Note that the definition of the maps
$\Sigma_{\bar{h}}(\varrho^{\prime},\varrho)$ (for
$\varrho^{\prime}\preceq\varrho$) is similar to the maps
$\Sigma_{h}(\varrho^{\prime},\varrho)$ defined by the universal property of
colimits (see (LABEL:eq:sigma_h-action)). Just like in the previous
subsection, we utilise the isomorphic view of minimal executions to define our
semantic map
$\mathbf{LTS}_{\tau}\rTo^{\llbracket\\_\rrbracket}\mathbf{PSh}(A_{\bar{\tau}}^{\star})$:

  * •

For a given transition system, we let $\llbracket
X\rrbracket=\Sigma_{\bar{h}}\bar{F}_{X}$.

  * •

For a given branching simulation function $X\rTo^{f}Y$, we let $\llbracket
f\rrbracket_{\varrho}(p)=p_{f}$.

######  Lemma 5.45.

The above mapping $\llbracket\\_\rrbracket$ is a faithful functor.

Finally, we have obtained the desired result of this section.

######  Theorem 5.46.

A branching simulation function $f$ is a branching bisimulation function iff
$\llbracket f\rrbracket$ is a bisimulation map in
$\mathbf{PSh}(A_{\bar{\tau}}^{\star})$.

##  6 Related work and Conclusion

The core idea of Goguen’s sheaf semantics [16] is: systems are diagrams of
sheaves, behaviour (interconnection) of systems is their limit (colimit). In
retrospect, Goguen gave a sheaf semantics of nondeterministic automata by
constructing presheaves on the Alexandroff topology induced by the downward
closed subsets of ${A}^{\star}$ (in contrast to presheaves over
${A}^{\star}$). However, it is well known that the category of sheaves on
Alexandroff spaces induced by a poset $(X,\preceq)$ is equivalent to the
category of presheaves on $X$ (a consequence of the so-called comparison lemma
in topos theory; see [27, Corollary 3 on Page 590]). In short, we use simpler
structures to represent executions and focused on defining bisimulations
abstractly which were absent in [16].

Relational presheaves [31] generalise transition systems that are labelled by
words from the free monoid ${A}^{\star}$. The idea was to accommodate the
earlier presheaf approaches [34, 23] with algebraic structure on labels. The
most insightful observation of [31] was the well-known ‘saturation’
construction on transition systems can be captured using a 2-adjunction
induced by a homomorphism between ${A}^{\star}_{\tau},{A}^{\star}$. Unlike
[31], our left adjoint $\Sigma_{h}$ records the minimal executions induced by
a transition system with silent steps. We expect this to be relevant for
probabilistic systems, where minimal executions are used to define a
probability measure (cf. [6]).

Open maps between presheaves as defined in [23] are instances of the open maps
in a topos as introduced in [22]. This is because open maps between presheaves
(as in [23]) are natural transformations whose naturality square is a weak
pullback in $\mathbf{Set}$ (cf. [22, Example 1.1]). We discarded the open maps
between presheaves because they are incapable of establishing complete
refinement between an implementation and its specficiation; though it is still
interesting to assert whether the bisimulation maps (Def. 3.1) satisfy the
axioms given in [22].

Prefix orders are generalisations of trees proposed in [10] to study
executions of dynamical systems in an order theoretic manner. In [5], the
authors defined functional bisimulation between prefix orders by
reinterpreting the definition of open maps in concrete categories. Our
bisimulation maps are an instance of this general definition (Section 3). It
is unclear, though, how to enrich prefix orders with observations so that we
can model labelled executions in a uniformly. This question lead us to model
observations as presheaves.

To sum up, bisimulation maps between presheaves are versatile enough to
capture different notions of behavioural equivalence. We demonstrated this by
characterising $\forall$-fair bisimulation and branching bisimulation, two
notions that are notoriously difficult to capture with a coalgebraic approach.
The clear distinction between time and observation proved fruitful in dealing
with silent actions, but we also expect our framework to lend itself well to
modelling hybrid systems. For instance, sheaves over the translation-invariant
interval domain $\mathbb{IR}_{/\vartriangleright}$ were introduced in [30] to
model hybrid systems. It will be interesting to explore whether bisimulation
maps between such sheaves (Remark 3.2) coincides with stateless bisimulation
[7, 11, 32].

We thank the anonymous reviewers of FOSSACS’19 for their feedback on an
earlier draft that greatly improved this manuscript. In particular, Reviewer 1
not only identified a mistake in our earlier characterisation of branching
bisimulation, but also provided a detailed feedback including the proofs in
the appendix for which we are grateful. We thank Barbara König and Christina
Mika for valuable comments on earlier drafts of this paper. We also thank
Pieter Cuijpers for asking us about the importance of presheaf categories in
system modelling, which formed the basis of Section 2. Moreover, we are
grateful to Alex Simpson for discussing early ideas and in particular, for
guiding our attention from sheaves on Alexandroff spaces induced by the poset
${A}^{\star}$ to just presheaves on ${A}^{\star}$. Finally, we acknowledge
Paul Taylor’s diagram package for commutative diagrams.

## References

  * [1] Abramsky, S., _What are the fundamental structures of concurrency?: We still don’t know!_ , Electronic Notes in Theoretical Computer Science 162 (2006), pp. 37 – 41, essays on Algebraic Process Calculi.
  * [2] Adámek, J., H. Herrlich and G. E. Strecker, “Abstract and Concrete Categories,” Wiley-Interscience, New York, NY, USA, 1990.
  * [3] Baeten, J. C. M., T. Basten and M. A. Reniers, “Process Algebra: Equational Theories of Communicating Processes,” Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 2009.
  * [4] Baeten, J. C. M. and R. J. van Glabbeek, _Another look at abstraction in process algebra_ , in: T. Ottmann, editor, _Automata, Languages and Programming_ (1987), pp. 84–94.
  * [5] Beohar, H. and P. J. L. Cuijpers, _Open maps in concrete categories and branching bisimulation for prefix orders_ , Electronic Notes in Theoretical Computer Science 319 (2015), pp. 51 – 66, the 31st Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXI).
  * [6] Beohar, H. and S. Küpper, _On path-based coalgebras and weak notions of bisimulation_ , in: F. Bonchi and B. König, editors, _7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)_ , Leibniz International Proceedings in Informatics (LIPIcs) 72 (2017), pp. 6:1–6:17.
  * [7] Beohar, H., D. E. Nadales Agut, D. A. van Beek and P. J. L. Cuijpers, _Hierarchical states in the compositional interchange format_ , in: _Proceedings Seventh Workshop on Structural Operational Semantics, SOS_ , 2010, pp. 42–56.
  * [8] Cattani, G. L. and G. Winskel, _Profunctors, open maps and bisimulation_ , Mathematical Structures in Computer Science 15 (2005), p. 553–614.
  * [9] Caucal, D., _Branching bisimulation for context-free processes_ , in: R. K. Shyamasundar, editor, _FSTTCS_ (1992), pp. 316–327.
  * [10] Cuijpers, P. J. L., _Prefix orders as a general model of dynamics_ , in: I. Mackie, M. Ayala-Rincón and E. Bonelli, editors, _Proc. of Developments in Computation Models_ , DCM’13, Buenos Aires, Argentina, 2013, pp. 25–29.
  * [11] Cuijpers, P. J. L. and M. A. Reniers, _Hybrid process algebra_ , The Journal of Logic and Algebraic Programming 62 (2005), pp. 191 – 245\.
  * [12] Cuijpers, P. J. L. and M. A. Reniers, _Lost in translation: Hybrid-time flows vs. real-time transitions_ , in: M. Egerstedt and B. Mishra, editors, _Hybrid Systems: Computation and Control_ (2008), pp. 116–129.
  * [13] Eberhart, C. and T. Hirschowitz, _What’s in a game?: A theory of game models_ , in: _Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science_ , LICS ’18 (2018), pp. 374–383.
URL http://doi.acm.org/10.1145/3209108.3209114

  * [14] Eberhart, C., T. Hirschowitz and T. Seiller, _An intensionally fully-abstract sheaf model for $\pi$ (expanded version)_, Logical Methods in Computer Science Volume 13, Issue 4 (2017).
URL https://lmcs.episciences.org/4069

  * [15] Fiore, M., G. L. Cattani and G. Winskel, _Weak bisimulation and open maps_ , in: _Proc. 14th Symposium on Logic in Computer Science_ , 1999, pp. 67–76.
  * [16] Goguen, J. A., _Sheaf semantics for concurrent interacting objects_ , in: _Mathematical Structures in Computer Science_ , 1992, pp. 159–191.
  * [17] Hennessy, M. C. B. and C. P. Stirling, _The power of the future perfect in program logics_ , Information and Control 67 (1985), pp. 23 – 52.
  * [18] Henzinger, T. A., O. Kupferman and S. K. Rajamani, _Fair simulation_ , Inf. Comput. 173 (2002), pp. 64–81.
  * [19] Hildebrandt, T. T., _Towards categorical models for fairness: fully abstract presheaf semantics of SCCS with finite delay_ , Theoretical Computer Science 294 (2003), pp. 151 – 181.
  * [20] Hirschowitz, T. and D. Pous, _Innocent strategies as presheaves and interactive equivalences for ccs_ , Scientific Annals of Computer Science 22 (2013), pp. 147–199.
  * [21] Hojati, R., “A BDD-Based Environment for Formal Verification of Hardware Systems,” Ph.D. thesis, EECS Department, University of California, Berkeley (1996).
URL http://www2.eecs.berkeley.edu/Pubs/TechRpts/1996/3052.html

  * [22] Joyal, A. and I. Moerdijk, _A completeness theorem for open maps_ , Annals of Pure and Applied Logic 70 (1994), pp. 51 – 86.
  * [23] Joyal, A., M. Nielsen and G. Winskel, _Bisimulation from open maps_ , Information and Computation 127 (1996), pp. 164 – 185.
  * [24] Kupferman, O., N. Piterman and M. Y. Vardi, “Fair Equivalence Relations,” Springer, Berlin, Heidelberg, 2003 pp. 702–732.
  * [25] Kwiatkowska, M., _Survey of fairness notions_ , Information and Software Technology 31 (1989), pp. 371 – 386.
  * [26] Mac Lane, S., “Categories for the Working Mathematician,” Number 5 in Graduate texts in Mathematics, Springer, NY, 1998, second edition.
  * [27] Mac Lane, S. and I. Moerdijk, “Sheaves in geometry and logic: a first introduction to topos theory,” Universitext, Springer, 1992.
  * [28] Polderman, J. W. and J. C. Willems, “Introduction to Mathematical Systems Theory: A Behavioral Approach,” Texts in Applied Mathematics 26, Springer-Verlag, New York, 1998, 1 edition.
  * [29] Rutten, J. J. M. M., _Universal coalgebra: a theory of systems_ , Theoretical Computer Science 249 (2000), pp. 3 – 80.
  * [30] Schultz, P. and D. I. Spivak, _Temporal Type Theory: A topos-theoretic approach to systems and behavior_ (2017).
URL https://arxiv.org/abs/1710.10258

  * [31] Sobociński, P., _Relational presheaves, change of base and weak simulation_ , Journal of Computer and System Sciences 81 (2015), pp. 901 – 910, 11th International Workshop on Coalgebraic Methods in Computer Science, CMCS 2012 (Selected Papers).
  * [32] van Beek, D. A., K. L. Man, R. M. A., J. E. Rooda and R. R. H. Schiffelers, _Syntax and consistent equation semantics of hybrid Chi_ , The Journal of Logic and Algebraic Programming 68 (2006), pp. 129 – 210.
  * [33] van Glabbeek, R. J. and W. P. Weijland, _Branching time and abstraction in bisimulation semantics_ , J. ACM 43 (1996), pp. 555–600.
  * [34] Winskel, G. and M. Nielsen, _Presheaves as transition systems_ , in: _Proceedings of the DIMACS Workshop on Partial Order Methods in Verification_ , POMIV ’96 (1997), pp. 129–140.

##  Appendix A Proofs

######  Theorem A.1 (Theorem 3.3).

Every bisimulation map in a (pre)sheaf category is a retract; thus, every
bisimulation map is an epimorphism.

######  Proof A.2.

In the commutative square (LABEL:eq:bisim-presheaf), take $P=0$ the initial
object in $\mathbf{PSh}(\mathbf{C})$ (the proof for sheaves is similar),
$Q=G$, $g=!_{G}$, $n=\text{id}_{G}$, and $m=!_{P}$. Clearly, $0\rMono{!_{G}}G$
is the monomorphism since any two parallel arrows with initial object as the
common codomain ought to be isomorphic. Thus, $f$ is a retract in
$\mathbf{PSh}(\mathbf{C})$ since there is an arrow $k$ such that $f\circ
k=\text{id}_{G}$. Hence, $f$ is an epimorphism.

##  Appendix B Proofs Concerning Section 4

######  Proposition B.1 (Proposition 4.4).

The above map
$\mathbf{FTS}\rTo^{\llbracket\\_\rrbracket}\mathbf{PSh}({A}^{\infty})$ is a
faithful functor.

######  Proof B.2.

It is clear that a given fair transition system
$(X,A,\rightarrow,\text{Fair}_{X})$ induces a presheaf $\llbracket
X\rrbracket$ on ${A}^{\infty}$. Let
$X\cup\\{\Omega\\}\rTo^{f}Y\cup\\{\Omega\\}$ be a given fair simulation
function and let $p\in\llbracket X\rrbracket(\sigma)$. Then $f\circ p$
preserves the transition structure since $f$ satisfies (1); thus,

$p(\sigma^{\prime})$

for any $\sigma^{\prime}a\preceq\sigma$ if $\sigma\in{A}^{\star}$ (or
$\sigma^{\prime}a\prec\sigma$ if $\sigma\in{A}^{\omega}$). Moreover, if
$\sigma\in{A}^{\omega}$, then $\llbracket
f\rrbracket_{\sigma}(p(\sigma))=\Omega$ by construction. Thus, $\llbracket
f\rrbracket_{\sigma}\circ p\in\llbracket Y\rrbracket(\sigma)$.

Furthermore, $f$ induces a natural transformation $\llbracket
X\rrbracket\rTo^{\llbracket f\rrbracket}\llbracket Y\rrbracket$ because for
any $\sigma^{\prime}\preceq\sigma$ and $p\in\llbracket X\rrbracket(\sigma)$,
we find that

$f\circ(p\cdot\sigma^{\prime})=f\circ(p|_{\downarrow\sigma^{\prime}})=(f\circ
p)|_{\downarrow\sigma^{\prime}}=(f\circ p)\cdot\sigma^{\prime}.$

Lastly, to show that $\llbracket\\_\rrbracket$ is faithful, assume that
$\llbracket f\rrbracket=\llbracket g\rrbracket$. Then we find that
$\varepsilon_{f(x)}=\llbracket
f\rrbracket_{\varepsilon}(\varepsilon_{x})=\llbracket
g\rrbracket_{\varepsilon}(\varepsilon_{x})=\varepsilon_{g(x)}$, for any $x\in
X$. Thus, $f=g$.

######  Theorem B.5 (Theorem 4.5).

A fair simulation function $f$ is a fair bisimulation if, and only if, the
underlying map $\llbracket f\rrbracket$ is a bisimulation map in
$\mathbf{PSh}({A}^{\infty})$.

######  Proof B.6.

$\Rightarrow$ Consider the commutative square as depicted below in
$\mathbf{PSh}({A}^{\infty})$.

$\begin{diagram}$ (10)

We will prove the existence of $Q\rTo^{k}\llbracket X\rrbracket$ by well-
founded induction. Note that the relation $\preceq$ is a well-founded relation
on ${A}^{\infty}$. To see this, let $U\subseteq{A}^{\infty}$ and let
$\sigma\in U$, for some $\sigma\in{A}^{\infty}$. Since the history of $\sigma$
is discrete, i.e., $\downarrow\sigma\setminus\\{\sigma\\}$ is isomorphic to
$\downarrow n$ (for some $n$ when $\sigma$ is finite) or ${\rm Nature}$ (when
$\sigma$ is infinite), we know that the infimum
$\bigsqcap(\downarrow\sigma\cap U)$ exists. Thus, every nonempty subset of
${A}^{\infty}$ has a minimal element; whence, $\preceq$ is a well-founded
relation on ${A}^{\infty}$.

For the base case, let $\sigma=\varepsilon$. Notice that the map $\llbracket
f\rrbracket_{\varepsilon}$ is surjective since the given $f$ is surjective.
Moreover, since every epi splits in $\mathbf{Set}$, there is a map $\llbracket
Y\rrbracket(\varepsilon)\rTo^{h}\llbracket X\rrbracket(\varepsilon)$ such that
$\llbracket f\rrbracket_{\varepsilon}\circ h=\text{id}_{\llbracket
Y\rrbracket(\varepsilon)}$. Thus, we define

$k_{\varepsilon}(q)=\begin{cases}m_{\varepsilon}(g\raisebox{4.95134pt}{$\scriptscriptstyle-\\!1$}_{\varepsilon}(q)),&\text{if}\
q\in g_{\varepsilon}(P(\varepsilon))\\\
h(n_{\varepsilon}(q)),&\text{otherwise}.\end{cases}$

Clearly, $\llbracket f\rrbracket_{\varepsilon}\circ
k_{\varepsilon}=n_{\varepsilon}$ and $k_{\varepsilon}\circ
g_{\varepsilon}=m_{\varepsilon}$.

For the inductive case, consider a family of functions $k_{\sigma^{\prime}}$
(for each $\sigma^{\prime}\preceq\sigma$) such that

  1. $I.1$

$k$ is a natural transformation up to $\sigma$, i.e.,
$k_{\sigma^{\prime\prime}}(q\cdot\sigma^{\prime\prime})=(k_{\sigma^{\prime}}(q))\cdot\sigma^{\prime\prime}$,
for any $\sigma^{\prime\prime}\preceq\sigma^{\prime}\preceq\sigma$ and $q\in
Q(\sigma^{\prime})$;

  2. $I.2$

the lower triangle commutes up to $\sigma$, i.e., $k_{\sigma^{\prime}}\circ
g_{\sigma^{\prime}}=m_{\sigma^{\prime}}$ (for any
$\sigma^{\prime}\preceq\sigma$);

  3. $I.3$

the upper triangle commutes up to $\sigma$, i.e., $\llbracket
f\rrbracket_{\sigma^{\prime}}\circ k_{\sigma^{\prime}}=n_{\sigma^{\prime}}$
(for any $\sigma^{\prime}\preceq\sigma$).

Next, we distinguish two cases based on the length of $\sigma$.

  1. (1)

Let $\sigma\in{A}^{\star}$. Then we know that $\sigma=\sigma^{\prime}a$, for
some $\sigma^{\prime}\in{A}^{\star},a\in A$. Let $\bar{q}\in Q(\sigma)$ and
assume that $\bar{q}\not\in g_{\sigma}(P(\sigma))$ (otherwise, simply take
$k_{\sigma}(\bar{q})=m_{\sigma}(g\raisebox{4.95134pt}{$\scriptscriptstyle-\\!1$}_{\sigma}(\bar{q}))$).
Then there are some $q^{\prime}\in Q(\sigma^{\prime})$ and $q\in\llbracket
Y\rrbracket(\sigma^{\prime})$ such that
$q^{\prime}=\bar{q}\cdot\sigma^{\prime}$, $n_{\sigma^{\prime}}(q^{\prime})=q$,
and $q=(n_{\sigma}(\bar{q}))\cdot\sigma^{\prime}$. And by the induction
hypothesis we find an execution $p\in\text{Exec}(X,\sigma^{\prime})$ such that
$k_{\sigma^{\prime}}(q^{\prime})=p$ and $\llbracket
f\rrbracket_{\sigma^{\prime}}(p)=q$. Thus, $f(p)\prec n_{\sigma}(\bar{q})$.
And using (2) we find a strict extension $p^{\prime}$ of $p$ (i.e.,
$p^{\prime}\prec p$) such that $f(p^{\prime})=n_{\sigma}(\bar{q})$. Clearly,
$p^{\prime}\cdot\sigma^{\prime}=p$. Therefore, we let
$k_{\sigma}(\bar{q})=p^{\prime}$. Clearly,
$(k_{\sigma}(\bar{q}))\cdot\sigma^{\prime}=k_{\sigma^{\prime}}(\bar{q}\cdot\sigma^{\prime})$.
Moreover, $\llbracket f\rrbracket_{\sigma}\circ
k_{\sigma}(\bar{q})=n_{\sigma}(\bar{q})$; thus, the upper triangles commute up
to $\sigma$. Lastly, commutativity of the lower triangle up to $\sigma$
follows directly from $k_{\sigma^{\prime}}$. Hence, the inductive hypothesis
($I.1\land I.2\land I.3$) is satisfied by $k_{\sigma}$.

  2. (2)

Let $\sigma\in{A}^{\omega}$. Let $\bar{q}\in Q(\sigma)$ and assume that
$\bar{q}\not\in g_{\sigma}(P(\sigma))$. Then for every $i\in{\rm Nature}$,
there are some $q^{\prime}_{i}\in Q(\sigma_{i})$ and $q_{i}\in\llbracket
Y\rrbracket(\sigma_{i})$ (where $\sigma_{i}=\sigma|_{i}\in{A}^{\star}$) such
that $q_{i}^{\prime}=\bar{q}\cdot\sigma_{i}$,
$n_{\sigma_{i}}(q_{i}^{\prime})=q_{i}$, and
$q_{i}=(n_{\sigma}(\bar{q}))\cdot\sigma_{i}$. By induction hypothesis, for
each $i$, we find some execution $p_{i}\in\text{Exec}(X)$ such that
$k_{\sigma_{i}}(q_{i}^{\prime})=p_{i}$ and $\llbracket
f\rrbracket_{\sigma_{i}}(p_{i})=f(p_{i})=q_{i}$. Note that this sequence
$(p_{i})_{i\in{\rm Nature}}$ is strictly increasing because using the
induction hypothesis $I.1$, we find (for any $i\in{\rm Nature}$):

$p_{i+1}\cdot\sigma_{i}=(k_{\sigma_{i+1}}(q_{i+1}^{\prime}))\cdot\sigma_{i}=k_{\sigma_{i}}(q_{i+1}^{\prime}\cdot\sigma_{i})=k_{\sigma_{i}}(q_{i}^{\prime})=p_{i}.$

Thus, $p_{i}\prec p_{i+1}$. Clearly, the supremum $\bigsqcup_{i\in{\rm
Nature}}f(p_{i})$ exists since it evaluates to the execution
$n_{\sigma}(\bar{q})$. So, from (3) we know that the supremum
$\bigsqcup_{i\in{\rm Nature}}p_{i}$ also exists and, moreover,
$f(\bigsqcup_{i\in{\rm Nature}}p_{i})=n_{\sigma}(\bar{q})$. Therefore, we let
$k_{\sigma}(\bar{q})=\bigsqcup_{i\in{\rm Nature}}p_{i}$.

Clearly,
$(k_{\sigma}(\bar{q}))\cdot\sigma_{i}=p_{i}=k_{\sigma_{i}}(\bar{q}\cdot\sigma_{i})$,
for any $i\in{\rm Nature}$. Moreover, $\llbracket f\rrbracket_{\sigma}\circ
k_{\sigma}(\bar{q})=n_{\sigma}(\bar{q})$; thus, the upper triangle commutes up
to $\sigma$. Lastly, commutativity of the lower triangle up to $\sigma$
follows directly from each $k_{\sigma_{i}}$. Hence, the inductive hypothesis
($I.1\land I.2\land I.3$) is satisfied by $k_{\sigma}$.

$\Leftarrow$ Let $X\cup\\{\Omega\\}\rTo^{f}Y\cup\\{\Omega\\}$ be a fair
simulation function such that $\llbracket f\rrbracket$ is a bisimulation map
in $\mathbf{PSh}({A}^{\infty})$. The function $f$ is surjective because the
map $\llbracket f\rrbracket_{\varepsilon}$ is surjective (cf. Theorem 3.3).
Next, we show that $f$ satisfies the condition in (2). Let $f(x)$ (for some
$x\in X,a\in A,y\in Y$) and let $q\in\text{Exec}(Y)$ witnessing this
transition. Construct two presheaves $P,Q\in\mathbf{PSh}({A}^{\infty})$ as
follows:

  * •

$P(\varepsilon)=\\{\varepsilon_{x}\\}$ and $P(\sigma)=\emptyset$ (for all
$\sigma\neq\varepsilon$).

  * •

$Q(\varepsilon)=\\{\varepsilon_{f(x)}\\}$, $Q(a)=\\{q\\}$, and
$Q(\sigma)=\emptyset$ (for $\sigma\not\in\\{\varepsilon,a\\}$) with
$q\cdot\varepsilon=\varepsilon_{f(x)}$.

Consider the square drawn in (10) and take $m,n$ as the obvious injections
with $g_{\varepsilon}(\varepsilon_{x})=\varepsilon_{f(x)}$ and
$g_{\sigma}=\emptyset$ (for $\sigma\neq\varepsilon$). Then this square
commutes, i.e., $\llbracket f\rrbracket\circ m=n\circ g$. Moreover, the map
$g$ is clearly a mono in $\mathbf{PSh}({A}^{\infty})$. Thus, there is a
diagonal map $Q\rTo^{k}\llbracket X\rrbracket$ such that the two triangles
commute (see (10)). Therefore, there is an execution $p\in\llbracket
X\rrbracket(a)$ such that $p\cdot\varepsilon=\varepsilon_{x}$ and $f\circ p=q$
(due to the commutativity of lower and upper triangles, respectively). I.e.,
there is a transition $x$ and $f(\text{last}(p))=y$.

It remains to show that $f$ satisfies (3). Consider an increasing sequence of
finite executions $(p_{i})_{i\in{\rm Nature}}$. The interesting case is when
the supremum $\bigsqcup_{i\in{\rm Nature}}f\circ p_{i}$ exists. The other case
when the supremum $\bigsqcup_{i\in{\rm Nature}}p_{i}$ exists is trivial, since
a simulation function already preserves such limit executions. Let
$\sigma_{i}=\max\text{dom}(p_{i})$ (for each $i\in{\rm Nature}$). Note that
the supremum $\bigsqcup_{i\in{\rm Nature}}\sigma_{i}$ exists since
${A}^{\infty}$ is a directed complete poset. Now construct the following
presheaves $P,Q\in\mathbf{PSh}({A}^{\infty})$.

  * •

$P(\sigma_{i})=\\{p_{i}\\}$ and $P(\sigma)=\emptyset$ (for
$\sigma\not\in\bigsqcup_{i\in{\rm Nature}}\sigma_{i}$) with
$p_{i}\cdot\sigma_{j}=p_{j}$ (for $j\leq i$).

  * •

$Q(\sigma_{i})=\\{f\circ p_{i}\\}$, $Q(\bigsqcup_{i\in{\rm
Nature}}\sigma_{i})=\bigsqcup_{i\in{\rm Nature}}f\circ p_{i}$, and
$Q(\sigma)=\emptyset$ (for $\sigma\not\in\bigsqcup_{i\in{\rm
Nature}}\sigma_{i}$ or $\sigma\neq\bigsqcup_{i\in{\rm Nature}}\sigma_{i}$)
with $(\bigsqcup_{i\in{\rm Nature}}f\circ p_{i})\cdot\sigma_{i}=f\circ p_{i}$
and $(f\circ p_{i})\cdot\sigma_{j}=f\circ(p_{i}\cdot\sigma_{j})$. Notice that
the last equation holds because $\llbracket f\rrbracket$ is a natural
transformation, which is due to $f$ being a fair simulation function (cf.
Proposition 4.4).

Furthermore, taking $m,n,$ and $g$ as the obvious injections in (10), we again
find that the square drawn in (10) commutes. Thus, there is a map
$Q\rTo^{k}\llbracket X\rrbracket$ such that the two triangles commute.
Therefore, there is an execution $p\in\text{FExec}(X)$ such that
$p|_{\text{dom}(p_{i})}=p_{i}$ (for each $i\in{\rm Nature}$) and $f\circ
p=\bigsqcup_{i\in{\rm Nature}}f\circ p_{i}$. Next, we claim that
$p=\bigsqcup_{i\in{\rm Nature}}p_{i}$. Clearly, $p$ is an upper bound of the
sequence $(p_{i})_{i\in{\rm Nature}}$. Let $p^{\prime}$ be another upper bound
of this sequence. Then,
$p^{\prime}(\sigma_{i})=p_{i}(\sigma_{i})=p(\sigma_{i})$ (for any $i\in{\rm
Nature}$). Moreover, $p^{\prime}(\bigsqcup_{i\in{\rm
Nature}}\sigma_{i})=\Omega=p(\bigsqcup_{i\in{\rm Nature}}\sigma_{i})$. Thus,
$p=p^{\prime}$; whence $p$ is the supremum of the sequence $(p_{i})_{i\in{\rm
Nature}}$.

######  Theorem B.9 (Theorem 4.10).

Two states $x$ and $x^{\prime}$ are related by a $\forall$-fair bisimulation
relation if, and only if, there is a fair bisimulation function $f$ such that
$f(x)=f(x^{\prime})$.

######  Proof B.10.

Let $(X,A,\rightarrow,\text{Fair}_{X})$ be a fair transition system.

$\Rightarrow$ Assume a given fair bisimulation function
$X\cup\\{\Omega\\}\rTo^{f}Y\cup\\{\Omega\\}$ with some fair transition system
$(Y,A,\rightarrow,\text{Fair}_{Y})$. Then we show that the equivalence
relation $\mathcal{R}=\\{(x,x^{\prime})\mid f(x)=f(x^{\prime})\\}$ satisfies
the transfer properties of a $\forall$-fair bisimulation relation.

Let $x\mathcal{R}y$ and $x$. Using (1) we have $f(x)$ and therefore $f(y)$,
since $f(x)=f(y)$. Using (2) we find some $y^{\prime}\in X$ such that $y$ and
$f(y^{\prime})=f(x^{\prime})$. Thus, $x^{\prime}\mathcal{R}y^{\prime}$.

Let $p\in\text{Fair}_{X}$ and let $q$ be an infinite execution such that
$p=_{\mathcal{R}}q$. Further, let $\sigma=\max\text{dom}(p)$. Clearly,
$\sigma\in{A}^{\omega}$. Let $r_{i}=r\cdot(\sigma|_{i})$, for each $i\in{\rm
Nature}$ and $r\in\\{p,q\\}$. Then we find $f\circ p_{i}=f\circ q_{i}$ because
$p=_{\mathcal{R}}q$. Now using (3), we find $q=\bigsqcup_{i\in{\rm
Nature}}q_{i}\in\text{Fair}_{X}$ because

$f\circ\bigsqcup_{i\in{\rm Nature}}p_{i}=\bigsqcup_{i\in{\rm Nature}}f\circ
p_{i}=\bigsqcup_{i\in{\rm Nature}}f\circ q_{i}=f\circ\bigsqcup_{i\in{\rm
Nature}}q_{i}.$

$\Leftarrow$ Assume a given $\forall$-fair bisimulation $\mathcal{R}\subseteq
X\times X$ which, by definition, is an equivalence relation. We construct a
matching fair bisimulation function whose codomain is the quotient system
$Y=\\{[x]=\\{x^{\prime}\mid(x,x^{\prime})\in\mathcal{R}\\}\mid x\in X\\}$ with
$[x]$. The fairness predicate on the quotient system $Y$ is defined as
follows:

$\text{Fair}_{Y}=\\{f\circ p\mid p\in\text{Fair}_{X}\\},$ (11)

where $X\cup\\{\Omega\\}\rTo^{f}Y\cup\\{\Omega\\}$ by $f(x)=[x]$ and
$f(\Omega)=\Omega$. We claim that the predicate $\text{Fair}_{Y}$ is well
defined, i.e., independent of chosen representatives. To prove this, we show
that

$\forall_{p,p^{\prime}}\ \big{(}f\circ p=f\circ
p^{\prime}\implies(p\in\text{Fair}_{X}\iff
p^{\prime}\in\text{Fair}_{X})\big{)}.$

So let $p,p^{\prime}$ be such that $f\circ p=f\circ p^{\prime}$. Then we find
that $\text{dom}(p)=\text{dom}(p^{\prime})$ and
$\forall_{\sigma\in\text{dom}(p)}\ p(\sigma)\mathcal{R}p^{\prime}(\sigma)$.
I.e., $p=_{\mathcal{R}}p^{\prime}$. Clearly, from Definition 4.7(2) we obtain
$p\in\text{Fair}_{X}\iff p^{\prime}\in\text{Fair}_{X}$. Thus,
$\text{Fair}_{Y}$ is well defined.

It is straightforward to see that $f$ is a surjective fair simulation. The
function $f$ satisfies (1) because $x$. Moreover, $f$ preserves fairness by
the construction (11) of $\text{Fair}_{Y}$.

Now to show that $f$ satisfies (3), assume an increasing sequence of finite
executions $(p_{i})_{i\in{\rm Nature}}$. The interesting case is when the
supremum $q=\bigsqcup_{i\in{\rm Nature}}f\circ p_{i}$ exists. The other case
when the supremum $\bigsqcup_{i\in{\rm Nature}}p_{i}$ exists is trivial since
a fair simulation function preserves this limit. So consider the former case.
Then define an infinite execution $\text{dom}(q)\rTo^{p}X$ as follows:

$p(\sigma)=\begin{cases}p_{|\sigma|}(\sigma),&\mbox{if
}\sigma\in\text{dom}(q)\cap{A}^{\star}\\\
\Omega,&\mbox{otherwise}.\end{cases}$

Note that $p$ is a well defined function since the domain of a fair infinite
execution has one unique infinite word. Moreover, we know that $p$ is an
infinite execution because of the given increasing sequence of finite
executions.

Moreover, using (11), we find some $p^{\prime}\in\text{Fair}_{X}$ such that
$q=f\circ p^{\prime}$. Clearly,
$\text{dom}(p)=\text{dom}(q)=\text{dom}(p^{\prime})$. In addition,

$f(p(\sigma))=f(p_{|\sigma|}(\sigma))=q(\sigma)=f(p^{\prime}(\sigma))\qquad\text{(for
any $\sigma\in{A}^{\star}$)}.$

Clearly, $p(\max\text{dom}(q))=\Omega=p^{\prime}(\max\text{dom}(q))$ by the
construction of an infinite execution. Thus, $p=_{\mathcal{R}}p^{\prime}$. So,
from Definition 4.7(2), we conclude that $p=\bigsqcup_{i\in{\rm
Nature}}p_{i}\in\text{Fair}_{X}$.

It remains to show that 2 holds. So, assume $f(x)$. By definition of $f$it
follows that $[x]$, which means there exist $x_{1}\in[x],x_{2}\in y$ such that
$x_{1}$. By Definition 4.7(1), it follows then that there exists an
$x^{\prime}$ such that $x$, i.e. $f(x_{2})=f(x^{\prime})=y$.

###  B.1 Closure of $\forall$-fair bisimulation relations under relational
composition and union

######  Lemma B.23.

There are two $\forall$-fair bisimulation relations which are not closed under
relational composition.

######  Proof B.24.

Consider the following system $X=\\{\Box_{i},z\mid\Box\in\\{x,y,z\\}\land
i\in\\{1,2,3\\}\\}$:

$x_{1}$$x_{2}$$x_{3}$$z_{1}$$z_{2}$$z_{3}$$z$$y_{1}$$y_{2}$$y_{3}$$a$$a$$a$$a$$a$$a$$b$$b$$b$$b$$b$$b$$b$$\mathcal{R}$$\mathcal{R}^{\prime}$

where dashed and dotted lines show the relations $\mathcal{R}$ and
$\mathcal{R}^{\prime}$, respectively. Furthermore, consider the following
notion of fairness (note that $b^{0}=\varepsilon$):

$\text{Fair}_{X}=\\{p\mid\text{$p$ is an infinite execution on
$X$}\land\forall_{n\in{\rm Nature}}\ p(ab^{n})\in\\{x_{2},z_{2},y_{2}\\}\\}.$

Clearly, $\mathcal{R}$ and $\mathcal{R}^{\prime}$ are two $\forall$-fair
bisimulation relations. However, their composition
$\mathcal{R}^{\prime}\circ\mathcal{R}$ is not a $\forall$-fair bisimulation.
To see this, consider two infinite executions: $\downarrow
a{b}^{\omega}\rTo^{p,q}X$ with $p(\varepsilon)=x_{1}$, $q(\varepsilon)=y_{1}$
and $p(ab^{n})=x_{2}$, $q(ab^{n})=y_{3}$ (for all $n\in{\rm Nature}$).
Moreover, let $p(a{b}^{\omega})=\Omega=q(a{b}^{\omega})$. Clearly,
$p=_{\mathcal{R}^{\prime}\circ\mathcal{R}}q$ because
$p(\varepsilon)\mathcal{R}z\mathcal{R}^{\prime}q(\varepsilon)$ and
$p(ab^{n})\mathcal{R}z\mathcal{R}^{\prime}q(ab^{n})$ (for all $n\in{\rm
Nature}$). Yet, $p$ is a fair execution (i.e., $p\in\text{Fair}_{X}$) and $q$
is an unfair execution (i.e., $q\not\in\text{Fair}_{X}$). Thus the relation
$\mathcal{R}^{\prime}\circ\mathcal{R}$ violates Definition 4.7(2). This shows
that the lemma statement holds if we define $\forall$-fair bisimulation
relations as in [24], i.e., without requiring the underlying relation to be an
equivalence.

Next, we show that how the above counterexample can be modified even if the
underlying relations are equivalence relations. First, notice that both
$\mathcal{R}$ and $\mathcal{R}^{\prime}$ are symmetric relations (dashed lines
and dotted lines are without any arrows). Consider the following extension of
the two relations:

$\displaystyle\mathcal{T}$ $\displaystyle=\
\mathcal{R}\cup\text{id}_{X}\cup\\{(z,z_{2}),(z_{2},z)\\}$
$\displaystyle\mathcal{T}^{\prime}$ $\displaystyle=\
\mathcal{R}^{\prime}\cup\text{id}_{X}\cup\\{(z,z_{3}),(z_{3},z)\\}.$

Clearly, $\mathcal{T}$ is an equivalence relation; notice that the addition of
pairs $(z,z_{2})$ and $(z_{2},z)$ in the relation $\mathcal{R}$ results in a
transitive and symmetric relation. Moreover, $z$ and $z_{2}$ are clearly
$\forall$-fair bisimilar. On similar grounds, we can argue that
$\mathcal{T}^{\prime}$ is a $\forall$-fair bisimulation relation. However, it
is straightforward to see that the relation $\mathcal{T}\mathcal{T}^{\prime}$
is not an equivalence relation because it is not transitive
($(x_{1},z_{1}),(z_{1},y_{1})\in\mathcal{T}\mathcal{T}^{\prime}$; however,
$(x_{1},y_{1})\not\in\mathcal{T}\mathcal{T}^{\prime}$). Thus,
$\mathcal{T}\mathcal{T}^{\prime}$ is not a $\forall$-fair bisimulation
relation. ∎

######  Lemma B.25.

There are two $\forall$-fair bisimulation relations which are not closed under
union. This still holds if we restrict to Streett fairness constraints rather
than arbitrary fairness constraints.

######  Proof B.26.

Consider the following system $X=\\{\Box_{i}\mid\Box\in\\{x,y\\}\land
i\in\\{1,2\\}\\}$:

$x_{1}$$y_{1}$$x_{2}$$y_{2}$$a$$a$$a$$a$$a$$a$$a$$a$

whose fairness predicate is defined as follows:

$\text{Fair}_{X}=\\{p\mid|\\{n\in\mathbb{N}\mid
p(a^{n})=x_{i}\\}|=|\\{n\in\mathbb{N}\mid
p(a^{n})=y_{i}\\}|,i\in\\{1,2\\}\\}.$

Note that the symbol $p$ in $\text{Fair}_{X}$ is ranged over all the infinite
executions induced by the fair transition system above. Informally, this means
that the state $x_{i}$ is infinitely often reached if, and only if, $y_{i}$
(for $i\in\\{1,2\\}$) is infinitely often reached. It should be noted that
this constraint can be seen to be a Streett constraint specified by the pairs
$(x_{1},y_{1}),(y_{1},x_{1}),(x_{2},y_{2}),(y_{2},x_{2})$.

Next, we construct two $\forall$-fair bisimulation relations:

$\displaystyle\mathcal{R}_{1}=$ $\displaystyle\
\\{(x_{1},y_{2}),(y_{1},x_{2}),(y_{2},x_{1}),(x_{2},y_{1})\\}$
$\displaystyle\mathcal{R}_{2}=$ $\displaystyle\
\\{(x_{1},x_{2}),(y_{1},y_{2}),(x_{2},x_{1}),(y_{2},y_{1})\\}.$

First, we observe that $\mathcal{R}_{1}$ and $\mathcal{R}_{2}$ are both
symmetric. We show for $\mathcal{R}_{2}$ that also (1) and (2) of Definition
4.7 hold; it can be shown completely analogously for $\mathcal{R}_{1}$
(observe the symmetric nature of the system).

  1. (1)

Assume $x_{i}$ then $x_{3-i}$ and $(y_{i},y_{3-i})\in\mathcal{R}_{2}$. If
$x_{i}$ then $x_{3-i}$ and $(x_{i},x_{3-i})\in\mathcal{R}_{2}$. Analogously
for transitions emanating from $y_{i}$.

  2. (2)

Assume $p\in\text{Fair}_{X}$, then for $i=1,2$, we find
$|\\{n\in\mathbb{N}\mid p(a^{n})=x_{i}\\}|=|\\{n\in\mathbb{N}\mid
p(a^{n})=y_{i}\\}|$. Now, if $q=_{\mathcal{R}_{2}}p$, then

$q(\sigma)=\begin{cases}x_{3-i}&\text{if\ }p(\sigma)=x_{i}\\\
y_{3-i}&\text{if\ }p(\sigma)=y_{i}\end{cases},$

i.e. $|\\{n\in\mathbb{N}\mid q(a^{n})=x_{i}\\}|=|\\{n\in\mathbb{N}\mid
p(a^{n})=x_{3-i}\\}|=|\\{n\in\mathbb{N}\mid
p(a^{n})=y_{3-i}\\}|=|\\{n\in\mathbb{N}\mid q(a^{n})=y_{i}\\}|$, thus
$q\in\text{Fair}_{X}$.

Now we consider $\mathcal{R}=\mathcal{R}_{1}\cup\mathcal{R}_{2}$ and the fair
infinite execution $p$ such that

$p(\sigma)=\begin{cases}x_{1}&\text{if\ }|\sigma|\text{\ is\ even}\\\
y_{1}&\text{if\ }|\sigma|\text{\ is\ odd}\end{cases}.$

Moreover, we consider the unfair infinite execution $q$ such that
$q(\sigma)=x_{2}$ for all finite words $\sigma$. Then for all finite words
$\sigma$, we have $p(\sigma)\mathcal{R}q(\sigma)$, because for all $\sigma$ of
even length $p(\sigma)=x_{1}\ \mathcal{R}_{2}\ x_{2}=q(\sigma)$ and for all
$\sigma$ of odd length $p(\sigma)=y_{1}\ \mathcal{R}_{1}\ x_{2}=q(\sigma)$. So
$p=_{\mathcal{R}}q$, but $q$ is not fair, so $\mathcal{R}$ cannot be a
$\forall$-fair bisimulation.

Also note that $\mathcal{R}_{1}$ and $\mathcal{R}_{2}$ can be extended to
equivalence relations by adding just the reflexive pairs (which trivially does
not impact the bisimulation property), so this lemma even holds when
restricted to equivalence relations.

We will now demonstrate why the choice to restrict $\forall$-fair bisimulation
to equivalences rather than merely to symmetric relations 333It is easy to see
that if we do not require $\forall$-fair bisimulations to be symmetric, we
obtain a different notion: Just take two states $x$ and $y$ with a self loop
each, where the (unique) infinite run from $y$ is fair and the one from $x$ is
not, then $x$ could be related to $y$ but not vice-versa. is sensible:
$\forall$-fair bisimulations would not be closed under transitivity otherwise.

######  Lemma B.31.

If we only require $\mathcal{R}$ in the definition of $\forall$-fair
bisimulation to be symmetric rather than an equivalence, then $\forall$-fair
bisimulation is not closed under transitivity.

######  Proof B.32.

Consider the following system $X=\\{x_{i}^{j}\mid i,j\in\mathbb{N}\\}$ over a
single letter alphabet (the action is omitted):
$x_{1}^{1}$$x_{1}^{2}$$x_{1}^{3}$$\dots$$x_{2}^{1}$$x_{2}^{2}$$x_{2}^{3}$$\dots$$\vdots$$\vdots$$\vdots$$\ddots$

Where all infinite executions, except for $x_{1}^{1}\rightarrow
x_{2}^{2}\rightarrow x_{3}^{3}\rightarrow...$ are fair. Let
$\mathcal{R}=\\{(x_{i}^{j},x_{i}^{j+1}),(x_{i}^{j+1},x_{i}^{j}),(x_{i}^{j},x_{i}^{j})\mid
i,j\in\mathbb{N}\\}$, then $\mathcal{R}$ clearly is a $\forall$-fair
bisimulation – except for transitivity of $\mathcal{R}$. The transitive
closure $\mathcal{R}^{\prime}$ of $\mathcal{R}$ is not a $\forall$-fair
bisimulation, though, because $x_{1}^{1}\rightarrow x_{2}^{1}\rightarrow
x_{3}^{1}\rightarrow...=_{\mathcal{R}^{\prime}}x_{1}^{1}\rightarrow
x_{2}^{2}\rightarrow R_{3}^{3}\rightarrow...$, $x_{1}^{1}\rightarrow
x_{2}^{1}\rightarrow x_{3}^{1}\rightarrow...$ is fair, but
$x_{1}^{1}\rightarrow x_{2}^{2}\rightarrow R_{3}^{3}\rightarrow...$ is not.

##  Appendix C Proofs Concerning Section 5

######  Proposition C.1 (Proposition 5.21).

The categories ${A}^{\star}_{\tau},{A}^{\star}$ have binary products.

######  Proof C.2.

Note that ${A}^{\star}_{\tau}={(A\cup\\{\tau\\})}^{\star}$. Therefore, by
showing that ${A}^{\star}$ for arbitrary $A$ has binary products, we also show
that ${A}^{\star}_{\tau}$ does. Moreover, in a poset viewed as a category,
binary product corresponds to meet, so for any
$\sigma,\sigma^{\prime}\in{A}^{\star}$, we define
$\sigma\sqcap\sigma^{\prime}$ as the unique element whose history is
$\downarrow\sigma\cap\downarrow\sigma^{\prime}$. It remains to show that
$\sqcap$ satisfies the universal property of product. Clearly,
$\sigma\sqcap\sigma^{\prime}\preceq\sigma$ and
$\sigma\sqcap\sigma^{\prime}\preceq\sigma^{\prime}$ because
$\downarrow\sigma\supseteq\downarrow\sigma\cap\downarrow\sigma^{\prime}\subseteq\downarrow\sigma^{\prime}$.
Suppose $\sigma\succeq\bar{\sigma}\preceq\sigma^{\prime}$. Then,
$\downarrow\sigma\supseteq\downarrow\bar{\sigma}\subseteq\downarrow\sigma^{\prime}\implies\downarrow\bar{\sigma}\subseteq\downarrow\sigma\cap\downarrow\sigma^{\prime}\implies\bar{\sigma}\preceq\sigma\sqcap\sigma^{\prime}.$

######  Lemma C.3 (Lemma 5.24).

Given a set $J$ and a small category $\mathbf{C}=\coprod_{j\in
J}\mathbf{C}_{j}$ with the natural injections $\iota_{j}$, then for any
functor $F$ from $\mathbf{C}$ to a cocomplete category $\mathbf{D}$, we have

$\varinjlim_{\mathbf{C}}F\cong\coprod_{j\in
J}\varinjlim_{\mathbf{C}_{j}}F\circ\iota_{j}.$

######  Proof C.4.

We are going to use the Yoneda embedding to derive $D\cong D^{\prime}$
whenever $\mathbf{D}(D,\\_)\cong\mathbf{D}(D^{\prime},\\_)$, for any two
objects $D,D^{\prime}\in\mathbf{D}$. Recall the abstract definition of a
colimit from [26]: the colimit $\varinjlim_{\mathbf{C}}F$ is a representation
of the functor $[\mathbf{C},\mathbf{D}](F,\Delta\\_)$, i.e., we have an
isomorphism
$\mathbf{D}(\varinjlim_{\mathbf{C}}F,D)\cong[\mathbf{C},\mathbf{D}](F,\Delta
D)$ natural in $D\in\mathbf{D}$. Thus, we can derive

$\displaystyle\mathbf{D}(\coprod_{j\in
J}\varinjlim_{\mathbf{C}_{j}}F\circ\iota_{j},D)$ $\displaystyle\cong\
\prod_{j\in J}\mathbf{D}(\varinjlim_{\mathbf{C}_{j}}F\circ\iota_{j},D)$
$\displaystyle\cong\ \prod_{j\in
J}[\mathbf{C}_{j},\mathbf{D}](F\circ\iota_{j},\Delta(D)\circ\iota_{j})$
$\displaystyle\cong\ \prod_{j\in
J}\int_{C\in\mathbf{C}_{j}}\mathbf{D}(F\iota_{j}C,\Delta(D)\iota_{j}C)$
$\displaystyle\cong\int_{j\in
J,C\in\mathbf{C}_{j}}\mathbf{D}(F\iota_{j}C,\Delta(D)\iota_{j}C)$
$\displaystyle\cong\ \int_{C\in\mathbf{C}}\mathbf{D}(FC,\Delta DC)$
$\displaystyle\cong\ [\mathbf{C},\mathbf{D}](F,\Delta D)$ $\displaystyle\cong\
\mathbf{D}(\varinjlim_{\mathbf{C}}F,D).$

Clearly, all the isomorphisms are natural in $D$; thus, we obtain the desired
isomorphism from the Yoneda embedding.

######  Theorem C.5 (Theorem 5.25).

For a given transition system $(X,A_{\tau},\rightarrow)$ and
$\varrho\in{A}^{\star}$, we have

$\Sigma_{h}F_{X}(\varrho)\cong\text{MExec}(X,\varrho).$

######  Proof C.6.

Notice that the result in (8) can be seen as the colimit of the diagram:

${A_{\tau,\varrho}^{\star}}^{\text{op}}\rEmbedding^{\iota_{\varrho}}{{A}^{\star}_{\tau}}^{\text{op}}\rTo^{F_{X}}\mathbf{Set},$

where
$A_{\tau,\varrho}^{\star}=\\{\sigma\in{A}^{\star}_{\tau}\mid\varrho\preceq
h(\sigma)\\}$ is a sub-forest of ${A}^{\star}_{\tau}$. Clearly, we can
decompose the ordered set in the following way. Here, $M(\varrho)$ is the set
of minimal words $\sigma$ such that $h(\sigma)=\varrho$, i.e.,
$M(\varrho)=\\{\sigma\in{A}^{\star}_{\tau}\mid\downarrow\sigma\cap
h\raisebox{4.95134pt}{$\scriptscriptstyle-\\!1$}(\varrho)=\\{\sigma\\}\\}$:

$A_{\tau,\varrho}^{\star}\cong\coprod_{\sigma\in
M(\varrho)}\\{\sigma^{\prime}\mid\sigma\preceq\sigma^{\prime}\\}.$

This decomposition is due to the downward totality of the set
${A}^{\star}_{\tau}$. Lemma 5.24 is now applicable and, upon applying, results
in the following isomorphism:

$\varinjlim_{\sigma\in
A_{\tau,\varrho}^{\star}}F_{X}\iota_{\varrho}\sigma\cong\coprod_{\sigma\in
M(\varrho)}\varinjlim_{\sigma^{\prime}\succeq\sigma}F_{X}(\sigma^{\prime}).$

Notice that the index category
$\\{\sigma^{\prime}\mid\sigma^{\prime}\succeq\sigma\\}$ (for each
$\sigma\in{A}^{\star}_{\tau}$) is a directed set; thus, the colimit
$\varinjlim_{\sigma^{\prime}\succeq\sigma}F_{X}(\sigma^{\prime})$ can be
computed using (9). Next, we claim that for any $\sigma\in M(\varrho)$, we
have the following isomorphism:

$\varinjlim_{\sigma^{\prime}\succeq\sigma}F_{X}(\sigma^{\prime})\cong\text{Exec}(X,\sigma).$
(12)

Next, define two maps
$\varinjlim_{\sigma^{\prime}\succeq\sigma}F_{X}(\sigma^{\prime})\pile{\rTo~{}f\\\
\lTo~{}g}\text{Exec}(X,\sigma)$:

$f[p,\sigma^{\prime}]_{\sim}=p\cdot\sigma\ \text{(for
$p\in\text{Exec}(X,\sigma^{\prime})$)}\qquad g(p)=[p,\sigma]_{\sim}\
\text{(for $p\in\text{Exec}(X,\sigma)$)}.$

The function $f$ is well-defined because
$(p_{1},\sigma_{1})\sim(p_{2},\sigma_{2})\implies\exists_{\sigma_{3}}(\sigma_{1}\succeq\sigma_{3}\preceq\sigma_{2}\land
p_{1}\cdot\sigma_{3}=p_{2}\cdot\sigma_{3})\implies
p_{1}\cdot\sigma=p_{2}\cdot\sigma$ (the last implication is because
$\sigma\preceq\sigma_{3}$). Moreover,
$f(g(p))=f([p,\sigma]_{\sim})=p\cdot\sigma=p$ and
$g(f([p,\sigma^{\prime}]_{\sim}))=g(p\cdot\sigma)=[p,\sigma^{\prime}]_{\sim}$
because
$(p\cdot\sigma)\cdot\sigma=p\cdot\sigma\implies(p\cdot\sigma,\sigma)\sim(p,\sigma^{\prime})$.

Thus, the isomorphism in (12) holds. Lastly, using (14), it is clear that
$\coprod_{\sigma\in
M(\varrho)}\text{Exec}(X,\sigma)\cong\text{MExec}(X,\varrho)$.

######  Theorem C.7 (Theorem 5.26).

For any $\varrho,\varrho^{\prime}\in{A}^{\star}$ with
$\varrho^{\prime}\preceq\varrho$, the square in (LABEL:eq:naturality-mexec)
commutes.

######  Proof C.8.

Recall the construction of the map $\Sigma_{h}(\varrho,\varrho^{\prime})$ (for
$\varrho^{\prime}\preceq\varrho$) and recall the following diagram
(LABEL:eq:sigma_h-action). Note that
$\sigma_{\varrho^{\prime}}=\bigsqcap\\{\sigma^{\prime}\preceq\sigma\mid
h(\sigma^{\prime})=\varrho^{\prime}\\}$ is a unique minimal word
$\sigma^{\prime}$ in the history of $\sigma$ with
$h(\sigma^{\prime})=\varrho$.

Furthermore, from the proof of Theorem 5.25, we know that

$\varinjlim_{\sigma\in
A_{\tau,\varrho}^{*}}F_{X}(\iota_{\varrho}(\sigma))\cong\coprod_{\sigma\in
M(\varrho)}\varinjlim_{\sigma^{\prime}\succeq\sigma}F_{X}(\sigma^{\prime})\cong\coprod_{\sigma\in
M(\varrho)}F_{X}(\sigma).$

Thus, the injections of the above colimit (or the vertical arrows in the
square drawn below) map an execution $p\in F_{X}(\sigma)$ (for some
$h(\sigma)=\varrho$) to a minimal execution $p\cdot\sigma_{\varrho}\in
F_{X}(\sigma_{\varrho})$.  Consider an execution $p\in F_{X}(\sigma)$.
Clearly, $\sigma_{\varrho^{\prime}}\preceq\sigma$ and using (14), we find that
$p\cdot\sigma_{\varrho^{\prime}}\in\coprod_{\sigma\in
M(\varrho)}F_{X}(\sigma)$. From the commutativity of the above square, we
obtain

$p\cdot\sigma_{\varrho^{\prime}}=\Sigma_{h}(\varrho,\varrho^{\prime})(p\cdot\sigma_{\varrho}).$
(13)

Thus, we can simplify the action $\Sigma_{h}(\varrho,\varrho^{\prime})$ in
terms of a map:

$\coprod_{\sigma\in
M(\varrho)}F_{X}(\sigma)\rTo^{f(\varrho,\varrho^{\prime})}\coprod_{\sigma\in
M(\varrho^{\prime})}F_{X}(\sigma),\ \text{where
$f(\varrho,\varrho^{\prime})(p,\sigma)=(p\cdot{\sigma_{\varrho^{\prime}}},\sigma_{\varrho^{\prime}})$}.$

Next, we further simplify the elements of the set $\coprod_{\sigma\in
M(\varrho)}F_{X}(\sigma)$:

$\forall_{p}\ \Big{(}p\in\text{MExec}(X,\varrho)\iff\max\text{dom}(p)\in
M(\varrho)\Big{)}.$ (14)

  * $\Leftarrow$

Let $\max\text{dom}(p)\in M(\varrho)$, for some $p$. Further, suppose

$p^{\prime}\in\downarrow p\cap\\{q\in\text{Exec}(X)\mid
h(\max\text{dom}(q))=\varrho\\}.$

Clearly, $p^{\prime}\preceq p$ and $h(\max\text{dom}(p^{\prime}))=\varrho$.
Then $\max\text{dom}(p^{\prime})\preceq\max\text{dom}(p)$ and since
$\max\text{dom}(p)\in M(\varrho)$, we find that
$\max\text{dom}(p^{\prime})=\max\text{dom}(p)$. Thus, $p^{\prime}=p$.

  * $\Rightarrow$

Let $p\in\text{MExec}(X,\varrho)$ and let $\max\text{dom}(p)=\sigma$, for some
$\sigma$. Then $\downarrow p\cap\\{q\in\text{Exec}(X)\mid
h(\max\text{dom}(q))=\varrho\\}=\\{p\\}$. Moreover, $\downarrow\sigma\cap
h\raisebox{4.95134pt}{$\scriptscriptstyle-\\!1$}(\varrho)\neq\emptyset$
because $h(\sigma)=\varrho$. So, let $\sigma^{\prime}\preceq\sigma$ such that
$h(\sigma^{\prime})=\varrho$. Then $p\cdot\sigma^{\prime}\preceq p$. However,
since $p$ is minimal, we find that $p\cdot\sigma^{\prime}=p$, i.e.,
$\sigma^{\prime}=\sigma$.

To prove this theorem it remains to show that the above square commutes where
$\pi_{\\_}$ forgets the domain of a minimal execution. This is trivial since
$\text{mpast}(\varrho,\varrho^{\prime})\circ\pi_{\varrho}(p,\sigma)=p|_{\downarrow\sigma_{\varrho^{\prime}}}=p\cdot\sigma_{\varrho^{\prime}}=\pi_{\varrho^{\prime}}\circ
f(\varrho,\varrho^{\prime})(p,\sigma)$.

######  Lemma C.9 (Lemma 5.33).

For a given branching simulation $X\rTo^{f}Y$ and a minimal execution
$p\in\text{MExec}(X,\varrho)$, we have $p_{f}\in\text{MExec}(Y,\varrho)$.

######  Proof C.10.

Let $p\in\text{MExec}(X,\varrho)$. We prove this lemma by performing
structural induction on $p$.

  * •

If $\text{dom}(p)=\varepsilon$, then $\text{dom}(p_{f})=\varepsilon$,
$p_{f}(\varepsilon)=f(p(\varepsilon))$ is trivially minimal.

  * •

If $p^{\prime}$ and $a\in A$, then $p_{f}^{\prime}$ and
$\text{last}(q)=f(\text{last}(p))$, thus, $p_{f}=q$. By induction hypothesis,
$p_{f}^{\prime}$ is minimal at
$\varrho^{\prime}=h(\max\text{dom}(p^{\prime}))$ (i.e.,
$p_{f}^{\prime}\in\text{MExec}(Y,\varrho^{\prime})$) and since $p$ ends with a
transition labelled $a\in A$, we know that $p_{f}$ is also minimal at
$\varrho^{\prime}a$.

  * •

If $p^{\prime}$ then $p$ and $p^{\prime}$ have the same observable trace. Yet,
this case is inapplicable since $p^{\prime}\prec p$ and thus, $p$ is not
minimal.

######  Theorem C.14 (Theorem 5.34).

The above mapping
$\mathbf{LTS}_{\tau}\rTo^{\llbracket\\_\rrbracket}\mathbf{PSh}({A}^{\star})$
is a faithful functor.

######  Proof C.15.

Lemma 5.33 ensures that for any $p\in\Sigma_{h}F_{X}\varrho$, we also have
$p_{f}\in\Sigma_{h}F_{Y}\varrho$. We use the isomorphic view and show that
$\llbracket f\rrbracket$ is a natural transformation, i.e., for any
$\varrho^{\prime}\preceq\varrho$, we have
$\text{mpast}(\varrho,\varrho^{\prime})\circ\llbracket
f\rrbracket_{\varrho}=\llbracket
f\rrbracket_{\varrho^{\prime}}\circ\text{mpast}(\varrho,\varrho^{\prime})$. So
let $p\in\text{MExec}(X,\varrho)$ with $\sigma=\max\text{dom}(p)$ and
$\sigma^{\prime}=\max\text{dom}(p_{f})$. Then

$\displaystyle\ \text{mpast}(\varrho,\varrho^{\prime})\circ\llbracket
f\rrbracket_{\varrho}(p)=\llbracket
f\rrbracket_{\varrho^{\prime}}\circ\text{mpast}(\varrho,\varrho^{\prime})(p)$
$\displaystyle\iff$ $\displaystyle\
\text{mpast}(\varrho,\varrho^{\prime})(p_{f})=\llbracket
f\rrbracket_{\varrho^{\prime}}(p\mid_{\downarrow\varrho^{\prime}})$
$\displaystyle\iff$ $\displaystyle\
p_{f}\cdot\sigma^{\prime}_{\varrho^{\prime}}=(p\cdot\sigma_{\varrho^{\prime}})_{f}.$
(15)

This we can show by structural induction on $p$. For the base case, let
$p=\varepsilon_{x}$. Then $\varrho^{\prime}=\varrho=\varepsilon$ and
$p_{f}\cdot\sigma^{\prime}_{\varrho^{\prime}}=\varepsilon_{f(x)}=(p\cdot\sigma_{\varrho^{\prime}})_{f}$.
For the inductive case, let $p^{\prime}$ with $p\in\text{MExec}(X,\varrho)$
and $\max\text{dom}(p^{\prime})=\sigma$. Clearly, $a\in A$, otherwise, if
$a=\tau$, then $p$ is not minimal. Note that $(\sigma
a)_{\varrho^{\prime}}=\sigma_{\varrho^{\prime}}$ and thus,

$p\cdot(\sigma a)_{\varrho^{\prime}}=p|_{\downarrow(\sigma
a)_{\varrho^{\prime}}}=p|_{\downarrow\sigma_{\varrho^{\prime}}}=p^{\prime}|_{\downarrow\sigma_{\varrho^{\prime}}}=p^{\prime}\cdot\sigma_{\varrho^{\prime}}.$
(16)

Note that $p^{\prime}$ may not be a minimal execution at $\varrho^{\prime}$;
yet,
$p^{\prime}\cdot\sigma_{\varrho^{\prime}}\in\text{MExec}(X,\varrho^{\prime})$
is minimal due to Equation (14). Let
$\sigma^{\prime}=\max\text{dom}((p^{\prime}\cdot\sigma_{\varrho^{\prime}})_{f})$.
From Lemma 5.33, we know that
$(p^{\prime}\cdot\sigma_{\varrho^{\prime}})_{f}\in\text{MExec}(Y,\varrho^{\prime})$.
Then, by the induction hypothesis and substituting $p$ by
$p^{\prime}\cdot\sigma_{\varrho^{\prime}}$ in (15) we obtain:

$(p^{\prime}\cdot\sigma_{\varrho^{\prime}})_{f}\cdot\sigma^{\prime}_{\varrho^{\prime}}=((p^{\prime}\cdot\sigma_{\varrho^{\prime}})\cdot\sigma_{\varrho^{\prime}})_{f}=(p^{\prime}\cdot\sigma_{\varrho^{\prime}})_{f}$
(17)

Moreover, by the definition of $p_{f}$, we find that
$(p^{\prime}\cdot\sigma_{\varrho^{\prime}})_{f}\ext@arrow
0359\arrowfill@\relbar\relbar\twoheadrightarrow{}{\tau^{n}}{}p^{\prime}_{f}$
with $\text{dom}(p_{f})=\sigma^{\prime}\tau^{n}a$, for some $n\in{\rm
Nature}$. Note that
$p_{f}^{\prime}=(p^{\prime}\cdot\sigma_{\varrho^{\prime}})_{f}$, whenever
$n=0$. Then we find
$(\sigma^{\prime}\tau^{n}a)_{\varrho^{\prime}}=\sigma^{\prime}_{\varrho^{\prime}}$
because $\sigma^{\prime}\prec\sigma^{\prime}\tau^{n}a$. Thus, we have

$p_{f}\cdot(\sigma^{\prime}\tau^{n}a)_{\varrho^{\prime}}=p_{f}|_{\downarrow(\sigma^{\prime}\tau^{n}a)_{\varrho^{\prime}}}=p_{f}|_{\downarrow\sigma^{\prime}_{\varrho^{\prime}}}=(p_{f}^{\prime}\cdot\sigma_{\varrho^{\prime}})_{f}|_{\downarrow\sigma^{\prime}_{\varrho^{\prime}}}=(p_{f}^{\prime}\cdot\sigma_{\varrho^{\prime}})_{f}\cdot\sigma^{\prime}_{\varrho^{\prime}}.$

Using the above equation, (16), and (17), we can conclude that

$(p\cdot(\sigma
a)_{\varrho^{\prime}})_{f}=(p^{\prime}\cdot\sigma_{\varrho^{\prime}})_{f}=(p_{f}^{\prime}\cdot\sigma_{\varrho^{\prime}})_{f}\cdot\sigma^{\prime}_{\varrho^{\prime}}=p_{f}\cdot(\sigma^{\prime}\tau^{n}a)_{\varrho^{\prime}}.$

The faithfulness of $\llbracket\\_\rrbracket$ is similar to the strong case
since empty executions are always minimal executions.

######  Proposition C.18 (Proposition 5.39).

The above mapping ${{\rm Nature}}^{\text{op}}\rTo^{\mathcal{O}}\mathbf{Set}$
is a presheaf.

######  Proof C.19.

We need to show that $\mathcal{O}$ is a functor:

  * •

$\mathcal{O}$ preserves identities: Let $\sigma\in\mathcal{O}(n)$, then

$\sigma\cdot n=\begin{cases}\varepsilon&\text{if\
}n=0\wedge\sigma=\bar{\tau}\\\ \bar{\tau}&\text{if\
}n>0\wedge\sigma=\bar{\tau}\\\ \sigma\mid_{n}&\text{if\
}\sigma\neq\bar{\tau}\end{cases}=\begin{cases}\bar{\tau}&\text{if\
}n>0\wedge\sigma=\bar{\tau}\\\ \sigma&\text{if\
}\sigma\neq\bar{\tau}\end{cases}=\sigma$

  * •

$\mathcal{O}$ respects composition: Let $\sigma\in\mathcal{O}(n)$; $l\leq
m\leq n$, then:

$\displaystyle(\sigma\cdot m)\cdot l=\begin{cases}\varepsilon\cdot l&\text{if\
}m=0\wedge\sigma=\bar{\tau}\\\ \bar{\tau}\cdot l&\text{if\
}m>0\wedge\sigma=\bar{\tau}\\\ \sigma\mid_{m}\cdot l&\text{if\
}\sigma\neq\bar{\tau}\end{cases}$ $\displaystyle=$
$\displaystyle\begin{cases}\varepsilon\mid_{l}&\text{if\
}m=0\wedge\sigma=\bar{\tau}\\\ \bar{\tau}&\text{if\
}l>0\wedge\sigma=\bar{\tau}\\\ \varepsilon&\text{if\ }l=0\wedge
m>0\wedge\sigma=\bar{\tau}\\\ (\sigma\mid_{m})\mid_{l}&\text{if\
}\sigma\neq\bar{\tau}\end{cases}=\begin{cases}\varepsilon&\text{if\
}l=0\wedge\sigma=\bar{\tau}\\\ \bar{\tau}&\text{if\
}l>0\wedge\sigma=\bar{\tau}\\\ \sigma\mid_{l}&\text{if\
}\sigma\neq\bar{\tau}\end{cases}=\sigma\cdot l$

######  Proposition C.20 (Proposition 5.43).

The mapping $\bar{F}_{X}$ induced by a transition system
$(X,A_{\tau},\rightarrow)$ is a contravariant functor.

######  Proof C.21.

  * •

Preservation of identities: Let $p\in\bar{F}_{X}(\sigma)$. Then

$p\cdot\sigma=\begin{cases}p&\text{if\ }\exists
n\in\mathbb{N},\sigma=(n,\overline{\tau})\\\
p\mid_{\downarrow\sigma}&\text{if\ }\sigma\in{A}^{\star}_{\tau}\end{cases}=p.$

  * •

Respecting composition: Let $\sigma_{3}\preceq\sigma_{2}\preceq\sigma_{1}$ and
let $p\in\bar{F}_{X}(\sigma_{1})$, for some $p\in\text{Exec}(X)$ and
$\sigma_{1},\sigma_{2},\sigma_{3}\in A_{\tau\bar{\tau}}^{\star}$. Then, we
need to prove

$(p\cdot\sigma_{2})\cdot\sigma_{3}=p\cdot\sigma_{3}.$ (18)

We do the following case distinction to prove the above equation.

    1. (1)

Let $\sigma_{1}\in{A}^{\star}_{\tau}$. Then, by the construction of
$A_{\tau\bar{\tau}}^{\star}$, we know that
$\sigma_{3},\sigma_{2}\in{A}^{\star}_{\tau}$. Moreover,
$(p\cdot\sigma_{2})\cdot\sigma_{3}=(p|_{\downarrow\sigma_{2}})|_{\downarrow\sigma_{3}}=p|_{\downarrow\sigma_{3}}=p\cdot\sigma_{3}$
since $\downarrow\sigma_{3}\subseteq\downarrow\sigma_{2}$.

    2. (2)

Let $\sigma_{1}\not\in{A}^{\star}_{\tau}$. Then,
$\sigma_{1}=(n_{1},\bar{\tau})$, for some $n_{1}>0$.

      1. (a)

Let $\sigma_{2}\in{A}^{\star}_{\tau}$. Then, $\sigma_{2}=\varepsilon$ and
$\sigma_{3}=\varepsilon$. Moreover,
$(p\cdot\sigma_{2})\cdot\sigma_{3}=(p|_{\\{\varepsilon\\}})|_{\\{\varepsilon\\}}=p|_{\\{\varepsilon\\}}=p\cdot\sigma_{3}$.

      2. (b)

Let $\sigma_{2}\not\in{A}^{\star}_{\tau}$. Then,
$\sigma_{2}=(n_{2},\bar{\tau})$, for some $n_{2}>0$ and $n_{2}\leq n_{1}$. We
further distinguish the following cases:

        1. i.

Let $\sigma_{3}\in{A}^{\star}_{\tau}$. Then, $\sigma_{3}=\varepsilon$.
Moreover,
$(p\cdot\sigma_{2})\cdot\sigma_{3}=p|_{\\{\varepsilon\\}}=p\cdot\sigma_{3}$.

        2. ii.

Let $\sigma_{3}\not\in{A}^{\star}_{\tau}$. Then,
$\sigma_{3}=(n_{3},\bar{\tau})$, for some $n_{3}>0$ and $n_{3}\leq n_{2}$.
Moreover, $(p\cdot\sigma_{2})\cdot\sigma_{3}=p=p\cdot\sigma_{3}$.

######  Theorem C.22 (Theorem 5.44).

For a given transition system $(X,A_{\tau},\rightarrow)$, we find that

$\Sigma_{\bar{h}}\bar{F}_{X}(\bar{\tau})\cong\coprod_{n\in{\rm
Nature}}\text{Exec}(X,\tau^{n}),\qquad\Sigma_{\bar{h}}\bar{F}_{X}(\varrho)\cong\text{MExec}(X,\varrho)\quad(\text{for
any $\varrho\neq\bar{\tau}$}).$

Moreover, the above isomorphisms are natural in $\varrho\in
A_{\bar{\tau}}^{\star}$. I.e., for any $\varrho^{\prime}\preceq\varrho$ with
$\varrho,\varrho^{\prime}\in{A}^{\star}$, the square in (LABEL:eq:naturality-
mexec) and the following square commute.

######  Proof C.23.

Most of the proof remains similar to the proof of Theorem 5.25. For instance,
the case when $\varrho\in{A}^{\star}\setminus\\{\varepsilon\\}$ remains
unchanged due to the way $\bar{h}$ is constructed. The calculation when
$\varrho=\varepsilon$ also remains similar except that we have to consider
terms $\bar{F}_{X}(n,\bar{\tau})$ (for $n>0$), which are pairwise equivalent
by the way, i.e., for all $n,m>0$ we have
$\bar{F}_{X}(n,\bar{\tau})=F_{X}(m,\bar{\tau})$. Moreover, the structure
${A_{\tau\bar{\tau}}^{\star}}^{\text{op}}$ is directed, i.e., we can compute
the colimit using (9). Also, since
$\bar{F}_{X}(n,\bar{\tau})=\coprod_{m\in{\rm Nature}}\text{Exec}(X,\tau^{m})$,
we have
$\Sigma_{\bar{h}}\bar{F}_{X}(\varepsilon)\cong\text{MExec}(X,\varepsilon)$.

The only difference in computation is when $\varrho=\bar{\tau}$. In this case,
we have to take the colimit over the decreasing sequence
$(1,\bar{\tau})\succ(2,\bar{\tau})\succ\cdots$ and we observe that the action
of $\bar{F}_{X}$ between any two elements in this sequence is an identity on
the set $\coprod_{n\in{\rm Nature}}\text{Exec}(X,\tau^{n})$. Thus, we conclude
that $\Sigma_{\bar{h}}\bar{F}_{X}(\bar{\tau})\cong\coprod_{n\in{\rm
Nature}}\text{Exec}(X,\tau^{n})$.

Next, we need to show that the square drawn in the theorem statement commutes.
For this, we recall that
$\Sigma_{\bar{h}}\bar{F}_{X}(\bar{\tau})\cong\varinjlim_{\bar{\tau}\succeq\bar{h}(n,\bar{\tau})}\bar{F}_{X}(n,\bar{\tau})$.
So due to the universal property of the colimits, we have the following
commutative square. Notice that the vertical arrows, which are the injections
of the corresponding colimits, are identities. The left vertical arrow is an
identity because the restriction of $\bar{F}_{X}$ between any two elements
having the constant $\bar{\tau}$ (say,
$(n^{\prime},\bar{\tau})\preceq(n,\bar{\tau})$) is an identity, i.e.,
$p\cdot(n^{\prime},\bar{\tau})=p$ (for any $p\in\bar{F}_{X}(n,\bar{\tau})$).
The right vertical arrow is an identity because the elements in
$\bar{F}_{X}(\varepsilon)$ are already minimal elements w.r.t.
$\varrho=\varepsilon$. Thus, for any $p\in\bar{F}_{X}(n,\bar{\tau})$, we
conclude that $\Sigma_{\bar{h}}(\bar{\tau},\varepsilon)(p)=p|_{\varepsilon}$.

######  Lemma C.24 (Lemma 5.45).

The mapping $\llbracket f\rrbracket$ induced by a branching simulation $f$
between $(X,A_{\tau},\rightarrow),(Y,A_{\tau},\rightarrow)$ is a faithful
functor.

######  Proof C.25.

The proof is the same as Theorem 5.34, except that we have to prove the
commutativity of the following naturality square when
$\varrho^{\prime}=\varepsilon\preceq\bar{\tau}=\varrho$. Let
$p\in\coprod_{n\in{\rm Nature}}\text{Exec}(X,\tau^{n})$. Then there is some
$x\in X$ such that $\varepsilon_{x}\ext@arrow
0359\arrowfill@\relbar\relbar\twoheadrightarrow{}{\tau^{n}}{}p$, for some
$n\in{\rm Nature}$. Moreover, by the definition of ${\\_}_{f}$, we can deduce
$\varepsilon_{f(x)}\ext@arrow
0359\arrowfill@\relbar\relbar\twoheadrightarrow{}{\tau^{m}}{}p_{f}$, for some
$m\leq n$. Clearly, we have $\llbracket
f\rrbracket_{\varepsilon}(p|_{\varepsilon})=\varepsilon_{f(x)}=(p_{f})|_{\varepsilon}=(\llbracket
f\rrbracket_{\bar{\tau}}p)|_{\varepsilon}$.

######  Theorem C.26 (Theorem 5.46).

A branching simulation function $f$ is a branching bisimulation function if,
and only if, the induced map $\llbracket f\rrbracket$ is a bisimulation map in
$\mathbf{PSh}(A_{\bar{\tau}}^{\star})$.

######  Proof C.27.

$\Rightarrow$ Consider the commutative square as depicted below in
$\mathbf{PSh}(A_{\bar{\tau}}^{\star})$.

$\begin{diagram}$ (19)

We prove the existence of $Q\rTo^{k}\llbracket X\rrbracket$ by structural
induction on the elements $\varrho\in A_{\bar{\tau}}^{\star}$. For the base
case, let $\varrho=\varepsilon$. Notice that the map $\llbracket
f\rrbracket_{\varepsilon}$ is surjective since the given $f$ is surjective.
Moreover, since every epi splits in $\mathbf{Set}$, there is a map $\llbracket
Y\rrbracket(\varepsilon)\rTo^{h}\llbracket X\rrbracket(\varepsilon)$ such that
$\llbracket f\rrbracket_{\varepsilon}\circ h=\text{id}_{\llbracket
Y\rrbracket(\varepsilon)}$. Thus, we define

$k_{\varepsilon}(q)=\begin{cases}m_{\varepsilon}(g\raisebox{4.95134pt}{$\scriptscriptstyle-\\!1$}_{\varepsilon}(q)),&\text{if}\
q\in g_{\varepsilon}P(\varepsilon)\\\
h(n_{\varepsilon}(q)),&\text{otherwise}.\end{cases}$

Clearly, $\llbracket f\rrbracket_{\varepsilon}\circ
k_{\varepsilon}=n_{\varepsilon}$ and $k_{\varepsilon}\circ
g_{\varepsilon}=m_{\varepsilon}$.

Before we tackle the inductive case, we prove the following claim:

$\forall_{p\in\text{Exec}(X),q\in\text{Exec}(Y)}\ p_{f}$ (20)

To see this, let $p_{f}$. Then, we find that $\text{last}(p_{f})$. Using the
reflection of $\tau$-transition (i.e., (6)) we find that there are states
$x,x^{\prime}\in X$ such that $\text{last}(p_{f})\ext@arrow
0359\arrowfill@\relbar\relbar\twoheadrightarrow{}{\varepsilon}{}x$ and
$fx=\text{last}(p_{f}),fx^{\prime}=\text{last}(q)$. Let $\bar{p},p^{\prime}$
be the extension of $p$ that ends in states $x,x^{\prime}$, respectively. To
complete the proof, it suffices to show that $\bar{p}_{f}=p_{f}$. And this
follows directly from the fact that $f$ satisfies the stuttering of
$\tau$-transitions (i.e., (5)). This completes the proof of Claim 20.

For the inductive case, consider a family of functions $k_{\varrho^{\prime}}$
(for each $\varrho^{\prime}\preceq\varrho$) such that

  1. (1)

$k$ is a natural transformation up to $\varrho$, i.e.,
$n_{\varrho^{\prime\prime}}(q\cdot\varrho^{\prime\prime})=(n_{\varrho^{\prime}}(q))\cdot\varrho^{\prime\prime}$,
for any $\varrho^{\prime\prime}\preceq\varrho^{\prime}\preceq\varrho$ and
$q\in Q(\varrho^{\prime})$;

  2. (2)

the lower triangle commutes up to $\varrho$, i.e., $k_{\varrho^{\prime}}\circ
g_{\varrho^{\prime}}=m_{\varrho^{\prime}}$ (for any
$\varrho^{\prime}\preceq\varrho$);

  3. (3)

the upper triangle commutes up to $\varrho$, i.e., $\llbracket
f\rrbracket_{\varrho^{\prime}}\circ k_{\varrho^{\prime}}=n_{\varrho^{\prime}}$
(for any $\varrho^{\prime}\preceq\varrho$).

We are now going to construct a function $k_{\varrho a}$ such that the desired
properties (as described in the above inductive hypothesis) are satisfied.

Let $\bar{q}\in Q(\varrho a)$ and assume that $\bar{q}\not\in g_{\varrho
a}P(\varrho a)$ (otherwise, simply take $k_{\varrho a}(\bar{q})=m_{\varrho
a}(g\raisebox{4.95134pt}{$\scriptscriptstyle-\\!1$}_{\varrho a}(\bar{q}))$).
Then there are some $q^{\prime}\in Q(\varrho)$ and $q\in\llbracket
Y\rrbracket(\varrho)$ such that $q^{\prime}=\bar{q}\cdot\varrho$,
$n_{\varrho}(q^{\prime})=q$, and $q=(n_{\varrho a}(\bar{q}))\cdot\varrho$. By
induction hypothesis, we find a minimal execution
$p\in\text{MExec}(X,\varrho)$ such that $k_{\varrho}(q^{\prime})=p$ and
$\llbracket f\rrbracket_{\varrho}(p)=q$. Thus, $\text{last}(p_{f})\ext@arrow
0359\arrowfill@\relbar\relbar\twoheadrightarrow{}{}{}y$, for some $y\in Y$.
Using (6), we find a matching sequence of transitions
$\text{last}(p)\ext@arrow
0359\arrowfill@\relbar\relbar\twoheadrightarrow{}{}{}x$ (for some
$x,x^{\prime}$) such that $f(x)=y$ and $f(x^{\prime})=\text{last}(n_{\varrho
a}(\bar{q}))$. Let $p^{\prime}$ be the extension of $p$ which witnesses the
above sequence transitions that end in states $x^{\prime}$. Clearly,
$\bar{p}\in\text{MExec}(X,\varrho a)$ and $\bar{p}\cdot\varrho=p$. Moreover,
$\llbracket f\rrbracket_{\varrho a}(\bar{p})=\bar{p}_{f}=n_{\varrho
a}(\bar{q})$ follows directly from Claim 20. Therefore, we let $k_{\varrho
a}(\bar{q})=p^{\prime}$. Clearly, $(k_{\varrho
a}(\bar{q}))\cdot\varrho=k_{\varrho}(\bar{q}\cdot\varrho)$. Moreover,
$\llbracket f\rrbracket_{\varrho a}(k_{\varrho a}(\bar{q}))=n_{\varrho
a}(\bar{q})$; thus, the upper triangle commutes up to $\varrho a$. Lastly,
commutativity of the lower triangle up to $\varrho a$ follows directly from
$k_{\varrho}$.

The argument for the remaining case $\bar{\tau}$ is analogous to the induction
step above, where $\varepsilon$ plays the role of $\varrho$. Note that then
$q=\varepsilon_{\tilde{y}}$ for some $\tilde{y}\in Y$,
$p=\varepsilon_{\tilde{x}}$ for some $\tilde{x}\in X$. and we find the
execution $p^{\prime}$ to be in $\coprod_{n\in{\rm
Nature}}\text{Exec}(X,\tau^{n})$.

$\Leftarrow$ We have to show two properties: $f$ is surjective and $f$
satisfies the reflection property (6), which we will in turn differentiate
according to whether a silent or non-silent action is being considered.

  * •

First, we show that $f$ is surjective. From Theorem 3.3 we know that
$\llbracket f\rrbracket_{\varepsilon}$ is surjective. So for any $y\in Y$,
there is some $x\in X$ such that $\llbracket
f\rrbracket_{\varepsilon}(\varepsilon_{x})=\varepsilon_{f(x)}=\varepsilon_{y}$.
Thus, $f(x)=y$ and so $f$ must be surjective.

  * •

Let $f(x)$, $a\in A$. We let $q$ be the execution that corresponds to the
transition $f(x)$. Now construct two presheaves in
$\mathbf{PSh}(A_{\bar{\tau}}^{\star})$:

    * –

$P(\varepsilon)=\\{\varepsilon_{x}\\}$ and $P(\varrho)=\emptyset$ (for
$\varrho\neq\varepsilon$).

    * –

$Q(\varepsilon)=\\{\varepsilon_{f(x)}\\},Q(a)=\\{q\\},Q(\varrho)=\emptyset$
(for $\varrho\not\in\\{\varepsilon,a\\}$) with
$q\cdot\varepsilon=\varepsilon_{f(x)}$.

Consider the square in (19) with the maps
$g_{\varepsilon}(\varepsilon_{x})=\varepsilon_{f(x)}$,
$m_{\varepsilon}(\varepsilon_{x})=\varepsilon_{x}$,
$n_{\varepsilon}(\varepsilon_{f(x)})=\varepsilon_{f(x)}$ and $n_{a}(q)=q$.
Clearly, $g$ is a mono in $\mathbf{PSh}(A_{\bar{\tau}}^{\star})$ and the
square in (19) commutes, i.e., $\llbracket f\rrbracket\circ m=n\circ g$. Since
$\llbracket f\rrbracket$ is assumed to be a bisimulation map, there is a map
$Q\rTo^{k}\llbracket X\rrbracket$ such that the upper and lower triangle in
(19) commute, i.e., $\llbracket f\rrbracket\circ k=n$ and $k\circ g=m$.

We compute $\llbracket f\rrbracket_{a}\circ k_{a}(q)=n_{a}(q)=q$. Thus we find
a $p\in\llbracket X\rrbracket(a)$ such that $p_{f}=q$ and by restriction to
$\varepsilon$ using $m=k\circ g$, we also obtain
$p\mid_{\varepsilon}=\varepsilon_{x}$. By the definition of $p_{f}$, this
means that $x\ext@arrow
0359\arrowfill@\relbar\relbar\twoheadrightarrow{}{\tau}{}x^{\prime}$ and
$f(x^{\prime\prime})=y$ as required.

  * •

The case of a $\tau$-step $f(x)$ (corresponding to an execution $q$ observable
at $\bar{\tau}$) can be shown analogously to the visible $a$-step, where we
consider the set $Q(\bar{\tau})=\\{q\\}$ instead of $Q(a)$ and argue
identically, else.