Multi….>>

# On path-based coalgebras and weak notions of bisimulation

Harsh Beohar Sebastian Küpper
Theoretical Computer Science Group
Universität Duisburg-Essen
<EMAIL_ADDRESS>
###### Abstract

It is well known that the theory of coalgebras provides an abstract definition
of behavioural equivalence that coincides with strong bisimulation across a
wide variety of state-based systems. Unfortunately, the theory in the presence
of so-called silent actions is not yet fully developed. In this paper, we give
a coalgebraic characterisation of branching (delay) bisimulation in the
context of labelled transition systems (fully probabilistic systems). It is
shown that recording executions (up to a notion of stuttering), rather than
the set of successor states, from a state is sufficient to characterise the
respected bisimulation relations in both cases.

##  1 Introduction

Since its inception, coalgebra-based modelling of systems provides a simple
and abstract definition of behavioural equivalence that coincides with the so-
called strong bisimulation relations across a wide variety of dynamical
systems (see [19] for an introduction). Two states are said to be
behaviourally equivalent if they are mapped to a common point by a coalgebra
homomorphism. Unfortunately, the theory in the presence of so-called _silent_
actions is not yet well developed, albeit some general constructions (with
varying level of generality) characterising Milner’s weak bisimulation [16]
are proposed in the literature (see, for instance, [12, 22, 9, 7, 8] and the
references therein).

Another refinement of strong bisimulation is _branching bisimulation_ proposed
by [25] [25], which is the coarsest equivalence (in the [23] spectrum [23])
preserving the branching structure of a state [24]. In this context, we are
unaware of any prior work that captured branching bisimulation in the
framework of coalgebras. Moreover, a natural notion of behavioural equivalence
should preserve the branching structure of a state just like strong
bisimulation does in the absence of silent action.

[6] [6] have considered silent transitions coalgebraically by removing them
all together by considering the labels as words rather than single letters.
This approach is not useful when characterising branching bisimulation (or
even weak bisimulation) because not all silent transitions can always be
removed from the system without violating the transfer properties of branching
(weak) bisimulation. In [12, 9, 7, 8], weak bisimulation is captured in two
phases: first, a given coalgebra is transformed into a coalgebra (possibly
over a different base category) which captures the “saturation” effect of a
silent action; second, it is shown that the notion of behavioural equivalence
on this transformed coalgebra coincides with weak bisimulation on the
corresponding dynamical system. In [22] the authors used Aczel-Mendler style
formulation of strong bisimulation in the latter step.

Figure 1: The states $x_{1},y_{1}$ are weakly bisimilar, but not branching
bisimilar.

Nevertheless, it is well known that the saturation step (i.e. adding strong
$a$-transitions for each weak $a$-transition to the transition system) is not
sound with respect to branching bisimulation even in the case of labelled
transition systems [25]; thus, a different approach to characterise it is
required. The reason is that $\tau$-steps can enable or disable choice in an
observable behaviour, something that is hidden by the saturation step. For
weak bisimulation this point is irrelevant; however, branching bisimulation
(which is finer than weak bisimulation) requires that $\tau$-steps which are
required to answer an observable action may only lead to states that are still
in bisimulation relation with the original state. For instance, consider the
states $x_{1},y_{1}$ described in Figure 1. They are _not_ branching bisimilar
because the transition $y_{1}\xrightarrow{a}y_{4}$ can be simulated by the
transitions $x_{1}\xrightarrow{\tau}x_{2}\xrightarrow{a}x_{4}$, but the
intermediate state $x_{2}$ cannot be related with the state $y_{1}$ because
$y_{1}$ can fire a $b$-transition which $x_{2}$ cannot simulate.

Our research hypothesis is that recording executions (up to a notion of
stuttering) generated by a state (instead of the set of successor states) is
sufficient to capture branching bisimulation across different classes of
systems. Stated differently, it is the set of executions (not the set of
successor states) which specifies the branching structure of a state in the
presence of silent actions. In particular, we will substantiate this claim for
the class of labelled transition systems and fully probabilistic systems in
this paper.

In lieu of the above hypothesis, we restructure the classical coalgebraic
machinery in the following way. We begin by studying a notion of _paths_ on an
arbitrary set $X$ (denoted $\mathrm{Path}(X)$) in Section 2, which is general
enough to specify the executions of a labelled transition system and a fully
probabilistic system. Intuitively, a path on $X$ can be viewed as a finite
sequence that alternates between the elements of $X$ and an action in the
alphabet $A_{\tau}=A\uplus\\{\tau\\}$, where $\tau\not\in A$ is the silent
action. Now for every path $p\in\mathrm{Path}(X)$ there is a unique stutter
invariant path ${p}^{{\dagger}}\in\mathrm{Path}(X)$ associated with it, which
intuitively can be constructed by removing the $\tau$ self-loops. This is
reminiscent of a coloured trace from [25], which is obtained from a concrete
coloured trace in a process graph whose nodes are labelled by a fixed set of
colours. In the sequel, stutter invariance induces an equivalence relation
$\sim$ on the set $\mathrm{Path}(X)$ whose quotient is denoted as
${\mathrm{Path}}_{\sim}(X)$. Furthermore, it turns out that both the mappings
$\mathrm{Path}(X),{\mathrm{Path}}_{\sim}(X)$ are endofunctors on the category
of sets $\mathbf{Set}$.

Now what is missing in our approach is the type of dynamics (also known as the
branching type in the theory of coalgebras). For instance, a labelled
transition system can be viewed as a coalgebra of type
$\mathcal{P}\circ(A_{\tau}\times\mathrm{id})$ over the base category
$\mathbf{Set}$. Here $\mathcal{P}$ is the covariant powerset functor and
$A_{\tau}\times\mathrm{id}$ is the product functor whose left component is
fixed. In other words, the branching type of labelled transition system is
nondeterministic. Therefore, to characterise branching bisimulation, we
consider coalgebras of type $\mathcal{P}\circ\mathrm{Path}_{\sim}$ over the
base category $\mathbf{Set}$. In Section 3, we show that behavioural
equivalence in this coalgebra coincides with the traditional branching
bisimulation relation [25]. Moreover, this framework can also be used to
characterise the weak bisimulation, delay bisimulation, and eta-bisimulation
relations; however, for reasons of space, this is worked out in Appendix I.

Nevertheless, the situation is not so straightforward in the case of a fully
probabilistic system. Often such systems are modelled as coalgebras of type
$\mathcal{D}\circ(A_{\tau}\times\mathrm{id})$ over the base category
$\mathbf{Set}$, where $\mathcal{D}$ is the sub-distribution functor. It turns
out that one needs a notion of measurable space and a measure on the set of
maximal executions111An execution of a fully probabilistic system is _maximal_
if it is an infinite execution or it stops in a state with the sum of
probabilities of all outgoing transitions as $0$. in order to define branching
(weak) bisimulation relations over the states of a fully probabilistic system
(cf. [4, 21]). Thus, it is natural to consider fully probabilistic systems as
‘weighted’ coalgebras of type $\mathcal{G}\circ(A_{\tau}\times\mathrm{id})$
over the base category of measurable spaces $\mathbf{Meas}$. Here,
$\mathcal{G}$ is the well-known Giry monad of probability measures [17].

In Section 5, just like in the discrete case, we consider coalgebras of type
$\mathcal{G}\circ\mathrm{Path}_{\sim}$ over the base category $\mathbf{Meas}$
to characterise probabilistic delay bismulation, which was mistakenly [20]
called probabilistic branching bisimulation in [21, 22]. The crux of the
matter is in defining $\mathrm{Path}(X)$ and ${\mathrm{Path}}_{\sim}(X)$ as
endofunctors on the category $\mathbf{Meas}$. In other words, we need to
resolve the following issues: first, which subsets of $\mathrm{Path}(X)$ and
${\mathrm{Path}}_{\sim}(X)$ are measurable; second, whether
$\mathrm{Path}(X)\rTo^{\mathrm{Path}(f)}\mathrm{Path}(Y)$ (for a given
$X\rTo^{f}Y$ in $\mathbf{Set}$) is a measurable function or not; third,
constructions of measures on the sets $\mathrm{Path}(X)$ and
${\mathrm{Path}}_{\sim}(X)$. These issues are explored in Section 4, for which
some preliminary knowledge on topology, domain theory, and measure theory is
required. In Section 6, we discuss future directions for research and present
some concluding remarks. All the complete proofs pertaining to each section
can be found in the appendices II-V.

##  2 Preliminaries

This section is devoted to formally introduce a notion of path and stutter
equivalent path on a set $X$, which will be used throughout the paper. As
mentioned earlier, a path on $X$ can be intuitively viewed as a finite
sequence that alternates between the elements of the set $X$ and an action in
the alphabet $A_{\tau}$. However, we abstain from this operational view in
favour of Definition 1 to reason about paths from a functional perspective.

Let $A_{\tau}^{*}$ be the set of finite words with $\varepsilon\in
A_{\tau}^{*}$ denoting the empty sequence. We write $\preceq$ to denote the
prefix ordering on words and let
$\downarrow\\!{\sigma}=\\{\sigma^{\prime}\mid\sigma^{\prime}\preceq\sigma\\}$.

######  Definition 1.

A _path_ $p$ on a set $X$ is a function whose codomain is $X$ and domain is
the set of all prefixes of some word in $A_{\tau}^{*}$.

Let $\mathrm{Path}(X)$ be the set of all paths on a given set $X$. Then, this
lifts to an endofunctor on the category of sets $\mathbf{Set}$ by letting:
$\mathrm{Path}(f)(p)=f\circ p$, for every function $X\rTo^{f}Y$.

Every path $p\in\mathrm{Path}(X)$ has a _trace_ associated with it. Moreover,
every path $p\in\mathrm{Path}(X)$ reaches a _last_ element from the set $X$.
Symbolically, we write

$\mathrm{trace}(p)=\max\mathrm{dom}(p)\quad\text{and}\quad\mathrm{last}(p)=p(\mathrm{trace}(p)).$

######  Proposition 1.

Let $X\rTo^{f}Y$ be a function. Then, for every path $p\in\mathrm{Path}(X)$ we
have $\mathrm{trace}(p)=\mathrm{trace}(fp)$ and
$f\mathrm{last}(p)=\mathrm{last}(fp)$.

Figure 2: Two systems having same branching structure.

The above proposition states that the functor $\mathrm{Path}$ preserves the
trace of a path, which is quite strong for our purpose. To exemplify this,
consider two labelled transition systems and a function between the states as
shown in Figure 2. Since the $\tau$-step from the state $x_{1}$ does not
disable any choice of observable action offered by $x_{1}$, we would like to
declare the states $x_{1}$ and $x_{2}$ as equivalent. In other words, we would
like to assert that $f$ is a homomorphism between the coalgebras
$(X=\\{x_{1},x_{2},x_{3}\\},\alpha)$ and $(Y=\\{y_{1},y_{2}\\},\beta)$, where
the functions $\alpha,\beta$ return all the generated executions. However, we
note that this is not the case because the $f$-image of the execution
$p=\langle x_{1}\ \tau\ x_{2}\ a\ x_{3}\rangle\in\alpha(x_{1})$ is $\langle
y_{1}\ \tau\ y_{1}\ a\ y_{2}\rangle$ which is not an execution from $y_{1}$.
Thus, the key observation is to relate the executions of two systems up to
stuttering, which leads to the following definition.

######  Definition 2.

A function $\phi$ with $\mathrm{dom}(\phi)=\mathrm{dom}(p)$ and
$\mathrm{cod}(\phi)=A_{\tau}^{*}$ is a _stutter basis_ for a path
$p\in\mathrm{Path}(X)$ if it can be constructed inductively by the following
rules:

  1. 1.

$\phi(\varepsilon)=\varepsilon$.

  2. 2.

if $\sigma^{\prime}\tau\in\mathrm{dom}(p)$ and
$p(\sigma^{\prime}\tau)=p(\sigma^{\prime})$ then
$\phi(\sigma^{\prime}\tau)=\phi(\sigma^{\prime})$.

  3. 3.

if $\sigma^{\prime}\tau\in\mathrm{dom}(p)$ and $p(\sigma^{\prime}\tau)\neq
p(\sigma^{\prime})$ then
$\phi(\sigma^{\prime}\tau)=\phi(\sigma^{\prime})\tau$.

  4. 4.

if $\sigma^{\prime}a\in\mathrm{dom}(p)$ and $a\in A$ then
$\phi(\sigma^{\prime}a)=\phi(\sigma^{\prime})a$.

As an example, consider a path $p=\langle x_{1}\ \tau\ x_{1}\ a\
x_{2}\rangle$. Then, the function $\phi$ defined as
$\phi(\tau)=\phi(\varepsilon)=\varepsilon$ and $\phi(\tau a)=a$ is a stutter
basis $\phi$ for the path $p$. However, if $p=\langle x_{1}\ \tau\ x_{2}\ a\
x_{3}\rangle$ with $x_{1}\neq x_{2}$, then $\phi=\mathrm{id}$ is a stutter
basis for $p$.

######  Theorem 2.

For any path there is a unique stutter basis.

######  Lemma 3.

Let $\phi$ be the stutter basis for a path $p\in\mathrm{Path}(X)$ with
$\mathrm{dom}(p)=\downarrow\\!{\sigma}$, for some $\sigma\in A_{\tau}^{*}$.
Then, $\phi(\downarrow\\!{\sigma})=\ \downarrow\\!{\phi(\sigma)}.$

######  Definition 3.

Given a path $p\in\mathrm{Path}(X)$ and its corresponding stutter basis
$\phi$, then a function $\phi(\mathrm{dom}(p))\rTo^{{p}^{{\dagger}}}X$ is the
_stutter invariant_ path relative to $p$ if ${p}^{{\dagger}}\circ\phi=p$.

Notice that for the function ${p}^{{\dagger}}$ to be a path its domain should
be a prefix closed subset of a word, which follows directly from Lemma 3.

The notion of stutter invariant path induces an equivalence relation on the
set of all paths as follows. Two paths $p,q\in\mathrm{Path}(X)$ are said to be
_stutter equivalent_ , denoted $p\sim q$, if and only if they have the
identical stutter invariant path, i.e., ${p}^{{\dagger}}={q}^{{\dagger}}$. Let
${\mathrm{Path}}_{\sim}(X)$ be the set of all the paths up to stutter
equivalence. This lifts to a functor as well:

${\mathrm{Path}}_{\sim}(f)[p]_{\sim}=[f\circ p]_{\sim}\qquad\text{for any
$p\in\mathrm{Path}(X)$ and $X\rTo^{f}Y$}.$ (1)

To prove that the above map is well-defined, we need the following lemma.

######  Lemma 4.

For any $p\in\mathrm{Path}(X)$ and any $X\rTo^{f}Y$, we have
$f\circ{p}^{{\dagger}}\sim f\circ p$.

######  Theorem 5.

The mapping in (1) is well defined and $\mathrm{Path}_{\sim}$ is an
endofunctor on $\mathbf{Set}$.

Notation We write $\pi_{X}$ for the quotient map that maps a path
$p\in\mathrm{Path}(X)$ to ${[p]}_{\sim}$.

We end this subsection with few properties on (stutter equivalent) paths.

######  Lemma 6.

Let $p\in\mathrm{Path}(X),q\in\mathrm{Path}(Y)$, and $X\rTo^{f}Y$.

  1. 1.

If $fp\sim q$ and $\mathrm{trace}(q)\in\tau^{*}a\tau^{*}$ then
$q(\varepsilon)=fp(\varepsilon)\land\mathrm{trace}(p)\in\tau^{*}a\tau^{*}$.

  2. 2.

$\mathrm{last}(p)=\mathrm{last}({p}^{{\dagger}})$.

  3. 3.

If $fp\sim q$, then $f(\mathrm{last}(p))=\mathrm{last}(q)$.

  4. 4.

$\pi_{Y}\circ\mathrm{Path}(f)={\mathrm{Path}}_{\sim}(f)\circ\pi_{X}$.

  5. 5.

Let $V_{i}\subseteq{\mathrm{Path}}_{\sim}(Y)$ (for $i\in I$) be a family of
pairwise disjoint sets. Then,

${{\mathrm{Path}}_{\sim}(f)}^{-1}\Big{(}\bigcup_{i\in I}V_{i}\Big{)}\ =\
\bigcup_{i\in I}{{\mathrm{Path}}_{\sim}(f)}^{-1}(V_{i})\enspace.$

### Coalgebraic preliminaries

######  Definition 4.

Let $\mathbf{C}$ be a category and let $\mathbf{C}\rTo^{F}\mathbf{C}$ be an
endofunctor. An _$F$ -coalgebra_ over the base category $\mathbf{C}$ is a
tuple $(X,\alpha)$, where $X$ is an object in $\mathbf{C}$ and
$X\rTo^{\alpha}FX$ is an arrow in $\mathbf{C}$. Given two objects $(X,\alpha)$
and $(Y,\beta)$, an $F$-coalgebra homomorphism is an arrow $X\rTo^{f}Y$ in
$\mathbf{C}$ such that $Ff\circ\alpha=\beta\circ f$.

######  Definition 5.

Let $\mathbf{C}$ be a concrete category over the category of sets
$\mathbf{Set}$, i.e., there is a faithful functor
$\mathbf{C}\rTo^{|\\_|}\mathbf{Set}$. Let $(X,\alpha)$ be an $F$-coalgebra
over the concrete category $\mathbf{C}$. Then, two points $x,x^{\prime}\in|X|$
are said to be _$F$ -behaviourally equivalent_ if and only if there is an
$F$-coalgebra $(Y,\beta)$ and an $F$-coalgebra homomorphism $X\rTo^{f}Y$ such
that $f(x)=f(x^{\prime})$.

In Section 3, we will let $\mathbf{C}=\mathbf{Set}$ and $|\\_|=\mathrm{id}$;
however, in Section 5, we will let $\mathbf{C}=\mathbf{Meas}$ and the faithful
functor $|\\_|$ to be the forgetful functor which forgets the sigma algebras
associated with the underlying sets.

##  3 Branching bisimulation on labelled transition systems

The goal is to characterise branching bisimulation of [25] [25] using a
coalgebraic approach based on paths as outlined in the introduction.

######  Definition 6.

A _labelled transition system_ is a triple $(X,A_{\tau},\rightarrow)$, where
$X$ is a set of states, $A_{\tau}$ a set of actions, and $\rightarrow\subseteq
X\times A_{\tau}\times X$ is the so-called _transition relation_.

As usual, we write $x\xrightarrow{a}x^{\prime}$ and $\ext@arrow
0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{}{}\subseteq X\times
A^{*}\times X$ to denote an element $(x,a,x^{\prime})\in\rightarrow$ and the
weak reachability relation, respectively. The latter is defined as the
smallest relation satisfying the following inference rules:
$\frac{}{x\ext@arrow
0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{\varepsilon}{}x}\qquad\frac{x\ext@arrow
0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{\sigma}{}x^{\prime}\
x^{\prime}\xrightarrow{a}x^{\prime\prime}}{x\ext@arrow
0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{\sigma
a}{}x^{\prime\prime}}.$

######  Definition 7.

Let $(X,A_{\tau},\rightarrow)$ be a labelled transition system. A symmetric
relation $R\subseteq X\times X$ is called a _branching bisimulation_ relation
[25] if and only if for any $x,y,x^{\prime}\in X$ and $a\in A_{\tau}$, if
$x\xrightarrow{a}x^{\prime}\land xRy$ then $(x^{\prime}Ry\land
a=\tau)\vee\exists_{y^{\prime},y^{\prime\prime}}\ y\ext@arrow
0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{\varepsilon}{}y^{\prime}\xrightarrow{a}y^{\prime\prime}\land
xRy^{\prime}\land x^{\prime}Ry^{\prime\prime}.$ Two states $x\in X$ and
$x^{\prime}\in X$ are _branching bisimlar_ if and only if there exists a
branching bisimulation relation $R$ such that $xRx^{\prime}$.

Next, we construct a $\mathcal{P}\circ\mathrm{Path}_{\sim}$-coalgebra based on
paths, where $\mathcal{P}$ is the covariant power set endofunctor on the
category of sets $\mathbf{Set}$.

An _execution_ starting from a state $x\in X$ of a labelled transition system
$(X,A_{\tau},\rightarrow)$ is a path $p\in\mathrm{Path}(X)$ such that
$p(\sigma)\xrightarrow{a}p(\sigma a)$, for all $\sigma a\in\mathrm{dom}(p)$.
Let $\mathrm{Exec}(x)$ be the set of all executions starting from $x$. Such a
transition system can be modelled as a coalgebra $(X,\pi_{X}\circ\alpha)$,
where transition function $\alpha$ is given as:

$\alpha(x)=\\{p\mid
p\in\mathrm{Exec}(x)\land\mathrm{trace}(p)\in\tau^{*}a\\}\cup\\{p\mid
p\in\mathrm{Exec}(x)\land\mathrm{trace}(p)\in\tau^{*}\\}.$

######  Remark 1.

At this stage, we would like to highlight the distinction between a path and
an execution made in this paper. It should be noted that all executions of a
system (under investigation) are paths; however, the converse may not be true.
This is not unusual because after all the executions of a system are generated
on the basis of how behaviour of the system is specified (for instance, by the
transition relation in the case of labelled transition systems and by the
transition function in the case of fully probabilistic system).

Next, we state the main result of this section.

######  Theorem 7.

Let $(X,A_{\tau},\rightarrow)$ be a labelled transition system and
$(X,\pi_{X}\circ\alpha)$ be the corresponding
$\mathcal{P}\circ\mathrm{Path}_{\sim}$-coalgebra. Then, two states
$x,x^{\prime}\in X$ are branching bisimilar if and only if the states
$x,x^{\prime}$ are $\mathcal{P}\circ\mathrm{Path}_{\sim}$-behaviourally
equivalent.

###### Proof.

$\Rightarrow$ Let $R\subseteq X\times X$ be the largest branching bisimulation
on the given labelled transition system. Then, from [25] we know that $R$ is
an equivalence relation. So let $X\rTo^{f}X/R$ be the quotient map. Now to
show that $f$ is indeed the required
$\mathcal{P}\circ\mathrm{Path}_{\sim}$-coalgebra homomorphism, we first
construct a coalgebra $X/R\rTo^{\beta}\mathcal{P}{\mathrm{Path}}_{\sim}(X/R)$:

$\beta(f(x))=\\{{\mathrm{Path}}_{\sim}(f)(p)\mid
p\in\alpha(x)\\},\qquad\text{for all}\ x\in X\enspace.$

Clearly, $\beta$ is a total function because $f$ is surjective. Next, we claim
that $\beta$ is well-defined, i.e., independent of the chosen representative.
Let $x,x^{\prime}\in X$ such that $f(x)=f(x^{\prime})$. Then, we need to show
that $\beta(f(x))=\beta(f(x^{\prime}))$. Suppose ${[fp]}_{\sim}\in\beta(f(x))$
with $p\in\alpha(x)$. Then, by structural induction on the word
$\sigma\in\mathrm{dom}(p)$ we show that there is a path
$p^{\prime}\in\alpha(x^{\prime})$ such that $f\circ(p|_{\sigma})\sim f\circ
p^{\prime}$. Here, we write $p|_{\sigma}$ to denote the restriction of the
function $p$ to the sub-domain $\downarrow\\!{\sigma}$. To see this, without
loss of generality, let $\sigma a\in\mathrm{dom}(p)$. Then by the induction
hypothesis we find an execution $p^{\prime}\in\alpha(x^{\prime})$ such that
$f\circ(p|_{\sigma})\sim f\circ p^{\prime}$. Note that
$p(\sigma)\xrightarrow{a}p(\sigma a)$ and using Lemma 6(3) we get
$f\circ(p|_{\sigma})\sim f\circ p^{\prime}\implies p(\sigma)\ R\
\mathrm{last}(p^{\prime})$. Let $a\in A$. Then, using the transfer property of
branching bisimulation we get $\mathrm{last}(p^{\prime})\ext@arrow
0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{\varepsilon}{}y\xrightarrow{a}y^{\prime}$
such that $p(\sigma)Ry$ and $p(\sigma a)Ry^{\prime}$ since $p(\sigma)$ and
$\mathrm{last}(p^{\prime})$ are branching bisimilar. Moreover, from the
stuttering lemma [25] we know that any intermediate state visited in the path
$\mathrm{last}(p^{\prime})\ext@arrow
0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{\varepsilon}{}y$ is also
$R$-related to $p(\sigma)$. Therefore, there is a path
$p^{\prime\prime}\in\mathrm{Path}(X)$ which extends $p^{\prime}$ such that
$f\circ(p|_{\sigma a})\sim f\circ p^{\prime\prime}$. In addition, if $a=\tau$
then we either have $p(\sigma\tau)\ R\ \mathrm{last}(p^{\prime})$ or
$\mathrm{last}(p^{\prime})\ext@arrow
0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{\varepsilon}{}y\xrightarrow{\tau}y^{\prime}$,
for some $y,y^{\prime}$, with $p(\sigma)Ry$ and $p(\sigma\tau)Ry^{\prime}$.
Suppose the former is true, then clearly we have $f\circ(p|_{\sigma\tau})\sim
f\circ p^{\prime}$. The latter case is similar to the case when $a\in A$.
Thus, for every $p\in\alpha(x)$ there is a path
$p^{\prime}\in\alpha(x^{\prime})$ such that $f\circ p\sim f\circ p^{\prime}$.
Likewise, we can show the symmetric property when the role of $x$ and
$x^{\prime}$ is interchanged. This completes the proof of the above claim.
Clearly, we have $\beta\circ
f=\mathcal{P}{\mathrm{Path}}_{\sim}(f)\circ\alpha$.

$\Leftarrow$ Let $(Y,\beta)$ be a
$\mathcal{P}\circ\mathrm{Path}_{\sim}$-coalgebra and $X\rTo^{f}Y$ be a
$\mathcal{P}\circ\mathrm{Path}_{\sim}$-coalgebra homomorphism. Below we rather
illustrate why the relation $xRx^{\prime}\iff f(x)=f(x^{\prime})$ is a
witnessing branching bisimulation. The proof can be found in Theorem III.1. ∎

Consider the two labelled transition systems drawn below enclosed inside the
two rectangles. Here, $X\rTo^{\alpha}\mathcal{P}{\mathrm{Path}}_{\sim}(X)$ and
$Y\rTo^{\beta}\mathcal{P}{\mathrm{Path}}_{\sim}(Y)$ denote the corresponding
path-based

$x_{1}$$\alpha:$$x_{2}$$x_{3}$$x_{4}$$x_{5}$$x_{1}^{\prime}$$x_{2}^{\prime}$$x_{3}^{\prime}$$\tau$$a$$a$$b$$a$$b$$y_{1}$$\beta:$$y_{2}$$b$$a$

coalgebras with $X=\\{x_{i},x_{j}^{\prime}\mid
i\in\\{1,2,3,4,5\\},j\in\\{1,2,3\\}\\}$ and $Y=\\{y_{1},y_{2}\\}$.
Furthermore, let $X\rTo^{f}Y$ be a function defined as $f(x)=y_{1}$ if
$x\in\\{x_{1},x_{1}^{\prime},x_{2}\\}$; otherwise $f(x)=y_{2}$. To illustrate
why $R$ (as defined above) is a witnessing branching bisimulation, consider
the transition $x_{1}^{\prime}\xrightarrow{b}x_{3}^{\prime}$ and
$x_{1}Rx_{1}^{\prime}$. Clearly, $\langle x_{1}^{\prime}\ b\
x_{3}^{\prime}\rangle\in\alpha(x_{1})$, which further implies that $\langle
y_{1}\ b\ y_{2}\rangle\in\beta(y_{1})$. Since
$\mathcal{P}{\mathrm{Path}}_{\sim}(f)\circ\alpha=\beta\circ f$ we know that
there is an execution $p$ such that $f\circ p$ is stutter equivalent to
$\langle y_{1}\ b\ y_{2}\rangle$. And by inspection we note that $p=\langle
x_{1}\ \tau\ x_{2}\ b\ x_{5}\rangle$ is such an execution. Moreover,
$x_{2}Ry_{1}$ and $x_{5}Ry_{2}$ which is required by the transfer property of
a branching bisimulation relation.

In hindsight, using the terminology of [24], a
$\mathcal{P}\mathrm{Path}_{\sim}$-coalgebra homomorphism preserves the
branching structure of states. As a consequence, two behaviourally equivalent
states have the same set of executions under the image of a
$\mathcal{P}\mathrm{Path}_{\sim}$-coalgebra homomorphism up to stutter
invariance. For instance, in the above example, the sets of all executions
having trace $\tau^{*}a$ from the states $x_{1}$ and $x_{1}^{\prime}$ are
$\\{\langle x_{1}\ a\ x_{3}\rangle,\langle x_{1}\ \tau\ x_{2}\ a\
x_{4}\rangle\\}$ and $\\{\langle x_{1}^{\prime}\ a\ x_{2}^{\prime}\rangle\\}$,
respectively. Notice that the $f$-image of these two sets are equivalent up to
stutter invariance. A similar argument can be observed for the set of
executions from $x_{1},x_{1}^{\prime}$ having trace $\tau^{*}b$.

Though we have focussed on branching bisimulation, this approach can also be
used to capture weak, $\eta$ and delay bisimulation, by defining $\alpha$
differently, saturating $\tau$ leading transitions, trailing $\tau$
transitions or both, respectively. This is made explicit in Appendix I.

##  4 A measurable space on paths

As mentioned in the introduction, we will consider coalgebras of type
$\mathcal{G}\circ\mathrm{Path}_{\sim}$ over the base category $\mathbf{Meas}$
to characterise probabilistic delay bisimulation. However, before we do so, we
have to fix which subsets of the sets $\mathrm{Path}(X)$ and
${\mathrm{Path}}_{\sim}(X)$ are measurable together with the construction of a
measure on the space of paths, which can be a challenging issue in its own
right. In this section, we resolve these fundamental issues by first recalling
some basic definitions of measure theory taken from [17].

######  Definition 8.

A set $\Sigma_{X}\subseteq\mathcal{P}(X)$ of subsets of $X$ is a _sigma-
algebra_ on $X$ if and only if $X\in\Sigma_{X}$ and $\Sigma_{X}$ is closed
under the set complements and countable unions. Then, the tuple
$(X,\Sigma_{X})$ is called a _measurable space_. A _measure_ space is a
measurable space $(X,\Sigma_{X})$ with a measure
$\Sigma_{X}\rTo^{\mu_{X}}\left[0,\infty\right]$, i.e., $\mu_{X}$ is a function
satisfying $\mu(\emptyset)=0$ and the _sigma-additivity_ property: for any
countable family of pairwise disjoint sets $U_{i}\in\Sigma_{X}$ (for $i\in I$)
we have

$\mu_{X}(\bigcup_{i\in I}U_{i})=\sum_{i\in I}\mu_{X}(U_{i})\enspace.$

A _probability_ space $(X,\Sigma_{X},\mu_{X})$ is a measure space with
$\mu_{X}(X)=1$. A _discrete_ space is a measure space such that $X$ is
countable and $\Sigma_{X}=\mathcal{P}(X)$.

Here, the arbitrary sum of a family $\\{r_{i}\mid i\in I\\}$ of nonnegative
real numbers is defined as $\sum_{i\in I}r_{i}=\sup\\{\sum_{i\in J}r_{i}\mid
J\subseteq_{\mathrm{f}}I\\}$ (cf. [21]), where $J\subseteq_{\mathrm{f}}I\iff
J\subseteq I\land\text{$J$ is a finite set}$.

We want to endow a notion of measurability on the set
${\mathrm{Path}}_{\sim}(X)$; however, for simplicity we first restrict
ourselves to the set of all paths on $X$, i.e., $\mathrm{Path}(X)$. It turns
out that the set of all paths carries a topological structure (precisely, they
form what is known as Alexandroff topology [2]) and also satisfies the so-
called Kolmogorov separability axiom. Once we have a topological space, the
convention is to consider the smallest sigma-algebra generated by the set of
all open sets (also known as the Borel sigma-algebra) as the set of measurable
sets.

######  Definition 9.

A _topology_ on a set $X$ consists of a set of open sets
$\mathcal{O}_{X}\subseteq\mathcal{P}(X)$ such that: first, the empty set and
the whole space are in $\mathcal{O}_{X}$; second, the set $\mathcal{O}_{X}$ is
closed under finite intersection and arbitrary unions. A topological space
$(X,\mathcal{O}_{X})$ is an _Alexandroff_ space if the set $\mathcal{O}_{X}$
is closed under arbitrary intersection. A topological space
$(X,\mathcal{O}_{X})$ satisfies the _Kolmogorov separability axiom_ ($X$ is a
$T_{0}$ space) if any two distinct points are topologically distinguishable,
i.e., $\forall_{x,x^{\prime}\in X}\ x\neq
x^{\prime}\implies\exists_{U\in\mathcal{O}_{X}}\ (x\in U\land
x^{\prime}\not\in U)\vee(x\not\in U\land x^{\prime}\in U).$

It is well-known that the set of all upward closed subsets generated by a
poset forms a $T_{0}$ Alexandroff space. In particular, our set of paths
$\mathrm{Path}(X)$ carries the following order:

$p\preceq
q\iff\mathrm{dom}(p)\subseteq\mathrm{dom}(q)\land\forall_{\sigma\in\mathrm{dom}(p)}\
q(\sigma)=p(\sigma)\enspace.$

Actually, the above ordering is a prefix order in the sense of [10] [10].

######  Definition 10.

A _prefix order_ is a partial order whose every principal ideal is a totally
ordered set.

######  Proposition 8.

The history of a path $p\in\mathrm{Path}(X)$ is downward total, i.e., the set
$\downarrow\\!{p}=\\{p^{\prime}\mid p^{\prime}\preceq p\\}$ is a totally
ordered set.

######  Proposition 9.

The set of all paths $\mathrm{Path}(X)$ on a set $X$ forms a $T_{0}$
Alexandroff space, whose open sets are upward closed subsets of
$\mathrm{Path}(X)$, i.e.,
$\mathcal{O}_{\mathrm{Path}(X)}=\\{U\subseteq\mathrm{Path}(X)\mid
U=\uparrow\\!{U}\\}$. Here, the set $\uparrow\\!{U}=\\{p^{\prime}\mid\exists\
p\in U\land p\preceq p^{\prime}\\}$ denotes future of paths in the set $U$.

At this stage, we note the following relationship between stutter paths and
the order $\preceq$.

######  Lemma 10.

Let $X$ be a set. Then we have the following property: for any two paths
$p_{1},p_{2}\in\mathrm{Path}(X)$, if
${p}^{{\dagger}}_{1}\preceq{p}^{{\dagger}}_{2}$ then
$\exists_{p\in\mathrm{Path}(X)}\ p\sim p_{1}\land p\preceq p_{2}$.

Every point $x\in X$ in an Alexandroff space has a special neighbourhood
associated with it, often called the _smallest neighbourhood_ of $x$, denoted
$\mathcal{N}(x)=\bigcap\\{U\mid U\in\mathcal{O}_{X}\land x\in U\\}$. In
particular, this structure, in the case of paths, is the principal filter
generated by a path.

######  Proposition 11.

For a path $p\in\mathrm{Path}(X)$, the smallest neighbourhood of $p$
represents the future of the path $p$, i.e., $\uparrow\\!{p}=\mathcal{N}(p)$.
In contrast, the closure $\mathrm{cl}(p)$ of a path $p\in\mathrm{Path}(X)$ –
the smallest closed set that contains $p$ – represents the history of $p$,
i.e., $\mathrm{cl}(p)=\downarrow\\!{p}$.

The next proposition states that the subsets of paths which belong to the
Borel sigma-algebra $\mathcal{B}(\mathcal{O}_{\mathrm{Path}(X)}))$ are
measurable.

######  Proposition 12.

The tuple $(\mathrm{Path}(X),\Sigma_{\mathrm{Path}(X)})$, where
$\Sigma_{\mathrm{Path}(X)}=\mathcal{B}(\mathcal{O}_{\mathrm{Path}(X)})$, is a
measurable space. Here, $\mathcal{B}(\mathcal{X})$ denotes the smallest sigma-
algebra generated by $\mathcal{X}\subseteq\mathcal{P}(X)$.

Next, we establish that the
$\mathrm{Path}(X)\rTo^{\mathrm{Path}(f)}\mathrm{Path}(Y)$ (for a given
$X\rTo^{f}Y$) is measurable, i.e., if $V\in\Sigma_{\mathrm{Path}(Y)}$ then
${f}^{-1}V\in\Sigma_{\mathrm{Path}(X)}$. For this, we need the following
result.

######  Theorem 13.

For any $X\rTo^{f}Y$, the function $\mathrm{Path}(f)$ is an order embedding,
i.e., for any $p,p^{\prime}\in\mathrm{Path}(X)$ we have $p\preceq
p^{\prime}\iff f\circ p\preceq f\circ p^{\prime}$.

Since every order preserving function is continuous and every continuous
function is Borel measurable, it follows that, in particular,
$\mathrm{Path}(f)$ is Borel measurable.

######  Corollary 1.

For any $X\rTo^{f}Y$, the function $\mathrm{Path}(f)$ is measurable.

In hindsight, the function $\mathrm{Path}(f)$ is an arrow in the category
$\mathbf{Meas}$. Next, we turn our attention on constructing a measurable
space on the set ${\mathrm{Path}}_{\sim}(X)$. The idea is to first define an
order on the quotient space ${\mathrm{Path}}_{\sim}(X)$, which can be
inherited from the underlying space of paths $\mathrm{Path}(X)$ by simply
letting:
${[p]}_{\sim}\preceq{[q]}_{\sim}\iff{p}^{{\dagger}}\preceq{q}^{{\dagger}}$,
for all $p,q\in\mathrm{Path}(X)$.

######  Lemma 14.

The relation $\preceq$ on the set ${\mathrm{Path}}_{\sim}(X)$ is a well-
defined partial order. Furthermore, the relation $\preceq$ on the set
${\mathrm{Path}}_{\sim}(X)$ is also a prefix order.

Once we have an order on the quotient space, we can establish that the
quotient maps are order preserving (or continuous in the topological sense).

######  Theorem 15.

The quotient function $\mathrm{Path}(X)\rTo^{\pi}{\mathrm{Path}}_{\sim}(X)$ is
order preserving. Consequently, the quotient function
$\mathrm{Path}(X)\rTo^{\pi}{\mathrm{Path}}_{\sim}(X)$ is Borel measurable,
where the sigma-algebra on paths is given by
$\Sigma_{{\mathrm{Path}}_{\sim}(X)}=\mathcal{B}(\mathcal{O}_{{\mathrm{Path}}_{\sim}(X)})$.

Next, we state the main theorem of this section.

######  Theorem 16.

For any $X\rTo^{f}Y$, the function ${\mathrm{Path}}_{\sim}(f)$ is order
preserving. Thus, the function ${\mathrm{Path}}_{\sim}(f)$ is Borel
measurable.

### Constructing measures on the space of paths

Often, measures on a space are constructed in a top-down manner by identifying
a measurable set of building blocks and defining a set-function on this
collection (for example, in the case of Lebesgue measures on $\mathbb{R}$, a
semi-closed interval $[r,r^{\prime})$ with $r\leq r^{\prime}$ is one such
building block and the set-function maps every interval of the form
$[r,r^{\prime})$ to the value $r^{\prime}-r$). In turn, measure extension
theorems (for instance, the well-known Carathéodory-Hahn extension theorem;
see [18, pp 356]) are invoked to lift the set-function on building blocks to a
measure on the whole measurable space. In this paper, we will follow a similar
recipe; our building blocks will be open subsets of paths. As for measure
extension theorems, we will use a result (cf. Theorem 17) established by [3]
[3]. Below, we recall some definitions on a topological space necessary to
state this result.

######  Definition 11.

Let $(X,\mathcal{O}_{X})$ be a topological space. A function
$\mathcal{O}_{X}\rTo^{\mu}\left[0,\infty\right]$ is a _valuation_ if and only
if the following conditions are satisfied.

  1. 1.

The function $\mu$ is strict, i.e., $\mu(\emptyset)=0$

  2. 2.

The function $\mu$ is order preserving, i.e., for any two open sets
$U,U^{\prime}\in\mathcal{O}_{X}$, we have $U\subseteq U^{\prime}$ implies
$\mu(U)\leq\mu(U^{\prime})$.

  3. 3.

The function $\mu$ is modular, i.e., for any two open sets
$U,U^{\prime}\in\mathcal{O}_{X}$, we have $\mu(U)+\mu(U^{\prime})=\mu(U\cup
U^{\prime})+\mu(U\cap U^{\prime})$.

A valuation $\mu$ is _Scott-continuous_ if and only if for any directed family
of open sets $(U_{i})_{i\in I}$ we have $\mu(\bigcup_{i\in I}U_{i})=\sup_{i\in
I}\mu(U_{i})$. Lastly, a valuation $\mu$ is _locally finite_ if and only if
every point has a finitely valued open neighbourhood.

######  Definition 12.

A space $(X,\mathcal{O}_{X})$ is _locally compact_ if and only if for every
point $x$ and open set $U$ with $x\in U$, there is a compact subset
$V\subseteq X$ such that $x\in\mathrm{int}(V)$ and $V\subseteq U$. Here,
$\mathrm{int}(V)$ denotes the interior of $V\subseteq X$.

######  Definition 13.

A topological space $(X,\mathcal{O}_{X})$ is _sober_ if and only if every
irreducible closed set is a closure of a unique point. A closed set $C$ is
_irreducible_ if and only if $C$ is nonempty and it cannot be expressed as
union of two smaller closed subsets, i.e., if $C=C_{1}\cup C_{2}$ and
$C_{1},C_{2}$ are closed sets, then $C=C_{1}$ or $C=C_{2}$.

We call a subset $C\subseteq X$ _non-sober_ if $C$ is irreducible, $C$ is
closed, and it cannot be stated as a closure of point (i.e., $\nexists_{x\in
X}\ C=\mathrm{cl}(x)$).

######  Theorem 17 ([3]).

Every locally finite and Scott-continuous valuation on a locally compact sober
space extends uniquely to a Borel measure.

The restrictions on $\mathcal{O}_{X}\rTo^{\mu}\left[0,\infty\right]$ imposed
by the above theorem are not unreasonable; at-least for our purpose. In
Section 5, we will construct a locally finite and a Scott-continuous valuation
on open subsets of paths, which is induced by a given fully-probabilistic
transition system. Nevertheless, we cannot immediately apply Theorem 17
because our space $\mathrm{Path}(X)$ is not a sober space, even though it is
locally compact, i.e., every path $p\in\mathrm{Path}(X)$ has a compact
neighbourhood (since $p\in\uparrow\\!{p}$). As a result, in the following, we
first ‘soberify’ our space $\mathrm{Path}(X)$ and use Theorem 17 to construct
a Borel measure on $\mathrm{Path}(X)$ by lifting a given locally finite and
Scott-continuous valuation
$\mathcal{O}_{\mathrm{Path}(X)}\rTo^{\mu}\left[0,\infty\right]$.

######  Remark 2.

By inspection, we note that our space $\mathrm{Path}(X)$ is non-sober. For
instance, if $X$ is non-empty then unfolding a $\tau$-loop results in an
infinite chain of paths without any maximum since the domain of a path is a
set of prefixes generated by some _finite_ word.

Recall that, for a set $X$, both sets of paths $\mathrm{Path}(X)$ and stutter-
equivalent paths ${\mathrm{Path}}_{\sim}(X)$ are prefix orders. We want to
construct measures on both kinds of spaces, therefore below we work with a
class of _simple_ prefix orders which generalises both the structures.

######  Definition 14.

A prefix order is _simple_ if the history of every point is a finite set.

For example, the sets $\mathrm{Path}(X)$ and ${\mathrm{Path}}_{\sim}(X)$ are
simple prefix orders.

######  Proposition 18.

A directed subset of a prefix order is always totally ordered. In addition, an
irreducible downward closed subset of a prefix order is always totally
ordered.

Next, we construct a space $X^{\infty}$ consisting of all points from $X$ in
which the non-sober sets (w.r.t. Alexandroff topology) are added as limit
points.

$\displaystyle X^{\infty}=$ $\displaystyle\
X\cup\\{\infty_{C}\mid\text{$C\subseteq X$ is a non-sober set w.r.t.
Alexandroff topology}\\}.$ $\displaystyle\preceq^{\prime}=$
$\displaystyle\preceq\cup\ \\{(\infty_{C},\infty_{C})\mid\infty_{C}\in
X^{\infty}\\}\cup\\{(x,\infty_{C})\mid x\in C\\}.$

As an example, consider the prefix order $(\mathbb{N},\leq)$ with their
natural ordering. The sober space
$\mathbb{N}^{\infty}=\mathbb{N}\cup\\{\infty_{\mathbb{N}}\\}$ is isomorphic to
the well-known set of extended natural numbers $\mathbb{N}_{\omega}$.

######  Lemma 19.

The set $X^{\infty}$ is prefix ordered by the relation $\preceq^{\prime}$, if
$(X,\preceq)$ is a prefix order.

Henceforth, we do not distinguish between the relation $\preceq$ and
$\preceq^{\prime}$. Notice that being sober is a topological property and
therefore, we need a ‘right’ notion of topology on $X^{\infty}$ to qualify it
as sober. For instance, if we take upward closed sets as open sets (just like
in the case of $X$) we find that the space $X^{\infty}$ is still non-sober; as
a result, $X^{\infty}$ is non-sober w.r.t. Alexandroff topology. However, if
we endow $X^{\infty}$ with a Scott topology then the space becomes sober
w.r.t. this finer topology. For example, in the case of extended natural
numbers, the problematic case of the directed set $\mathbb{N}$ (which was non-
sober w.r.t. Alexandroff topology) is actually not a Scott-closed set222A
subset $C\subseteq X$ of a prefix order $(X,\preceq)$ is Scott closed if and
only if $C$ is downward closed and for any directed set $D\subseteq C$, if
$\sup D$ exists then $\sup D\in C$. since $\sup\mathbb{N}=\infty_{\mathbb{N}}$
and $\infty_{\mathbb{N}}\not\in\mathbb{N}$.

######  Proposition 20.

Let $(X,\preceq)$ be a simple prefix order. A subset $U\subseteq X^{\infty}$
is _Scott_ open if and only if $U$ is upward closed and it is inaccessible by
directed joins, i.e., for any directed set $D\subseteq X^{\infty}$ if $\sup D$
exists and $\sup D\in U$ then $D\cap U\neq\emptyset$. Let
$\mathcal{S}_{X^{\infty}}$ denote the collection of Scott open subsets of
$X^{\infty}$. Then, the space $(X^{\infty},\mathcal{S}_{X^{\infty}})$ is a
sober space.

To apply Theorem 17, we need to first construct a locally finite and Scott-
continuous valuation on our new sober space
$\mathrm{Path}^{\scriptscriptstyle\infty}(X)$. In the following theorem, we
will construct one such valuation on
$\mathrm{Path}^{\scriptscriptstyle\infty}(X)$ from an old valuation
$\mathcal{O}_{\mathrm{Path}(X)}\rTo^{\mu}\left[0,\infty\right]$.

######  Theorem 21.

Let $(X,\preceq)$ be a prefix order and let
$\mathcal{O}_{X}\rTo^{\mu}\left[0,\infty\right]$ be a locally finite and
Scott-continuous valuation. Then, the function
$\mathcal{S}_{X^{\infty}}\rTo^{\tilde{\mu}}\left[0,\infty\right]$ defined as
follows:

$\tilde{\mu}(V)=\mu(V\cap X)\quad\text{(for every Scott-open set
$V\in\mathcal{S}_{X^{\infty}}$)}$

is a Scott-continuous valuation. If $X$ is simple then $\tilde{\mu}$ is
locally finite.

As a result, the function $\tilde{\mu}$ lifts to a unique Borel measure on the
sigma-algebra
$\Sigma_{\mathrm{Path}^{\scriptscriptstyle\infty}(X)}=\mathcal{B}(\mathcal{S}_{\mathrm{Path}^{\scriptscriptstyle\infty}(X)})$
due to Theorem 17. However, in order to reflect back this measure on the
original sigma-algebra $\Sigma_{\mathrm{Path}(X)}$, it is sufficient to
establish that $\Sigma_{\mathrm{Path}(X)}$ is contained in the Borel sigma-
algebra induced by Scott-open sets, i.e.,
$\Sigma_{\mathrm{Path}(X)}\subseteq\Sigma_{\mathrm{Path}^{\scriptscriptstyle\infty}(X)}=\mathcal{B}(\mathcal{S}_{\mathrm{Path}^{\scriptscriptstyle\infty}(X)})$.
The next theorem states under what conditions the set-containment between the
two sigma-algebras
$\Sigma_{\mathrm{Path}(X)},\Sigma_{\mathrm{Path}^{\scriptscriptstyle\infty}(X)}$
is possible.

######  Theorem 22.

For countable sets $A$ and $X$, the sigma-algebra $\Sigma_{\mathrm{Path}(X)}$
is contained in the Borel sigma-algebra
$\Sigma_{\mathrm{Path}^{\scriptscriptstyle\infty}(X)}$. Moreover, we also have
$\Sigma_{{\mathrm{Path}}_{\sim}(X)}\subseteq\Sigma_{\mathrm{Path}^{\scriptscriptstyle\infty}_{\sim}(X)}$.

######  Corollary 2.

Suppose the sets $A$ and $X$ are countable. Then every locally finite and
Scott-continuous valuations
$\mathcal{O}_{\mathrm{Path}(X)}\rTo^{\mu}\left[0,\infty\right]$ and
$\mathcal{O}_{{\mathrm{Path}}_{\sim}(X)}\rTo^{\mu}\left[0,\infty\right]$ lifts
to a unique Borel measure
$\Sigma_{\mathrm{Path}(X)}\rTo^{\tilde{\mu}}\left[0,\infty\right]$ and
$\Sigma_{{\mathrm{Path}}_{\sim}(X)}\rTo^{\tilde{\mu}}\left[0,\infty\right]$,
respectively.

##  5 Probabilistic delay bisimulation

In this section, we use the concepts developed in the previous section to
characterise probabilistic delay bisimulation relation between the states of a
fully probabilistic system.

######  Definition 15.

A _(fully) probabilistic transition system_ is a triple $(X,A_{\tau},P)$
consisting of a countable set of states $X$, a countable set of actions
$A_{\tau}$, and a _probability transition function_ $X\times A_{\tau}\times
X\rTo^{P}\left[0,1\right]$ such that for every $x\in X$, the set
$\\{(a,x^{\prime})\mid 0<P(x,a,x^{\prime})\\}$ is finite and
$\sum_{(a,x^{\prime})\in A_{\tau}\times X}P(x,a,x^{\prime})\in\\{0,1\\}$.

Given a probabilistic transition system $(X,A_{\tau},P)$, an _execution_ $p$
is a path on $X$ such that $\forall_{\sigma a\in\mathrm{dom}(p)}\
0<P(p(\sigma),a,p(\sigma a)).$ Let $\mathrm{Exec}(x)$ be the set of all
executions starting from the state $x$. We write $\hat{a}=\varepsilon$ if
$a=\tau$ and $\hat{a}=a$ if $a\in A$.

######  Definition 16.

An equivalence relation $R\subseteq X\times X$ on a probabilistic transition
system $(X,A_{\tau},P)$ is a _probabilistic delay bisimulation_ [4, 21] if and
only if

$\forall_{x,x^{\prime}\in X}\ xRx^{\prime}\implies\forall_{x^{\prime\prime}\in
X,a\in A_{\tau}}\ \
P(x,\tau^{*}\hat{a},[x^{\prime\prime}]_{R})=P(x^{\prime},\tau^{*}\hat{a},[x^{\prime\prime}]_{R})\enspace.$

Two states $x,x^{\prime}\in X$ are _probabilistic delay bisimilar_ if and only
if there is a probabilistic delay bisimulation $R$ such that $xRx^{\prime}$.

Here, the probabilities associated with weak transitions are defined
(originally given in [22]) in the following way. For $x\in X,Y\subseteq
X,L\subseteq A_{\tau}^{*}$, we let

  * •

$\begin{aligned} x\xrightarrow{L}Y=&\
\\{p\in\mathrm{Exec}(x)\mid\mathrm{trace}(p)\in L\land\mathrm{last}(p)\in Y\
\land\\\ &\ \qquad\forall_{q}\ (q\prec p\land\mathrm{trace}(q)\in
L)\implies\mathrm{last}(q)\not\in Y\\}.\end{aligned}$

  * •

$P(x,L,Y)=\sum_{p\in x\xrightarrow{L}Y}\mu_{P}(p)$, where
$\mathrm{Path}(X)\rTo^{\mu_{P}}\left[0,1\right]$ is defined as:

$\mu_{P}(p)=\begin{cases}\prod_{\sigma
a\in\mathrm{dom}(p)}P(p(\sigma),a,p(\sigma a)),&\text{if
}p\in\mathrm{Exec}(x),\ \text{for some $x\in X$}\\\
0,&\text{otherwise}\end{cases}.$

######  Proposition 23.

For a given fully probabilistic system $(X,A_{\tau},P)$, the induced function
$\mu_{P}$ on paths is order reversing. Moreover, $\mu_{P}(\varepsilon_{x})=1$
(for any $x\in X$).

In contrast to Section 3, our base category will be rather the category of
measurable spaces and measurable functions $\mathbf{Meas}$.

######  Definition 17.

Below we recall the well known Giry functor $\mathcal{G}$ (see e.g. [17]):

  * •

Let $(X,\Sigma_{X})$ be a measurable space. Then,
$\mathcal{G}(X,\Sigma_{X})=(\mathcal{G}X,\Sigma_{\mathcal{G}X})$, where
$\mathcal{G}X$ is the set of all probability measures on the measurable space
$(X,\Sigma_{X})$. The sigma-algebra $\Sigma_{\mathcal{G}X}$ is the smallest
sigma-algebra such that the evaluation maps
$\mathcal{G}X\rTo^{\epsilon_{U}}\left[0,1\right]$ are Borel measurable, for
every $U\in\Sigma_{X}$.

  * •

For any arrow $X\rTo^{f}Y$ in $\mathbf{Meas}$, we let
$\mathcal{G}(f)(\mu)=\mu\circ{f}^{-1}$.

Figure 3: An example motivating separation closure.

To motivate the next definition, consider the transition system depicted in
Figure 3 and assume a nonzero probability with each of the drawn transitions.
Furthermore, let $p_{1},p_{1}^{\prime}$, and $p_{2}$ be the three executions
that reach the states $x_{1},x_{1}^{\prime}$, and $x_{2}$, resp., from the
state $x_{0}$. Notice that
$P(x_{0},\tau^{*},\\{x_{1},x_{1}^{\prime},x_{2}\\})$ is the sum of the
probabilities associated only with the executions $p_{1},p_{2}$. The execution
$p_{1}^{\prime}$ is not considered in the above computation because one can
reach the set of target states $\\{x_{1},x_{1}^{\prime},x_{2}\\}$ with the
execution $p_{1}$ which is a prefix of $p_{1}^{\prime}$. This means, the
execution $p_{1}^{\prime}$ is redundant and neglected while computing the
probability to reach the above target states. Such redundancies at the level
of paths are identified by the following notion of separation closure.

######  Definition 18.

Let $(X,\mathcal{O}_{X})$ be an Alexandroff space. The _separation closure_ of
a subset $U\subseteq X$ is the set $U^{\star}=\\{x\in U\mid\mathrm{cl}(x)\cap
U=\\{x\\}\\}.$ A subset $U\subseteq X$ is _separated_ if $U=U^{\star}$.

In the context of the previous example (Figure 3), let
$U=\\{p_{1},p_{1}^{\prime},p_{2}\\}$. Then, we find that $\downarrow\\!{x}\cap
U=\\{x\\}$, for $x\in\\{p_{1},p_{2}\\}$, while for the execution
$p_{1}^{\prime}$ we find that $\downarrow\\!{p_{1}^{\prime}}\cap
U=\\{p_{1},p_{2}\\}$. Thus, $U^{\star}=\\{p_{1},p_{2}\\}$ which were the only
executions needed to compute the probability to reach one of the target
states. Incidentally, a separated subset of paths $U\subseteq\mathrm{Path}(X)$
(i.e., $U=U^{\star}$) is minimal in the sense that any two distinct paths
$p,p^{\prime}\in U$ are not in the prefix relation $\preceq$, i.e.,
$p\not\preceq p^{\prime}$ and $p^{\prime}\not\preceq p$. The following
proposition asserts this.

######  Proposition 24.

In an Alexandroff space $(X,\mathcal{O}_{X})$, a separated subset $U\subseteq
X$ (i.e., $U=U^{\star}$) has topologically distinguishable points. Moreover,

  1. 1.

the separation closure of a set is always separated, i.e.,
$U^{\star}={U^{\star}}^{\star}$, for any $U\subseteq X$.

  2. 2.

the collection of separated sets is hereditary, i.e., if $U_{1}\subseteq
U_{2}$ and $U_{2}=U_{2}^{\star}$, then $U_{1}=U_{1}^{\star}$.

  3. 3.

for any subset $U\subseteq X$, we have $(\uparrow\\!{U})^{\star}\subseteq
U^{\star}$. Moreover the converse also holds, if the underlying space $X$ is a
$T_{0}$ space. Here, upward closure is w.r.t. the specialisation order
$\preceq$, i.e., $x\preceq
x^{\prime}\iff\mathrm{cl}(x)\subseteq\mathrm{cl}(x^{\prime})$, for any
$x,x^{\prime}\in X$.

Thus, separation closure provides an alternative way to compute $P(x,L,Y)$.

######  Lemma 25.

For a given system $(X,A_{\tau},P)$, define the set $x\ext@arrow
0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{L}{}Y=\\{p\in\mathrm{Path}(X)\mid
p(\varepsilon)=x\land\mathrm{trace}(p)\in L\land\mathrm{last}(p)\in Y\\}.$
Then, $\sum_{p\in x\xrightarrow{L}Y}\mu_{P}(p)=\sum_{p\in(x\ext@arrow
0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{L}{}Y)^{\star}}\mu_{P}(p)$.

It should be noted that for a given probabilistic transition system
$(X,A_{\tau},P)$, we have $x\xrightarrow{L}Y\subseteq(x\ext@arrow
0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{L}{}Y)^{\star}$; however,
the converse is not true in general.

The next theorem highlights a property characteristic to fully probabilistic
systems. It states that if a separated subset of paths $U$ has a lower bound
$p$, i.e., $\forall_{q\in U}\ p\preceq q$, then the sum of probabilities
associated with each path in $U$ is bounded by the weight of $p$. This
property is due to the order reversing nature of the function $\mu_{P}$ (cf.
Proposition 23).

######  Theorem 26.

Given a system $(X,A_{\tau},P)$, a path $p\in\mathrm{Path}(X)$, and a
separated set of paths $U\subseteq\mathrm{Path}(X)$ such that $p\preceq U$,
i.e., $\forall_{q\in U}\ p\preceq q$. Then, $\sum_{q\in
U}\mu_{P}(q)\leq\mu_{P}(p)$.

Next we focus on the construction of probability measures on the space
$\mathrm{Path}(X)$. From Corollary 2, it suffices to construct a locally-
finite and Scott-continuous valuation on the open subsets of paths. The
following theorem extends the function $\mu_{P}$ (induced by a given fully
probabilistic system $(X,A_{\tau},P)$) to such a valuation on paths.

######  Theorem 27.

Given a system $(X,A_{\tau},P)$, then the function
$\mathcal{O}_{\mathrm{Path}(X)}\rTo^{\tilde{\mu}_{P}}\left[0,\infty\right]$
defined as $\tilde{\mu}_{P}(U)=\mu_{P}(U^{\star})$ (for every open set $U$) is
a locally finite and Scott-continuous valuation.

Now we have all the technical machinery to encode a given probabilistic
transition system $(X,A_{\tau},P)$ as a coalgebra
$X\rTo^{\alpha}\mathcal{G}{\mathrm{Path}}_{\sim}(X)$, where
$\Sigma_{X}=\mathcal{P}(X)$ (since $X$ is countable). The transition system
$\alpha$ is defined, coalgebraically, as follows:

$\alpha(x)(U)=\tilde{\mu}_{P}({\pi_{X}}^{-1}(U)\
\cap\uparrow\\!{\varepsilon_{x}}),\qquad\text{for every}\
U\in\Sigma_{{\mathrm{Path}}_{\sim}(X)}\enspace.$ (2)

Here, we abuse notation by using $\tilde{\mu}_{P}$ to denote a measure on
$\Sigma_{\mathrm{Path}(X)}$. Note that this measure is rather constructed by
extending the valuation given in Theorem 27.

######  Proposition 28.

The mapping in (2) is a probability measure.

Now we are ready to state the main result of this section.

######  Theorem 29.

Two states are probabilistic delay bisimilar if and only if they are
$\mathcal{G}\circ\mathrm{Path}_{\sim}$-behaviourally equivalent.

###### Proof.

$\Rightarrow$ Let $R$ be a probabilistic delay bisimulation, let $(X,\alpha)$
be the $\mathcal{G}\circ\mathrm{Path}_{\sim}$-coalgebra induced by
$(X,A_{\tau},P)$, and let $X\rTo^{f}X/R$ be the quotient map. We will
construct a coalgebra on the quotient set $X/R$ in two stages. First, we
construct a measure $\nu_{f(x)}$ (for each $x\in X$) on the space
${\mathrm{Path}}_{\sim}(X/R)$ using the extension result (cf. Corollary 2)
such that it coincides with the pushforward measure $(\alpha(x))_{*}$ on the
open subsets $V\in\mathcal{O}_{{\mathrm{Path}}_{\sim}(X/R)}$. Second, we
invoke the well-known application (taken from [17, Proposition 2.10]) of
Dynkin’s $\lambda-\pi$ theorem to conclude that the measure
$\nu_{f(x)}=(\alpha(x))_{*}$.

Let $x\in X$. Define a function
$\mathcal{O}_{{\mathrm{Path}}_{\sim}(X/R)}\rTo^{\nu_{f(x)}}\left[0,\infty\right]$
as follows:

$\nu_{f(x)}(V)=\tilde{\mu}_{P}({\pi}^{-1}{{\mathrm{Path}}_{\sim}(f)}^{-1}V\cap\uparrow\\!{\varepsilon_{x}}),\qquad\text{for
every}\ V\in\mathcal{O}_{{\mathrm{Path}}_{\sim}(X/R)}.$ (3)

We need a technical result proven in [21, Lemma 24] in order to show that
$\nu_{f(x)}$ is well defined, i.e., for any $xRx^{\prime}$ and open set
$V\in\mathcal{O}_{{\mathrm{Path}}_{\sim}(X/R)}$ we have
$\nu_{f(x)}(V)=\nu_{f(x^{\prime})}(V)$. (See Theorem V.6 for the proof of this
claim). Moreover, the function $\nu_{f(x)}$ is a valuation, which immediately
follows from (3) and the fact that $\mu$ is a valuation. Therefore, from
Corollary 2, the valuation $\nu_{f(x)}$ extends to a Borel measure
$\tilde{\nu}_{f(x)}$ on the space ${\mathrm{Path}}_{\sim}(X/R)$.

Recall that the pushforward measure
$(\alpha(x))_{*}(V)=\alpha(x)({{\mathrm{Path}}_{\sim}(f)}^{-1}(V))$ (for each
Borel set $V\in\Sigma_{{\mathrm{Path}}_{\sim}(X/R)}$), is also a measure on
the space ${\mathrm{Path}}_{\sim}(X/R)$. Clearly, for any
$V\in\mathcal{O}_{{\mathrm{Path}}_{\sim}(X/R)}$, we have
$(\alpha(x))_{*}(V)=\nu_{f(x)}(V)=\tilde{\nu}_{f(x)}(V)$ due to Equation (2).
Since both $\tilde{\nu}_{f(x)}$ and $(\alpha(x))_{*}$ are probability
measures, so from [17, Proposition 2.10] we get
$\tilde{\nu}_{f(x)}=(\alpha(x))_{*}$. Now letting
$\beta(f(x))=\tilde{\nu}_{f(x)}$, we find that $f$ is a coalgebra homomorphism
because
$\beta(f(x))(V)=\tilde{\nu}_{f(x)}(V)=(\alpha(x))_{*}(V)=\alpha(x)({{\mathrm{Path}}_{\sim}(f)}^{-1}V)$,
for every $V\in\Sigma_{{\mathrm{Path}}_{\sim}(X/R)}$.

$\Leftarrow$ Let $(X,A_{\tau},P)$ be a fully probabilistic system and
$(X,\alpha)$ be the corresponding
$\mathcal{G}\circ\mathrm{Path}_{\sim}$-coalgebra. Moreover, let $(Y,\beta)$ be
a $\mathcal{G}\circ\mathrm{Path}_{\sim}$-coalgebra and $X\rTo^{f}Y$ be a
$\mathcal{G}\circ\mathrm{Path}_{\sim}$ coalgebra homomorphism. In the appendix
(Theorem V.6), we show that the equivalence relation $xRx^{\prime}\iff
f(x)=f(x^{\prime})$ is a probabilistic delay bisimulation. Below we rather
illustrate why $R$ is a witnessing bisimulation relation. ∎

Consider the two probabilistic transition systems drawn below,

$x_{1}$$\alpha:$$x_{2}$$x_{3}$$x_{4}$$x_{1}^{\prime}$$x_{2}^{\prime}$$x_{3}^{\prime}$$x_{4}^{\prime}$$\tau,\frac{1}{3}$$\tau,\frac{1}{3}$$a,\frac{1}{3}$$b,1$$\tau,\frac{1}{2}$$a,\frac{1}{2}$$b,1$$y_{1}$$\beta:$$y_{2}$$y_{3}$$y_{4}$$\tau,\frac{1}{2}$$a,\frac{1}{2}$$b,1$

together with the path-based coalgebras
$X\rTo^{\alpha}\mathcal{G}{\mathrm{Path}}_{\sim}(X)$ and
$Y\rTo^{\beta}\mathcal{G}{\mathrm{Path}}_{\sim}(Y)$ where
$X=\\{x_{i},x_{j}^{\prime}\mid i,j\in\\{1,2,3,4\\}\\}$ and $Y=\\{y_{i}\mid
i\in\\{1,2,3,4\\}\\}$. Furthermore, let $X\rTo^{f}Y$ be a function defined as
$f(z_{i})=y_{i}$, where $z\in\\{x,x^{\prime}\\}$ and $i\in\\{1,2,3,4\\}$. To
see why the relation $R$ (as defined above) is a witnessing bisimulation,
consider the equation

$\alpha(x_{1})\Big{(}\bigcup_{p\in x_{1}\ext@arrow
0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{\tau^{*}b}{}[x_{4}]_{R}}\uparrow\\!{{[p]}_{\sim}}\Big{)}=\alpha(x_{1}^{\prime})\Big{(}\bigcup_{p\in
x_{1}^{\prime}\ext@arrow
0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{\tau^{*}b}{}[x_{4}]_{R}}\uparrow\\!{{[p]}_{\sim}}\Big{)},$
(4)

which can be derived from the facts $x_{1}Rx_{1}^{\prime}$ and $\beta\circ
f=\mathcal{G}{\mathrm{Path}}_{\sim}(f)\circ\alpha$ (see Theorem V.6 for the
proof in the general case). The two terms in Equation 4 denote the
probabilities of reaching the equivalence class $[x_{4}]_{R}$ from the states
$x_{1}$ and $x_{1}^{\prime}$. This can be seen, for instance, by deriving
$\alpha(x_{1})(\bigcup_{p\in x_{1}\ext@arrow
0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{\tau^{*}b}{}[x_{4}]_{R}}\uparrow\\!{{[p]}_{\sim}})=P(x_{1},\tau^{*}b,[x_{4}]_{R})$
using Equation 2, definition of $\tilde{\mu}_{P}$, Proposition 3, and Lemma
25. Moreover, the probability to reach the equivalence class $[x_{4}]_{R}$
from $x_{1},x_{1}^{\prime}$ is $\frac{1}{2}$ because
$P(x_{1},\tau^{*}b,[x_{4}]_{R})=\sum_{i=1}^{\infty}(\frac{1}{3})^{i}=\frac{1}{2}=P(x_{1}^{\prime},\tau^{*}b,[x_{4}]_{R})$.

##  6 Discussion and conclusion

The main message of this paper is that behavioural equivalence in a path-based
coalgebra is sufficient to capture branching bisimulation. In particular, we
considered coalgebras of type $F\circ\mathrm{Path}_{\sim}$ over a concrete
category $\mathbf{C}$, where $F$ is an endofunctor modelling the branching
type of the system under investigation. We showed that behavioural equivalence
when $F=\mathcal{P}$ and $\mathbf{C}=\mathbf{Set}$ coincides with the
traditional branching bisimulation [25]. In a similar spirit, we also showed
that behavioural equivalence when $F=\mathcal{G}$ and
$\mathbf{C}=\mathbf{Meas}$ coincides with the probabilistic delay bisimulation
[4, 21, 22].

Interestingly, in the case of labelled transition systems, we can use the
final chain based algorithm presented in [1] to minimise the system with
respect to branching bisimulation. The following prerequisites for this
algorithm are satisfied in this context: first, a terminal object exists in
$\mathbf{Set}$; second, $\mathbf{Set}$ is equipped with a
(epi,mono)-factorisation structure; third, the functor
$\mathcal{P}\circ\mathrm{Path}_{\sim}$ preserves monomorphisms. However, for
the probabilistic case, more research is required to find out whether the
above conditions are valid or not.

In retrospect, our paper comes short in one regard when comparing with the
recent works [7, 9, 12] on capturing weak bisimulation; namely, there is no
abstract construction given to construct our path-based coalgebras from the
system under study. In particular, we would like to construct a path-based
coalgebra, for instance, $X\rTo^{\alpha^{\prime}}F{\mathrm{Path}}_{\sim}(X)$
from a given coalgebra of type $X\rTo^{\alpha}F(A_{\tau}\times X)$.

In this regard, it might be interesting to extend the initial work of [13]
[13]: Given a system $X\rTo TFX$ over $\mathbf{Set}$ ($T$ is a monad modelling
the branching type and $F$ is an endofunctor modelling the transition type),
then the traces (executions) can be described as an arrow $X\rTo I$ ($X\times
I\rTo I$) in the Kleisli category of $T$ with $I$ being the initial algebra of
$F$. Note that this insight of [13] works under some technical requirements
and it is unclear whether these requirements hold in a more general setting of
$\mathbf{Meas}$. This was already voiced by [15] [15] in conjunction with
generic trace semantics for probabilistic systems that were modelled over the
base category $\mathbf{Meas}$.

Another way to generalise the result of this paper is to consider the
executions of a system as first-class citizens from the onset. Such a venture
is carried out by [10] [10] under the banner of prefix orders. Prefix orders
are partially ordered sets whose principal ideals are totally ordered sets.
The homomorphisms on such structures are called history preserving functions,
those order preserving functions that preserve the principal ideals of the
underlying ordered sets. [5] [5] extended the theory of open maps [14] to the
concrete category setting to get a characterisation of traditional branching
bisimulation. Therefore, it will be worthwhile to study whether the measure
theoretic concepts proposed here can be lifted to the more general setting of
prefix orders to capture probabilistic branching bisimulation. Lastly, it will
be interesting to construe a notion of behavioural equivalence in the open map
approach akin to the theory of coalgebras, where the notion of bisimulation is
parametric to a functor modelling the branching type of system under study.

### Acknowledgements

The authors thank the anonymous reviewers of the conference CALCO’17 for their
feedbacks on an earlier draft of this paper. The authors also thank Barbara
König for various discussions regarding this work and for her earlier comments
which led to significant improvements of this paper. The authors would also
like to thank Pieter Cuijpers for his various feedbacks and continuing support
over the course of this work.

This work has been carried out as part of the “Behavioural Equivalences:
Environmental Aspects, Metrics and Generic Algorithms” (BEMEGA) project
supported by Deutsche Forschungsgemeinschaft (DFG).

## References

  * [1] J. Adámek, F. Bonchi, M. Hülsbusch, B. König, S. Milius and A. Silva  “A Coalgebraic Perspective on Minimization and Determinization” LNCS/ARCoSS 7213  In _Proc. of FOSSACS ’12_ Springer, 2012, pp. 58–73
  * [2] P. Alexandroff  “Diskrete Räume”  In _Rec. Math. N.S._ 2(44).3, 1937, pp. 501–519
  * [3] M. Alvarez-Manilla  “Extension of valuations on locally compact sober spaces”  In _Topology and its Applications_ 124.3, 2002, pp. 397 –433
  * [4] C. Baier and H. Hermanns  “Weak Bisimulation for Fully Probabilistic Processes”  In _Proc. of CAV_ London, UK: Springer, 1997, pp. 119–130
  * [5] H. Beohar and P.J.L. Cuijpers  “Open Maps in Concrete Categories and Branching Bisimulation for Prefix Orders”  In _ENTCS_ 319, 2015, pp. 51 –66  DOI: http://dx.doi.org/10.1016/j.entcs.2015.12.005
  * [6] F. Bonchi, S. Milius, A. Silva and F. Zanasi  “Killing epsilons with a dagger: A coalgebraic study of systems with algebraic label structure” Coalgebraic Methods in Computer Science  In _TCS_ 604, 2015, pp. 102 –126
  * [7] T. Brengos  “On Coalgebras with Internal Moves”  In _Proc. of CMCS_ Springer, 2014, pp. 75–97  DOI: 10.1007/978-3-662-44124-4_5
  * [8] T. Brengos  “Weak bisimulation for coalgebras over order enriched monads”  In _Logical Methods in Computer Science_ 11.2, 2015  DOI: 10.2168/LMCS-11(2:14)2015
  * [9] T. Brengos, M. Miculan and M. Peressotti  “Behavioural equivalences for coalgebras with unobservable moves”  In _JLAP_ 84.6, 2015, pp. 826 –852  DOI: http://dx.doi.org/10.1016/j.jlamp.2015.09.002
  * [10] P.J.L. Cuijpers  “Prefix orders as a general model of dynamics”  In _Proc. of Developments in Computation Models_ , DCM’13, 2013, pp. 25–29
  * [11] A. Finkel and J. Goubault-Larrecq  “Forward Analysis for WSTS, Part I: Completions”  In _Proc. of STACS_ 3 Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 2009, pp. 433–444
  * [12] S. Goncharov and D. Pattinson  “Coalgebraic Weak Bisimulation from Recursive Equations over Monads”  In _Proc. of ICALP, Part II_ Springer, 2014, pp. 196–207  DOI: 10.1007/978-3-662-43951-7_17
  * [13] B. Jacobs and A. Sokolova  “Traces, Executions and Schedulers, Coalgebraically”  In _CALCO’09_ Springer, pp. 206–220  DOI: 10.1007/978-3-642-03741-2_15
  * [14] A. Joyal, M. Nielson and G. Winskel  “Bisimulation and open maps”  In _Proc. of 8th Annual IEEE Symposium on Logic in Computer Science_ , 1993, pp. 418–427  DOI: 10.1109/LICS.1993.287566
  * [15] H. Kerstan and B. König  “Coalgebraic Trace Semantics for Continuous Probabilistic Transition Systems”  In _Logical Methods in Computer Science_ 9.4, 2013  DOI: 10.2168/LMCS-9(4:16)2013
  * [16] R. Milner  “A Calculus of Communicating Systems” 92, Lecture Notes in Computer Science  Berlin Heidelberg: Springer, 1980
  * [17] P. Panangaden  “Labelled Markov Processes”  London: Imperial College Press, 2009
  * [18] H. L. Royden and P. M. Fitzpatrick  “Real analysis”  Pearson, 2010
  * [19] J.J.M.M. Rutten  “Universal coalgebra: a theory of systems”  In _TCS_ 249.1, 2000, pp. 3 –80  DOI: http://dx.doi.org/10.1016/S0304-3975(00)00056-6
  * [20] A. Sokolova  “Personal communication”, 2016
  * [21] A. Sokolova, E. de Vink and H. Woracek  “Coalgebraic Weak Bisimulation for Action-Type Systems”  In _SACS_ 19 “A.I. Cuza” University Press, Iaşi, 2009, pp. 93–144  “A.I. Cuza” University, Iaşi, România
  * [22] A. Sokolova, E. Vink and H. Woracek  “Weak Bisimulation for Action-Type Coalgebras”  In _ENTCS_ 122, 2005, pp. 211 –228  DOI: http://dx.doi.org/10.1016/j.entcs.2004.06.050
  * [23] R.J. Glabbeek  “The linear time — Branching time spectrum II”  In _Proc. of CONCUR_ Springer, 1993, pp. 66–81  DOI: 10.1007/3-540-57208-2_6
  * [24] R.J. Glabbeek  “What is Branching Time Semantics and Why to Use It?”  In _Current Trends in Theoretical Computer Science_ River Edge, USA: World Scientific Publishing, 2001, pp. 469–479
  * [25] R.J. Glabbeek and W.P. Weijland  “Branching Time and Abstraction in Bisimulation Semantics”  In _J. ACM_ 43.3 New York, NY, USA: ACM, 1996, pp. 555–600  DOI: 10.1145/233551.233556

##  Appendix I Nondeterministic Automata: The spectrum of bisimulations in the
presence of silent transitions

We have already seen how to capture branching bisimulation using the
$\mathit{Path}_{\sim}$ functor. By adapting the modelling technique for the
coalgebra $\alpha$ to saturate leading or trailing sequences of $\tau$
transitions, we can obtain delay, $\eta$ and weak bisimulation as well. For
this purpose, we model $(X,\rightarrow)$ coalgebraically as
$\alpha:X\rightarrow\mathcal{P}(\mathit{Path}_{\sim}(X))$ as follows:

Weak Bisimulation

$\displaystyle\alpha(x)=\\{[(p(\epsilon),a,p(\tau^{n}a\tau^{m}))]\mid$
$\displaystyle\mathsf{dom}(p)=\tau^{n}a\tau^{m},$ $\displaystyle\forall
i<n:p(\tau^{i})\xrightarrow{\tau}p(\tau^{i+1}),$ $\displaystyle\
p(\tau^{n})\xrightarrow{a}p(\tau^{n}a),$ $\displaystyle\forall
j<m:p(\tau^{n}a\tau^{j})\xrightarrow{\tau}p(\tau^{n}a\tau^{j+1}),$
$\displaystyle a\in A_{\tau}\\}\cup\\{[x]\mid x\in X\\}$

$\eta$ Bisimulation

$\displaystyle\alpha(x)=\\{[q]\mid$ $\displaystyle
q=(p(\epsilon),\tau,p(\tau),...,p(\tau^{n})a,p(\tau^{n}a\tau^{m})),$
$\displaystyle\mathsf{dom}(p)=\tau^{n}a\tau^{m},$ $\displaystyle\forall
i<n:p(\tau^{i})\xrightarrow{\tau}p(\tau^{i+1}),$ $\displaystyle\
p(\tau^{n})\xrightarrow{a}p(\tau^{n}a),$ $\displaystyle\forall
j<m:p(\tau^{n}a\tau^{j})\xrightarrow{\tau}p(\tau^{n}a\tau^{j+1}),$
$\displaystyle a\in A_{\tau}\\}\cup\\{[x]\mid x\in X\\}$

Delay Bisimulation

$\displaystyle\alpha(x)=\\{[q]\mid$ $\displaystyle
q=(p(\epsilon),a,p(\tau^{n}a),\tau,p(\tau^{n}a\tau),...,p(\tau^{n}a\tau^{m})),$
$\displaystyle\mathsf{dom}(p)=\tau^{n}a\tau^{m},$ $\displaystyle\forall
i<n:p(\tau^{i})\xrightarrow{\tau}p(\tau^{i+1}),$ $\displaystyle\
p(\tau^{n})\xrightarrow{a}p(\tau^{n}a),$ $\displaystyle\forall
j<m:p(\tau^{n}a\tau^{j})\xrightarrow{\tau}p(\tau^{n}a\tau^{j+1}),$
$\displaystyle a\in A_{\tau}\\}\cup\\{[x]\mid x\in X\\}$

Using an example that allows to distinguish all four notions of bisimulation,
we will demonstrate these ways of modelling LTS.

######  Example I.1.

Consider the set of actions $A_{\tau}=\\{a,b,\tau\\}$ that contains two non-
silent transition $a$ and $b$. We define a transition system over $A_{\tau}$
and the state set $X=\\{A,B,C,D,E\\}$ as depicted below:

$A$$B$$C$$D$$E$$a,\tau$$\tau$$b$$\tau$$b$$\tau$$a,b,\tau$$\tau$$b$$a$

We will now model this system using the $\mathcal{P}\circ\mathsf{Path}_{\sim}$
functor in order to get each of the four notions of bisimilarity as the
behavioural equivalence and compute Algorithm B (or, equivalently, Algorithm
C). We will identify each equivalence class of paths with its paths and write
down the computed sets of paths explicitly. The paths that are redundant are
printed in grey. Redundant in this context means that there exists another
representative of the same equivalence class in the set.

Branching Bisimulation

To obtain branching bisimulation as behavioural equivalence, we model the
transition system by the following table:

$\alpha\colon X\rightarrow\mathcal{P}(\mathit{Path}_{\sim}(X))$
---
$A$ | $\\{(A),(A,b,A),(A,b,A,\tau,D),(A,a,D),(A,\tau,D),(A,\tau,E),(A,\tau,E,a,D),(A,b,A,\tau,E)\\}$
$B$ | $\\{(B),(B,b,B),(B,b,B,\tau,E),(B,\tau,E),(B,\tau,E,a,D),(B,\tau,D),(B,b,B,\tau,D)\\}$
$C$ | $\\{(C),(C,b,C),(C,b,C,\tau,D),(C,a,D),(C,b,D),(C,\tau,D),(C,\tau,E),(C,\tau,E,a,D)\\}$
$D$ | $\\{(D)\\}$
$E$ | $\\{(E),(E,a,D)\\}$

Weak Bisimulation

To obtain weak bisimulation as behavioural equivalence, we model the
transition system by the following table:

$\alpha\colon X\rightarrow\mathcal{P}(\mathit{Path}_{\sim}(X))$
---
$A$ | $\\{(A),(A,b,A),(A,b,D),(A,b,E),(A,\tau,D),(A,\tau,E),(A,a,D)\\}$
$B$ | $\\{(B),(B,b,B),(B,b,D),(B,b,E),(B,\tau,D),(B,\tau,E),(B,a,D)\\}$
$C$ | $\\{(C),(C,b,C),(C,b,D),(C,b,E),(C,\tau,D),(C,\tau,E),(C,a,D)\\}$
$D$ | $\\{(D)\\}$
$E$ | $\\{(E),(E,a,D)\\}$

$\eta$ Bisimulation

To obtain $\eta$ bisimulation as behavioural equivalence, we model the
transition system by the following table:

$\alpha\colon X\rightarrow\mathcal{P}(\mathit{Path}_{\sim}(X))$
---
$A$ | $\\{(A),(A,\tau,D),(A,\tau,E),(A,\tau,E,a,D),(A,b,A),(A,b,D),(A,b,E),(A,a,D)\\}$
$B$ | $\\{(B),(B,\tau,D),(B,\tau,E),(B,\tau,E,a,D),(B,b,B),(B,b,D),(B,b,E)\\}$
$C$ | $\\{(C),(C,\tau,D),(C,\tau,E),(C,\tau,E,a,D),(C,b,C),(C,b,D),(C,b,E),(C,a,D)\\}$
$D$ | $\\{(D)\\}$
$E$ | $\\{(E),(E,a,D)\\}$

Delay Bisimulation

Finally, to obtain delay bisimulation as behavioural equivalence, we model the
transition system by the following table:

$\alpha\colon X\rightarrow\mathcal{P}(\mathit{Path}_{\sim}(X))$
---
$A$ | $\\{(A),(A,\tau,D),(A,\tau,E),(A,a,D),(A,b,A),(A,b,A,\tau,D),(A,b,A,\tau,E)\\}$
$B$ | $\\{(B),(B,\tau,D),(B,\tau,E),(B,a,D),(B,b,B),(B,b,B,\tau,D),(B,b,B,\tau,E)\\}$
$C$ | $\\{(C),(C,\tau,D),(C,\tau,E),(C,a,D),(C,b,C),(C,b,C,\tau,D),(C,b,C,\tau,E),(C,b,D)\\}$
$D$ | $\\{(D)\\}$
$E$ | $\\{(E),(E,a,D)\\}$

##  Appendix II Proofs concerning Section 2

######  Proposition II.1 (Proposition 1).

Let $X\rTo^{f}Y$ be a function. Then, for every path $p\in\mathrm{Path}(X)$ we
have $\mathrm{trace}(p)=\mathrm{trace}(fp)$ and
$f\mathrm{last}(p)=\mathrm{last}(fp)$.

###### Proof.

Let $p\in\mathrm{Path}(X)$. Then,
$\mathrm{trace}(p)=\max\mathrm{dom}(p)=\max\mathrm{dom}(fp)=\mathrm{trace}(fp)$.
Furthermore,
$\mathrm{last}(fp)=fp\max\mathrm{dom}(fp)=fp\max\mathrm{dom}(p)=f\mathrm{last}(p)$.
∎

######  Theorem II.2 (Theorem 2).

For any path there is a unique stutter basis for the given path.

###### Proof.

Let $\phi,\phi^{\prime}$ be the two witnessing stutter bases for $p$ with
$\sigma=\max\mathrm{dom}(p)$. We prove $\phi=\phi^{\prime}$ by structural
induction on the words in $\downarrow\\!{\sigma}$. Without loss of generality,
let $\sigma^{\prime}a\in\downarrow\\!{\sigma}$. Then, we distinguish the
following cases:

  1. 1.

Let $a\in A$. Then, by the induction hypothesis we have
$\phi(\sigma^{\prime})=\phi^{\prime}(\sigma^{\prime})\implies\phi(\sigma^{\prime})a=\phi^{\prime}(\sigma^{\prime})a\implies\phi(\sigma^{\prime}a)=\phi^{\prime}(\sigma^{\prime}a).$

  2. 2.

Let $a=\tau$. Let $p(\sigma^{\prime}\tau)=p(\sigma^{\prime})$. (The proof of
the other case when $p(\sigma^{\prime}\tau)\neq p(\sigma^{\prime})$ is similar
to the previous case.) Again using the induction hypothesis we get
$\phi(\sigma^{\prime})=\phi^{\prime}(\sigma^{\prime})\implies\phi(\sigma^{\prime}\tau)=\phi^{\prime}(\sigma^{\prime}\tau)$.∎

######  Lemma II.3 (Lemma 3).

Let $\phi$ be the stutter basis for a given path $p$ with
$\mathrm{dom}(p)=\downarrow\\!{\sigma}$. Then, $\phi(\downarrow\\!{\sigma})=\
\downarrow\\!{\phi(\sigma)}.$

###### Proof.

Let $\phi$ be the stutter basis for the path $p$ with
$\mathrm{dom}(p)=\downarrow\\!{\bar{\sigma}}$. To prove that $\phi$ is history
preserving, it suffices to show that $\phi$ is order preserving and $\phi$
satisfies the backward simulation property (i.e.,
$\forall_{\sigma^{\prime},\sigma}\
\sigma^{\prime}\preceq\phi(\sigma)\implies\exists_{\sigma^{\prime\prime}}\
\sigma^{\prime\prime}\preceq\sigma\land\phi(\sigma^{\prime\prime})=\sigma^{\prime}$).
For order preservation, consider $\sigma\preceq\sigma^{\prime}$, for some
$\sigma,\sigma^{\prime}\in\downarrow\\!{\bar{\sigma}}$. Without loss of
generality, let $\sigma^{\prime}=\sigma a$. Then, either
$\phi(\sigma^{\prime})=\phi(\sigma)a$ or $\phi(\sigma^{\prime})=\phi(\sigma)$.
I.e., in either case we have $\phi(\sigma)\preceq\phi(\sigma^{\prime})$.

For the backward simulation, let $\sigma^{\prime}\preceq\phi(\sigma)$. Again,
without loss of generality, let $\phi(\sigma)=\sigma^{\prime}a$. If
$a\neq\varepsilon$, then by the construction of $\phi$, we know that there is
some $\sigma^{\prime\prime}$ such that
$\sigma=\sigma^{\prime\prime}a\land\phi(\sigma^{\prime\prime})=\sigma^{\prime}$.
If $a=\varepsilon$, then again by the construction of $\phi$ we know that
there is some $\sigma^{\prime\prime}$ such that
$\sigma=\sigma^{\prime\prime}\tau\land\phi(\sigma^{\prime\prime})=\sigma^{\prime}$.
Thus, there is some $\sigma^{\prime\prime}$ such that
$\sigma^{\prime\prime}\preceq\sigma$ and
$\phi(\sigma^{\prime\prime})=\sigma^{\prime}$. ∎

######  Lemma II.4 (Lemma 4).

For any $p\in\mathrm{Path}(X)$ and any $X\rTo^{f}Y$, we have
$f\circ{p}^{{\dagger}}\sim f\circ p$.

###### Proof.

Let $\phi,\phi^{\prime},\phi^{\prime\prime}$ be the stutter bases for the
paths $fp,p,f{p}^{{\dagger}}$, respectively. Consider the following
commutative diagram with $\mathrm{dom}(p)=\downarrow\\!{\sigma}$. We prove
that $\phi=\phi^{\prime\prime}\phi^{\prime}$ by induction on the words in
$\downarrow\\!{\sigma}$. Without loss of generality, let
$\sigma^{\prime}a\in\downarrow\\!{\sigma}$. If $a\in A$, then the result
follows directly from the inductive hypothesis. So, let $a=\tau$. Then we
distinguish the following cases.

  1. 1.

Let $fp(\sigma^{\prime}\tau)=fp(\sigma^{\prime})$ and let
$p(\sigma^{\prime}\tau)=p(\sigma^{\prime})$. Then we have
$\phi^{\prime}(\sigma^{\prime}\tau)=\phi^{\prime}(\sigma^{\prime})\implies\phi^{\prime\prime}\phi^{\prime}(\sigma^{\prime}\tau)=\phi^{\prime\prime}\phi^{\prime}(\sigma^{\prime})$.
And using induction hypothesis we get
$\phi^{\prime\prime}\phi^{\prime}(\sigma^{\prime}\tau)=\phi(\sigma^{\prime})$.
Moreover, $\phi(\sigma^{\prime})=\phi(\sigma^{\prime}\tau)$ since
$fp(\sigma^{\prime}\tau)=fp(\sigma^{\prime})$.

  2. 2.

Let $fp(\sigma^{\prime}\tau)=fp(\sigma^{\prime})$ and let
$p(\sigma^{\prime}\tau)\neq p(\sigma^{\prime})$. Then we have
$\phi^{\prime}(\sigma^{\prime}\tau)=\phi^{\prime}(\sigma^{\prime})\tau$.
Furthermore, $fp(\sigma^{\prime}\tau)=fp(\sigma^{\prime})\implies
f{p}^{{\dagger}}\phi^{\prime}(\sigma^{\prime}\tau)=f{p}^{{\dagger}}\phi^{\prime}(\sigma^{\prime})$.
I.e.,
$f{p}^{{\dagger}}\phi^{\prime}(\sigma^{\prime})\tau=f{p}^{{\dagger}}\phi^{\prime}(\sigma^{\prime})$.
So by the construction of a stutter basis we have
$\phi^{\prime\prime}(\phi^{\prime}(\sigma^{\prime})\tau)=\phi^{\prime\prime}\phi^{\prime}(\sigma^{\prime})$.
Using induction hypothesis we get
$\phi^{\prime\prime}(\phi^{\prime}(\sigma^{\prime})\tau)=\phi^{\prime\prime}\phi^{\prime}(\sigma^{\prime})=\phi(\sigma^{\prime})$.
Moreover, $\phi(\sigma^{\prime})=\phi(\sigma^{\prime}\tau)$ since
$fp(\sigma^{\prime}\tau)=fp(\sigma^{\prime})$. Thus,
$\phi^{\prime\prime}\phi^{\prime}(\sigma^{\prime}\tau)=\phi^{\prime\prime}(\phi^{\prime}(\sigma^{\prime})\tau)=\phi(\sigma^{\prime}\tau)$.

  3. 3.

Let $fp(\sigma^{\prime}\tau)\neq fp(\sigma^{\prime})$ and let
$p(\sigma^{\prime}\tau)=p(\sigma^{\prime})$. This case is not possible.

  4. 4.

Let $fp(\sigma^{\prime}\tau)\neq fp(\sigma^{\prime})$ and let
$p(\sigma^{\prime}\tau)\neq p(\sigma^{\prime})$. Then we have
$\phi(\sigma^{\prime}\tau)=\phi(\sigma^{\prime})\tau$ and
$\phi^{\prime}(\sigma^{\prime}\tau)=\phi^{\prime}(\sigma^{\prime})\tau$. Using
$p={p}^{{\dagger}}\phi^{\prime}$ in $fp(\sigma^{\prime}\tau)\neq
fp(\sigma^{\prime})$ we get
$f{p}^{{\dagger}}\phi^{\prime}(\sigma^{\prime}\tau)\neq
f{p}^{{\dagger}}\phi^{\prime}(\sigma^{\prime})$. Then, by the construction of
a stutter basis we get
$\phi^{\prime\prime}\phi^{\prime}(\sigma^{\prime}\tau)=\phi^{\prime\prime}\phi^{\prime}(\sigma^{\prime})\tau$.
I.e., using the induction hypothesis we get
$\phi^{\prime\prime}\phi^{\prime}(\sigma^{\prime}\tau)=\phi(\sigma^{\prime})\tau=\phi(\sigma^{\prime}\tau)$.

Thus, $\phi=\phi^{\prime\prime}\phi^{\prime}$. I.e.,
${(fp)}^{{\dagger}}\phi=fp=f{p}^{{\dagger}}\phi^{\prime}={(f{p}^{{\dagger}})}^{{\dagger}}\phi^{\prime\prime}\phi^{\prime}={(f{p}^{{\dagger}})}^{{\dagger}}\phi$.
Moreover, the function $\phi$ is an epi; therefore, we conclude that
${(fp)}^{{\dagger}}={(f{p}^{{\dagger}})}^{{\dagger}}$. ∎

######  Theorem II.5 (Theorem 5).

The mapping ${\mathrm{Path}}_{\sim}(f)$ given in (1) is well defined and is an
endofunctor on the category of sets.

###### Proof.

We first show that the definition given in (1) is independent of the chosen
representative. I.e., If $[p]_{\sim}=[p^{\prime}]_{\sim}$ then
${\mathrm{Path}}_{\sim}(f)[p]_{\sim}={\mathrm{Path}}_{\sim}(f)[p^{\prime}]_{\sim}$.
Let $p\sim p^{\prime}$. Then,
${p}^{{\dagger}}={p^{\prime}}^{{\dagger}}\implies
f\circ{p}^{{\dagger}}=f\circ{p^{\prime}}^{{\dagger}}\implies{(f\circ{p}^{{\dagger}})}^{{\dagger}}={(f\circ{p^{\prime}}^{{\dagger}})}^{{\dagger}}.$
Furthermore, using Lemma 4 we get ${(f\circ p)}^{{\dagger}}={(f\circ
p^{\prime})}^{{\dagger}}$. Thus, $f\circ p\sim f\circ p^{\prime}$.

The mapping $\mathrm{Path}_{\sim}$ preserves identity:

${\mathrm{Path}}_{\sim}(\mathrm{id}_{X})[p]_{\sim}=[\mathrm{id}\circ
p]_{\sim}=[p]_{\sim}=\mathrm{id}_{{\mathrm{Path}}_{\sim}(X)}[p]_{\sim}.$

The mapping $\mathrm{Path}_{\sim}$ preserves composition. Let $X\rTo^{f}Y$ and
$Y\rTo^{g}Z$. Then,

$\displaystyle{\mathrm{Path}}_{\sim}(g)\circ{\mathrm{Path}}_{\sim}(f)[p]_{\sim}=$
$\displaystyle\ {\mathrm{Path}}_{\sim}(g)([f\circ p]_{\sim})$ $\displaystyle=$
$\displaystyle\ [g\circ f\circ p]_{\sim}$ $\displaystyle=$ $\displaystyle\
{\mathrm{Path}}_{\sim}(g\circ f)[p]_{\sim}.$

######  Lemma II.6 (Lemma 6).

Let $p\in\mathrm{Path}(X),q\in\mathrm{Path}(Y)$, and $X\rTo^{f}Y$.

  1. 1.

If $fp\sim q$ and $\mathrm{trace}(q)\in\tau^{*}a\tau^{*}$ then
$q(\varepsilon)=fp(\varepsilon)\land\mathrm{trace}(p)\in\tau^{*}a\tau^{*}$.

  2. 2.

$\mathrm{last}(p)=\mathrm{last}({p}^{{\dagger}})$.

  3. 3.

If $fp\sim q$, then $f(\mathrm{last}(p))=\mathrm{last}(q)$.

  4. 4.

$\pi_{Y}\circ\mathrm{Path}(f)={\mathrm{Path}}_{\sim}(f)\circ\pi_{X}$.

  5. 5.

Let $V_{i}\subseteq{\mathrm{Path}}_{\sim}(Y)$ (for $i\in I$) be a family of
pairwise disjoint sets. Then,

${{\mathrm{Path}}_{\sim}(f)}^{-1}\Big{(}\bigcup_{i\in I}V_{i}\Big{)}\ =\
\bigcup_{i\in I}{{\mathrm{Path}}_{\sim}(f)}^{-1}(V_{i})\enspace.$

###### Proof.

  1. 1.

For any paths $p\in\mathrm{Path}(X),q\in\mathrm{Path}(Y)$ with $X\rTo^{f}Y$
and $fp\sim q$, the following properties hold.

    1. (a)

$q(\varepsilon)=fp(\varepsilon)$.

    2. (b)

If $\mathrm{trace}(q)\in\tau^{*}a\tau^{*}$ then
$\mathrm{trace}(p)\in\tau^{*}a\tau^{*}$.

For (a), we know from the the construction of the stutter invariant to $q$:
$q(\varepsilon)={q}^{{\dagger}}(\varepsilon)$. Thus, we have
$q(\varepsilon)={q}^{{\dagger}}(\varepsilon)={(fp)}^{{\dagger}}(\varepsilon)=fp(\varepsilon)$.

For (b), let $\mathrm{trace}(q)\in\tau^{*}a\tau^{*}$. Then, it suffices to
show that $\mathrm{trace}({q}^{{\dagger}})\in\tau^{*}a\tau^{*}$. So let
$\mathrm{dom}(q)=\downarrow\\!{\tau}^{n}a\tau^{m}$, for some $n,m\geq 0$ and
let $\phi$ be the stutter basis for $q$. Then, by the construction of $\phi$
we have $\phi(\tau^{n}a\tau^{m})=\tau^{n^{\prime}}a\tau^{m^{\prime}}$ with
$n^{\prime}\leq n$ and $m^{\prime}\leq m$. Thus,
$\mathrm{trace}({q}^{{\dagger}})\in\tau^{*}a\tau^{*}$. Therefore, we have
$\mathrm{trace}({(fp)}^{{\dagger}})=\mathrm{trace}({q}^{{\dagger}})\in\tau^{*}a\tau^{*}$.
And since $\mathrm{trace}(p)=\mathrm{trace}((fp))$ (Proposition 1) we conclude
that
$\mathrm{trace}(fp)\in\tau^{*}a\tau^{*}\implies\mathrm{trace}(p)\in\tau^{*}a\tau^{*}$.

  2. 2.

Let $\mathrm{dom}(p)=\downarrow\\!{\sigma}$. Then, we derive

$\displaystyle\ p(\sigma)={p}^{{\dagger}}\phi(\sigma)$ $\displaystyle(\because
p={p}^{{\dagger}}\circ\phi)$ $\displaystyle\iff$ $\displaystyle\
p\max\downarrow\\!{\sigma}={p}^{{\dagger}}\max\downarrow\\!{(\phi\sigma)}$
$\displaystyle(\because\sigma=\max\downarrow\\!{\sigma})$ $\displaystyle\iff$
$\displaystyle\
\mathrm{last}(p)={p}^{{\dagger}}\max\phi(\downarrow\\!{\sigma})$
$\displaystyle(\because\downarrow\\!{\phi(\sigma)}=\phi(\downarrow\\!{\sigma}))$
$\displaystyle\iff$ $\displaystyle\
\mathrm{last}(p)=\mathrm{last}({p}^{{\dagger}}).$

  3. 3.

Let $p\in\mathrm{Path}(X)$ and $q\in\mathrm{Path}(Y)$ with
${(fp)}^{{\dagger}}={q}^{{\dagger}}$. Then, we have

$\mathrm{last}(q)=\mathrm{last}({q}^{{\dagger}})=\mathrm{last}({(fp)}^{{\dagger}})=\mathrm{last}(fp)=f\mathrm{last}(p).$

  4. 4.

Trivial.

  5. 5.

Let ${[p]}_{\sim}\in{{\mathrm{Path}}_{\sim}(f)}^{-1}(\bigcup_{i\in I}V_{i})$.
I.e., there is a unique $j\in I$ (because of disjointness) with
${[fp]}_{\sim}\in V_{i}$. Thus, ${[p]}_{\sim}\in\bigcup_{i\in
I}{{\mathrm{Path}}_{\sim}(f)}^{-1}(V_{i})$. The other direction, i.e., the
case $\bigcup_{i\in
I}{{\mathrm{Path}}_{\sim}(f)}^{-1}(V_{i})\subseteq{{\mathrm{Path}}_{\sim}(f)}^{-1}\Big{(}\bigcup_{i\in
I}V_{i}\Big{)}$ is trivial.∎

##  Appendix III Proof concerning Section 3

######  Theorem III.1 (Theorem 7).

Let $(X,A_{\tau},\rightarrow)$ be a labelled transition system and
$(X,\pi_{X}\circ\alpha)$ be the corresponding
$\mathcal{P}\circ\mathrm{Path}_{\sim}$-coalgebra. Then, two states
$x,x^{\prime}\in X$ are branching bisimilar if and only if the states
$x,x^{\prime}$ are $\mathcal{P}\circ\mathrm{Path}_{\sim}$-behaviourally
equivalent.

###### Proof.

Let $(Y,\beta)$ be a $\mathcal{P}\circ\mathrm{Path}_{\sim}$-coalgebra and let
$X\rTo^{f}Y$ be a $\mathcal{P}\circ\mathrm{Path}_{\sim}$-coalgebra
homomorphism. Define a relation $xRx^{\prime}\iff f(x)=f(x^{\prime})$. Let
$x_{1}\xrightarrow{a}x_{2}$ and $x_{1}Rx_{1}^{\prime}$. Below, we only
consider $a\in A$. Define a path $\\{\varepsilon,a\\}\rTo^{p}X$ as
$p(\varepsilon)=x_{1}$ and $p(a)=x_{2}$. Then, by the construction of $\alpha$
we have $p\in\alpha(x)$. Furthermore,

$\displaystyle\
{[fp]}_{\sim}\in\mathcal{P}({\mathrm{Path}}_{\sim}(f))\circ\pi_{X}\circ\alpha(x)$
$\displaystyle\ \implies{[fp]}_{\sim}\in\beta(f(x))$
$\displaystyle(\because\mathcal{P}({\mathrm{Path}}_{\sim}(f))\circ\pi_{X}\circ\alpha=\beta\circ
f)$ $\displaystyle\ \implies{[fp]}_{\sim}\in\beta(f(x^{\prime}))$
$\displaystyle(\because f(x)=f(x^{\prime}))$ $\displaystyle\
\implies{[fp]}_{\sim}\in\mathcal{P}({\mathrm{Path}}_{\sim}(f))\circ\pi_{X}\circ\alpha(x^{\prime}).$
$\displaystyle(\because\mathcal{P}({\mathrm{Path}}_{\sim}(f))\circ\pi_{X}\circ\alpha=\beta\circ
f)$

I.e., there is a path $p^{\prime}\in\mathrm{Exec}(x_{1}^{\prime})$ such that
$fp\sim fp^{\prime}$. Note that ${(fp)}^{{\dagger}}=fp$ since
$p={p}^{{\dagger}}$ and $p$ is a one-step execution with observation
$a\neq\tau$. Let $\phi$ be the stutter basis for $p^{\prime}$. Next, we claim
that

$fp^{\prime}(\sigma)=fp\phi(\sigma),\qquad\text{for any}\
\sigma\in\mathrm{dom}(p^{\prime}).$ (5)

To see this, let $\sigma\in\mathrm{dom}(p^{\prime})$. Then,
$fp^{\prime}(\sigma)={(fp^{\prime})}^{{\dagger}}\phi(\sigma)={(fp)}^{{\dagger}}\phi(\sigma)=fp\phi(\sigma)$.
Notice that ${(fp^{\prime})}^{{\dagger}}={(fp)}^{{\dagger}}$ because $fp\sim
fp^{\prime}$. This proves the above claim.

Using Lemma 3 and construction of $\alpha$ we get
$\mathrm{trace}(p^{\prime})\in\tau^{*}a$ since $\mathrm{trace}(p)=a$. So let
$\mathrm{dom}(p^{\prime})=\tau^{m}a$, for some $m\geq 0$. Next, we claim that
for any $\sigma\in\downarrow\\!{\tau}^{m}$ we have $fp^{\prime}(\sigma)=f(x)$.
So, let $\sigma\in\downarrow\\!{\tau}^{m}$. Then, using (5) we get
$fp^{\prime}(\sigma)=fp\phi(\sigma)$. Clearly, by the construction of $\phi$
we have $\phi(\sigma)\in\tau^{m^{\prime}}$ (for some $m^{\prime}\leq m$). But,
$\mathrm{dom}(p)=\\{\varepsilon,a\\}$, so $\phi(\sigma)=\varepsilon$. Thus,
$fp^{\prime}(\sigma)=fp(\varepsilon)=f(x)$. I.e., $x_{1}^{\prime}\ext@arrow
0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{\varepsilon}{}p^{\prime}(\tau^{m})$
and $fp^{\prime}(\tau^{m})=f(x_{1}).$ Moreover, using (5) we also have
$fp^{\prime}(\tau^{m}a)=fp\phi(\tau^{m}a)=fp\phi(\tau^{m})a=fp(a)=f(x_{2}).$
Thus, $x^{\prime}\ext@arrow
0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{\varepsilon}{}p^{\prime}(\tau^{m})\xrightarrow{a}p^{\prime}(\tau^{m}a)$
and $fp^{\prime}(\tau^{m}a)=f(x_{2})$. And construction of the relation $R$
gives $x_{1}^{\prime}\ R\ p^{\prime}(\tau^{m})$ and $x_{2}\ R\
p^{\prime}(\tau^{m}a)$. ∎

##  Appendix IV Proofs concerning Section 4

######  Lemma IV.1 (Lemma 10).

Let $X$ be a set. Then we have the following property:

$\forall_{p_{1},p_{2}\in\mathrm{Path}(X)}\
{p}^{{\dagger}}_{1}\preceq{p}^{{\dagger}}_{2}\implies\exists_{p\in\mathrm{Path}(X)}\
p\sim p_{1}\land p\preceq p_{2}.$

###### Proof.

Assume ${p_{1}}^{{\dagger}}\leq{p_{2}}^{{\dagger}}$, then by definition
${p_{2}}^{{\dagger}}\mid_{\mathrm{dom}({p_{1}}^{{\dagger}})}={p_{1}}^{{\dagger}}$.
Observe that due to the structure of paths, it follows that there exists a
word $w\in\mathrm{dom}({p_{2}}^{{\dagger}})$ such that
${p_{2}}^{{\dagger}}\mid_{\mathrm{dom}({p_{1}}^{{\dagger}})}={p_{2}}^{{\dagger}}\mid_{\downarrow\\!{\sigma}}$,
in fact it is true that $\sigma=\max\mathrm{dom}({p_{1}}^{{\dagger}})$. We
will show that then there must also be a word
$\sigma^{\prime}\in\mathrm{dom}(p_{2})$ such that
${(p_{2}\mid_{\downarrow\\!{\sigma^{\prime}}})}^{{\dagger}}={p_{2}}^{{\dagger}}\mid_{\downarrow\\!{\sigma}}$,
i.e.
${(p_{2}\mid_{\downarrow\\!{\sigma^{\prime}}})}^{{\dagger}}={p_{1}}^{{\dagger}}$,
thus $p_{2}\mid_{\downarrow\\!{\sigma^{\prime}}}\sim p_{1}$ and, by
definition, $p_{2}\mid_{\downarrow\\!{\sigma^{\prime}}}\leq p_{2}$ as
required.

It remains to show that whenever for a given path $p$, we choose any
$\sigma\in\mathrm{dom}({p}^{{\dagger}})$, then there exists a word
$\sigma^{\prime}\in\mathrm{dom}(p)$, such that
${(p\mid_{\downarrow\\!{\sigma^{\prime}}})}^{{\dagger}}={p}^{{\dagger}}\mid_{\downarrow\\!{\sigma}}$.
This follows from the definition of a stutter basis; just take
$\sigma^{\prime}$ as a pre-image of the stutter basis $\phi$ for $p$ of
$\sigma$ (this need not be unique). The result is clear by choosing the
stutter basis $\phi\mid_{\downarrow\\!{\sigma^{\prime}}}$ for
$p\mid_{\downarrow\\!{\sigma^{\prime}}}$. ∎

######  Theorem IV.2 (Theorem 13).

For any $X\rTo^{f}Y$, the function $\mathrm{Path}(f)$ is strictly order
preserving. Moreover, $\mathrm{Path}(f)$ also satisfies the following
property:

$\forall_{p\in\mathrm{Path}(X),q\in\mathrm{Path}(Y)}\ q\prec
f(p)\implies\exists_{p^{\prime}\in\mathrm{Path}(X)}\ p^{\prime}\prec p\land
f(p^{\prime})=q\enspace.$

###### Proof.

Let $p,p^{\prime}\in\mathrm{Path}(X)$ with $p\prec p^{\prime}$. It suffices to
show that $fp\prec fp^{\prime}$. Clearly,
$\mathrm{dom}(fp)=\mathrm{dom}(p)\subset\mathrm{dom}(p)^{\prime}=\mathrm{dom}(fp^{\prime})$.
Moreover, for any $\sigma\in\mathrm{dom}(fp)$ we have
$fp(\sigma)=f(p(\sigma))=f(p^{\prime}(\sigma))=fp^{\prime}(\sigma)$ Thus,
$fp\prec fp^{\prime}$.

For the other property, let $q\prec fp$, for some
$p\in\mathrm{Path}(X),q\in\mathrm{Path}(Y)$. Define a function
$\mathrm{dom}(q)\rTo^{p^{\prime}}X$ as follows:
$\forall_{\sigma\in\mathrm{dom}(q)}\ p^{\prime}(\sigma)=p(\sigma)$. Clearly,
$\mathrm{dom}(q)$ is a prefix-closed set due to the construction of $q$.
Therefore, we just need to verify that $p^{\prime}\preceq p$. Clearly,
$\mathrm{dom}(p^{\prime})=\mathrm{dom}(q)\subset\mathrm{dom}(fp)=\mathrm{dom}(p)$.
Thus, by construction of $p^{\prime}$ we have $p^{\prime}\prec p$. Lastly,
$fp^{\prime}=q$ follows from $\mathrm{dom}(fp^{\prime})=\mathrm{dom}(q)$ and
for any $\sigma\in\mathrm{dom}(q)$ we have
$fp^{\prime}(\sigma)=fp(\sigma)=q(\sigma)$ (since $q\prec fp$). ∎

######  Lemma IV.3 (Lemma 14).

The relation $\preceq$ on the set ${\mathrm{Path}}_{\sim}(X)$ is a well-
defined partial order.

###### Proof.

We first prove that the relation $\preceq$ is well defined. Let
${[p_{1}]}_{\sim}={[p_{2}]}_{\sim}$ and ${[q_{1}]}_{\sim}={[q_{2}]}_{\sim}$.
Then,

${[p_{1}]}_{\sim}\preceq{[q_{1}]}_{\sim}\iff{p}^{{\dagger}}_{1}\preceq{q}^{{\dagger}}_{1}\iff{p}^{{\dagger}}_{2}\preceq{q}^{{\dagger}}_{2}\iff{[p_{2}]}_{\sim}\preceq{[q_{2}]}_{\sim}\enspace.$

Reflexivity is obvious. For antisymmetry, let
${[p]}_{\sim}\preceq{[q]}_{\sim}$ and ${[q]}_{\sim}\preceq{[p]}_{\sim}$. Then,
we find ${p}^{{\dagger}}\preceq{q}^{{\dagger}}$ and
${q}^{{\dagger}}\preceq{p}^{{\dagger}}$. I.e.,
${p}^{{\dagger}}={q}^{{\dagger}}$. Therefore, ${[p]}_{\sim}={[q]}_{\sim}$. For
transitivity, let ${[p_{1}]}_{\sim}\preceq{[p_{2}]}_{\sim}$ and
${[p_{2}]}_{\sim}\preceq{[p_{3}]}_{\sim}$. Then,
${p}^{{\dagger}}_{1}\preceq{p}^{{\dagger}}_{2}$ and
${p}^{{\dagger}}_{2}\preceq{p}^{{\dagger}}_{3}$. Thus,
${p}^{{\dagger}}_{1}\preceq{p}^{{\dagger}}_{3}$; hence,
${[p_{1}]}_{\sim}\preceq{[p_{3}]}_{\sim}$. ∎

######  Theorem IV.4 (Theorem 15).

The quotient function $\mathrm{Path}(X)\rTo^{\pi}{\mathrm{Path}}_{\sim}(X)$ is
order preserving. Consequently, the quotient function
$\mathrm{Path}(X)\rTo^{\pi}{\mathrm{Path}}_{\sim}(X)$ is Borel measurable,
where the sigma-algebra on paths is given by
$\Sigma_{{\mathrm{Path}}_{\sim}(X)}=\mathcal{B}(\mathcal{O}_{{\mathrm{Path}}_{\sim}(X)})$.

###### Proof.

Let $p\preceq q$ with $p,q\in\mathrm{Path}(X)$. Then, it suffices to show that
${p}^{{\dagger}}\preceq{q}^{{\dagger}}$. Let $\phi,\phi^{\prime}$ be the
stutter bases for the paths $p,q$, respectively. Without loss of generality,
let $\max\mathrm{dom}(q)=\max\mathrm{dom}(p)a$, for some $a\in A_{\tau}$.
Also, let $\mathrm{dom}(p)=\downarrow\\!{\sigma}$, for some $\sigma\in
A_{\tau}^{*}$. For the function $q$, we write the restriction of $q$ to the
sub-domain $\downarrow\\!{\sigma}$ as $q|_{\sigma}$. Note that $q|_{\sigma}=p$
(since $p\preceq q$). Next, we claim that the restriction
$\phi^{\prime}|_{\sigma}$ is a stutter basis for $p$. Let
$\sigma^{\prime}a\in\downarrow\\!{\sigma}$. Then we distinguish the following
cases:

  * •

Let $a=\tau$ and $p(\sigma^{\prime}\tau)=p(\sigma^{\prime})$. Then,
$p(\sigma^{\prime}\tau)=p(\sigma^{\prime})\implies
q(\sigma^{\prime}\tau)=q(\sigma^{\prime})$ (since $p\preceq q$). Thus,
$\phi^{\prime}(\sigma^{\prime}\tau)=\phi^{\prime}(\sigma^{\prime})$, i.e.,
$\phi^{\prime}|_{\sigma}(\sigma^{\prime}\tau)=\phi^{\prime}|_{\sigma}(\sigma^{\prime})$.

  * •

Let $a=\tau$ and $p(\sigma^{\prime}\tau)\neq p(\sigma^{\prime})$. Then,
$q(\sigma^{\prime}\tau)\neq q(\sigma^{\prime})$. Thus,
$\phi^{\prime}(\sigma^{\prime}\tau)=\phi^{\prime}(\sigma^{\prime})\tau$ which
further implies that
$\phi^{\prime}|_{\sigma}(\sigma^{\prime}\tau)=\phi^{\prime}|_{\sigma}(\sigma^{\prime})\tau$.

  * •

Let $a\in A$. Similar to the previous case.

Thus, $\phi^{\prime}$ is a stutter basis for $p$ and from the uniqueness of
stutter basis for $p$ (cf. Theorem 2) we have $\phi^{\prime}|_{\sigma}=\phi$.
Therefore, $\phi(\sigma^{\prime})=\phi^{\prime}(\sigma^{\prime})$, for all
$\sigma^{\prime}\in\downarrow\\!{\sigma}$. Furthermore, from the construction
of $\phi^{\prime}$ we have $\phi^{\prime}(\sigma a)=\phi^{\prime}(\sigma)a$ or
$\phi^{\prime}(\sigma\tau)=\phi^{\prime}(\sigma)$. Thus, in either case, we
have $\phi(\sigma)\preceq\phi^{\prime}(\sigma a)$. Hence,
$\mathrm{dom}({p}^{{\dagger}})=\downarrow\\!{\phi(\sigma)}\subseteq\downarrow\\!{\phi^{\prime}(\sigma
a)}=\mathrm{dom}({q}^{{\dagger}})$. Let
$\sigma^{\prime}\in\mathrm{dom}({p}^{{\dagger}})$. Since $\phi$ is the stutter
basis for $p$, we know that there is $\sigma^{\prime\prime}\in\mathrm{dom}(p)$
such that $\phi(\sigma^{\prime\prime})=\sigma^{\prime}$. Then,

$\displaystyle{q}^{{\dagger}}(\sigma^{\prime})=$ $\displaystyle\
{q}^{{\dagger}}\phi(\sigma^{\prime\prime})$ $\displaystyle=$ $\displaystyle\
{q}^{{\dagger}}\phi^{\prime}(\sigma^{\prime\prime})$
$\displaystyle(\because\phi^{\prime}|_{\sigma}=\phi)$ $\displaystyle=$
$\displaystyle\
q(\sigma^{\prime\prime})=p(\sigma^{\prime\prime})={p}^{{\dagger}}\phi(\sigma^{\prime\prime})={p}^{{\dagger}}(\sigma^{\prime}).$

Thus, ${p}^{{\dagger}}\preceq{q}^{{\dagger}}$, whenever $p\preceq q$. ∎

######  Theorem IV.5 (Theorem 16).

For any $X\rTo^{f}Y$, the function ${\mathrm{Path}}_{\sim}(f)$ is order
preserving. Thus, the function ${\mathrm{Path}}_{\sim}(f)$ is Borel
measurable.

###### Proof.

Let $p,q\in\mathrm{Path}(X)$ with ${[p]}_{\sim}\preceq{[q]}_{\sim}$. Since
${[p]}_{\sim}\preceq{[q]}_{\sim}$, we have
${p}^{{\dagger}}\preceq{q}^{{\dagger}}$. Moreover, from Theorem 13 we know
that
$\mathrm{Path}(f)({p}^{{\dagger}})\preceq\mathrm{Path}(f)({q}^{{\dagger}})$.
Thus, $f\circ({p}^{{\dagger}})\preceq f\circ({q}^{{\dagger}})$. And using
Theorem 15 we get
${(f\circ{p}^{{\dagger}})}^{{\dagger}}\preceq{(f\circ{q}^{{\dagger}})}^{{\dagger}}$.
Lastly, Lemma 4 gives us ${(f\circ p)}^{{\dagger}}\preceq{(f\circ
q)}^{{\dagger}}$; thus, ${[f\circ p]}_{\sim}\preceq{[f\circ q]}_{\sim}$, i.e.,
${\mathrm{Path}}_{\sim}(f){[p]}_{\sim}\preceq{\mathrm{Path}}_{\sim}(f){[q]}_{\sim}$.
∎

######  Proposition IV.6 (Proposition 18).

A directed subset of a prefix order is always totally ordered. In addition, an
irreducible downward closed subset of a prefix order is always totally
ordered.

###### Proof.

Let $D\subseteq\mathrm{Path}(X)$ be a directed subset of paths with $p,q\in D$
for $p\neq q$. Then, we find some $p^{\prime}\in D$ such that $p\preceq
p^{\prime}$ and $q\preceq p^{\prime}$, since $D$ is directed. And downward
totality tells us $p\preceq q$ or $q\preceq p$. Thus, every directed set is
totally order.

Furthermore, it is well-known that every irreducible downward closed subset of
a partial order is an ideal (see, e.g., [11]). Thus, in particular, every
directed subset of paths is totally ordered. ∎

######  Lemma IV.7 (Lemma 19).

The set $X^{\infty}$ is prefix ordered by the relation $\preceq^{\prime}$,
whenever $(X,\preceq)$ is a prefix order.

###### Proof.

That the relation $\preceq^{\prime}$ is a partial order follows directly from
the construction of $\preceq^{\prime}$. The interesting case is to show that
the $X^{\infty}$ satisfies the downward totality. Let $p_{1},p_{2},p_{3}\in
X^{\infty}$ such that $p_{1}\preceq^{\prime}p_{3}$ and
$p_{2}\preceq^{\prime}p_{3}$. If $p_{3}\in X$ then the result follows directly
from $\preceq$. So suppose $p_{3}=\infty_{C}$, for some non-sober subset
$C\subseteq X$. Then, we find $p_{1},p_{2}\in C$. And since irreducible closed
sets are totally ordered (Proposition 18), we have $p_{1}\preceq p_{2}\lor
p_{2}\preceq p_{1}$, i.e., $p_{1}\preceq^{\prime}p_{2}\lor
p_{2}\preceq^{\prime}p_{1}$. ∎

######  Proposition IV.8 (Proposition 20).

Let $(X,\preceq)$ be a simple prefix order. A subset $U\subseteq X^{\infty}$
is _Scott_ open if and only if $U$ is upward closed and it is inaccessible by
directed joins, i.e., for any directed set $D\subseteq X^{\infty}$ if $\sup D$
exists and $\sup D\in U$ then $D\cap U\neq\emptyset$. Let
$\mathcal{S}_{X^{\infty}}$ denote the collection of Scott open subsets of
$X^{\infty}$. Then, the space $(X^{\infty},\mathcal{S}_{X^{\infty}})$ is a
sober space.

###### Proof.

Let $C\subseteq X^{\infty}$ be an irreducible closed set. Recall that $C$ is
Scott closed if and only if $C$ is downward closed and for any directed set
$D\subseteq C$, if $\sup D$ exists then $\sup D\in C$. Moreover, an
irreducible closed set is totally ordered (cf. Proposition 18) and every chain
is a directed set. If $C=\downarrow\\!{p}$ for some $p$, then clearly $\sup C$
exists and $C=\mathrm{cl}(p)=\downarrow\\!{p}$. On the other hand, if $C$ is
an infinite chain, then $C$ can be either a non-sober set w.r.t. Alexandroff
topology with or without the limit point $\infty_{C}$. However, if $C$ is
without the limit point $\infty_{C}$, then $C$ is not a Scott-closed set
because the supremum $\sup C=\infty_{C}$ exists in the $X^{\infty}$ and
$\infty_{C}\not\in C$. Thus, if $C$ is an infinite chain then
$C=\downarrow\\!{\infty}_{C}$, whenever $C$ is an irreducible Scott-closed
set. Clearly, we have $C=\downarrow\\!{\sup}{\ C}$, for any irreducible Scott
closed set $C$. Thus, the space $(X^{\infty},\mathcal{S}_{X^{\infty}})$ is
sober. ∎

######  Theorem IV.9 (Theorem 21).

Let $(X,\preceq)$ be a prefix order and let
$\mathcal{O}_{X}\rTo^{\mu}\left[0,\infty\right]$ be a locally finite and
Scott-continuous valuation. Then, the function
$\mathcal{S}_{X^{\infty}}\rTo^{\tilde{\mu}}\left[0,\infty\right]$ defined in
the following way:

$\tilde{\mu}(V)=\mu(V\cap X)\quad\text{(for every Scott-open set
$V\in\mathcal{S}_{X^{\infty}}$)}$

is a Scott-continuous valuation. If $X$ is simple then $\tilde{\mu}$ is
locally finite.

###### Proof.

First we note that $V\cap X\in\mathcal{O}_{X}$, whenever
$V\in\mathcal{S}_{X^{\infty}}$. To see this, let $p,p^{\prime}\in X$ with
$p\preceq p^{\prime}$ and $p\in V\cap X$. Clearly, $p\in V$ and $V$ is an
upward closed set, i.e., $p^{\prime}\in V$. Moreover, $p^{\prime}\in V\cap X$.
Secondly, we note that the function $\tilde{\mu}$ is strict since the function
$\mu$ is strict and $\emptyset=\emptyset\cap X$.

Next, we show that $\tilde{\mu}$ is order preserving. Let $V\subseteq
V^{\prime}$, for some $V,V^{\prime}\in\mathcal{S}_{X^{\infty}}$. Then $V\cap
X\subseteq V^{\prime}\cap X$. And the order preservation of $\mu$ gives
$\tilde{\mu}(V)=\mu(V\cap X)\leq\mu(V^{\prime}\cap
X)=\tilde{\mu}(V^{\prime})$.

The modularity of $\tilde{\mu}$ follow directly from the modularity of $\mu$
since the operator $\cap$ distributes over union, i.e., for
$\Box\in\\{\cup,\cap\\}$ and $V,V^{\prime}\in\mathcal{S}_{X^{\infty}}$ we have

$(V\cap X)\ \Box\ (V^{\prime}\cap X)=(V\Box V^{\prime})\cap X.$

Lastly, to show that $\tilde{\mu}$ is Scott-continuous, let $(V_{i})_{i\in I}$
be a directed family of open sets with each
$V_{i}\in\mathcal{S}_{X^{\infty}}$. Then, we find that the family $(V_{i}\cap
X)_{i\in I}$ is a directed family of open sets in $X$. Moreover,

$\tilde{\mu}(\bigcup_{i\in I}V_{i})=\mu((\bigcup_{i\in I}V_{i})\cap
X)=\mu(\bigcup_{i\in I}(V_{i}\cap X))=\sup_{i\in I}\mu(V_{i}\cap X)=\sup_{i\in
I}\tilde{\mu}(V_{i}).$

For local finiteness, we assume that $X$ is a simple prefix order. Then, we
claim that the set
${U}_{{\scriptscriptstyle\infty}}=U\cup\\{\infty_{C}\mid\exists_{p\in U}\
p\preceq\infty_{C}\\}$ is Scott-open, whenever $U\in\mathcal{O}_{X}$. From
this local finiteness of $\tilde{\mu}$ directly follows from the local
finiteness of $\mu$.

So let $U$ be Alexandroff-open set, i.e., $U\in\mathcal{O}_{X}$. Clearly,
${U}_{{\scriptscriptstyle\infty}}$ is upward closed. Now it remains to show
that $U$ is inaccessible by directed joins. Let $D\subseteq X^{\infty}$ be a
directed subsets of paths with ${p}_{{\scriptscriptstyle\infty}}=\sup D$ and
${p}_{{\scriptscriptstyle\infty}}\in U$. Then, we distinguish the following
two cases:

  1. 1.

Let ${p}_{{\scriptscriptstyle\infty}}\in X$. Notice that every directed set
$D\subseteq X$ is a chain (Proposition 18). Moreover, only finite chains in
the ordered set $X$ has suprema. And since in a finite chain the supremum
coincides with maximum, we find that ${p}_{{\scriptscriptstyle\infty}}\in D$.
Thus, $D\cap{U}_{{\scriptscriptstyle\infty}}\neq\emptyset$.

  2. 2.

Let ${p}_{{\scriptscriptstyle\infty}}=\infty_{C}$, for some non-sober set $C$
in $X$. Then, by construction we find some $p^{\prime}\in U$ such that
$p^{\prime}\preceq\infty_{C}$. Moreover, we have $p\preceq\infty_{C}$, for all
$p\in D$. Thus, by downward totality of paths (cf. Lemma 19) we find

$\forall_{p\in D}\ p\preceq p^{\prime}\lor p^{\prime}\preceq p.$

We claim that $\exists_{p\in D}\neg(p\preceq p^{\prime})$. Suppose otherwise
that $\forall_{p\in D}\ p\preceq p^{\prime}$. Then, we find $\infty_{C}=\sup
D\preceq p^{\prime}$. I.e., $p^{\prime}=\infty_{C}$. But $p^{\prime}\in X$.
Thus, a contradiction. Hence, $p^{\prime}\preceq p$, for some $p\in D$. And
$U$ is upward closed, i.e., $p\in U$. Therefore,
$D\cap{U}_{{\scriptscriptstyle\infty}}\neq\emptyset$.

Thus, for every open set $U\in\mathcal{O}_{X}$, the set
${U}_{{\scriptscriptstyle\infty}}$ is Scott-open. ∎

######  Theorem IV.10 (Theorem 22).

For countable sets $A$ and $X$, the sigma-algebra $\Sigma_{\mathrm{Path}(X)}$
is contained in the Borel sigma-algebra induced by Scott-open sets, i.e.,
$\Sigma_{\mathrm{Path}(X)}\subseteq\Sigma_{\mathrm{Path}^{\scriptscriptstyle\infty}(X)}=\mathcal{B}(\mathcal{S}_{\mathrm{Path}^{\scriptscriptstyle\infty}(X)})$.
Moreover, we also have
$\Sigma_{{\mathrm{Path}}_{\sim}(X)}\subseteq\Sigma_{\mathrm{Path}^{\scriptscriptstyle\infty}_{\sim}(X)}$.

###### Proof.

It suffices to show that $\mathrm{Path}(X)$ is measurable in the space
$\mathrm{Path}^{\scriptscriptstyle\infty}(X)$, i.e.,
$\mathrm{Path}(X)\in\Sigma_{\mathrm{Path}^{\scriptscriptstyle\infty}(X)}$.
From this result follows directly by constructing the trace sigma-algebra
restricted to $\mathrm{Path}(X)$, i.e.,
$\Sigma_{\mathrm{Path}^{\scriptscriptstyle\infty}(X)}|_{\mathrm{Path}(X)}=\\{U\cap\mathrm{Path}(X)\mid
U\in\Sigma_{\mathrm{Path}^{\scriptscriptstyle\infty}(X)}\\}$. Since
$\mathrm{Path}(X)$ is measurable we have
$\Sigma_{\mathrm{Path}^{\scriptscriptstyle\infty}(X)}|_{\mathrm{Path}(X)}\subseteq\Sigma_{\mathrm{Path}^{\scriptscriptstyle\infty}(X)}$.
Moreover, every open set $U\in\mathcal{O}_{\mathrm{Path}(X)}$ is contained in
$\Sigma_{\mathrm{Path}^{\scriptscriptstyle\infty}(X)}|_{\mathrm{Path}(X)}$
because $U={U}_{{\scriptscriptstyle\infty}}\cap\mathrm{Path}(X)$ and
${U}_{{\scriptscriptstyle\infty}}\in\Sigma_{\mathrm{Path}^{\scriptscriptstyle\infty}(X)}$;
thus,
$\Sigma_{\mathrm{Path}(X)}\subseteq\Sigma_{\mathrm{Path}^{\scriptscriptstyle\infty}(X)}|_{\mathrm{Path}(X)}$.

Thus, it suffices to show that the set $\mathrm{Path}(X)$ is measurable in
$\mathrm{Path}^{\scriptscriptstyle\infty}(X)$. Next, we claim that every
singleton $\\{p\\}$ (for $p\in\mathrm{Path}(X)$) is measurable in the space
$\mathrm{Path}^{\scriptscriptstyle\infty}(X)$, i.e.,
$\\{p\\}\in\Sigma_{\mathrm{Path}^{\scriptscriptstyle\infty}(X)}$, for every
$p\in\mathrm{Path}(X)$. To see this, first note that
$\\{p\\}=\downarrow\\!{p}\cap{(\uparrow\\!{p})}_{{\scriptscriptstyle\infty}}$.
From Theorem 21 we know that ${(\uparrow\\!{p})}_{{\scriptscriptstyle\infty}}$
is a Scott-open. Clearly, the history $\downarrow\\!{p}$ is a Scott-closed
set. Moreover, every open and closed set are Borel sets and since sigma-
algebra is closed under countable intersection, we find that the singleton
$\\{p\\}\in\Sigma_{\mathrm{Path}^{\scriptscriptstyle\infty}(X)}$ is Borel
measurable.

Now to complete the proof, it is sufficient to show that the Alexandroff open
set
$\uparrow\\!{\varepsilon_{x}}=\\{p\in\mathrm{Path}(X)\mid\varepsilon_{x}\preceq
p\\}$ is countable (for $x\in X$). From this it follows that the set
$\mathrm{Path}(X)$ is Borel measurable
$\mathrm{Path}(X)\in\Sigma_{\mathrm{Path}^{\scriptscriptstyle\infty}(X)}$
because the set $\mathrm{Path}(X)=\bigcup_{x\in
X}\uparrow\\!{\varepsilon_{x}}$ is countable (since countable unions of
countable sets is countable).

Thus, it remains to verify that the set $\uparrow\\!{\varepsilon_{x}}$ is
countable. Consider the following sets

$\uparrow\\!{(\varepsilon_{x},n)}=\\{p\in\uparrow\\!{\varepsilon_{x}}\mid|\max\mathrm{dom}(p)|=n\\},$

where $|\sigma|$ denote the length of the word $\sigma\in A_{\tau}^{*}$.
Clearly,
$\uparrow\\!{\varepsilon_{x}}=\bigcup_{n\in\mathbb{N}}\uparrow\\!{(\varepsilon_{x},n)}$.
Now, by induction on $n$ we prove that each set
$\uparrow\\!{(\varepsilon_{x},n)}$ is countable. Suppose that the set
$\uparrow\\!{(\varepsilon_{x},n)}$ is countable. Then, a path in
$\uparrow\\!{(\varepsilon_{x},n)}$ can be extended to only countably many
paths in $\uparrow\\!{(\varepsilon_{x},n+1)}$ because the sets $A$ and $X$
are. Let $p\in\mathrm{Path}(X)$. For $a\in A_{\tau},x\in X$, we write
$p_{a,x}$ to denote the path that extends $p$ such that
$p_{a,x}(\max\mathrm{dom}(p)a)=x$. Then, the set $\\{p_{a,x}\mid a\in
A_{\tau}\land x\in X\\}$ (for a given $p$) is isomorphic to the countable set
$A\times X$ (Cartesian product of countable sets is countable). Therefore, the
set
$\uparrow\\!{(\varepsilon_{x},n+1)}=\bigcup_{p\in\uparrow\\!{(\varepsilon_{x},n)}}\\{p_{a,x}\mid
a\in A_{\tau}\land x\in X\\}$ is countable. Thus, the set
$\uparrow\\!{\varepsilon_{x}}$ is also countable (since countable union of
countable sets is a countable set).

In the context of stutter equivalent paths, we show that
${\mathrm{Path}}_{\sim}(X)\in\Sigma_{\mathrm{Path}^{\scriptscriptstyle\infty}_{\sim}(X)}$.
First observe that every singleton $\\{{[p]}_{\sim}\\}$ is measurable in
$\mathrm{Path}^{\scriptscriptstyle\infty}_{\sim}(X)$ because
$\\{{[p]}_{\sim}\\}=\downarrow\\!{{[p]}_{\sim}}\cap{(\uparrow\\!{{[p]}_{\sim}})}_{{\scriptscriptstyle\infty}}$.
Lastly, $\mathrm{Path}(X)=\bigcup_{p\in\mathrm{Path}(X)}\\{{[p]}_{\sim}\\}$ is
measurable since countable union of measurable sets is measurable. ∎

##  Appendix V Proofs concerning Section 5

######  Proposition V.1 (Proposition 24).

In an Alexandroff space $(X,\mathcal{O}_{X})$, a separated subset $U\subseteq
X$ (i.e., $U=U^{\star}$) has topologically distinguishable points. Moreover,

  1. 1.

the separation closure of a set is always separated, i.e.,
$U^{\star}={U^{\star}}^{\star}$, for any $U\subseteq X$.

  2. 2.

the collection of separated sets is hereditary, i.e., if $U_{1}\subseteq
U_{2}$ and $U_{2}=U_{2}^{\star}$, then $U_{1}=U_{1}^{\star}$.

  3. 3.

for any subset $U\subseteq X$, we have $(\uparrow\\!{U})^{\star}\subseteq
U^{\star}$. Moreover the converse also holds, if the underlying space $X$ is a
$T_{0}$ space. Here, upward closure is w.r.t. the specialisation order
$\preceq$, i.e., $x\preceq
x^{\prime}\iff\mathrm{cl}(x)\subseteq\mathrm{cl}(x^{\prime})$, for any
$x,x^{\prime}\in X$.

###### Proof.

Let $U=U^{\star}$ be a separated set and let $x,x^{\prime}\in U$ with $x\neq
x^{\prime}$. Then, $\mathrm{cl}(x)\cap U=\\{x\\}$ and
$\mathrm{cl}(x^{\prime})\cap U=\\{x^{\prime}\\}$. Thus,
$x^{\prime}\not\in\mathrm{cl}(x),x\not\in\mathrm{cl}(x^{\prime})$. Clearly,
the points $x,x^{\prime}$ are topologically distinguishable because there is
an open set $X\setminus\mathrm{cl}(x)$ which contains $x^{\prime}$, but not
$x$, i.e., $x^{\prime}\in X\setminus\mathrm{cl}(x)$ and $x\not\in
X\setminus\mathrm{cl}(x)$.

1

Let $U\subseteq X$ and let $x\in U^{\star}$. Then, we show that
$\mathrm{cl}(x)\cap U^{\star}=\\{x\\}$. Suppose otherwise that there is a
point $x^{\prime}\in\mathrm{cl}(x)\cap U^{\star}$ with $x\neq x^{\prime}$.
Then, $x^{\prime}\in U^{\star}$. Moreover, from the above we find
$x^{\prime}\not\in\mathrm{cl}(x)$; but this violates the assumption
$x^{\prime}\in\mathrm{cl}(x)$. Therefore, $x\in{U^{\star}}^{\star}$. The other
direction ${U^{\star}}^{\star}\subseteq U^{\star}$ is trivial.

2

Let $U_{1}\subseteq U_{2}$ and $U_{2}=U_{2}^{\star}$. Then, it suffices to
show that $U_{1}\subseteq U_{1}^{\star}$, i.e., $\mathrm{cl}(x)\cap
U_{1}=\\{x\\}$, for any $x\in U_{1}$. Let $x\in U_{1}$. Then, we find
$\mathrm{cl}(x)\cap U_{1}\subseteq\mathrm{cl}(x)\cap U_{2}=\\{x\\}$. Clearly,
$x\in\mathrm{cl}(x)\cap U_{1}$. Thus, $\mathrm{cl}(x)\cap U_{1}=\\{x\\}$;
whence, $x\in U_{1}^{\star}$.

3

Let $x\in(\uparrow\\!{U})^{\star}$. Then,
$\mathrm{cl}(x)\cap\uparrow\\!{U}=\\{x\\}$. I.e., $y\preceq x$ for some $y\in
U$. And by the definition of specialisation order we find
$\mathrm{cl}(y)\subseteq\mathrm{cl}(x)$ (i.e., $y\in\mathrm{cl}(x)$). But
$\mathrm{cl}(x)\cap\uparrow\\!{U}=\\{x\\}$, thus, $y=x$ and $x\in U$.
Moreover, $\mathrm{cl}(x)\cap
U\subseteq\mathrm{cl}(x)\cap\uparrow\\!{U}=\\{x\\}$; whence, $x\in U^{\star}$.

For the other direction, let $x\in U^{\star}$. Clearly, $x\in\uparrow\\!{U}$
because $x\in U$. Thus, it remains to show that
$\mathrm{cl}(x)\cap\uparrow\\!{U}=\\{x\\}$. Suppose $y\neq x$ and
$y\in\mathrm{cl}(x)\cap\uparrow\\!{U}$, i.e., $y\in\mathrm{cl}(x)$ and
$y\in\uparrow\\!{U}$. Then, we find some $x^{\prime}\in U$ such that
$y\in\uparrow\\!{x^{\prime}}$ and $x^{\prime}\in U$. By transitivity of the
specialisation order we find, $x^{\prime}\preceq y\preceq x$. Moreover, $x\in
U^{\star}$; thus, $x^{\prime}=x$. And, since the given space $X$ is $T_{0}$,
we know that $\preceq$ is antisymmetric. Thus, $y=x$, which contradicts the
assumption $y\neq x$; whence $x\in(\uparrow\\!{U})^{\star}$.∎

######  Lemma V.2 (Lemma 25).

For a given probabilistic transition system $(X,A_{\tau},P)$, define a set as
follows: $x\ext@arrow
0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{L}{}Y=\\{p\in\mathrm{Path}(X)\mid
p(\varepsilon)=x\land\mathrm{trace}(p)\in L\land\mathrm{last}(p)\in Y\\}.$
Then, $\sum_{p\in x\xrightarrow{L}Y}\mu_{P}(p)=\sum_{p\in(x\ext@arrow
0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{L}{}Y)^{\star}}\mu_{P}(p)$.

###### Proof.

We begin by proving that $x\xrightarrow{L}Y\subseteq(x\ext@arrow
0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{L}{}Y)^{\star}$. Let $p\in
x\xrightarrow{L}Y$. Then, we need to show that $\mathcal{N}(p)\cap x\ext@arrow
0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{L}{}Y=\\{p\\}$. Suppose
otherwise that $\mathcal{N}(p)\cap x\ext@arrow
0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{L}{}Y\neq\\{p\\}$. Note that
$p\in\mathcal{N}(p)=\downarrow\\!{p}$ and $p\in x\ext@arrow
0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{L}{}Y$ (because $p\in
x\xrightarrow{L}Y$). Therefore, $\\{p\\}\subseteq\mathcal{N}(p)\cap
x\ext@arrow 0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{L}{}Y$. Now
consider a path $q\in\downarrow\\!{p}\cap q\in x\ext@arrow
0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{L}{}Y$ with $p\neq q$. Then,
we find $q\prec p$, $\mathrm{trace}(q)\in L$, and $\mathrm{last}(q)\in Y$.
Moreover, $q\prec p$ and $p(\varepsilon)=x$ implies that $q(\varepsilon)=x$,
i.e., $q\in\mathrm{Exec}(x)$. Thus, $p\not\in x\xrightarrow{L}Y$, which is a
contradiction. Hence, $\sum_{p\in
x\xrightarrow{L}Y}\mu_{P}(p)\leq\sum_{p\in(x\ext@arrow
0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{L}{}Y)^{\star}}\mu_{P}(p)$.

Now consider a path $p\in(x\ext@arrow
0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{L}{}Y)^{\star}$. We will
first show that if $p\in\mathrm{Exec}(x)$ then $p\in x\xrightarrow{L}Y$. Let
$p\in(x\ext@arrow
0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{L}{}Y)^{\star}$ with
$p\in\mathrm{Exec}(x)$. Then, we need to show that there is no path $q$ such
that $q\prec p$, $\mathrm{trace}(q)\in L$, and $\mathrm{last}(q)\in Y$.
Suppose otherwise that there is a $q$ with $q\prec p$, $\mathrm{trace}(q)\in
L$, and $\mathrm{last}(q)\in Y$. Then, $q\in x\ext@arrow
0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{L}{}Y$. But,
$\mathcal{N}(p)\cap x\ext@arrow
0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{L}{}Y\neq\\{p\\}$, since
$q\in\mathcal{N}(p)$ and $q\in x\ext@arrow
0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{L}{}Y$. Thus,
$p\not\in(x\ext@arrow
0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{L}{}Y)^{\star}$, which is a
contradiction. Hence, $(x\ext@arrow
0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{L}{}Y)^{\star}\cap\mathrm{Exec}(x)=x\xrightarrow{L}Y$.
Moreover, for any $p\in(x\ext@arrow
0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{L}{}Y)^{\star}$ and
$p\not\in\mathrm{Exec}(x)$ we have $\mu_{P}(p)=0$. Thus, $\sum_{p\in
x\xrightarrow{L}Y}\mu_{P}(p)=\sum_{p\in(x\ext@arrow
0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{L}{}Y)^{\star}}\mu_{P}(p)$.
∎

######  Theorem V.3 (Theorem 26).

Let $p\in\mathrm{Path}(X)$ be a path and let $U\subseteq\mathrm{Path}(X)$ be a
separated set of paths such that $p\preceq U$, i.e., $\forall_{q\in U}\
p\preceq q$. Then, $\sum_{q\in U}\mu_{P}(q)\leq\mu_{P}(p)$.

###### Proof.

We first compute:

$\displaystyle\sum_{q\in U}\mu_{P}(q)=\sum_{q\in
U\cap\bigcup\\{\mathrm{Exec}(x)\mid x\in X\\}}\prod_{\sigma
a\in\mathrm{dom}(q)}P(q(\sigma),y,q(\sigma a))$ $\displaystyle=$
$\displaystyle\sum_{q\in U\cap\bigcup\\{\mathrm{Exec}(x)\mid x\in
X\\}}\prod_{\sigma a\in\mathrm{dom}(p)}P(p(\sigma),a,P(\sigma
a))\cdot\prod_{\sigma
a\in\mathrm{dom}(q)\setminus\mathrm{dom}(p)}P(q(\sigma),a,q(\sigma a))$
$\displaystyle=$ $\displaystyle\sum_{q\in U\cap\bigcup\\{\mathrm{Exec}(x)\mid
x\in X\\}}\mu_{P}(p)\cdot\prod_{\sigma
a\in\mathrm{dom}(q)\setminus\mathrm{dom}(p)}P(q(\sigma),a,q(\sigma a))$
$\displaystyle=$ $\displaystyle\mu_{P}(p)\cdot\sum_{q\in
U\cap\bigcup\\{\mathrm{Exec}(x)\mid x\in X\\}}\prod_{\sigma
a\in\mathrm{dom}(q)\setminus\mathrm{dom}(p)}P(q(\sigma),a,q(\sigma a)).$

Now asume $U$ is finite – if it is not, pick arbitrarily a finite
$\overline{U}\subseteq_{\mathrm{f}}U$, the result for an infinite $U$ follows
then by definition of infinite sums – then, by separation, there exists an
$n\in\mathbb{N}_{0}$, such that for all $q_{1},q_{2}\in
U\cap\bigcup\\{\mathrm{Exec}(x)\mid x\in X\\}$ it holds that $q_{1}\neq
q_{2}\Rightarrow\mathrm{dom}(q_{1})\cap\mathrm{dom}(q_{2})\cap
A_{\tau}^{n}=\emptyset$. From $\sum_{(a,x^{\prime})\in A_{\tau}\times
X}P(x,a,x^{\prime})\in\\{0,1\\}$ and non-negativity of $P$ it follows for any
path $q\in U\cap\bigcup\\{\mathrm{Exec}(x)\mid x\in X\\}$ that

$\prod_{\sigma
a\in\mathrm{dom}(q)\setminus\mathrm{dom}(p)}P(q(\sigma),a,q(\sigma
a))\leq\prod_{\sigma a\in(\mathrm{dom}(q)\setminus\mathrm{dom}(p))\cap
A_{\tau}^{\leq n}}P(q(\sigma),a,q(\sigma a))$

We will now show that, in turn

$\sum_{q\in U\cap\bigcup\\{\mathrm{Exec}(x)\mid x\in X\\}}\prod_{\sigma
a\in(\mathrm{dom}(q)\setminus\mathrm{dom}(p))\cap A_{\tau}^{\leq
n}}P(q(\sigma),a,q(\sigma a))\leq 1.$

Plugging this into the previous computation yields the desired result.

In order to see that

$\sum_{q\in U\cap\bigcup\\{\mathrm{Exec}(x)\mid x\in X\\}}\prod_{\sigma
a\in(\mathrm{dom}(q)\setminus\mathrm{dom}(p))\cap A_{\tau}^{\leq
n}}P(q(\sigma),a,q(\sigma a))\leq 1$

holds, we model the weights each path $q\in
U\cap\bigcup\\{\mathrm{Exec}(x)\mid x\in X\\}$ contributes to the sum using a
rooted, directed tree $G=(V,E)$, where $V$ is the set of vertices and $E$ is
the set of edges. In this tree, each vertex is labelled with a path $q$ and
and will be associated with a weight $w(q)$ that is the sum of all weights of
$q^{\prime}\in U\cap\bigcup\\{\mathrm{Exec}(x)\mid x\in X\\}$ in the above
sum, i.e. it holds that

$w(q)=\sum_{q^{\prime}\in U\cap\bigcup\\{\mathrm{Exec}(x)\mid x\in
X\\},\mathrm{dom}(q^{\prime})\supseteq\mathrm{dom}(q)}\prod_{\sigma
a\in(\mathrm{dom}(q^{\prime})\setminus\mathrm{dom}(q))\cap A_{\tau}^{\leq
n}}P(q^{\prime}(\sigma),a,q^{\prime}(\sigma a)).$

For this purpose, build the tree from the root downwards as follows. The root
is labelled $p$. Now, given a vertex with label $q$, if $q\in U$, $q$ is a
leaf, otherwise consider all pairs $(a,x)\in A_{\tau}\times X$ such that there
exists a $q^{\prime}\in U$ with
$\max\mathrm{dom}(q)a\in\mathrm{dom}(q^{\prime})$ and
$q^{\prime}\mid_{\mathrm{dom}(q)}=q$. For all such $(a,x)$, there exists a
successor vertex labelled
$q^{\prime}\mid_{\downarrow\\!{\max\mathrm{dom}(q)a}}$ and the edge
$e=(q,q^{\prime}\mid_{\downarrow\\!{\max\mathrm{dom}(q)a}})$ has weight

$w(e)=P(q^{\prime}(\max\mathrm{dom}(q)),a,q^{\prime}(\max\mathrm{dom}(q)a)).$

Note, that if $U$ is non-empty, this is a mutually exclusive choice, because
of separetedness of $U$; if $U$ is empty, then the sum is taken over an empty
set, and the result holds trivially. Now, given any vertex $v$, we can
inductively define its weight $w(v)$ via a case distinction. If $v$ is a leaf,
then $w(v)=1$. Otherwise,

$w(v)=\sum_{\\{v^{\prime}\mid(v,v^{\prime})\in E\\}}w(v,v^{\prime})\cdot
w(v).$

This way, we ensure that each node labelled as $q$ has the weight

$w(q)=\sum_{q^{\prime}\in U\cap\bigcup\\{\mathrm{Exec}(x)\mid x\in
X\\},\mathrm{dom}(q^{\prime})\supseteq\mathrm{dom}(q)}\prod_{\sigma
a\in(\mathrm{dom}(q^{\prime})\setminus\mathrm{dom}(q))\cap A_{\tau}^{\leq
n}}P(q^{\prime}(\sigma),a,q^{\prime}(\sigma a)).$

In particular, it holds that

$w(p)=\sum_{q\in U\cap\bigcup\\{\mathrm{Exec}(x)\mid x\in X\\}}\prod_{\sigma
a\in(\mathrm{dom}(q)\setminus\mathrm{dom}(p))\cap A_{\tau}^{\leq
n}}P(q(\sigma),a,q(\sigma a)).$

Now it is easy to see inductively, that for each vertex $q$ it holds that
$w(q)\leq 1$. If $q$ is a leaf, this follows by definition. Otherwise, we can
see inductively, that all successor vertices have a weight less than or equal
$1$. Now, let $x=q(\max\mathrm{dom}(q))$, then the weight of $q$ must be
smaller than or equal to $\sum_{(a,x^{\prime})\in A_{\tau}\times
X}P(x,a,x^{\prime})$ – each edge starting in $q$ corresponds to one such
$P(x,a,x^{\prime})$ and all these values get multiplied with a value that is
not greater than $1$ – and by definition of $P$, this smaller or equal to $1$,
which concludes the proof. ∎

######  Theorem V.4 (Theorem 27).

Let $(X,A_{\tau},P)$ be a given probabilistic transition system. Then, the
function
$\mathcal{O}_{\mathrm{Path}(X)}\rTo^{\tilde{\mu}_{P}}\left[0,\infty\right]$
defined as $\tilde{\mu}_{P}(U)=\mu_{P}(U^{\star})$ (for every open set
$U\in\mathcal{O}_{\mathrm{Path}(X)}$) is a locally finite and Scott-continuous
valuation.

###### Proof.

Clearly, $\tilde{\mu}_{P}$ is strict because $\emptyset^{\star}=\emptyset$ and
$\mu_{P}(\emptyset)=0$. Also, local finiteness is straightforward because for
any path $p$ we have a finitely valued open neighbourhood $\uparrow\\!{p}$.
Moreover, using Proposition 24.3 we find that
$\tilde{\mu}_{P}(\uparrow\\!{p})=\mu_{P}((\uparrow\\!{p})^{\star})=\mu_{P}(\\{p\\}^{\star})=\mu_{P}(p)<\infty$.

Order preservation

Let $U_{1}\subseteq U_{2}$ for some
$U_{1},U_{2}\in\mathcal{C}_{\mathrm{Path}(X)}$. Let $p\in U_{1}^{\star}$.
I.e., $p\in U_{2}$. Since $U_{2}^{\star}$ contains all the minimal elements of
$U_{2}$, we find some $q\in U_{2}^{\star}$ such that $q\preceq p$. Thus, we
can partition the set $U_{1}^{\star}$ in the following way: $p\approx
p^{\prime}\iff\exists_{q\in U_{2}^{\star}}\ q\preceq p\land q\preceq
p^{\prime}$. To verify transitivity of $\approx$, let $p\approx p^{\prime}$
and $p^{\prime}\approx p^{\prime\prime}$. Then we find $q\preceq p,q\preceq
p^{\prime},q^{\prime}\preceq p^{\prime}$, and $q^{\prime}\preceq
p^{\prime\prime}$, for some $q,q^{\prime}\in U_{2}^{\star}$. By downward
totality of paths we have $q\preceq q^{\prime}\vee q^{\prime}\preceq q$. In
any case, $q=q^{\prime}$ since $q,q^{\prime}\in U_{2}^{\star}$. Thus,
$p\approx p^{\prime\prime}$. Next, we prove that for any $q\in U_{2}^{\star}$
and $[p]_{q}=\\{p^{\prime}\in U_{1}^{\star}\mid p\approx p^{\prime}\\}$ with
$p\in U_{1}^{\star}$ and $q\preceq p$ we have
$\mu_{P}(q)\geq\sum_{p^{\prime}\in[p]_{q}}\mu_{P}(p^{\prime})$. Note that each
$p^{\prime}\in[p]_{q}$ is a future of $q$, i.e., $q\preceq p^{\prime}$ and any
two paths in $p^{\prime},p^{\prime\prime}\in[p]_{q}$ are topologically
distinguishable paths (i.e., in order theoretic terms they are incomparable).
Furthermore, probabilistic transition system are image finite, i.e., there are
finitely many elements $p^{\prime}\in[p]_{q}$ with $\mu_{P}(p^{\prime})\geq 0$
and the sum of outgoing transitions is either 0 or 1. I.e., there are some
finitely many real numbers $r_{1},\cdots,r_{n}\in(0,1)$ such that
$\sum_{i=1}^{n}r_{i}\leq 1$ and
$\sum_{p^{\prime}\in[p]_{q}}\mu_{P}(p^{\prime})=\sum_{i=1}^{n}r_{i}\mu_{P}(q)\leq\mu_{P}(q)$.
Thus, $\mu_{P}(U_{1}^{\star})\leq\mu_{P}(U_{2}^{\star})$. The proof for the
case when $U_{1},U_{2}$ are infinite sets follows immediately from above.

Modularity

Let $U_{1},U_{2}\in\mathcal{O}_{\mathrm{Path}(X)}$ be any two open sets. Then
we find

$\displaystyle\tilde{\mu}_{P}(U_{1})+\tilde{\mu}_{P}(U_{2})=$ $\displaystyle\
\mu_{P}(U_{1}^{\star})+\mu_{P}(U_{2}^{\star})$ $\displaystyle=$
$\displaystyle\
\sup\\{\mu_{P}(\bar{U}_{1})\mid\bar{U}_{1}\subseteq_{\mathrm{f}}U_{1}^{\star}\\}+\sup\\{\mu_{P}(\bar{U}_{2})\mid\bar{U}_{2}\subseteq_{\mathrm{f}}U_{2}^{\star}\\}$
$\displaystyle=$ $\displaystyle\
\sup\\{\mu_{P}(\bar{U}_{1})+\mu_{P}(\bar{U}_{2})\mid\bar{U}_{1}\subseteq_{\mathrm{f}}U_{1}^{\star}\land\bar{U}_{2}\subseteq_{\mathrm{f}}U_{2}^{\star}\\}.$

and

$\displaystyle\tilde{\mu}_{P}(U_{1}\cup U_{2})+$
$\displaystyle\tilde{\mu}_{P}(U_{1}\cap U_{2})=\mu_{P}((U_{1}\cup
U_{2})^{\star})+\mu_{P}((U_{1}\cap U_{2})^{\star})$ $\displaystyle=$
$\displaystyle\
\sup\\{\mu_{P}(\bar{U})\mid\bar{U}\subseteq_{\mathrm{f}}(U_{1}\cup
U_{2})^{\star}\\}+\sup\\{\mu_{P}(\bar{U}^{\prime})\mid\bar{U}^{\prime}\subseteq_{\mathrm{f}}(U_{1}\cap
U_{2})^{\star}\\}$ $\displaystyle=$ $\displaystyle\
\sup\\{\mu_{P}(\bar{U})+\mu_{P}(\bar{U}^{\prime})\mid\bar{U}\subseteq_{\mathrm{f}}(U_{1}\cup
U_{2})^{\star}\land\bar{U}^{\prime}\subseteq_{\mathrm{f}}(U_{1}\cap
U_{2})^{\star}\\}.$

Let $\bar{U}_{1}\subseteq_{\mathrm{f}}U_{1}^{\star}$ and
$\bar{U}_{2}\subseteq_{\mathrm{f}}U_{2}^{\star}$. Let
$\bar{U}\subseteq(U_{1}\cup U_{2})^{\star}$ and
$\bar{U}^{\prime}\subseteq(U_{1}\cap U_{2})^{\star}$ be the smallest sets
satisfying the condition (respectively):

$\forall_{p\in\bar{U}_{1}\cup\bar{U}_{2}}\exists_{q\in\bar{U}}\ q\preceq
p\qquad\text{and}\qquad\forall_{p\in\bar{U}_{1}\cap\bar{U}_{2}}\exists_{q\in\bar{U}^{\prime}}\
q\preceq p.$

Then, we find that the sets $\bar{U},\bar{U}^{\prime}$ are finite since the
given sets $\bar{U}_{1}\cup\bar{U}_{2},\bar{U}_{1}\cap\bar{U}_{2}$ are finite.
Next, we prove the inequality
$\mu_{P}(\bar{U}_{1})+\mu_{P}(\bar{U}_{2})\leq\mu_{P}(\bar{U})+\mu_{P}(\bar{U}^{\prime})$
indirectly by establishing:

$\mu_{P}(\bar{U}_{1})+\mu_{P}(\bar{U}_{2})\leq\mu_{P}(\bar{U}\cup\bar{U}^{\prime}).$

Let $p_{1}\in\bar{U}_{1},p_{2}\in\bar{U}_{2}$. I.e., there are paths
$q_{1},q_{2}\in\bar{U}$ such that $q_{1}\preceq p_{1}$ and $q_{2}\preceq
p_{2}$. If $q_{1}\neq q_{2}$ then we are done. So suppose $q_{1}=q_{2}$. Then,
we find that $p_{1},p_{2}\in U_{1}\cap U_{2}$ because $U_{1},U_{2}$ are open
sets. I.e., there are paths $q_{1}^{\prime},q_{2}^{\prime}\in\bar{U}^{\prime}$
such that $q_{1}^{\prime}\preceq p_{1}$ and $q_{2}^{\prime}\preceq p_{2}$.
Notice that $q_{1}^{\prime}\preceq p_{1}$ and $q_{1}\preceq p_{1}$. So by
downward totality we get $q_{1}\preceq q_{1}^{\prime}\lor
q_{1}^{\prime}\preceq q_{1}$. Consider the case $q_{1}^{\prime}\preceq q_{1}$.
Then, we find $q_{1}^{\prime}\in U_{1}\cup U_{2}$ and $q_{1}=q_{1}^{\prime}$
since $q_{1}\in(U_{1}\cup U_{2})^{\star}$. Therefore, the above condition
simplifies to $q_{1}\preceq q_{1}^{\prime}$. Likewise, we can derive
$q_{1}\preceq q_{2}^{\prime}$. Thus,
$\mu_{P}(p_{1})+\mu_{P}(p_{2})\leq\mu_{P}(q)+\mu_{P}(q_{1}^{\prime})+\mu_{P}(q_{2}^{\prime})$.

For the other direction, let $\bar{U}\subseteq_{\mathrm{f}}(U_{1}\cup
U_{2})^{\star}$ and $\bar{U}^{\prime}\subseteq_{\mathrm{f}}(U_{1}\cap
U_{2})^{\star}$. Let $\bar{U}_{1}\subseteq U_{1}^{\star}$ and
$\bar{U}_{2}\subseteq U_{2}^{\star}$ (respectively) be the smallest sets
satisfying the conditions:

$\forall_{p\in(\bar{U}\cap
U_{1})\cup\bar{U}^{\prime}}\exists_{q\in\bar{U}_{1}}\ q\preceq
p\qquad\text{and}\qquad\forall_{p\in(\bar{U}\cap
U_{2})\cup\bar{U}^{\prime}}\exists_{q\in\bar{U}_{2}}\ q\preceq p.$

Then, the sets $\bar{U}_{1},\bar{U}_{2}$ are finite just because the given
sets $\bar{U},\bar{U}^{\prime}$ are finite. Next, we prove the inequality:
$\mu_{P}(\bar{U})+\mu_{P}(\bar{U}^{\prime})\leq\mu_{P}(\bar{U}_{1})+\mu_{P}(\bar{U}_{2})$.
Let $p\in\bar{U},q\in\bar{U}^{\prime}$. Then, we find $p\in U_{1}\cup U_{2}$.
So let $p\in U_{1}$ (the case when $p\in U_{2}$ is symmetric). Then, we find
$p\in\bar{U}\cap U_{1}$. Clearly, $p,q\in(\bar{U}\cap
U_{1})\cup\bar{U}^{\prime}$. I.e., there are some paths
$p^{\prime},q^{\prime}\in\bar{U}_{1}$ such that $p^{\prime}\preceq p$ and
$q^{\prime}\preceq q$. If $p^{\prime}\neq q^{\prime}$, then we are done. So
suppose $p^{\prime}=q^{\prime}$. Then, we observe that $q\in(\bar{U}\cap
U_{2})\cup\bar{U}^{\prime}$ (because $q\in\bar{U}^{\prime}$). I.e., there is
some $q^{\prime\prime}\in\bar{U}_{2}$ such that $q^{\prime\prime}\preceq q$.
Thus,
$\mu_{P}(p)+\mu_{P}(q)\leq\mu_{P}(p^{\prime})+\mu_{P}(q^{\prime\prime})$.

Scott-continuity

Let $(U_{i})_{i\in I}$ be a directed family of open sets. Then, we have to
show that $\tilde{\mu}_{P}(\bigcup_{i\in I}U_{i})=\sup_{i\in
I}\tilde{\mu}_{P}(U_{i})$. First, we note that $U_{i}\subseteq\bigcup_{j\in
I}U_{j}$ (for each $i\in I$). Thus, by order preservation of $\tilde{\mu}_{P}$
we get $\tilde{\mu}_{P}(U_{i})\leq\tilde{\mu}_{P}(\bigcup_{j\in I}U_{j})$, for
each $i\in I$. And by the universal property of $\sup$ we find that
$\sup_{i\in I}\tilde{\mu}_{P}(U_{i})\leq\tilde{\mu}_{P}(\bigcup_{i\in
I}U_{i})$.

Therefore, it remains to show that $\tilde{\mu}_{P}(\bigcup_{i\in
I}U_{i})\leq\sup_{i\in I}\tilde{\mu}_{P}(U_{i})$. I.e., we have to prove

$\sup\left\\{\mu_{P}(\bar{U})\mid\bar{U}\subseteq_{\mathrm{f}}\Big{(}\bigcup_{i\in
I}U_{i}\Big{)}^{\star}\right\\}\leq\sup\left\\{\mu_{P}(U_{i}^{\star})\mid i\in
J\land J\subseteq_{\mathrm{f}}I\right\\}.$

Let $\bar{U}\subseteq_{\mathrm{f}}(\bigcup_{i\in I}U_{i})^{\star}$ and
$p\in\bar{U}$. Then there exists an $i\in I$ such that $p\in U_{i}=:U_{p}$.
Since $\bar{U}$ is finite, we can write $\bar{U}=\\{p_{1},p_{2},...,p_{n}\\}$
for some natural number $n\geq 1$. We now inductively define a _finite family_
of open sets $V_{m}$ as follows: $V_{p_{1}}=U_{p_{1}}$ and given an $m\geq 1$,
there exists a set $V_{p_{m+1}}$ such that $V_{p_{m+1}}\supseteq V_{p_{m}}\cup
U_{p_{m+1}}$ (since the given family $(U_{i})_{i\in I}$ is directed). It is
clear that $\bar{U}$ is separated (cf. Proposition 24.2). Thus, we can
conclude

$\bar{U}\subseteq
V_{p_{n}}\implies\tilde{\mu}_{P}(\bar{U})\leq\tilde{\mu}_{P}(V_{p_{n}})\implies\mu_{P}(\bar{U})\leq\mu(V_{p_{n}}^{*})\enspace.\qed$

######  Proposition V.5 (Proposition 28).

The mapping defined in (2) induced by a probabilistic transition system is a
probability measure.

###### Proof.

Clearly,
$\alpha(x)(\emptyset)=\tilde{\mu}_{P}(\emptyset\cap\uparrow\\!{\varepsilon_{x}})=\tilde{\mu}_{P}(\emptyset)=0$.
Now, let $(U_{i})_{i\in I}$ be a countable family of pairwise disjoint Borel
subsets $U_{i}\in\Sigma_{{\mathrm{Path}}_{\sim}(X)}$ (for each $i\in I$).
Then, we claim that for any $i,j\in I$ with $i\neq j$ we have
${\pi_{X}}^{-1}(U_{i})\cap{\pi_{X}}^{-1}(U_{j})=\emptyset$. Suppose otherwise
we have $p\in{\pi_{X}}^{-1}(U_{i})\cap{\pi_{X}}^{-1}(U_{j})$. Then,
${[p]}_{\sim}\in U_{i}\cap U_{j}$ violating the aforementioned assumption.
Thus,

$\displaystyle\alpha(x)(\bigcup_{i\in I}U_{i})$
$\displaystyle=\tilde{\mu}_{P}\Big{(}{\pi_{X}}^{-1}\big{(}\bigcup_{i\in
I}U_{i}\big{)}\cap\uparrow\\!{\varepsilon_{x}}\Big{)}$
$\displaystyle=\tilde{\mu}_{P}\Big{(}\big{(}\bigcup_{i\in
I}{\pi_{X}}^{-1}(U_{i})\big{)}\cap\uparrow\\!{\varepsilon_{x}}\Big{)}$
$\displaystyle=\tilde{\mu}_{P}\Big{(}\bigcup_{i\in
I}\big{(}{\pi_{X}}^{-1}(U_{i})\cap\uparrow\\!{\varepsilon_{x}}\big{)}\Big{)}$
$\displaystyle=\sum_{i\in
I}\tilde{\mu}_{P}\big{(}{\pi_{X}}^{-1}(U_{i})\cap\uparrow\\!{\varepsilon_{x}}\big{)}=\sum_{i\in
I}\alpha(x)(U_{i}).$

Lastly,