3.1.1 State bisimulations and zigzags

Definition 3.5. Given an LMP $\mathbb {S}=(S,\Sigma, \{\tau _a \mid a\in L \})$ , an (internal) state bisimulation $R$ in $\mathbb {S}$ is a binary relation on $S$ such that if $s\mathrel {R}t$ , then for all $C \in \Sigma (R)$ , it holds that

\begin{equation*}\forall a\in L \; \tau _a(s,C)=\tau _a(t,C).\end{equation*}

We say that $s$ and $t$ are state bisimilar, denoted as $s\sim _{\textsf {s},\mathbb {S}} t$ , if there exists a state bisimulation $R$ such that $s\mathrel {R}t$ .

We will often drop the subscript $\mathbb {S}$ and simply write $s\sim _{\textsf {s}} t$ if there is no need for clarification. We have the following well-known result:

3.1.2 Direct sums

Definition 3.10. Given two LMPs $\mathbb {S}$ and $\mathbb {S}'$ , the direct sum LMP $\mathbb {S}\oplus \mathbb {S'}$ has the sum of measurable spaces $(S\oplus S',\Sigma \oplus \Sigma ')$ as underlying measurable space, and Markov kernels:

\begin{align*} \tau _a^\oplus (\textrm {inl}(x),A\oplus A') &\mathrel {\mathop :}= \tau _a(x,A) && x\in S,\\ \tau _a^\oplus (\textrm {inr}(x),A\oplus A') &\mathrel {\mathop :}= \tau _a(x,A') && x\in S'. \end{align*}

The above construction corresponds to the categorical coproduct or sum in the category $\textbf {LMP}$ . It is straightforward from the definition that the following equivalence holds:

(2) \begin{align} \tau _a(s,A)= \tau '_{\!\!a}(s',A') \iff \tau ^{\oplus }_a(\textrm {inl}(s),A\oplus A') = \tau ^{\oplus }_a(\textrm {inr}(s'),A\oplus A'). \end{align}

If $R\subseteq S\times S$ , we can “lift” it to relations $R_l$ and $R_r$ on $S\oplus S'$ and $S'\oplus S$ , respectively, as follows:

(3) \begin{equation} R_l\mathrel {\mathop :}= \{(\textrm {inl}(s),\textrm {inl}(t))\mid s\mathrel {R}t \},\qquad R_r\mathrel {\mathop :}= \{(\textrm {inr}(s),\textrm {inr}(t))\mid s\mathrel {R}t \}. \end{equation}

It is easy to verify that if $R$ is a state bisimulation on $\mathbb {S}$ , then $R_l$ is a state bisimulation on $\mathbb {S}\oplus \mathbb {S'}$ . This only depends on the fact that $(\Sigma \oplus \Sigma ')(R)\upharpoonright S=\Sigma (R)$ (see Lemma 2.1). Additionally, note that this implies that state bisimilarity on the sum of two LMPs restricted to a summand is not smaller than the original bisimilarity on the latter.

As a warm-up for its future use in defining external bisimulations, we will consider the case of equal summands and relate state bisimilarity on $\mathbb {S}\oplus \mathbb {S}$ to state bisimilarity on $\mathbb {S}$ . In this setting, we can lift a relation $R$ on $S$ in various ways: to the left summand as $R_l$ above, to the right, in a crossed manner, or completely. We will focus on the latter case. If $R\subseteq S\times S$ , we define the following binary relation $R^+$ on $S\oplus S$ (i.e., $R^+ \subseteq (S\oplus S)\times (S\oplus S)$ ):

(4) \begin{equation} u \mathrel {R^+} v \iff \exists s,t\in S,\ s \mathrel {R} t \land u\in \{\textrm {inl}(s),\textrm {inr}(s) \} \land v\in \{\textrm {inl}(t),\textrm {inr}(t) \} \end{equation}

Note that $R^+$ is an equivalence relation if and only if $R$ is.

We have the following (unsurprising) characterization: state bisimilarity on the sum $\mathbb {S}\oplus \mathbb {S}$ is the complete lifting of bisimilarity on $\mathbb {S}$ . For this, we use the following auxiliary result.

Proof. We are considering the “leftmost” copy of $S$ , and hence the lhs equals $\{(x,y)\mid \textrm {inl}(x)\sim _{\textsf {s}, \mathbb {S}\oplus \mathbb {S}} \textrm {inl}(y) \}$ . For $(\!\subseteq\!)$ , it suffices to show that ${\sim }_{\textsf {s}, \mathbb {S}\oplus \mathbb {S}} \upharpoonright S$ is a state bisimulation on $\mathbb {S}$ . Let $(x,y)\in {\sim }_{\textsf {s}, \mathbb {S}\oplus \mathbb {S}} \upharpoonright S$ and $A\in \Sigma ({\sim }_{\textsf {s}, \mathbb {S}\oplus \mathbb {S}} \upharpoonright S)$ . First, we prove that $A\oplus A$ is ${\sim }_{\textsf {s}, \mathbb {S}\oplus \mathbb {S}}$ -closed (we already know it is measurable). Assume $u\in A\oplus A$ and $u\sim _{\textsf {s}, \mathbb {S}\oplus \mathbb {S}} v$ . Choose $s,t\in S$ such that $u\in \{\textrm {inl}(s),\textrm {inr}(s) \}$ and $v\in \{\textrm {inl}(t),\textrm {inr}(t) \}$ . Then, we have

\begin{equation*} \textrm {inl}(s)\sim _{\textsf {s}, \mathbb {S}\oplus \mathbb {S}} u\sim _{\textsf {s}, \mathbb {S}\oplus \mathbb {S}} v\sim _{\textsf {s}, \mathbb {S}\oplus \mathbb {S}} \textrm {inl}(t), \end{equation*}

where the relations in both extremes hold since $(\textrm {id}_S)^+$ is a bisimulation. Therefore, by transitivity of state bisimilarity, we conclude $(s,t)\in {\sim }_{\textsf {s}, \mathbb {S}\oplus \mathbb {S}} \upharpoonright S$ . Since $A$ is closed for ${\sim }_{\textsf {s}, \mathbb {S}\oplus \mathbb {S}} \upharpoonright S$ , we obtain $t\in A$ ; hence, $v\in A\oplus A$ and it is ${\sim }_{\textsf {s}, \mathbb {S}\oplus \mathbb {S}}$ -closed. We have

\begin{equation*} \tau _a(x,A) =\tau _a^\oplus (\textrm {inl}(x),A\oplus A) =\tau _a^\oplus (\textrm {inl}(y),A\oplus A) =\tau _a(y,A). \end{equation*}

For $(\supseteq )$ , recall that $(\sim _{\textsf {s}})_l$ is a state bisimulation on $\mathbb {S}\oplus \mathbb {S}$ .

3.1.3 A review of logic and event bisimulation

In Desharnais (Reference Desharnais1999), it was shown that for an LMP over an analytic state space, two states are bisimilar if and only if they satisfy exactly the same formulas of the following simple modal logic $\mathcal {L}$ :

(5) \begin{equation} \top \mid \varphi _1 \wedge \varphi _2 \mid \langle a \rangle _{\gt q}\varphi . \end{equation}

Given an LMP $\mathbb {S}$ , the semantics ${[\![ \varphi ]\!]}_{\mathbb {S}}$ is the set of states of $\mathbb {S}$ for which the formula holds. For instance, $[\![ \langle a \rangle _{\gt q}\varphi ]\!]$ can be recursively defined to be the set $\{s\in S\mid \tau _a(s,{[\![ \varphi ]\!]}) \gt q \}$ . These validity sets are measurable and preserved by zigzag morphisms, as shown in the following lemma (see (Desharnais et al. (Reference Desharnais, Edalat and Panangaden2002), Prop. 9.2) for a slightly more general statement):

In other words, the truth value of these formulas is preserved under zigzag morphisms.

In Danos et al. (Reference Danos, Desharnais, Laviolette and Panangaden2006), a new notion of “event” bisimulation is introduced, which shifts the focus from equivalence relations to the measurable structure of the LMP. In the same work, it is proved that the bisimilarity associated with this new concept is characterized by the logic $\mathcal {L}$ , and this holds for Markov processes defined on general measurable spaces. The following is the central concept in this type of bisimulations.

From Definition 3.15, we can quickly deduce that the union and intersection of stable families are stable. The next theorem identifies the smallest stable $\sigma$ -algebra. Let $[\![ \mathcal {L} ]\!]$ denote $\{{[\![ \varphi ]\!]} \mid \varphi \in \mathcal {L} \}$ .

3.2.1 Mutual transitivities

The question about transitivity for different notions of bisimilarity is not generally a straightforward one. For example, in the case of internal bisimulation of pointed LMPs as in Desharnais (Reference Desharnais1999), a logical characterization in analytic spaces is provided, which solves this question. In Panangaden (Reference Panangaden2009, Prop. 7.12), a proof of transitivity is given for the modified definition of $\oplus$ -bisimilarity that we will see in Section 3.5. For the categorical definitions that we will see in Section 3.3, the same question requires highly technical tools to be answered only in certain cases.

We can ask a more general question about the relationship between one notion of bisimulation and the composition of potentially different ones. The first known fact of this sort involving external bisimilarity concerns the “ $z$ -closure” of a relation. A relation $R\subseteq S\times S'$ is $z$ -closed if, for all $x,y\in S$ and $x',y'\in S'$ , $(x,x'),(y,x'),(y,y')\in R \implies (x,y')\in R$ . The $z$ -closure of a relation is the smallest $z$ -closed relation that contains it. In Bacci (Reference Bacci2013, Lem. 5.3.5), it is proven that if $R$ is a $\times$ -bisimulation between $\mathbb {S}$ and $\mathbb {S}'$ , then its $z$ -closure is also a $\times$ -bisimulation. From this, it can be deduced that $\sim ^\times$ is $z$ -closed: if $x\sim ^\times x'$ , $y\sim ^\times x'$ , and $y\sim ^\times y'$ , then $x\sim ^\times y'$ .

One interesting question regarding transitivity involves three LMPs, as in the following statement:

(7) \begin{equation} s \sim ^\times _{\mathbb {S}_0,\mathbb {S}_1} s' \;\wedge \; s'\sim ^\times _{\mathbb {S}_1,\mathbb {S}_2} s'' \implies s\sim ^\times _{\mathbb {S}_0,\mathbb {S}_2} s''. \end{equation}

The structures defined in Sánchez Terraf (Reference Sánchez Terraf2011, Exm. 1) provide a counterexample to (7). We reproduce it below with some modifications in the notation, as it will be useful on other occasions.

Example 3.30. We consider the LMP $\mathbb {U}$ from Example 3.3 and the following modifications:

\begin{align*} \mathbb {U}_s&=(U\setminus \{t\},\Upsilon \upharpoonright (U\setminus \{t\}),\{\tau _a\mid a\in L\}), \\ \mathbb {U}_t&=(U\setminus \{s\},\Upsilon \upharpoonright (U\setminus \{s\}),\{\tau _a\mid a\in L\}),\\ \mathbb {T}'&=((U\setminus \{s,t\})\cup \{t'\},\sigma (\mathcal {B}(I)\cup \mathcal {P}(\{t',x\})),\{\bar {\tau }_a\mid a\in L\}). \end{align*}

Here, we understand that the kernels in $\mathbb {U}_s$ and $\mathbb {U}_t$ are the appropriate restrictions. The kernels $\bar {\tau }_a$ coincide with $\tau _a$ if $a\in I\cap \mathbb {Q}$ , and for $E\in \sigma (\mathcal {B}(I)\cup \mathcal {P}(\{t',x\}))$ ,

\begin{equation*}\bar {\tau }_\infty (t',E)= \mathfrak {m}(E), \qquad \bar {\tau }_\infty (r,E)= 0 \text { for } r\neq t'.\end{equation*}

The fact that the nonmeasurable set $V$ is not available in $\mathbb {T}'$ allows for the bisimilarity $s\sim ^\times _{\mathbb {U}_s,\mathbb {T}'} t'$ . Additionally, it is clear that $t'\sim ^\times _{\mathbb {T}',\mathbb {U}_t} t$ . However, $s \nsim ^\times _{\mathbb {U}_s,\mathbb {U}_t} t$ . If they were bisimilar, $\textrm {inl}(s)$ and $\textrm {inr}(t)$ would be state bisimilar in $\mathbb {U}_s\oplus \mathbb {U}_t$ , and the proof that they are not closely resembles the one given in Example 3.7, where the state bisimilarity is explicitly calculated.

If two LMPs coincide in the implication (7), we know that $\sim _{\textsf {s},\mathbb {S}}$ and $\sim ^\times _{\mathbb {S},\mathbb {S}}$ coincide; therefore, the question can be understood as a connection between the internal bisimilarity on one of them and the external bisimilarity between the two. If $\mathbb {S}_0=\mathbb {S}_2$ , we obtain the implication $x\sim ^\times x' \; \wedge \; y\sim ^\times x' \implies x\sim _{\textsf {s}} y$ . It is not hard to see that this particular case also fails; a counterexample involves the LMP $\mathbb {U}_B$ (Example 3.9) obtained by modifying the $\sigma$ -algebra of $\mathbb {U}$ and allowing only Borel sets in the interval. Between $\mathbb {U}$ and $\mathbb {U}_B$ , it holds that $s\sim ^\times s$ and $t\sim ^\times s$ , but $s \nsim _{\textsf {s}} t$ in $\mathbb {U}$ . The failure of this property is reasonable because an external bisimulation does not impose conditions on what happens within one of the two LMPs.

The third type of transitivity corresponds to the case $\mathbb {S}_0=\mathbb {S}_1$ , namely,

One attempt to prove such a property proceeds by considering the direct sum $\mathbb {S}\oplus \mathbb {S}'$ . According to Proposition 3.23(2), $\widehat {{\sim }^\times }$ is an internal state bisimulation on $\mathbb {S}\oplus \mathbb {S}'$ . On the other hand, we recall that the left lift $(\sim _{\textsf {s},\mathbb {S}})_l$ is also a state bisimulation on $\mathbb {S}\oplus \mathbb {S}'$ . Furthermore, it is easy to see that the smallest equivalence relation containing these two internal bisimulations is an internal bisimulation too. We could conclude the proof if we show that its descent is a $\times$ -bisimulation. However, the following example serves to discard the possibility of proving that if $R$ is an internal bisimulation on $\mathbb {S} \oplus \mathbb {S}'$ , then $R_\times$ is a $\times$ -bisimulation.

Example 3.32. Let $\mathbb {S}$ be the discrete process consisting of two states, $x$ and $y$ , with a single transition from $x$ to $y$ with probability 1. Let $\mathbb {S}'$ be a copy of $\mathbb {S}$ with an additional third isolated state. These processes can be represented as in the diagrams:

\begin{equation*} \begin{array}{rcrr} \mathbb {S}: & x \longrightarrow y & \mathbb {S}': & x' \longrightarrow y'\\ & & & z' \end{array} \end{equation*}

Consider the following relation $R$ on $S\oplus S'$ and its descent $R_\times$ :

\begin{align*} R &= \{(\textrm {inl}(x),\textrm {inr}(x')), (\textrm {inl}(y),\textrm {inr}(z')), (\textrm {inr}(y'),\textrm {inr}(z'))\}, \\ R_\times &= \{(x,x'), (y,z')\}. \end{align*}

Then, $R$ is an internal bisimulation on $\mathbb {S}\oplus \mathbb {S}'$ , since the only nontrivial $R$ -closed sets are $\{\textrm {inl}(x), \textrm {inr}(x')\}$ and $\{ \textrm {inl}(y), \textrm {inr}(y'), \textrm {inr}(z')\}$ . However, $R_\times$ is not a $\times$ -bisimulation between $\mathbb {S}$ and $\mathbb {S}'$ , because the pair $(\varnothing, \{y'\})$ is $R$ -closed measurable, but $\tau (x,\varnothing )= 0\neq 1 = \tau '(x',\{y'\})$ .

Note that in this example, the relation $R$ is not an equivalence relation. This raises the following question:

By Proposition 3.23(2), we already know that for bisimulations of the correct type in the sum (which are not equivalence relations), the answer is positive. The question now is whether we still have this property for richer relations. In the particular case of $R={\sim }_{\textsf {s},\mathbb {S}\oplus \mathbb {S}'}$ , by Corollary 3.25, we know that $({\sim }_{\textsf {s},\mathbb {S}\oplus \mathbb {S}'})_\times = ({\sim }_{\textsf {s}})_\times \supseteq {\sim }^\times$ . Therefore, each of the following statements are equivalent to a positive answer to Question 3.33:

1. 1. There is a $\times$ -bisimulation that contains $({\sim }_{\textsf {s}})_\times$ ;

2. 2. $({\sim }_{\textsf {s}})_\times = {\sim ^\times }$ ;

3. 3. $\widehat {({\sim }_{\textsf {s}})_\times }$ is a state bisimulation on $\mathbb {S}\oplus \mathbb {S}'$ .

Corollary 3.63 states a particular case where the equality $({\sim }_{\textsf {s}})_\times = {\sim }^\times$ holds.

We conclude this section with a brief comment on the possibility of defining a processes “generated from a state.” Suppose we have a single LMP $\mathbb {S}$ and two states $s_0,s_1\in S$ such that $s_0\sim _{\textsf {s}} s_1$ . Our motivation lies in obtaining two LMPs $\mathbb {S}_0$ and $\mathbb {S}_1$ such that $s_0\in S_0$ , $s_1\in S_1$ , and $s_0\sim ^\times s_1$ . One trivial way to achieve this, as a consequence of Lemma 3.21, is to duplicate the LMP $\mathbb {S}$ . With this approach, the contexts of those states are exactly the same as before. A less trivial approach is to try to “minimize” the context of a state $s$ by defining an LMP generated by it. If $X_s$ were the base space of such an LMP, we would be interested in ensuring that it satisfies the following properties:

1. 1. $s\in X_s$ ;

2. 2. The probability of each trace starting in $s$ does not decrease in comparison with the original LMP;

3. 3. What remains outside $X_s$ must be irrelevant, that is, $\tau _a(r,S\smallsetminus X_s)=0$ for all $a\in L$ and $r\in X_s$ .

We cannot define $X_s$ as a $\subseteq$ -minimal set for these properties because oftentimes arbitrary points can be removed without modifying probabilities (e.g., when all measures are continuous). Thus, we can use a less strict concept of a sub-LMP, defined as follows: given $B\subseteq S$ which is a thick subset of all the measure spaces $(S,\Sigma, \tau _a(x,\cdot ))$ (cf. (Moroni (Reference Moroni2022), Prop. 4.34)), we define the process $\mathbb {S}\upharpoonright B = (B,\Sigma \upharpoonright B,\{\tau _a\upharpoonright _{B\times \Sigma \upharpoonright B}\mid a\in L\})$ . Thickness ensures that a sub-LMP containing $s$ will include all the relevant probabilistic information. This way, Item 3 above is guaranteed whenever $X_s\mathrel {\mathop :}= B$ is measurable. However, even with this idea, it may happen that $s,t \in S$ are state bisimilar in $\mathbb {S}$ , but they are not related by any external bisimulation between the respective generated LMPs. A case of this will be shown in Example 3.37 in the next section.

3.3.1 Categorical bisimilarity

A span between two objects $X, Y$ in a category $\textbf {C}$ consists of a third object $Z$ and two morphisms $f:Z\to X$ and $g:Z\to Y$ ; we will gather all of its components into a tuple as in $(Z,f,g)$ This serves as a generalization of a binary relation $Z$ , thought of as a diagram $X \xleftarrow {\pi _X} Z \xrightarrow {\pi _Y} Y$ in the category $\textbf {Set}$ (a “jointly monic span”), and it can be used to give a more general categorical definition of bisimulation. Dually, a cospan between $U$ and $V$ consists of an object $W$ and two morphisms with the same codomain $j:U \to W$ and $k:V\to W$ .

This definition is presented in Blute et al. (Reference Blute, Desharnais, Edalat and Panangaden1997), where zigzag morphisms include the surjectivity condition, which we omit in this work.

The following result indicates that the existence of a span allows us to generate an external state bisimulation.

The proof of this proposition generalizes the first part of Lemma 3.28, and if we focus on states, it means that ${\sim }^\wedge \subseteq {\sim }^\times$ . Additionally, it also shows a case where the transitivity (7) holds: $f(w)\sim ^\times w\sim ^\times g(w)\implies f(w)\sim ^\times g(w)$ .

The following example shows that the converse is not true in the following sense: there can be two LMPs in which each state from the first is externally bisimilar to one from the second and vice versa, yet no span exists that preserves that relation.

Example 3.37. We revisit the LMP $\mathbb {U}$ and the modifications of Example 3.30. In the LMPs $\mathbb {U}_s$ and $\mathbb {U}_t\oplus \mathbb {T'}$ , every element of the first is externally bisimilar to one from the second and vice versa. Indeed, the relation $R$ that identifies the states $s$ , $t$ , and $t'$ and also identifies the three copies of each state in $\mathbb {U}_s$ and $\mathbb {U}_t\oplus \mathbb {T'}$ is a bisimulation relation on the sum, as proven in Sánchez Terraf (Reference Sánchez Terraf2011, Exm. 1). Moreover, it is the bisimilarity $\sim _{\textsf {s}, \mathbb {U}_s\oplus (\mathbb {U}_t\oplus \mathbb {T}')}$ , and by Corollary 3.63, its descend to $\mathbb {U}_s \times (\mathbb {U}_t\oplus \mathbb {T'})$ is the external bisimilarity. However, we will prove that there is no span $\mathbb {U}_s \xleftarrow {f} \mathbb {W} \xrightarrow {g} \mathbb {U}_t\oplus \mathbb {T'}$ such that $f(w_0)=s$ and $g(w_0)=t$ for some $w_0$ in $W$ .

Assume, in search of a contradiction, that such a span exists and define $\bar {W}\mathrel {\mathop :}= W\setminus g^{-1}[T']$ and the sub-LMP $\bar {\mathbb {W}}\mathrel {\mathop :}= (\bar {W},\Sigma _W\upharpoonright {\bar {W}}, \{\tau ^W_a\upharpoonright _{\bar {W}\times \Sigma _W\upharpoonright {\bar {W}}}\})$ . We can then restrict the morphisms and consider $f\upharpoonright _{\bar {W}}:\bar {W}\to \mathbb {U}_s$ and $g\upharpoonright _{\bar {W}}\;:\;\bar {W}\to \mathbb {U}_t$ . We will prove that these restrictions are also zigzag morphisms. Their measurability follows from the fact that $\bar {W}$ is measurable. Now, let us verify that $f\upharpoonright _{\bar {W}}$ is zigzag: if $A\subseteq \mathbb {U}_s$ is measurable, and $\bar {w}\in \bar {W}$ , we want to show that $\tau ^W_a(\bar {w},f^{-1}[A]) = \tau ^W_a(\bar {w},(f\upharpoonright _{\bar {W}})^{-1}[A])$ . We write $f^{-1}[A] = (f^{-1}[A]\cap \bar {W})\cup (f^{-1}[A]\cap g^{-1}[T']) = (f\upharpoonright _{\bar {W}})^{-1}[A]\cup (f^{-1}[A]\cap g^{-1}[T'])$ . Since $f^{-1}[A]\cap g^{-1} [T']\subseteq g^{-1}[T']$ and $g(\bar {w})\notin T'$ , we have $\tau ^W_a(\bar {w},f^{-1}[A]\cap g^{-1}[T'])\leq \tau ^W_a(\bar {w},g^{-1}[T']) =\tau _a(g(\bar {w}),T')=0$ . Hence, $\tau _a(f\upharpoonright _{\bar {W}}(\bar {w}),A) =\tau _a(f(\bar {w}),A)= \tau ^W_a(\bar {w},f^{-1}[A]) = \tau ^W_a(\bar {w},(f\upharpoonright _{\bar {W}})^{-1}[A])$ , and this proves that $f\upharpoonright _{\bar {W}}$ is zigzag.

The case for $g\upharpoonright _{\bar {W}}$ is a bit simpler: if $B\subseteq \mathbb {U}_t$ is measurable, then $g^{-1}[B] =(g\upharpoonright _{\bar {W}})^{-1}[B]$ and thus

\begin{equation*}\tau _a(g\upharpoonright _{\bar {W}}(\bar {w}),B) = \tau _a(g(\bar {w}),B) = \tau ^W_a(\bar {w},g^{-1}[B]) = \tau ^W_a(\bar {w},(g\upharpoonright _{\bar {W}})^{-1}[B]),\end{equation*}

proving that this restriction is also zigzag.

We have constructed a span $\mathbb {U}_s \xleftarrow {f\upharpoonright _{\bar {W}}} \mathbb {\bar {W}} \xrightarrow {g\upharpoonright _{\bar {W}}} \mathbb {U}_t$ such that $f\upharpoonright _{\bar {W}}(w_0)=s$ and $g\upharpoonright _{\bar {W}}(w_0)=t$ . However, this is not possible because Proposition 3.36 would imply that $s\sim ^\times t$ , which contradicts what we observed in Example 3.30.

3.3.2 Coalgebraic bisimilarity

A stronger version of $\wedge$ -bisimilarity can be defined by appealing to coalgebraic concepts. LMPs can be presented as coalgebras for the $\textbf {Meas}$ -endofunctor $\Delta ^L$ (a power of the Giry (Reference Giry1981)) defined on objects as the measurable space:

\begin{equation*} \Delta ^L (S,\Sigma ) \mathrel {\mathop :}= (\{ \theta \mid \theta : L \to \Delta (S) \}, \Delta ^L(\Sigma )) \end{equation*}

where $\Delta ^L(\Sigma )$ is the initial $\sigma$ -algebra for the family of maps:

\begin{equation*} \{ \theta \mapsto \theta (a)(E) \mid E\in \Sigma, \; a\in L \}. \end{equation*}

In this setting, an LMP $(S,\Sigma, \{\tau _a \}_a)$ corresponds to the coalgebra structure $\tau : (S,\Sigma ) \to \Delta ^L (S,\Sigma )$ given by $\tau (a)(Q) \mathrel {\mathop :}= \tau _a(Q)$ for $a\in L$ and $Q\in \Sigma$ . Hence, zigzag morphisms correspond mutatis mutandis to those of $\Delta ^L$ -coalgebras.

The definition of bisimulation between coalgebras was introduced by Aczel and Mendler (Reference Aczel, Mendler, Pitt, Rydeheard, Dybjer, Pitts and Poigné1989) and adapted to our context of interest by de Vink and Rutten (Reference de Vink and Rutten1997).

It is clear that ${\sim }^\Delta \subseteq {\sim }^\wedge$ since a coalgebraic bisimulation is a particular case of a span in which a relation has an LMP structure and the projections are zigzag morphisms. Proposition 3.36 showed that ${\sim }^\wedge \subseteq {\sim }^\times$ , and therefore, we have ${\sim }^\Delta \subseteq {\sim }^\wedge \subseteq {\sim }^\times$ (Bacci (Reference Bacci2013, Prop. 5.2.4) gives a direct proof of ${\sim }^\Delta \subseteq {\sim }^\times$ ).

In Bacci et al. (Reference Bacci, Bacci, Larsen and Mardare2014, Thm. 16), it is stated that $\sim ^\times$ and $\sim ^{\Delta }$ are equivalent. To show this, the authors argue that every external bisimulation is also coalgebraic, first describing in Proposition 13 (op.cit.) a technical procedure to construct a measure $\mu \wedge \nu$ on a subset $R$ of product of two measure spaces $(X,\mu )$ and $(Y,\nu )$

As Gburek already observed in 2016 Gburek (Reference Gburek2016), Proposition 13 does not hold in general, but he proves it in the case of $R$ being a countably separated “quasi-equivalence” (a $z$ -transitive relation $R\subseteq X\times Y$ that projects surjectively onto $X$ and $Y$ ) with $X$ and $Y$ Polish.

Next, we offer a counterexample to the Proposition for a quasi-equivalence $R$ when $Y$ is not Polish.

Example 3.39. Recall that $I=(0,1)$ . Consider the measurable space $X=(I, \mathcal {B}(I)_V)$ equipped with $\mu \mathrel {\mathop :}= \mathfrak {m}_0$ , and $Y=(I,\mathcal {B}(I)_V) \oplus (I, \mathcal {B}(I))$ equipped with $\nu \mathrel {\mathop :}= \mathfrak {m}_1$ supported on $I\oplus \varnothing$ . Without loss of generality, assume that $\mathfrak {m}_0(V)\lt \mathfrak {m}_1(V)$ . Let $R\mathrel {\mathop :}= \{(a,\textrm {inl}(a))\mid a\in I\}\cup \{(a,\textrm {inr}(a))\mid a\in I\}$ ( $R$ is the union of the two “diagonals”) and let $\pi _X:R\to X$ and $\pi _Y:R\to Y$ be the canonical projections. Observe that for every $E$ and $F$ in the respective $\sigma$ -algebras, the implication

(8) \begin{equation} \pi _X^{-1}[E] =\pi _Y^{-1}[F] \implies \mu (E)=\nu (F) \end{equation}

holds: if the antecedent is true, the definition of $R$ implies that $F=E\oplus E$ ; in addition, the second summand of $Y$ forces $E$ to be Borel. Bacci et al. (Reference Bacci, Bacci, Larsen and Mardare2014, Prop. 13) states that under (8), there should exist a measure $\mu \wedge \nu$ such that $(\mu \wedge \nu )(\pi _X^{-1}[V]) = \mu (V)$ and $(\mu \wedge \nu )(\pi _Y^{-1}[V\oplus \varnothing ]) = \nu (V\oplus \varnothing )$ . Hence,

\begin{equation*} (\mu \wedge \nu )(\pi _X^{-1}[V])=\mathfrak {m}_0(V)\lt \mathfrak {m}_1(V) = (\mu \wedge \nu )(\pi _Y^{-1}[V\oplus \varnothing ]). \end{equation*}

But $\pi _Y^{-1}[V\oplus \varnothing ] \subseteq \pi _X^{-1}[V]$ , leading to a contradiction.

In any case, Bacci et al. (Reference Bacci, Bacci, Larsen and Mardare2014, Thm. 16) does not hold since Example 3.37 shows $ {\sim }^\times \nsubseteq {\sim }^\Delta$ . Nevertheless, the question about the equivalence between the bisimilarities $\sim ^\Delta$ and $\sim ^\wedge$ remains.

An antecedent to this question can be found in de Vink and Rutten (Reference de Vink and Rutten1997, Thm. 5.8), where it is proven that for LMP in the category of ultrametric spaces with expansive maps, every $\times$ -bisimulation that admits a Borel decomposition is also a $\Delta$ -bisimulation. However, this condition seems to be too restrictive.

Given a span $(\mathbb {T},f,g)$ , we could ask about the possibility of constructing a coalgebraic bisimulation that includes $(f\times g)[T]$ . However, this might be too much to ask for, as the question of whether ${\sim }^\wedge \subseteq {\sim }^\Delta$ does not necessarily imply that the same relation attests $\wedge$ -bisimilarity.

With this in mind, let us consider a very simple particular case where the answer to Question 3.40 is positive. We recall that if $(X,\Sigma _X)$ is a measurable space and $h:X\to Y$ , then $\Sigma _Y=\{B\subseteq Y\mid h^{-1}[B]\in \Sigma _X\}$ is the largest $\sigma$ -algebra on $Y$ that makes $h$ measurable. This is called the final $\sigma$ -algebra with respect to $h$ .

Proof. Since $\textbf {Set}$ has products, the injectivity of the span is equivalent to requiring $f\times g:T\to S\times S'$ to be injective. Thanks to this, $\tau _a$ is well defined. For a fixed $r=(f(t),g(t))$ , $\tau _a(r,\cdot )$ is a subprobability measure. If we fix $Q\in \Sigma _R$ ,

\begin{align*} \tau _a(\cdot, Q)^{-1}[(0,q)] &= \{(f(t),g(t))\in R\mid \tau _a((f(t),g(t)),Q)\lt q\} \\ & = \{(f(t),g(t))\in R\mid \tau _a^{\mathbb {T}}(t,(f\times g)^{-1}[Q])\lt q\} \\ &= (f\times g)[\{t\in T\mid \tau _a^{\mathbb {T}}(t,(f\times g)^{-1}[Q])\lt q\}]. \end{align*}

Given that $f\times g$ is injective, we have $(f\times g)^{-1}[(f\times g)[C]]=C$ for any set $C$ . Hence, by the definition of $\Sigma _R$ , $(f\times g)[\{t\in T\mid \tau _a^{\mathbb {T}}(t,(f\times g)^{-1}[Q])\lt q \}]\in \Sigma _R$ and we conclude that $\tau _a(\cdot, Q)$ is measurable.

This result is quite weak, as a monic span in $\textbf {Set}$ is (isomorphic to) a relation. Thus, the assumptions practically require a coalgebraic bisimulation. However, it does provide some insight when attempting to find a counterexample to Question 3.40: avoid considering injective spans (and therefore neither of the morphisms can be injective).

In Sokolova (Reference Sokolova2005), properties of coalgebraic bisimulation are listed (with proofs in Rutten (Reference Rutten2000)). The functors used there possess a particular property: they preserve weak pullbacks, or weakly preserve pullbacks. The second condition is weaker than the first, but both are equivalent if the category has pullbacks. The pullback of a cospan between two objects is a span between the same objects completing the diagram to form a commutative square, while also satisfying a universal property. The dual concept is that of a pushout. A weak pullback completes the commutative square without uniqueness in the universal property, and a semi-pullback only completes the commutative square. The importance of a functor preserving these constructions in some manner lies in the fact that bisimulations between their coalgebras exhibit good properties (Viglizzo, Reference Viglizzo2005, p.10). At the end of next Section 3.4, we will resume the discussion of the relationship between categorical and coalgebraic bisimilarity, since it also involves the bisimilarity defined in terms of cospans.

3.4.1 Quotients and finality

The converse to Proposition 3.44 also holds, but in order to prove it we need to construct a “quotient” of sorts, we will state most of the auxiliary results about it without proof.

For an LMP $\mathbb {S}=(S,\Sigma, \{\tau _a \}_a)$ and $\Lambda$ a stable sub- $\sigma$ -algebra, consider the projection $\pi : S \to S/\mathcal {R}(\Lambda )$ . We can endow $S/\mathcal {R}(\Lambda )$ with the following $\sigma$ -algebra and kernels:

\begin{equation*} \Lambda /\mathcal {R}(\Lambda )\mathrel {\mathop :}= \{\pi [Q] \mid Q\in \Lambda \}, \qquad \bar {\tau }_a(\pi (s),Q')\mathrel {\mathop :}=\tau _a(s,\pi ^{-1}[Q']), \end{equation*}

where $s\in S$ and $Q' \in \Lambda /\mathcal {R}(\Lambda )$ . These kernels are well defined and then

\begin{equation*} \mathbb {S}/\Lambda \mathrel {\mathop :}= (S/\mathcal {R}(\Lambda ),\Lambda /\mathcal {R}(\Lambda ),\{\bar {\tau }_a \}_a) \end{equation*}

is an LMP and the canonical projection $\pi :\mathbb {S}\to \mathbb {S}/\Lambda$ is upgraded to a zigzag morphism. An antecedent of this construction is Doberkat (Reference Doberkat2005b), where the whole setting is restricted to analytic state spaces and countably generated $\Lambda$ .

It is to be noted that this is not a quotient “over $\textbf {Set}$ ,” but it will be shown to be one “over $\textbf {Meas}$ ,” since it is an instance of the following particular case of (Dubuc and Español (Reference Dubuc and Español2006), Def. 2.9):

For the rest of this section, let $\mathcal {G}$ and $\mathcal {V}$ be the forgetful functors from $\textbf {LMP}$ to $\textbf {Meas}$ and from $\textbf {LMP}$ to $\textbf {Set}$ , respectively. Next, we will briefly discuss $\mathcal {G}$ - and $\mathcal {V}$ -finality of zigzag morphisms.

Proof. Let $g_0:\mathbb {S}\to \mathbb {T}$ be a zigzag morphism and $\phi :\mathcal {G}(\mathbb {S}') \to \mathcal {G}(\mathbb {T})$ a measurable map such that $\mathcal {G}(g_0)=\phi \circ \mathcal {G}(\pi )$ . We complete the diagram in Figure 2 by defining $g:\mathbb {S}' \to \mathbb {T}$ by $g(\pi (s))=g_0(s)$ . To check well-definedness, assume that $\pi (s)=\pi (s')$ , which is the same as $\mathcal {G}(\pi )(s)=\mathcal {G}(\pi )(s')$ . By applying $\phi$ , we have $\mathcal {G}(g_0)(s)=\mathcal {G}(g_0)(s')$ by hypothesis, which is again the same as $g_0(s)=g_0(s')$ . As $g$ and $\phi$ coincide as maps between sets, $g$ is measurable. Let $B\subseteq T$ be measurable, then

\begin{multline*} \tau _a^{\mathbb {T}}(g(\pi (s)),B)= \tau _a^{\mathbb {T}}(g_0(s),B) = \tau _a^{\mathbb {S}}(s,g_0^{-1}[B]) =\\ = \tau _a^{\mathbb {S}}(s,\pi ^{-1}[g^{-1}[B]]) = \tau _a^{\mathbb {S}'}(\pi (s),g^{-1}[B]). \end{multline*}

This proves that $g$ is zigzag. As $\mathcal {G}$ is faithful, $g$ is unique.

Figure 2.

The projection $\pi$ is $(\textbf {LMP}\to \textbf {Meas})$ -final.

This result slightly strengthens the idea proposed in the last paragraph (Danos et al. (Reference Danos, Desharnais, Laviolette and Panangaden2006), Sect. 6), where epi-mono factorizations of zigzag morphisms are discussed. As it is expected, not all epimorphims behave as in other more structured categories:

We will need the following basic result for studying $\mathcal {V}$ -finality:

We immediately obtain:

In particular, if we alter the domain of the projection and view it as a function $\pi :(S,\Lambda, \{\tau _a\}_a) \to \mathbb {S}/\Lambda$ , we will always get a $\mathcal {V}$ -final morphism. A sufficient condition that appears in many contexts for $\mathcal {V}$ -finality (i.e., it implies the second item of Corollary 3.50) is $\Lambda =\Sigma (\mathcal {R}(\Lambda ))$ ; we do not know if it is necessary.

Back to our discussion of bisimilarities, we can show:

Proof. The ( $\Rightarrow$ ) direction is Proposition 3.44. For ( $\Leftarrow$ ), assume $\textrm {inl}(s)$ and $\textrm {inr}(s')$ are event bisimilar in $\mathbb {S}\oplus \mathbb {S}'$ . Let $\Lambda$ be a stable $\sigma$ -algebra on $\mathbb {S}\oplus \mathbb {S}'$ such that $\textrm {inl}(s)\mathrel {\mathcal {R}(\Lambda )}\textrm {inr}(s')$ . Then,

\begin{equation*}\mathbb {S} \xrightarrow {\pi \circ \, \textrm {inl}} (\mathbb {S}\oplus \mathbb {S}')/\Lambda \xleftarrow {\pi \circ \, \textrm {inr}} \mathbb {S}' \end{equation*}

is a cospan of zigzags witnessing $s\sim ^\vee s'$ .

Validity sets of formulas are preserved under sum, so we can conclude that

Since internal bisimilarity implies event bisimilarity, we then have:

3.4.2 From $\vee$ to $\wedge$ and coalgebraic bisimilarity

From Danos et al. (Reference Danos, Desharnais, Laviolette and Panangaden2006), we know that every span of LMP can be completed to a commutative square, and hence ${\sim ^\wedge } \subseteq {\sim ^\vee }$ holds in general. Whenever cospans can be completed to square, we have the reverse inclusion.

The hypothesis does not hold in general as it was shown in Sánchez Terraf (Reference Sánchez Terraf2011, Thm. 12). Nevertheless, a fair amout of research has been directed to the recovery of semi-pullbacks by considering LMP over better behaved spaces. An important antecedent is Edalat (Reference Edalat1999), which deals with LMP over analytic spaces with universally measurable transitions. Recall that Desharnais (Reference Desharnais1999) introduced generalized LMP to take advantage of this result. These are analogous to LMP with an analytic state space, but the functions $\tau _a(\cdot, A)$ are only required to be universally measurable for each $A\in \Sigma$ .

Later, it was proved that the category of LMP over analytic spaces has semi-pullbacks (more precisely, for the category of stochastic relations over analytic spaces), and furthermore, the upper vertex of the required span can be chosen to be Polish (Doberkat (Reference Doberkat2005a), Thm. 5.2).

The most recent results in this direction ensure the existence of semi-pullbacks for LMP over separable metrizable spaces where $\tau _a(s,\cdot )$ is a Radon measure for each $s$ and $a$ (Pachl and Sánchez Terraf (Reference Pachl and Sánchez Terraf2021), Thm. 5.1) and, in particular, for LMP over universally measurable separable spaces (Pachl and Sánchez Terraf (Reference Pachl and Sánchez Terraf2021), Thm. 5.3).

It can be checked from the proofs in Pachl and Sánchez Terraf (Reference Pachl and Sánchez Terraf2021) that the semi-pullbacks constructed in each case turn out to be pullbacks in $\textbf {Set}$ and therefore they are relations. We conclude:

3.5.1 From $\oplus$ -bisimilarity to events

In Panangaden (Reference Panangaden2009, Def. 7.2), a different definition of $\oplus$ -bisimulation is presented. In this variation, the equivalence relation is not required to be within the sum $S \oplus S'$ , but rather within a possibly larger process of which $\mathbb {S}$ and $\mathbb {S}'$ are direct summands. To provide clarity, we have rephrased this definition to explicitly specify the necessary inclusions.

In what follows we will show that this notion is the same as external event bisimilarity, that is, $\sim ^\vee$ .

The second equality can also be seen immediately since the Zhou filtration is monotone increasing from $\sigma ({[\![ \mathcal {L} ]\!]})$ to $\Sigma$ (Moroni and Sánchez Terraf (Reference Moroni and Sánchez Terraf2023), Figure 2). The same analysis shows that there are other $\sigma$ -algebras with this property.

Notice that in the case of event bisimilarity, the converse implication is also true.