On path-based coalgebras and weak notions of bisimulation

TL;DR

This paper develops a coalgebraic framework for understanding branching bisimulation in systems with silent actions, showing that recording execution paths up to stuttering suffices for behavioral equivalence.

Contribution

It introduces a coalgebraic characterization of branching bisimulation for labelled transition and probabilistic systems, addressing silent actions.

Findings

Recording execution paths characterizes branching bisimulation.

Coalgebraic approach unifies different system types.

Silent actions are effectively handled in the framework.

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 bisimulation in the context of labelled transition systems and 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 branching bisimulation in both cases.

Equations

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

$${\mathrm{Path}}_{\sim }(f)[p{]}_{\sim }=[f\circ p{]}_{\sim }\text{for any p∈Path(X) and XrTofY}.$$

$${{\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.$$

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

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

$${\mu }_X(\bigcup _{i\in I}{U}_i)=\sum _{i\in I}{\mu }_X(U_i).$$

$$p⪯q⟺\mathrm{dom}(p)\subseteq \mathrm{dom}(q)\wedge {\forall }_{\sigma \in \mathrm{dom}(p)}q(\sigma )=p(\sigma ).$$

$$X^{\infty }=$$

$${⪯}^{\prime }=$$

$$\tilde{\mu }(V)=\mu (V\cap X)\text{(for every Scott-open set V∈SX∞)}$$

$${\forall }_{x,x^{\prime }\in X}xR{x}^{\prime }⟹{\forall }_{x^{\prime \prime }\in X,a\in A_{\tau }}P(x,{\tau }^{\ast }\hat{a},[x^{\prime \prime }{]}_R)=P(x^{\prime },{\tau }^{\ast }\hat{a},[x^{\prime \prime }{]}_R).$$

$${\mu }_P(p)=\{\begin{array}{ll}{\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∈X}\\ 0,& \text{otherwise}\end{array}.$$

$$\alpha (x)(U)={\tilde{\mu }}_P({{\pi }_X}^{-1}(U)\cap \uparrow {\epsilon }_x),\text{for every}U\in {\Sigma }_{{\mathrm{Path}}_{\sim }(X)}.$$

$${\nu }_{f(x)}(V)={\tilde{\mu }}_P({\pi }^{-1}{{\mathrm{Path}}_{\sim }(f)}^{-1}V\cap \uparrow {\epsilon }_x),\text{for every}V\in {\mathcal{O}}_{{\mathrm{Path}}_{\sim }(X/R)}.$$

$$\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{)},$$

$$\alpha (x)=\{[(p(ϵ),a,p({\tau }^{n}a{\tau }^m))]\mid$$

$$\forall i<n:p({\tau }^i)\stackrel{\tau }{\to }p({\tau }^{i+1}),$$

$$p({\tau }^n)\stackrel{a}{\to }p({\tau }^{n}a),$$

$$\forall j<m:p({\tau }^{n}a{\tau }^j)\stackrel{\tau }{\to }p({\tau }^{n}a{\tau }^{j+1}),$$

$$a\in A_{\tau }\}\cup \{[x]\mid x\in X\}$$

$$\alpha (x)=\{[q]\mid$$

$$\mathsf{dom}(p)={\tau }^{n}a{\tau }^m,$$

$$\forall i<n:p({\tau }^i)\stackrel{\tau }{\to }p({\tau }^{i+1}),$$

$$p({\tau }^n)\stackrel{a}{\to }p({\tau }^{n}a),$$

$$\forall j<m:p({\tau }^{n}a{\tau }^j)\stackrel{\tau }{\to }p({\tau }^{n}a{\tau }^{j+1}),$$

$$a\in A_{\tau }\}\cup \{[x]\mid x\in X\}$$

$$\alpha (x)=\{[q]\mid$$

$$\mathsf{dom}(p)={\tau }^{n}a{\tau }^m,$$

$$\forall i<n:p({\tau }^i)\stackrel{\tau }{\to }p({\tau }^{i+1}),$$

$$p({\tau }^n)\stackrel{a}{\to }p({\tau }^{n}a),$$

$$\forall j<m:p({\tau }^{n}a{\tau }^j)\stackrel{\tau }{\to }p({\tau }^{n}a{\tau }^{j+1}),$$

$$a\in A_{\tau }\}\cup \{[x]\mid x\in X\}$$

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

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

$$=$$

$${{\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.$$

$$p(\sigma )=p^{†}\varphi (\sigma )$$

$$⟺$$

Full text

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.

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 [math]. 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

[TABLE]

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)$.

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:

$\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:

[TABLE]

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$.

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,

[TABLE]

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:

[TABLE]

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)$:

[TABLE]

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

[TABLE]

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:

[TABLE]

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.

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.

[TABLE]

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:

[TABLE]

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

[TABLE]

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:

[TABLE]

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}$.

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,

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:

[TABLE]

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:

[TABLE]

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

[TABLE]

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).

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

[TABLE]

$\eta$** Bisimulation**

[TABLE]

Delay Bisimulation

[TABLE]

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:

[TABLE]

Weak Bisimulation

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

[TABLE]

$\eta$** Bisimulation**

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

[TABLE]

Delay Bisimulation

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

[TABLE]

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:

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}$. {diagram} 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.

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:

[TABLE]

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

[TABLE]

Lemma II.6** (Lemma 6).**

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

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,

[TABLE]

Proof.

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

[TABLE] 3. 3.

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

[TABLE] 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,

[TABLE]

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

[TABLE]

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:

[TABLE]

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:

[TABLE]

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,

[TABLE]

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,

[TABLE]

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:

[TABLE]

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

[TABLE]

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,

[TABLE]

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:

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

[TABLE]

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

[TABLE]

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,

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:

[TABLE]

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

[TABLE]

We will now show that, in turn

[TABLE]

Plugging this into the previous computation yields the desired result.

In order to see that

[TABLE]

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

[TABLE]

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

[TABLE]

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,

[TABLE]

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

[TABLE]

In particular, it holds that

[TABLE]

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

[TABLE]

and

[TABLE]

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):

[TABLE]

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:

[TABLE]

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:

[TABLE]

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

[TABLE]

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

[TABLE]

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,

[TABLE]

Lastly, $\alpha(x)({\mathrm{Path}}_{\sim}(X))=\tilde{\mu}_{P}(\mathrm{Path}(X)\cap\uparrow\!{\varepsilon_{x}})=\tilde{\mu}_{P}(\uparrow\!{\varepsilon_{x}})=\mu_{P}(\varepsilon_{x})=1$. ∎

Theorem V.6** (Theorem 29).**

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

Proof.

$\Rightarrow$ For this direction, it was left to show that $\nu_{f(x)}$ in (3) is well-defined. We first recall a technical result from [21, Lemma 24]. For any branching bisimulation $R$, any $R$-saturated set $M\subseteq X$, and any saturated block $W\subseteq A_{\tau}^{*}$, the following equation holds

[TABLE]

A subset $M\subseteq X$ is $R$-saturated if for all $x\in M$, the whole equivalence class of $x$ is contained in $M$, i.e., $\forall_{x,x^{\prime}}\ (x\in M\land xRx^{\prime})\implies x^{\prime}\in M$. A subset $W\subseteq A_{\tau}^{*}$ is saturated if it can be decomposed into a collection of blocks $B_{i}$, for some index set $I$, i.e., $W=\bigcup_{i\in I}B_{i}$, where each block $B_{i}=\tau^{*}a_{1}\tau^{*}\cdots\tau^{*}a_{n}\tau^{*}$, for a word $a_{1}a_{2}\cdots a_{n}\in A_{\tau}^{*}$.

Let $U={\pi}^{-1}({{\mathrm{Path}}_{\sim}(f)}^{-1}V)$. First we claim that $\mathrm{trace}(U)=\{\mathrm{trace}(p)\mid{[fp]}_{\sim}\in V\}$ is saturated by establishing the equation:

[TABLE]

where the operation $A_{\tau}^{*}\rTo^{g}\mathcal{P}(A_{\tau}^{*})$ is defined inductively as follows: $g(\varepsilon)=\tau^{*}$ and $g(\sigma a)=g(\sigma)\tau^{*}a\tau^{*}$. The direction $\mathrm{trace}(U)\subseteq\bigcup_{{[fp]}_{\sim}\in U}g(\mathrm{trace}({p}^{{\dagger}}))$ because $\sigma\in g(\sigma)$, for any $\sigma\in A_{\tau}^{*}$. For the other direction, let $\sigma\in g(\mathrm{trace}({p}^{{\dagger}}))$, for some ${[fp]}_{\sim}\in V$. Let $\mathrm{trace}({p}^{{\dagger}})=a_{1}a_{2}\cdots a_{n}$ (for some $n\geq 1$). Then, we find $\sigma=\tau^{m_{1}}a_{1}\tau^{m_{2}}\cdots\tau^{m_{n}}a_{n}\tau^{m_{n+1}}$.

Define a path $q$ whose domain is $\sigma$ as follows:

[TABLE]

Clearly, ${p}^{{\dagger}}={q}^{{\dagger}}$, i.e., $p\sim q$. Thus, ${[fp]}_{\sim}={[fq]}_{\sim}\in V$; hence, $q\in\mathrm{trace}(U)$.

Next, we verify that $\mathrm{last}(U)$ is an $R$-saturated set. To see this let, $x\in\mathrm{last}(U)$ and $xRx^{\prime}$. Then, there is a path $p\in U$ such that $\mathrm{last}(p)=x$ and ${[fp]}_{\sim}\in V$. Suppose $\mathrm{dom}(p)=\varepsilon$. Then, we find that $f\circ\varepsilon_{x}=f\circ\varepsilon_{x^{\prime}}$ (because $xRx^{\prime}$). I.e., $\varepsilon_{x^{\prime}}\in U$. Now suppose $p$ has a non-empty domain, i.e., there is some path $p^{\prime}\prec p$ such that $\max\mathrm{dom}(p^{\prime})=\sigma$, $\max\mathrm{dom}(p)=\sigma a$, for some $\sigma\in A_{\tau}^{*},a\in A_{\tau}$. Then, we define a path $q$ whose domain is identical to $p$ as follows: $q(\sigma^{\prime})=p^{\prime}(\sigma^{\prime})$ if $\sigma^{\prime}\in\mathrm{dom}(p^{\prime})$ and $q(\sigma a)=x^{\prime}$. Again, we find that $f\circ p=f\circ q$ because $xRx^{\prime}$. Thus, $q\in U$, i.e., $x^{\prime}\in U$.

Now we can prove that $\nu_{f(x)}$ in (3) is well-defined. Suppose $xRx^{\prime}$. Then it suffices to show that $\tilde{\mu}(U\cap\varepsilon_{x})=\tilde{\mu}(U\cap\varepsilon_{x}^{\prime})$, where $U={\pi}^{-1}({{\mathrm{Path}}_{\sim}(f)}^{-1}V)$ and $V\in\mathcal{O}_{{\mathrm{Path}}_{\sim}(X/R)}$. This follows directly from the fact that $\tilde{\mu}(U\cap\varepsilon_{x})=\mu((U\cap\varepsilon_{x})^{\star})=P(x,\mathrm{trace}(U),\mathrm{last}(U))$ and Equation 6.

($\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. We will show that the equivalence relation $xRx^{\prime}\iff f(x)=f(x^{\prime})$ is a probabilistic branching bisimulation in two stages. First, we claim that

[TABLE]

Here, we abbreviate $f(x)\ext@arrow 0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{\tau^{*}\hat{a}}{}\{y\}$ by $f(x)\ext@arrow 0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{\hat{a}}{}\{y\}$. Notice that the sets $\bigcup_{q\in f(x)\ext@arrow 0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{\hat{a}}{}\{y\}}\uparrow\!{{[q]}_{\sim}}$ and $\bigcup_{p\in x\ext@arrow 0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{\hat{a}}{}{f}^{-1}\{y\}}\uparrow\!{{[p]}_{\sim}}$ are open sets (hence Borel sets). Second, we claim that

[TABLE]

Using the above two properties we can now prove the transfer property of bisimulation as follows:

[TABLE]

Next, we show the satisfaction of Property (7). For this we derive

[TABLE]

To show that why the last two steps in the above derivation are equivalent, we prove that $f(x)\ext@arrow 0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{\hat{a}}{}_{\!\!X}\{y\}=x\ext@arrow 0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{\hat{a}}{}{f}^{-1}\{y\}$. Let $p\in f(x)\ext@arrow 0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{\hat{a}}{}_{\!\!X}\{y\}$. Then we find $\varepsilon_{x}\preceq p$, $fp\sim q$, and $q\in f(x)\ext@arrow 0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{\hat{a}}{}\{y\}$, for some $q\in\mathrm{Path}(Y)$. From Lemma 6(1) and 6(3) we find that $p\in x\ext@arrow 0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{\hat{a}}{}{f}^{-1}\{y\}$. For the other direction, take $q=fp$ for any $p\in x\ext@arrow 0395\arrowfill@\relbar\relbar\twoheadrightarrow{}{\hat{a}}{}{f}^{-1}\{y\}$.

Lastly, we show the satisfaction of (8). Let $x\in X,y\in Y$. Then we derive

[TABLE]