For d, e ∈ S × S → [0, 1], we define d e if for all s, t ∈ S, d(s, t) ≤ e(s, t). According to, for example, [22, Lemma 3.2], S × S → [0, 1], is a complete lattice. Since the function Δ is a monotone function from a complete lattice to itself, we can conclude from the Knaster-Tarski fixed point theorem (see, for example, [13, Theorem 2.35]) that Δ has a least fixed point. We denote this least fixed point by δ. This least fixed point maps each pair of states to a real number in the interval [0, 1]: the probabilistic bisimilarity distance of the states. Distance zero captures probabilistic bisimilarity.

Theorem 6 ([21, Theorem 4.10]). For all s, t ∈ S, δ(s, t)=0 if and only if s ∼ t.

The probabilistic bisimilarity distance function δ is the limit of the distance functions δn which only consider the first n transitions when comparing the similarity of the behaviour of states. This result can be seen as an instance of the Kleene fixed point theorem [34].

Definition 7. For each n ≥ 0, the function δn : S × S → [0, 1] is defined by

$$\delta\_n(s,t) = \begin{cases} 0 & \text{if } n=0\\ \Delta(\delta\_{n-1})(s,t) & \text{otherwise.} \end{cases}$$

Proposition 8. limn→∞ δn = δ.

## 3 A Logical Characterization

Below, we present a logical characterization of the probabilistic bisimilarity distances. We start with a logic very similar to the one introduced by Desharnais et al. [20].

Definition 9. *The logic* L¬ *is defined by*

$$\varphi ::= a \mid \bigcirc \varphi \mid \neg \varphi \mid \varphi \ominus q \mid \varphi \vee \varphi$$

*where* a ∈ L *and* q ∈ Q ∩ [0, 1]*.*

The above logic is slightly different from the one presented in [20] as we consider Markov chains with labelled states, whereas Desharnais et al. studied Markov chains with labelled transitions. In particular, a and ϕ were combined as aϕ. Since we restrict our attention to finite state systems, we can restrict ourselves to finite disjunctions. In our setting, the constants true and false can be expressed as - a∈L a (recall that we assume that the set L is finite as well) and ¬true, respectively. The logic of Desharnais et al. also contains the operator ϕ q which is redundant, as observed in [21, page 336]. The logic considered by Desharnais [18] lacks negation, but does include ϕ q and conjunction. The real-valued interpretation of the logic of Desharnais et al., which considers labelled transitions, is adjusted to our setting of labelled states as follows.

Definition 10. *The function* -· : L¬ → S → [0, 1] *is defined by*

$$\begin{aligned} [a](s) &= \begin{cases} 1 & \text{if } \ell(s) = a \\ 0 & \text{otherwise} \end{cases} \\ [\bigcirc \varphi](s) &= [\varphi] \cdot \tau(s) \\ [\neg \varphi](s) &= 1 - [\varphi](s) \\ [\varphi \ominus q](s) &= \max([\varphi](s) - q, 0) \\ [\varphi \vee \psi](s) &= \max([\varphi](s), [\psi](s)) \end{aligned}$$

Note that false and true are the constant zero and constant one functions, respectively. The probabilistic bisimilarity distances can be characterized in terms of the logic.

Theorem 11 ([5, Theorem 40 and 44]). *For all* s*,* t ∈ S*,*

$$\delta(s, t) = \sup\_{\varphi \in \mathcal{L}\_{\neg}} \|\varphi\|(s) - \|\varphi\|(t).$$

In the remainder of this paper, we consider the following logic. This logic also characterizes probabilistic bisimilarity distances. As we will show later, this logic can explain the probabilistic bisimilarity distances more concisely than the logic presented above.

Definition 12. *The logic* L *is defined by*

$$\varphi ::= a \mid \bigcirc \varphi \mid \varphi \ominus q \mid \varphi \oplus q \mid \varphi \vee \varphi \mid \varphi \wedge \varphi \mid$$

*where* a ∈ L *and* q ∈ Q ∩ [0, 1]*.*

Note that negation has been removed and conjunction has been added. Also the operator ⊕q, which is dual to q, has been added. This logic is very similar to the one considered by Desharnais [18].

292 A. Rady and F. van Breugel

Definition 13. The function -· : L → S → [0, 1] of Definition 10 is modified by

$$\begin{array}{l} \left[\varphi \oplus q\right](s) = \min\{\left[\varphi\right](s) + q, 1\} \\ \left[\varphi \wedge \psi\right](s) = \min\{\left[\varphi\right](s), \left[\psi\right](s)\} \end{array}$$

As already mentioned above, also this logic characterizes the probabilistic bisimilarity distances.

Theorem 14. For all s, t ∈ S, δ(s, t) = supϕ∈L ϕ(s) − ϕ(t).

Proof sketch. Each formula of L can be rewritten to an equivalent formula of L¬. For example, if ϕ is rewritten to ψ then ϕ ⊕ q is rewritten to ¬(¬ψ q). Each formula of L has a dual: if ϕ= 1 − ψ then ϕ is a dual of ψ. For example, if ϕ is a dual of ψ then ϕ q is a dual of ψ ⊕ q. Each formula L¬ can be rewritten to an equivalent formula of L. For example, if ϕ is rewritten to ψ then ¬ϕ is rewritten to a dual of ψ. The result now follows from Theorem 11.

## 4 All Operators are Necessary

The logic L is a minimal logic that characterizes the probabilistic bisimilarity distances. That is, if we remove any operator from the logic then the resulting logic does not characterizes the probabilistic bisimilarity distances anymore. Due to lack of space, we only consider the logic L\, which does not have the q operator.

Definition 15. The logic L\ is defined by

$$\varphi ::= a \mid \bigcirc \varphi \mid \varphi \oplus q \mid \varphi \vee \varphi \mid \varphi \wedge \varphi \mid$$

where a ∈ L and q ∈ Q ∩ [0, 1].

Theorem 16. There exists a labelled Markov chain S, L, τ, and s, t ∈ S such that

$$\delta(s, t) > \sup\_{\varphi \in \mathcal{L}\_{\backslash \ominus}} \left[ \varphi \right](s) - \left[ \varphi \right](t).$$

Proof sketch. Consider the following labelled Markov chain.

It can be shown that δ(s, t) = 7 8 . Furthermore, we can prove that for all ϕ ∈ L\ and q ∈ Q ∩ [0, 1], if ϕ(u) < 1 8 − q 2 then ϕ(v) < 3 4 − q by structural induction on ϕ. Using this result and Theorem 14, we can also show that for all ϕ ∈ L\, ϕ(s) − ϕ(t) ≤ 27 32 by structural induction on ϕ.

## 5 Explainability

In general, the probabilistic bisimilarity distance of two states cannot be explained by a single formula, as we will show next. That is, generally there does not exist a distinguishing formula for every pair of states of a labelled Markov chain. But, as we will prove below, for every pair of states there exists a sequence of formulas that explains their distance.

Theorem 17. *There exists a labelled Markov chain* -S, L, τ, *and* s*,* t ∈ S *such that for all* ϕ ∈ L*,* δ(s, t) > ϕ(s) − ϕ(t)*.*

*Proof sketch.* Consider the following labelled Markov chain.

It can be shown that δ(s, t)=1. We can also prove that for all ϕ ∈ L, ϕ(s) − ϕ(t) < 1 by structural induction on ϕ.

As we will show next, for every pair of states (s, t) there exists a sequence of formulas (ξn)n such that δ(s, t) = limn→∞ ξn(s)−ξn(t). This sequence (ξn)n explains the distance δ(s, t).

Proposition 18. *For all* s*,* t ∈ S *there exists* (ξn)n *such that*

$$\delta(s, t) = \lim\_{n \to \infty} \left[ \xi\_n \right](s) - \left[ \xi\_n \right](t).$$

*Proof sketch.* This can be concluded from Theorem 14 and the following. Let X be a nonempty subset of R that is bounded above. Then there exists a sequence (xn)n in X that converges to sup X [8, page 4].

The proof of the above proposition is *not* constructive. Below, we will construct a sequence of formulas (ϕn st)n that explains the distance of the states s and t. In particular, ϕn st is constructed so that

$$\|\varphi\_{st}^{n}\|(s) = \delta\_{n}(s,t) \text{ and } \|\varphi\_{st}^{n}\|(t) = 0.$$

and, hence, ϕn st(s) − ϕn st(t) = δn(s, t). That is, the formula ϕn st explains the distance δn(s, t).

If n = 0 then δn(s, t)=0. We choose the formula false since

$$\text{[false]}(s) = 0 = \delta\_0(s, t) \text{ and } \text{[false]}(t) = 0.1$$

Let n > 0. For (s, t) ∈ S2 0 , also δn(s, t)=0. Again we choose the formula false to explain the distance. For (s, t) ∈ S2 1 , we have that δn(s, t)=1. In this case the formula (s) explains δn(s, t) since (s) = (t) and, therefore,

$$\left[\mathbb{I}(s)\right](s) = 1 = \delta\_n(s, t) \text{ and } \left[\mathbb{I}(s)\right](t) = 0.$$

#### 294 A. Rady and F. van Breugel

To construct a formula that explains distance δn(s, t) for (s, t) ∈ S2 ? , we rely on the following result about distances and nonexpansive functions. A function f ∈ S → [0, 1] is *nonexpansive* if for all s, t ∈ S, |f(s) − f(t)| ≤ δn(s, t). The set of nonexpansive functions is denoted by (S, δn) ------- [0, 1]. This set forms a convex polytope and is known as the *Lipschitz polytope*. We denote its *vertices* by V ((S, δn) -------[0, 1]).

Proposition 19. *For all* (s, t) ∈ S2 ? *and* n ≥ 0*, there exists* f n st ∈ (S, δn) *------*- (Q ∩ [0, 1]) *such that* δn+1(s, t) = f n st · (τ (s) − τ (t))*.*

*Proof sketch.* Let (s, t) ∈ S2 ? and n ≥ 0. Then

$$\delta\_{n+1}(s,t) = \inf\_{\omega \in \Omega\_{\mathbb{R}}(\tau(s), \tau(t))} \omega \cdot \delta\_n \dots$$

We can view δn+1(s, t) as the minimal cost of a transportation problem, where τ (s)(u) represents the amount transported from the origin u, τ (t)(v) captures the amount received at the destination v, δn(u, v) represents the transportation cost from u to v, and each ω captures a transportation plan, that is, ω(u, v) is the amount transported from u to v (see, for example, [40, page 15]).

From the Kantorovich-Rubinstein duality theorem [31] we can conclude that

$$\inf\_{\omega \in \Omega\_{\mathbb{R}}(\tau(s), \tau(t))} \omega \cdot \delta\_n = \sup\_{f \in (S, \delta\_n) \xrightarrow{} [0, 1]} f \cdot (\tau(s) - \tau(t)).$$

In this dual to the above transportation problem, each f represents a price function (see, for example, [40, page 81]). Since a linear function on a convex polytope attains its maximum at a vertex (see, for example, [49, Theorem 2 of Chapter 1]), we can conclude that

$$\sup\_{f \in (S, \delta\_n) \twoheadrightarrow [0, 1]} f \cdot (\tau(s) - \tau(t)) = \max\_{f \in V((S, \delta\_n) \twoheadrightarrow [0, 1])} f \cdot (\tau(s) - \tau(t)).$$

Since we can prove that V ((S, δn)------- [0, 1]) ⊆ (S, δn)------- (Q ∩ [0, 1]), there exists f n st ∈ (S, δn) ------- (Q ∩ [0, 1]) such that δn+1(s, t) = f n st · (τ (s) − τ (t)).

The function f n st plays a key role in the formula explaining δn(s, t). However, f n st is not necessarily unique. Consider the following labelled Markov chain.

For this example, the sequence (δn)n converges in three steps, that is, δ = δ3. We have that δ2(u, v) = 1 2 and δ3(s, t) = 1 2 . So we need the function f 2 st to

satisfy δ3(s, t) = f 2 st(u) − f 2 st(v) and |f 2 st(u) − f 2 st(v)| ≤ 1 2 . For each 0 ≤ q ≤ 1 2 , f 2 st(u) = 1 2 + q and f 2 st(v) = q satisfies these properties. As we will see, any f n st that satisfies these properties can be used to construct ϕn st. How to compute these functions f n st is the topic of the next section.

As we will show in Theorem 22, we can construct a formula ψn st that captures the function f n st, that is, ψn st = f n st. More about this soon. By means of ψn−1 st we can explain the distance δn(s, t) by the formula (ψn−1 st )(f n−1 st · τ (t)) since we have that

$$\begin{aligned} \left[ \left( \bigcirc \psi\_{st}^{n-1} \right) \odot \left( f\_{st}^{n-1} \cdot \tau(t) \right) \right](s) &= \max \{ \left( \bigcirc\_{st}^{n-1} \right) \cdot \tau(s) \big) - \left( f\_{st}^{n-1} \cdot \tau(t) \right), 0 \} \\ &= \max \{ \left( f\_{st}^{n-1} \cdot \tau(s) \right) - \left( f\_{st}^{n-1} \cdot \tau(t) \right), 0 \} \\ &= \max \{ f\_{st}^{n-1} \cdot \left( \tau(s) - \tau(t) \right), 0 \} \\ &= \max \{ \delta\_n(s, t), 0 \} \\ &= \delta\_n(s, t) \end{aligned}$$

and, similarly, we can deduce that

$$\left\| \left( \bigcirc \psi\_{st}^{n-1} \right) \odot \left( f\_{st}^{n-1} \cdot \tau(t) \right) \right\|(t) = \max \{ f\_{st}^{n-1} \cdot (\tau(t) - \tau(t)), 0 \} = 0.$$

Let us return to the formula ψn st that captures the function f n st. To construct ψn st we use the following result.

Lemma 20 ([2, Lemma A7.2]). *Let* f ∈ S → [0, 1]*. If for all* u*,* v ∈ S*, there exists* guv ∈ S → [0, 1] *such that* guv(u) = f(u) *and* guv(v) = f(v)*, then*

$$f = \min\_{u \in S} \max\_{v \in S} g\_{uv} = \max\_{u \in S} \min\_{v \in S} g\_{uv}.$$

To apply the above lemma, we need to construct for all u, v ∈ S a formula ψn stuv such that

$$\|\psi\_{stuv}^n\|(u) = f\_{st}^n(u) \text{ and } \|\psi\_{stuv}^n\|(v) = f\_{st}^n(v).$$

The details are provided in Definition 21 and Theorem 22. From Lemma 20 we can then conclude that

$$\left[\bigwedge\_{u \in S} \bigvee\_{v \in S} \psi\_{stuv}^n \right] = \left[\bigvee\_{u \in S} \bigwedge\_{v \in S} \psi\_{stuv}^n \right] = f\_{st}^n.$$

The above can be summarized as follows.

Definition 21. *For all* s*,* t ∈ S*,*

$$
\varphi\_{st}^{0} = \text{false}
$$

*and*

$$
\varphi\_{st}^1 = \begin{cases}
\text{false} \; if \; (s,t) \in S\_0^2 \cup S\_?^2 \\
\ell(s) \; if \; (s,t) \in S\_1^2
\end{cases}
$$

296 A. Rady and F. van Breugel

*For all* s*,* t ∈ S *and* n ≥ 2*,*

$$
\varphi\_{st}^{n} = \begin{cases}
\text{false} & \text{if } (s,t) \in S\_0^2 \\
\ell(s) & \text{if } (s,t) \in S\_1^2 \\
\left(\bigcirc \psi\_{st}^{n-1}\right) \ominus \left(f\_{st}^{n-1} \cdot \tau(t)\right) \operatorname{if}\left(s,t\right) \in S\_2^2
\end{cases}
$$

*For all* (s, t) ∈ S2 ? *and* n ≥ 1*,*

$$
\psi\_{st}^n = \bigwedge\_{u \in S} \bigvee\_{v \in S} \psi\_{stuv}^n
$$

*For all* (s, t) ∈ S2 ? *,* u*,* v ∈ S*, and* n ≥ 1*,*

$$
\psi\_{stuv}^{n} = \begin{cases}
\text{false} \ominus f\_{st}^{n}(u) & \text{if } f\_{st}^{n}(u) = f\_{st}^{n}(v) \\
\left(\varphi\_{uv}^{n} \ominus \left(\delta\_{n}(u,v) - \left(f\_{st}^{n}(u) - f\_{st}^{n}(v)\right)\right) \ominus f\_{st}^{n}(v)\right) \text{if } f\_{st}^{n}(u) > f\_{st}^{n}(v) \\
\left(\varphi\_{vu}^{n} \ominus \left(\delta\_{n}(u,v) - \left(f\_{st}^{n}(v) - f\_{st}^{n}(u)\right)\right) \ominus f\_{st}^{n}(u)\right) \text{otherwise}.
\end{cases}
$$

Note that, for (s, t) ∈ S2 ? and n ≥ 2, the formula ϕn st contains |S| 2 subformulas of the form ϕn−1 uv . As a consequence, the size of ϕn st grows exponentially in n. As we will see in Section 7, we can compute ϕn st in polynomial time by sharing subformulas.

The above definition shows some similarities with the sequence of formulas introduced in [43, Definition 8]. Their setting is different: the transitions are labelled (as in [20]), the transition function is deterministic, and the labelling of the transitions is probabilistic. Their logic is simpler than the one introduced in [20] since the systems they consider are simpler. The sequence of formulas that they introduce is syntactically simpler than the one we define above. Their formulas are only used to prove a logical characterization, although those formulas can also be used for explainability.

Consider the states s and t of the following labelled Markov chain.

By definition, ϕ0 st = false and ϕ1 st = false. For ϕ2 st we get

$$\left( \left( \bigvee \left( \left( \text{false} \oplus 0 \right) \vee \left( \text{false} \oplus 0 \right) \vee \dots \vee \left( \text{false} \oplus 0 \right) \right) \right) \land \right)$$

$$\left( \left( \text{false} \oplus 0 \right) \vee \left( \text{false} \oplus 0 \right) \vee \dots \vee \left( \text{false} \oplus 0 \right) \right) \land \right\ \begin{cases} \text{false} \oplus \left( \text{false} \oplus 0 \right) \vee \dots \vee \left( \text{false} \oplus 0 \right) \lor \left( \text{false} \oplus 0 \right) \\ \vdots \\ \left( \left( \text{false} \oplus 0 \right) \vee \left( \text{false} \oplus 0 \right) \vee \dots \vee \left( \text{false} \oplus 0 \right) \right) \mid \end{cases} \right) \text{ten} \text{ times}$$

This formula can be simplified to false. In the logic of Desharnais et al., which lacks ∧ and ⊕, one would need 111 additional ¬, making it less concise.

The formula ϕ3 st fills more than a page, but can be simplified to the formula (( ∧ )) 0.375. Although generally there does not exist a distinguishing formula for each pair of states (Theorem 17), in this case the formula ϕ3 st explains the distance of states s and t, since δ(s, t)=0.125, - ϕ3 st (s)=0.125 and - ϕ3 st (t)=0. The formula captures the probability of reaching a green state in one transition and subsequently reaching another green state.

The formula ϕ3 ts can be simplified to (( ∧ )) 0.5. Since we have that - ϕ3 ts (t)=0.125 and - ϕ3 ts (s)=0, the formula ϕ3 ts explains the distance δ(t, s)=0.125. The formula represents the probability of reaching a green state in one transition and subsequently reaching a purple state.

The outermost test can be removed from the explanation. Hence, the formulas ( ∧ ) and ( ∧ ) explain the distance of states s and t as well.

#### Theorem 22.

*Proof sketch.* This theorem can be proved by induction on n. Most steps of the proof have already been discussed above. To prove (c), let (s, t) ∈ S2 ? , u, v ∈ S and n ≥ 1. We need to distinguish three cases. Here we only consider the case that f n st(u) > f n st(v). Then

ψn stuv(u) = (ϕn uv (δn(u, v) − (f n st(u) − f n st(v)))) ⊕ f n st(v)(u) = min{max{ϕn uv(u) − (δn(u, v) − (f n st(u) − f n st(v))), 0} + f n st(v), 1} = min{max{δn(u, v) − (δn(u, v) − (f n st(u) − f n st(v))), 0} + f n st(v), 1} [induction hypothesis of (a)] = min{max{f n st(u) − f n st(v)), 0} + f n st(v), 1} = min{(f n st(u) − f n st(v)) + f n st(v), 1} [f n st(u) > f n st(v)] = min{f n st(u), 1} = f n st(u) ψn stuv(v) = (ϕn uv (δn(u, v) − (f n st(u) − f n st(v)))) ⊕ f n st(v)(v) = min{max{ϕn uv(v) − (δn(u, v) − (f n st(u) − f n st(v))), 0} + f n st(v), 1} = min{max{0 − (δn(u, v) − (f n st(u) − f n st(v))), 0} + f n st(v), 1} [induction hypothesis of (a)] = min{0 + f n st(v), 1} [f n st(u) − f n st(v) ≤ δn(u, v) since f n st is nonexpansive] = f n st(v)

Combining Proposition 8 and Theorem 22, we obtain the following explainability result.

Corollary 23. *For all* s*,* t ∈ S*,* limn→∞ ϕn st(s) − ϕn st(t) = δ(s, t)*.*

#### 6 Computing *f n st*

Proposition 19 states that the functions f n st exist. Below, we will show that these functions can be computed in polynomial time.

Let (s, t) ∈ S2 ? . The function f 0 st ∈ S ------- (Q ∩ [0, 1]) is defined as the constant zero function satisfies δ1(s, t) = f 0 st · (τ (s) − τ (t)) and can be computed in polynomial time. To prove that the remaining functions f n st, with n ≥ 1, can be computed in polynomial time as well, we use the primal network simplex algorithm to solve minimum-cost flow problems due to Orlin [42] and the ellipsoid method to solve linear programming problems due to Khachiyan [32]. As we will show below, f n st can be computed as FindVertex(δn, τ (s), τ (t)).

1 FindVertex(d, μ, ν)

$$\mu\_2 \qquad input : d \in \dot{S} \times S \stackrel{\circ}{\to} (\mathbb{Q} \cap [0, 1]) \text{ with } d(s, s) = 0 \text{ for all } s \in S, \quad \mu, \nu \in \mathcal{D}\_{\mathbb{Q}}(S)$$

$$f\_{\mathbb{R}} \quad f\_{\mu\nu} = \text{ vertex} \quad \text{of} \quad \{ f \in (S, d) \twoheadrightarrow [0, 1] \mid f \cdot (\mu - \nu) = d\_{\mu\nu} \} $$

6 return fμν

In line 4 we use Orlin's primal network simplex algorithm to compute the minimum cost for the following network (N,E). The nodes of the network consist of two copies of each u ∈ S, denoted u0 and u1. The supply of node u0 is μ(u) and the demand of node u1 is ν(u). Each edge (u0, v1) has cost d(u, v).

Each ω ∈ ΩR(μ, ν) corresponds to a feasible flow, where ω(u, v) captures the flow from u0 to v1. The constraints ω(u, S) = μ(u) and ω(S, u) = ν(u), defining ΩR(μ, ν), capture that the supply of u0 flows from u0 and the demand of u1 flows to u1. For a feasible flow ω, its cost is ω · d. Hence, dμν captures the minimum cost.

Note that, by definition, the supplies and demands are rational. We can prove that dμν = ω·d for some ω ∈ ΩQ(μ, ν). Since d is rational as well, we can conclude that dμν is also rational. Orlin's primal network simplex algorithm can compute the minimum cost and, hence, can be used to compute dμν. Orlin's algorithm is strongly polynomial: O(|N| 2|E| 2 log |N|). Since there are 2|S| nodes and |S| 2 edges, dμν can be computed in O(|S| 6 log |S|).

In line 5 we use Khachiyan's ellipsoid method to find a feasible solution of a linear programming problem with the variables xs, for s ∈ S, and the constraints

$$\begin{aligned} \forall s, t \in S: x\_s - x\_t &\le d(s, t) \\ \forall s \in S: x\_s &\ge 0 \\ \forall s \in S: x\_s &\le 1 \\ \sum\_{s \in S} x\_s \left( \mu(s) - \nu(s) \right) &= d\_{\mu \nu} \end{aligned}$$

By means of the ellipsoid method we can find a vertex of the convex polytope defined by the above constraints. This method is polynomial in the size of the constraints, in this case, the size of d, μ, ν, and dμν.

Let n ≥ 1 and (s, t) ∈ S2 ? . Since we can show that δn is rational and δn(s, s)=0 for all s ∈ S, we can apply FindVertex to δn, τ (s) and τ (t). In this case, line 4 computes infω∈ΩR(τ(s),τ(t)) ω · δn, which equals δn+1(s, t). As a consequence, FindVertex(δn, τ (s), τ (t)) returns f n st : (S, δn)-------(Q∩[0, 1]) such that f n st · (τ (s) − τ (t)) = δn+1(s, t).

As we already observed above, line 4 can be computed in polynomial time in the size of the labelled Markov chain and line 5 can be computed in polynomial time in the size of δn, τ (s), τ (t), and δn+1(s, t), which we can show to be polynomial time in the size of the labelled Markov chain and n. Hence, the running time of FindVertex(δn, τ (s), τ (t)) is polynomial in the size of the labelled Markov chain and n.

## 7 The Algorithm

Given a labelled Markov chain S, L, τ, and N ∈ N, we can explain the distances δ(s, t) for s, t ∈ S by computing the formulas ϕn st for 0 ≤ n ≤ N. To obtain this sequence of formulas, we implement Definition 21 as follows. Below, for s, t, u ∈ S, we use the array cells distance[s][t], function[s][t][u], and formula[s][t][n] to represent the distance δn−1(s, t), the function value f n−1 st (u), and the formula ϕn st, respectively. In line 5-17, we compute δ0, f 0 st, ϕ0 st, and ϕ1 st. The loop of line 20–50, first computes the distances δn (line 21–27), then determines the function f n st (line 30), and finally computes formulas ϕn+1 st (line 31–49).

$$\mathbb{P}\_2 \qquad input : \tau \in S \underset{\square}{\to} \mathcal{D}\_{\mathbb{Q}}(S), \ell \in S \to L, N \ge 1$$

3 output : (ϕn st) N n=0 for all s, t ∈ S

1 ExplainDistances(τ, , N):

```
4 ∼ = DecideProbabilisticBisimilarity(τ, ) for s ∈ S and t ∈ S
5 formula[s][t][0] = false
6 distance[s][t]=0
7 if s ∼ t
8 for 1 ≤ n ≤ N
9 formula[s][t][N] = false
10 else if (s) = (t)
11 for 1 ≤ n ≤ N
12 formula[s][t][N] = (s)
13 else
14 formula[s][t][1] = false
15 for u ∈ S
16 function[s][t][u]=0
17
18 n = 1
19 while n<N
20 for s ∈ S and t ∈ S
21 if (s) = (t)
22 distance[s][t]=1
23 if s ∼ t ∧ (s) = (t)
24 distance[s][t]=0
25 for u ∈ S
26 distance[s][t] += function[s][t][u] ∗ (τ (s)(u) − τ (t)(u))
27 for s ∈ S and t ∈ S
28 if s ∼ t ∧ (s) = (t)
29 function[s][t] = FindVertex(distance, τ (s), τ (t))
30 disjunction = false
31 for u ∈ S
32 conjunction = true
33 for v ∈ S
34 if function[s][t][u] = function[s][t][v]
35 subformula = false ⊕ function[s][t][u]
36 else
37 minusShift = distance[u][v] − |function[s][t][u] − function[s][t][v]|
38 plusShift = min {function[s][t][u], function[s][t][v]}
39 if function[s][t][u] > function[s][t][v]
40 subformula = (formula[u][v][n] 	 minusShift) ⊕ plusShift
41 else
42 subformula = (formula[v][u][n] 	 minusShift) ⊕ plusShift
43 disjunction ∨= subformula
44 conjunction ∧= disjunction
45 shift = 0;
46 for u ∈ S
47 shift += function[s][t][u] ∗ τ (t)(u)
48 formula[s][t][n + 1]=( disjunction) 	 shift
49 n = n + 1
```
Let us first discuss the correctness of the above algorithm. In line 4, ∼ is computed by deciding probabilistic bisimilarity. The loop spanning line 20–50 has the following invariant.

$$\forall s, t \in S: \text{distance}[s][t] = \delta\_{n-1}(s, t) \tag{1}$$

$$\forall (s, t) \in S\_?^2: \forall u \in S: \text{function}[s][t][u] = f\_{st}^{n-1}(u) \tag{2}$$

$$\forall s, t \in S: \forall 0 \le i \le n: \text{formula}[s][t][i] = \varphi\_{st}^i \tag{3}$$

Let us check that the above loop invariant holds when we reach line 21 for the first time. In line 7 we set distance to zero. Hence, (1) is satisfied when we reach line 21. In line 17 we set function to zero. Hence, (2) is also satisfied when we reach line 21. In line 6, 10, 13, and 15 we set formula such that (3) is satisfied when we reach line 21.

Next, we check that the loop maintains the above invariant, that is, if the invariant holds at line 21 then it also holds at line 50. Assume that the invariant holds at line 21. From (2) and line 22–27 we can conclude that

$$\text{distance}[s][t] = \begin{cases} 0 & \text{if } (s,t) \in S\_0^2\\ 1 & \text{if } (s,t) \in S\_1^2\\ f\_{st}^{n-1} \cdot (\tau(s) - \tau(t)) \text{ otherwise} \end{cases}$$

once we arrive at line 28. Hence, from Proposition 19 we can conclude that distance[s][t] = δn(s, t) for all s, t ∈ S. Therefore, (1) holds at line 50.

Since distance = δn at line 30 and, as we have seen in Section 6, FindVertex(δn, τ (s), τ (t)) returns f n st, we assign f n st to function[s][t] in line 30. Hence, (2) holds at line 50. We can also verify that line 31–49 ensure that (3) is maintained by the loop.

Finally, we will argue that the running time of the above algorithm is polynomial in the size of the labelled Markov chain and N. Probabilistic bisimilarity can be decided in polynomial time as was first shown by Baier [3]. More efficient algorithms have been proposed by Buchholz [7], Derisavi, Hermanns, and Sanders [17] and Valmari and Franceschinis [50]. Hence, line 4 is polynomial time.

Each line of 6–17 can be implemented in constant time. Since each line of this part is executed at most N|S| 3 times, the running time of line 5–17 is polynomial in the size of the labelled Markov chain and N.

The loop consisting of line 20–50 is executed N − 1 times. As we already discussed in Section 6, the running time of FindVertex(δn, τ (s), τ (t)) is polynomial in the size of the labelled Markov chain and n. When we arrive at line 30, distance equals δn and, hence, this line is polynomial in the size of the labelled Markov chain and n. All other lines of the loop can be implemented in constant time. Each line is executed at most |S| 4 times. Therefore, the running time of line 20–50 is polynomial in the size of the labelled Markov chain and N.

## 8 Conclusion

In this paper, we study a minor variation of the logic introduced by Desharnais et al. in [20]. In particular, we show that

As pointed out by Hillerström in [30], an early paper on computing distinguishing formulas, to explain why states are not bisimilar "arguments must be concise in the sense that an argument must not contain redundant or irrelevant information." This applies to our setting as well. The distinguishing formulas introduced in Definition 21 are in many cases far from concise. We leave the simplification of these formulas for future research.

One may wonder whether adding fixed points to the logic, in the form variables X and either operators μX and νX or equations of the form X = ϕ, would allow us to explain the probabilistic bisimilarity distance of two states by means of a single formula. A logic similar to the one studied in this paper that contains fixed points has been studied by De Alfaro et al. [1]. Whether simply adding fixed points to the logic suffices is not immediately clear as the pn and ⊕qn in the formula ψn uvst vary as n varies. Extending the logic so that the probabilistic bisimilarity distance of two states can be explained by means of a single formula is another potential topic for future research.

Graf and Sifakis [28] introduce the notion of a characteristic formula for a state s: a state satisfies this formula if and only if it is behaviourally equivalent to s. Characteristic formulas have been developed for probabilistic bisimilarity. For example, Deng and van Glabbeek [16] present characteristic formulas for probabilistic automata. Sack and Zhang [47] introduce a general framework to construct characteristic formulas for probabilistic automata. In the setting of probabilistic bisimilarity distances, a characteristic formula for a state s of a labelled Markov chain can be formalized in the following ways. The formula ϕs is a characteristic formula for the state s if

$$\text{for all states } t, \ \lceil \varphi\_s \rceil (s) - \lceil \varphi\_s \rceil (t) = \delta (s, t) \tag{4}$$

or

$$\text{for all states } t, \ \lceil \varphi\_s \rceil (t) = \delta(s, t). \tag{5}$$

It can be shown that (4) and (5) are equivalent: if there exists a formula that satisfies (4) then there also exists a (different) formula that satisfies (5). Whether such a formula or a sequence of such formulas exists for the logic studied in this paper is an open question that may be tackled in future research.

A preliminary implementation of the algorithm in Java is available [45]. Improving the code is another avenue for further research.

Acknowledgements The authors thank the referees for their very detailed and constructive feedback. The second author thanks the Department of Computer Science of the University of Oxford for hosting him for his sabbatical during which part of this research was carried out.

## References

and Viktor Kuncak, editors, *Proceedings of the 29th International Conference on Computer Aided Verification*, volume 10427 of *Lecture Notes in Computer Science*,

Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

## **Weighted and Branching Bisimilarities from Generalized Open Maps**

J´er´emy Dubut1() and Thorsten Wißmann2,3 ‹

1 National Institute of Advanced Industrial Science and Technology, Tokyo, Japan

<EMAIL_ADDRESS>
2 Radboud University, Nijmegen, the Netherlands

<EMAIL_ADDRESS>
3 Friedrich-Alexander-Universit¨at Erlangen-N¨urnberg, Erlangen, Germany

**Abstract.** In the open map approach to bisimilarity, the paths and their runs in a given state-based system are the first-class citizens, and bisimilarity becomes a derived notion. While open maps were successfully used to model bisimilarity in non-deterministic systems, the approach fails to describe quantitative system equivalences such as probabilistic bisimilarity. In the present work, we see that this is indeed impossible and we thus generalize the notion of open maps to also accommodate weighted and probabilistic bisimilarity. Also, extending the notions of strong path and path bisimulations into this new framework, we show that branching bisimilarity can be captured by this extended theory and that it can be viewed as the history preserving restriction of weak bisimilarity.

**Keywords:** Open maps · Weighted Bisimilarity · Probabilistic Bisimilarity · Branching Bisimilarity · Weak Bisimilarity

## **1 Introduction**

The theory of open maps is a categorical framework to reason about systems and their bisimilarities [16]. Given a category of systems and a description of the shape of the executions and how to extend them, open maps are morphisms with lifting properties with respect to those extensions. Intuitively, open maps are morphisms which preserve and reflect transitions of systems, that is, they are morphisms whose graphs are bisimulations. The theory covers various classical notions of bisimilarity. For example, two LTSs are strongly bisimilar if and only if there is a span of open maps between them. Varying the category of models and the execution shapes allows describing weak bisimilarity, timed bisimilarity, probabilistic Larsen and Skou bisimilarity, and history-preserving bisimilarity of event structures (see [16,3,12] for examples).

Another categorical framework for bisimilarity is coalgebra [22]. This time, given a category and an endofunctor describing respectively the type of state spaces and the type of transitions, a 'system' is understood as a coalgebra for this

‹ Supported by the NWO TOP project 612.001.852.

O. Kupferman and P. Sobocinski (Eds.): FoSSaCS 2023, LNCS 13992, pp. 308–327, 2023. https://doi.org/10.1007/978-3-031-30829-1 15

functor. Coalgebra homomorphisms are then very similar to open maps in spirit: they also are morphisms that preserve and reflect transitions. This intuition has been made formal by transformations between the categorical frameworks in both ways; from open maps to coalgebra [19], and conversely [25]. However, the latter suggests that open maps are only adapted to modeling non-deterministic systems and would struggle with other types of branchings, such as probabilistic.

In coalgebra, there are no particular difficulties in modeling weighted systems, and by extension, discrete probabilistic systems [17]. There is also some work for continuous probabilities, although the theory is much more complicated [5,4]. As we will explain more precisely later, there have been some attempts to do so with open maps in [3,5], but the result is somewhat disappointing.

Conversely, coalgebra is not adapted to bisimilarities for systems where transitions are not history-preserving, that is, for which the behavioral equivalence does not just depend on the transitions at a given state, but on the whole history of the execution that led to this state. That is the case for example for branching bisimilarity [23]. Branching bisimilarity arose precisely to make weak bisimilarity history-preserving. In [3], weak bisimilarity has been described using open maps by carefully choosing the underlying category, with a general theory developed in [9] using presheaf models. Branching bisimilarity has also been studied using open maps in [1,2], but indirectly, through a translation into presheaves.

To resume, the goal of this paper is to capture weighted and branching bisimilarities using a generalization of open maps. Concretely, the contributions are:

Full proofs can be found in the appendix: http://arxiv.org/abs/2301.07004

## **2 From Path Categories to Bisimilarity**

Before discussing weighted bisimilarity, let us first recall the main ideas of modeling bisimilarity via open maps, as introduced by Joyal et al. [16]. The definition is parametric in a functor J : P Ñ M, from a category P of paths to a category M of models or systems of interest. In the prime example, M is the category of labelled transition systems LTS as defined next:

**Definition 2.1.** *For a fixed set* A *of labels, the category* LTS *contains:*

*1.  We* write x a x1 to denote that px, a, x1 q P and simply refer to the LTS as X if and x0 are clear from the context. For disambiguation, we use Ñ for morphisms and for transitions.

2. Morphisms: a functional simulation f : pX, , x0qÑpY, , y0q is a function f : X Ñ Y with fpx0q " y0 and for all x a x1 in X, we have fpxq a fpx1 q.

A functional simulation f : X Ñ Y intuitively means that the system Y has at least the transitions of X, but possibly more. A special case of a functional simulation is the run of a word in a system:

**Definition 2.2.** For the label set A, let pA˚, ďq be the partially ordered set of words, ordered by the prefix ordering. The functor J : pA˚, ďq Ñ LTS sends a word w P A˚ to the LTS Jw " ptv | v ď wu, , εq of all prefixes of w with v a va for all a P A, va ď w.

This functor J (or more precisely, its image) is often called path category of LTS: the possible runs of a word w P A˚ in pX, , x0q correspond precisely to the functional simulations Jw Ñ pX, , x0q in LTS.

On the abstract level, for a general functor J : P Ñ M, we understand the set of morphisms r : Jw Ñ X for w P P and X P M as the runs of the path w in the model X. We can already make the trivial observation that all morphisms f : X Ñ Y in M preserve runs: given a run r : Jw Ñ X of some path w P P in X, there is a run f ¨ r : Jw Ñ Y of w in Y .

The converse does not hold for a general f : X Ñ Y in M: given a run of w in Y , there is not necessarily a run of w in X. If f reflects runs, it is called open:

**Definition 2.3.** For a functor J : P Ñ M, a morphism f : X Ñ Y in M is called open if f satisfies the following lifting property for all e: v Ñ w in P:

$$\begin{array}{ccccc} & Jv \ \neg r \rightarrow X & & &\\ for \ all & \begin{array}{c} & \downarrow \\ & \downarrow \\ & \downarrow \\ Jw & \xrightarrow{s} \rightarrow Y \end{array} & \begin{array}{c} & \begin{array}{c} & Jv \ \neg r \rightarrow X \\ \downarrow \\ & \downarrow \\ Jw & \xrightarrow{s} \end{array} & \begin{array}{c} & \downarrow \\ & \downarrow \\ Jw & \xrightarrow{s} \end{array} & \begin{array}{c} \\ \downarrow \\ Jw & \xrightarrow{s} \end{array} \end{array} \end{array}$$

That is, for all commutative squares (s ¨ Je " f ¨ r), there is d: Jw Ñ X in M that makes both triangles on the right commute (f ¨ d " s and d ¨ Je " r).

By construction, we can only make statements about states that are reachable via some run. Thus, one often restricts M beforehand to contain only models in which all states are reachable from the initial state.

For LTSs in which all states are reachable from the initial state, open maps are related to strong bisimulations [20]: open maps are precisely functions whose graph relation tpx, fxq | x P Xu is a strong bisimulation. Reformulated in the context of allegories [10], open maps are precisely the maps in the allegory of relations that are strong bisimulations. It is then natural to recover bisimulations as tabulations of open maps, that is:

**Definition 2.4.** For a functor J : P Ñ M, we say that two models X and Y are J-bisimilar, if there exist another model Z and two J-open maps f : Z Ñ X and g : Z Ñ Y , that is, if there is a span of J-open maps between them.

Of course, J-bisimilarity is a reflexive (identities are open maps) and symmetric (by permuting f and g in the definition) relation on models, but it is not transitive in general. It is when the category M has pullbacks [16].

Given a functor J : P Ñ M, there are more classical ways of defining bisimilarities given in [16]. The first one is *(strong) path bisimulations*, which are relations on runs (similar to history-preserving bisimulations) satisfying the usual bisimilarity conditions. The second one is by using a modal logic similar to the Hennessy-Milner theorem. In the case of LTSs with strong bisimilarity, all those notions describe the same notion of bisimilarity, but that is not true for general J : P Ñ M: it can only be proved that J-bisimilarity implies the existence of a (strong) path bisimulation, which itself implies that the two models satisfy the same formulas of the modal logic. In [6], some mild sufficient conditions in terms of trees (i.e., colimits of paths in M) are given for those three notions to coincide. In particular, all the examples of bisimilarities covered by open maps cited earlier satisfy these conditions.

We use coalgebra for uniform statements about state-based systems of different branching type (including non-deterministic and probabilistic branching):

**Definition 2.5.** *For an object* 1 *of a category* C *and an endofunctor* F : C Ñ C*, a* pointed coalgebra *is a pair of morphisms of* C *of the form* 1 i ÝÝÑ X ξ ÝÝÑ FX.

For example, LTSs can be modeled as pointed coalgebras with C " Set, 1 any singleton, and F " PpA ˆ q, where P is the power set functor. The usual notion of morphisms of coalgebras can be spelt out as follows:

**Definition 2.6.** *A* (proper) homomorphism *of pointed coalgebras from* pX, ξ, iq *to* pY, ζ, jq *is a morphism* f : X Ñ Y *of* C *such that the diagram on the right commutes.*

1 X FX Y FY i j œ ξ f œ F f ζ

Pointed coalgebras and proper homomorphisms always form a category, but in the case of LTSs as described above, this category is not equivalent to the category LTS. Indeed, proper homomorphisms are not just morphisms that preserve transitions, but similarly to open maps, they also reflect them. In [25], the authors proved that for a large class of endofunctors, whose coalgebras basically are non-deterministic, proper homomorphisms precisely correspond to J-open maps for a certain functor J. To model morphisms that are only required to preserve transitions, homomorphisms have to be made lax as follows (see [25]):

**Definition 2.7.** *Assume a relation* Ď *on every Hom-set* CpX, FY q*.

In the case of the functor PpA ˆ q, we can consider the pointwise inclusion on every Hom-set SetpX,PpA ˆ Y qq. With this, pointed coalgebras and lax homomorphisms form a category which is isomorphic to the category LTS. However, it is not true in general that they form a category, as a compatibility of Ď with the composition is needed as follows:

**Definition 2.8.** *A* partial order on F *is a collection of partial orders* Ď*, one for each Hom-set of the form* CpX, FY q *such that*

$$\forall X \xrightleftharpoons FY, \ X' \xrightarrow{g} X, \ Y \xrightarrow{h} Y'; \quad f\_1 \sqsubseteq f\_2 \quad \Rightarrow \quad Fh \cdot f\_1 \cdot g \equiv Fh \cdot f\_2 \cdot g.$$

*This is equivalent to the requirement that the Hom-functor* Cp , F q *factors through partially ordered sets:* Cp , F q: Cop ˆ C Ñ Pos.

*Remark 2.9.* The present definition subsumes the definition of order on a Setfunctor established by Hughes and Jacobs [11, Def 2.1] (details in the appendix).

**Lemma 2.10 [25].** *When* Ď *is a partial order on* F*, pointed coalgebras and lax homomorphisms form a category, which we denote by* LCoalgp1, Fq*.*

Much as with open maps, many flavors of bisimilarity can be recovered using spans of proper homomorphisms:

**Definition 2.11.** *We say that two pointed coalgebras are coalgebraically bisimilar if there is a span of proper homomorphisms between them.*

There are many ways of defining bisimilarities in coalgebra (see [13] for an overview), but they coincide for the purpose of the present paper.

# **3 Weighted Bisimilarity and Open Maps**

In this section, we describe known attempts to model weighted systems, and particularly probabilistic ones, using open maps. They all work with some variations of the (discrete) distribution functor on Set. We will denote this functor, which maps a set X to the set

$$\mathcal{D}X = \left\{ f \colon X \to \left[0, 1\right] \mid f^{-1}\left(\left(0, 1\right]\right) \text{ is finite and } \sum\_{x \in X} f(x) = 1 \right\},$$

by D and the variation where the condition " 1 is replaced by ď 1 by Dď1 (i.e. Dď1X :" DpX ` 1q). We will prove that, even though Larsen-Skou bisimulations for reactive systems can be modeled with open maps, that is impossible for bisimulations for generative systems.

### **3.1 Larsen-Skou Bisimilarity Using Open Maps**

In [3], Cheng et al. describe an open map situation for Probabilistic Transition Systems (PTSs), which corresponds to coalgebras for the functor pDp q ` <sup>1</sup>q<sup>A</sup>. In this setting, they consider Partial PTSs (PPTS) which are coalgebras for <sup>p</sup>D<sup>ε</sup> <sup>ď</sup><sup>1</sup><sup>p</sup> q `1qA where the sub-probability distributions can have values in hyperreals, allowing infinitesimals ε. The category of PTSs embeds in that of PPTSs, and the path category is the full subcategory of PPTSs consisting of finite linear systems whose probabilities of transitions are infinitesimals. It is then proved that J-bisimilarity, restricted to PTSs, for this path category corresponds to Larsen-Skou's probabilistic bisimilarity [18].

This open map situation has been reformulated in [7] in terms of coreflections: the obvious functor from PPTSs to TSs is a coreflection whose left-adjoint maps a LTS T to the PPTS whose underlying LTS is T and where all transitions have infinitesimal probabilities. In general, given a coreflection F : C Ñ D with leftadjoint G and a path category J on D, one automatically has the path category G ˝ J on C, and this construction preserves good properties of J. In particular, one has that two systems A and B are pG ˝ Jq-bisimilar if and only if F A and F B are J-bisimilar. Cheng et al.'s path category is obtained in this manner with the coreflection above and the standard path category on LTSs. In particular, it means that two PPTSs are bisimilar if and only if their underlying TSs are strongly bisimilar.

### **3.2 Impossibility Result for Generative Systems**

In [5], Desharnais et al. describe several bisimilarities for generative probabilistic systems, that is, coalgebras for the functor Dď1pA ˆ q, in a coalgebraic way. They pointed out that their efforts to model those bisimilarities using open maps failed [5, p. 188]. In the following, we see that it is in fact not possible. We will show that for generative probabilistic systems modeled by the category M :" LCoalgp1, Dď1pA ˆ qq, there is no open map characterization of the coalgebraic bisimilarity. Actually, the argument here is valid for many other types of weights and is not limited to reals.

Here, for two functions f,g : X Ñ Dď1pY q, f Ď g means that for all x P X, for all y P Y , fpxqpyq ď gpxqpyq, where ď is the usual ordering on r0, 1s.

In this situation:

**Theorem 3.1.** For M :" LCoalgp1, Dď1pA ˆ qq there is no category P and no functor J : P Ñ M such that for every h: X Ñ Y with reachable X the following equivalence holds:

h is J-open ðñ h is a proper homomorphism

and there is no P and no functor J such that for every X and Y :

X and Y are J-bisimilar ðñ X and Y are coalgebraically bisimilar.

Proof (Sketch). By contradiction, assume that there is such a J. We prove that there is a proper homomorphism of the form:

$$X = \begin{array}{c} \downarrow \downarrow \underbrace{\mathfrak{l}/n, \stackrel{a}{\longrightarrow} x\_1}\_{l/n, a} \stackrel{x\_1}{\longrightarrow} \end{array} \qquad \xrightarrow{h} \qquad Y = \begin{array}{c} \downarrow \stackrel{1}{\longrightarrow} y \\ \downarrow \stackrel{1}{\longrightarrow} y \end{array}$$

which cannot be J-open. Consider first the unique lax homomorphism 0M Ñ Y where 0M consists in one state and no transition. This is not a proper homomorphism, so it is not open by assumption. That is there is a square:

$$\begin{array}{ccc} JP & - \to 0 \text{m} \\ \downarrow{}\_{\phi} & & \downarrow\_{Y} \\ \downarrow{}\_{Q} & \to & Y \\ JQ & - \to Y \end{array}$$

with no lifting. It is mechanical to check that JP » 0M and JQ has at least one transition from its initial state to another state r w, a z with w ‰ 0. With n " 2 ¨ r 1 w s, the proper homomorphism h above is not open: there cannot be a morphism from JQ to X because w ą 1 n . [\

## **4 Generalized Open Maps**

The main argument of the proof of impossibility is the fact that sometimes, a transition with some probability w in the codomain comes from probabilities w1,...,wn with ř i wi " w in the domain, which makes a lifting morphism impossible with the current framework of open maps.

In this section, we will extend the open map framework with the main intuition that the lifting morphism *splits* the probability w into smaller parts w1,...,wn. After defining these generalized open maps, we show some basic properties of the bisimilarity generated by them.

## **4.1 Generalized Open Maps Situation**

Here, we describe our extension of the open maps framework. The data is similar: we start with a category of models M, but we need more than just a functor J : P Ñ M. Assume:

The classical open maps situation J : P Ñ M fits in this extension as follows. The category E is given by P with the intention that they model path shapes and their *extensions*. The functor JE is given by J. The category S is given by the discrete category |P|, that is, the category whose objects are those of P and whose morphisms are only identities. The functor JS is the only possible one respecting the conditions of the definition above.

In the general context of this extension, the interpretation is a bit different. Now V is meant to be a set of trees labelled by alphabets and weights. E still consists in extensions, extending trees into trees with longer branches. S then consists in *merging morphisms*, similar to the description above: for the example of weighted systems, those morphisms are allowed to merge states into one, as long as they sum up the weights of the in-going branches. Generally, those morphisms are allowed to perform some merges that are harmless for bisimilarity. With this data, we can define generalized open maps:

**Definition 4.1.** *A morphism* f : X Ñ Y *in* M *is called* (E,S)-open *if it satisfies the following* lifting property *for all* e: v Ñ w *in* E*:*

The interpretation starts the same as in usual open maps. Assume that we have a tree y in Y extending the image by f of the tree x in X. If f is open, there should be a tree x1 extending x and whose image by f is y. However, x1 may have a different shape than y, since it might be necessary to split transitions. That is what u and s are modeling: w is obtained from u by merging some states.

The connection with the classical open maps can be formulated as follows

**Proposition 4.2.** *Given a functor* J : P Ñ M *and a morphism* f : X Ñ Y *,*

f *is* J*-open if and only if* f *is* pP, |P|q*-open.*

Again, bisimilarity can be defined as the existence of a span of open maps

**Definition 4.3.** *We say that* X *and* Y *are* pE, Sq*-bisimilar if there is a span of* pE, Sq*-open maps between them.*

#### **4.2 Basic Properties**

In this section, we will prove general properties of pE, Sq-bisimilarity similar to the classical case. First, we show that if M has pullbacks, then pE, Sq-bisimilarity is an equivalence relation. Secondly, we describe two notions of path bisimulations, both implied by pE, Sq-bisimilarity. Finally, we prove that it is enough to check openness on some generators of E.

In order to see when pE, Sq-bisimilarity is an equivalence relation, we need to check symmetry, reflexivity, and transitivity. *Symmetry* always holds because we can always swap the legs of the span. For *reflexivity*, it is enough to prove that identities are open which is valid because S is a category and JS is a functor, as shown in the diagram on the right. The proof of *transitivity* relies on composition and pullbacks:

**Lemma 4.4.** pE, Sq*-open maps are closed under composition and pullbacks.*

**Theorem 4.5.** *If* M *has pullbacks, then* pE, Sq*-bisimilarity is a transitive relation, and thus is an equivalence relation.*

**Generalized Path Bisimulations.** In the classical open map setup [16], another notion of bisimilarity can be defined by using path extensions directly: so-called strong path and path bisimulations, which can be generalized as follows. Like originally [16], we assume that there is an element 0 P V , such that J0 is an initial object of M (note that 0 is not required to be initial in E or S). The intuition is that the unique morphism !X : J0 Ñ X points to the initial state of X. For example, J0 can be given by p1, id1, Kq in a category of pointed coalgebras if 1 is the final object of C and if Cp1, F1q has the least element K: 1 Ñ F1 (those conditions hold in the cases of interest).

**Definition 4.6.** *A* path simulation *from* A *to* B *in* M *is a set* R *of spans of the form* A a ÐÝÝ Jv b ÝÝÑ B *(for* v P V *) satisfying the following two properties*

*We say that* R *is a* strong path simulation *if it additionally satisfies the following:*

**–** *backward closure: for all spans* A a ÐÝ Jv b ÝÑ B *in* R *and all* e: w Ñ v P E*, we have that the span* A a¨JEe ÐÝÝÝÝ Jw b¨JEe ÝÝÝÝÑ B *belongs to* R*.*

Remark that this version of (strong) path bisimulations has the same type as the one by Joyal et al. [16], but satisfies more general conditions. In particular, when S is a discrete category, the formulation above is exactly the one from [16]. Obviously, a strong path bisimulation is a path bisimulation.

The main result of this section is the following.

**Theorem 4.7.** *Assume two models* A *and* B *in* M*. If there is a span* A f ÐÝÝ C g ÝÝÑ B *where* g *is a morphism of* M *and* f *is an* pE, Sq*-open map, then the following set is a strong path simulation:*

$$R\_{f,g} := \{ A \xleftarrow{a} Jv \xrightarrow{b} B \mid \exists c \colon Jv \to C \text{ with } a = f \cdot c \text{ and } b = g \cdot c \} $$

*Consequently, if* A *and* B *are* pE, Sq*-bisimilar, then there is strong path bisimulation between them.*

As in the classical case of [16], there is no reason for the converse to be true in general: there might be a strong path bisimulation between two models, but no span of generalized open maps. However, conditions from [6] could be accommodated to describe a general framework in which the converse holds. Since this is not the main focus of this paper, we will not do it here, but will show a particular case in Section 6.

**Generators of the Category of Extensions.** In the first example of open maps for LTSs introduced in Section 2, the path category was described as the poset of words with the prefix order. Consequently, to prove that a functional simulation is J-open, we have to prove the lifting property of Definition 4.1 with respect to all pairs w ď w1 . However, it is sufficient to check the lifting property for extensions by one letter: w1 " w.a for some a P A. The general reason is that, as a category, pA˚, ďq is generated by the morphisms w ď w.a, and verifying the lifting property with respect to generators of the category P is enough to obtain J-openness. This can be extended to generalized open maps, with additional care.

**Proposition 4.8.** *Assume a subgraph* E1 *of* E *that generates* E*, that is, every morphism of* E *is a finite composition of morphisms of* E1 *. Assume additionally, that for every* e P E1 *and* s P S *for which* JEe ¨JSs *is well-defined, there are* s1 P S *and* e1 P E1 *such that* JEe ¨ JSs " JSs1 ¨ JEe1

*. In that case, if a morphism of* M *satisfies the lifting property of Definition 4.1 for all morphisms in* E1 *, then it is* pE, Sq*-open. Also, if a set of spans satisfies the conditions of Definition 4.6, where* E *is replaced by* E1 *, then it is a (strong) path bisimulation.*

The first condition is satisfied when E is a free category and E1 is its class of generators. The second condition is satisfied for e.g. E " P and S " |P|.

## **5 Open Maps for Weighted Systems**

In this section, we will prove that weighted systems can be captured by this generalized open map theory for a large variety of weights, including those needed to capture probabilistic systems.

#### **5.1 Category of Coalgebras for Weighted Systems**

In this section, we will consider weighted functors as follows.

**Definition 5.1.** *Given a commutative monoid* pK, `, eq*, the K-weighted functor* pK, `, eq p q : Set Ñ Set *is defined as follows on sets and maps:*

*sets:* X Ñ pK, `, eq pXq " - μ: X Ñ K | μ´1pKzteuq *is finite*( *maps:* f : X Ñ Y Ñ pK, `, e<sup>q</sup> pfq pμq " ` y P YÑ ÿtμpxq | x P X, fpxq " yu ˘ An element μ of pK, `, eqpXq is a finite distributions sending each x P X to a weight in K. Whenever a map f : X Ñ Y identifies elements fpx1q " fpx2q " ¨¨¨ , then the functor action turns μ into a distribution on Y by adding up the weights μpx1q ` μpx2q`¨¨¨ as elements of X are sent to the same element in Y . Since μ is finite and K is commutative, this addition is well-defined.

Given a commutative monoid pK, `, eq and an alphabet A, we want to consider weighted systems as coalgebras for the functor pK, `, eq pAˆ q . As described in Section 2, we want to be able to talk about lax homomorphisms, so we need an order on pK, `, eq <sup>p</sup>A<sup>ˆ</sup> <sup>q</sup> as in Definition 2.8. For that, we need to assume an ordered commutative monoid pK, `, e, Ďq, that is, a monoid pK, `, eq with a partial order Ď such that ` is monotone in both its arguments.

**Lemma 5.2.** *Given an ordered commutative monoid* pK, `, e, Ďq*, then for all sets* X *and* Y *, the relation on the hom-set* Set` X,pK, `, eq pAˆY q˘ *defined by*

$$f\_1 \subseteq f\_2 \iff \forall x \in X, \,\forall y \in Y, \,\forall a \in A, \, f\_1(x)(a, y) \subseteq f\_2(x)(a, y)$$

*is an order on* pK, `, eq pAˆ q *.*

So, we have a category LCoalg ´ 1,pK, `, eq pAˆ q ¯ of pointed coalgebras and lax homomorphisms. The goal of this section is to design a generalized open maps situation for which pE, Sq-bisimilarity characterizes coalgebraic bisimilarity and more precisely for which pE, Sq-openness characterizes proper homomorphisms.

In the course of the constructions and proofs, we will need additional assumptions that we list here.

**Definition 5.3.** *We call an ordered commutative monoid* pK, `, e, Ďq *a* rearrangement monoid *if it satisfies the additional requirement that if* n, m ě 1 *and*

$$\sum\_{i=1}^{n} x\_i \equiv \sum\_{j=1}^{m} y\_j,$$

*then there exists a family* pui,j q1ďiďn,1ďjďm *such that*

$$\text{for all } j, \sum\_{i=1}^{n} u\_{i,j} \equiv y\_j \quad \text{and} \text{ for all } i, \sum\_{j=1}^{m} u\_{i,j} = x\_i.$$

*In addition, we say that a rearrangement monoid is* strict *if the condition above holds also when replacing* Ď *with* "*.*

The intuition is as follows. We have some weights arranged as x1,...,xn. We want to be able to decompose those weights into smaller weights, the ui,j s, and by rearranging those small weights obtaining weights smaller than the yj . This condition states that this is possible when there is enough weight in total. The special case of strictness is called the *row-column property* in [17].

**Lemma 5.4.** *For any subgroup* G *of the real numbers* pRn, `, ´, <sup>0</sup><sup>q</sup> *such that for all* x*,* y *in* G pminpx1, y1q,..., minpxn, ynqq P G*, the monoids* pG, `, 0, ďq *and* pGě0, `, 0, ďq*, where* ď *is the usual order on* Rn*, are strict rearrangement monoids.*

*For any lattice with bottom element* pL, ď, \, [, Kq*,* pL, \, K, ďq *is a rearrangement monoid if and only if* pL, ď, \, [q *is distributive. Furthermore, in that case, it is always strict.*

Another property is a form of positivity: we say that an ordered monoid is *positively ordered* if e is the bottom element for Ď, that is, for all k P K, e Ď k.

*Example 5.5.* The positive real line pR`, `, 0, ďq is a positively ordered strict rearrangement monoid and it is necessary to define probabilistic systems. Another example is the monoid of natural numbers pN, `, 0, ďq, which defines the bag functor. Finally, any distributive lattice with bottom element pL, \, K, ďq, typically powerset lattices pPpXq, Y, ∅, Ďq, is too. On the contrary, pR, `, <sup>0</sup>, ďq and <sup>p</sup>Z, `, 0, ďq are strict rearrangement monoids but are not positively ordered. Conversely pNě1, ˆ, 1, ďq is positively ordered but not a rearrangement monoid. Indeed, it is impossible to rearrange the inequality 2 ˆ 5 ď 3 ˆ 4.

#### **5.2 Generalized Open Maps Situation for Weighted Systems**

Let pK, `, e, Ďq be a commutative ordered monoid. Elements of VK are

The function JK maps

**–** a word w " pa1, k1q,...,pan, knq to the system

$$Jw = \boxed{\bullet 0 \xrightarrow{(a\_1, k\_1)} 1 \xrightarrow{(a\_2, k\_2)} \cdots \xrightarrow{(a\_n, k\_n)} n}$$

that is, to the coalgebra Jw: t0,...,nu Ñ KpAˆt0,...,nuq such that if b " ai`<sup>1</sup> and j " i ` 1 then Jwpiqpb, jq " ki`1, else " e.

**–** a triple pw1, b, w2q with w1 " pa1, k1q,...,pan, knq and w2 " l1,...,lm is mapped to the system

$$J(w\_1, b, w\_2) = \left| \bullet 0 \xrightarrow{\{a\_1, k\_1\}} 1 \xrightarrow{\{a\_2, k\_2\}} \cdots \xrightarrow{\{a\_n, k\_n\}} n \xrightarrow{\{b, l\_1\}} \begin{pmatrix} n+1, 1 \\ \vdots \\ \vdots \\ n+1, m \end{pmatrix} \right|$$

that is, Jpw1, b, w2qpnqpn ` 1, iq"pb, liq.

The category EK is defined as follows. For every w1, b, and w2, there is a unique edge e from w1 to pw1, b, w2q. The functor then maps this edge e to JEe, the obvious injection.

The category SK has two types of morphisms:

**Fig. 1.** Example of a lifting of a path extension in R`-weighted systems and for a singleton label alphabet |A| " 1, thus omitting action labels.

The functor JS then maps s of the second type to the proper homomorphism JSs which maps i to i and pn ` 1, jq to pn ` 1, spjqq.

As a piece of notation, for a morphism x: Jw1 Ñ X, with w1 of length n we denote xpnq P X by endpxq. We then say that a state p of X is reachable if there is a morphism of type x: Jw1 Ñ X with endpxq " p. By extension, we say that X is reachable if all its states are reachable.

#### **5.3 Equivalence between Open Maps and Proper Homomorphisms**

An example of an pE, Sq-open map h is provided in Figure 1, together with a path extension that is lifted. Like it is often the case in the non-deterministic systems, the lifting map d is not unique. Hence, only existence (and no uniqueness) is required in the lifting property. Since h is a proper homomorphism, it provides a lifting for all extensions, as we show in general:

**Theorem 5.6.** *Assume a lax homomorphism* f : X Ñ Y *. If* f *is* pEK, SKq*-open,* X *is reachable, and* K *is positively ordered, then* f *is a proper homomorphism. Conversely, if* f *is a proper homomorphism and* K *is a rearrangement monoid, then* f *is* pEK, SKq*-open. In particular, if* K *is a positively ordered rearrangement monoid, two weighted systems* X *and* Y *are* pEK, SKq*-bisimilar if and only if they are coalgebraically bisimilar.*

For an endofunctor on Set, to prove that coalgebraic bisimilarity is an equivalence relation it is enough to show that the functor preserves weak-pullbacks. In the case of the weighted functor, this is given by strictness (see also [17]):

**Corollary 5.7.** *If* K *is a positively ordered strict rearrangement monoid, then* pEK, SKq*-bisimilarity is an equivalence relation.*

#### **5.4 About Sub-distribution Functor**

Until now, we have not dealt with probabilistic systems, that is, coalgebras for the sub-distribution functor Dď1. Those coalgebras are particular cases of coalgebras for the weighted functor X Ñ pR`, `qpXq . We want to show in this section that it is equivalent to consider coalgebras for X Ñ Dď1pA ˆ Xq as coalgebras for X Ñ pR`, `qpAˆXq , in the sense that, two coalgebras for the former are bisimilar if and only if they are bisimilar when seen as coalgebras for the latter. The main ingredient is the following remark.

**Lemma 5.8.** *Assume a pointed coalgebra* 1 i ÝÝÑ X c ÝÝÑ Dď1pAˆXq *and assume given a lax (resp. proper) homomorphism* f *from* 1 j ÝÝÑ Y d ÝÝÑ pR`, `qpAˆY q *to* 1 i ÝÝÑ X c ÝÝÑ Dď1pA ˆ XqĎpR`, `qpAˆXq *. Then* Y d ÝÝÑ Dď1pA ˆ Y q *and* f *is a lax (resp. proper) homomorphism from* 1 j ÝÝÑ Y d ÝÝÑ Dď1pA ˆ Y q *to* 1 i ÝÝÑ X c ÝÝÑ Dď1pA ˆ Xq*.*

Remark that this property is not true for the proper distribution functor D. This suggests that we can define a generalized open maps situation ED, SD for coalgebras for the functor XÑ Dď1pA ˆ Xq by considering EpR`,`q, SpR`,`q as defined in Section 5.2, and restricting it to those v such that Jv is a coalgebra for X Ñ Dď1pA ˆ Xq.

**Corollary 5.9.** *A lax homomorphism from* 1 j ÝÝÑ Y d ÝÝÑ Dď1pA ˆ Y q *to* 1 i ÝÝÑ X c ÝÝÑ Dď1pA ˆ Xq *is* pED, SDq*-open if and only if it is* pEpR`,`q, SpR`,`qq*-open. Furthermore, two* Dď1pA ˆ q*-coalgebras are* pED, SDq*-bisimilar if and only if they are* pEpR`,`q, SpR`,`qq*-bisimilar.*

Finally, the main result of this section:

**Theorem 5.10.** *Let* f : X Ñ Y *be a lax homomorphism between* Dď1pA ˆ q*coalgebras* pX, c, iq *and* pY, d, jq*. If* pX, c, iq *is reachable and* f *is* pED, SDq*-open, then* f *is a proper homomorphism. Conversely, if* f *is a proper homomorphism, then it is* pED, SDq*-open. Moreover, two* Dď1pA ˆ q*-coalgebras* pX, c, iq *and* pY, d, jq *are* pED, SDq*-bisimilar if and only if they are coalgebraically bisimilar.*

## **6 Open Maps for Branching Bisimilarity**

In this section, we present a new way of modeling branching and weak bisimulations using our generalized framework of open maps. Using this additional flexibility, we do not need to rely on weak morphisms anymore, but on a slight modification of the morphism described in Definition 2.1. Concretely, we build a generalized open map situation such that stuttering branching bisimulations coincide with strong path bisimulations, and that in this case, they precisely characterize pE, Sq-bisimilarity. In addition, in this framework, path bisimulations precisely correspond to weak bisimulations, witnessing branching bisimilarity as the history-preserving analogue to weak bisimilarity.

## **6.1 LTSs with Internal Moves, Category and Bisimilarities**

**Definition 6.1.** *For a fixed set* A *of labels with a particular element* τ *(called* internal move*), the category* WLTS *contains the same objects as* LTS*, and its morphisms* f : pX, , x0qÑpY, , y0q *are functions* f : X Ñ Y *such that* fpx0q " y0 *and for all* x a x1 *in* X*, we have* fpxq a fpx1 q*, or* a " τ *and* fpxq " fpx1 q*.*

LTS is a (non-full) subcategory of WLTS, and in fact the LTS-morphisms will be used later in the paper. For easier distinction, we use the terminology *strong morphisms* for WLTS-morphisms that are also in LTS (alluding to *strong bisimulations* which were the bisimulation notion in LTS). Another notion of morphisms are so-called *weak morphisms* [3]:

**–** if x a x1 in X, then fpxq τ ‹ a τ ‹ fpx1 q in Y , **–** if x τ x1 in X, then fpxq τ ‹ fpx1 q in Y .

Though we do not use weak morphisms in the following development of the paper, it is worth mentioning the WLTS-morphisms form a proper subclass of the weak morphisms.

**Definition 6.2.** *A* branching bisimulation *from* pX, X, iXq *to* pY, Y , iY q *is a relation* R Ď X ˆ Y *such that* piX, iY q P R*, and for* px, yq P R*:*

$$\begin{array}{c} \text{ } & \text{ } if \, x \xrightarrow{a} \text{ } & x' \text{ } then\\ \text{ } & \text{ } a = \tau \text{ } and \, (x', y) \in R, \, or \\ \text{ } & y \xrightarrow{\tau} \text{ } & y\_1 \xrightarrow{\tau} \dots \xrightarrow{\tau} \text{ } y\_n \xrightarrow{a} \text{ } & z\_1 \xrightarrow{\tau} \dots \xrightarrow{\tau} \text{ } z\_m \text{ } such \text{ } that \, (x, y\_n),\\ \text{ } & \text{ } & (x', z\_1), \text{ } and \, (x', z\_m) \in R. \\ \text{ } & \text{ } & \text{ } & y'. \end{array}$$

*If furthermore in the second condition* px, yiq, px1 , ziq P R *for all* i *(and symmetrically in the third condition), then* R *is said to be* stuttering*.*

It is known from [23] that the largest branching bisimulation is stuttering, so that both notions generate the same bisimilarity. In the following, we will prove that strong path bisimulations are more naturally related to stuttering branching bisimulations thanks to their backward closure.

**Definition 6.3.** *A* weak bisimulation *from* pX, X, iXq *to* pY, Y , iY q *is a relation* R Ď X ˆ Y *such that* piX, iY q P R*, and for* px, yq P R*:*

It is clear that a (stuttering) branching bisimulation is a weak bisimulation.

#### **6.2 Generalized Open Maps for Branching Bisimulations**

In this section, we describe the generalized open maps situation that captures branching bisimulation. Like for plain LTSs (Def. 2.2), elements of V will be words on A, representing a finite linear LTS labelled by this word. However, to emphasize the particularity of the internal move τ , we will provide another presentation here.

Here, V is the set of sequences of the form: v " n1, a1, n2,...,nk, ak, nk`1 such that ai P Aztτ u and ni P N, e.g. τ τ aτ bcτ "p 2, a, 1, b, 0, c, 1. The natural numbers ni P N – tτ u ˚ represent the number of internal moves between two observable moves. Then, J maps this sequence to the usual linear LTS:

Elements of E append at most one observable (i.e. non-τ ) move:

The graph morphism JE : E Ñ M maps those edges to the obvious inclusion, mapping state pi, jq of Jv to the same state in Jw.

Strictly speaking, E is not a category, but just a graph, because we have a eb ÝÑ ab and ab ec ÝÑ abc, but there is no morphism from a to abc. To fit in the framework of Section 4, we take the free category FreepEq generated by this graph and the unique functor extending the graph homomorphism JE. By Proposition 4.8, it is equivalent to consider FreepEq and E for openness and path bisimulations, so we will talk of pE, Sq-openness, when we mean pFreepEq, Sqopenness, and all the statements and proofs will be done using E only.

Elements of S are trickier to describe. The intuition is that they are morphisms that merge states. In the context of LTSs with internal moves, merging happens when the source and the target of a τ -transition are mapped to the same state. This is crucial for the open maps we want to describe: to lift one τ -transition, it might be necessary to use several τ -transitions. With this knowledge, elements of S are as follows.

**– Merging internal moves**: morphisms in S from v " n1, a1,...,ak, nk`<sup>1</sup> to <sup>w</sup> " <sup>n</sup><sup>1</sup> 1, a1,...,ak, n<sup>1</sup> <sup>k</sup>`1 with ni ě n1 i are pk ` <sup>1</sup>q-tuples <sup>s</sup> " ps1,...,s<sup>k</sup>`1q of monotone surjective functions si : t0 ă 1 ă ... ă niuÑt0 ă 1 ă ... ă n1 iu. For example, there are two morphisms from aτ τ b "p 0, a, 2, b, 0 to aτ b "p 0, a, 1, b, 0,

one for each τ that can be dropped. The functor JS then maps s to the morphism from Jv to Jw defined by JSpsqpi, jq"psj piq, jq.

#### 324 J. Dubut and T. Wimann

As a piece of notation, for a morphism x: Jpn1, a1,...,ak, nk`<sup>1</sup>q Ñ X, we denote xpn<sup>k</sup>`1, k ` 1q P X by endpxq.

### **6.3 Equivalence of Bisimilarities**

In this section, we prove that pE, Sq-bisimilarity indeed coincides with branching bisimilarity. To do so, we prove first that for the present instance of E and S (Sec. 6.2), pE, Sq-bisimilarity coincides with strong path bisimilarity. In general, pE, Sq-bisimilarity implies strong path bisimilarity (Theorem 4.7), so it remains to show the converse direction for the present instance. To this end, we start by internalizing strong path bisimulations into objects of LTS/WLTS, in order to relate it them to open maps:

**Definition 6.4.** *For a strong path bisimulation* R *from* X *to* Y *, define the LTS* Rr " pR, R,pX ! ÐÝÝ J0 ! ÝÝÑ Y qq *to have transitions*

$$(X \xleftarrow{x} Jv \xrightarrow{y} Y) \xrightarrow{a} \_{R} (X \xleftarrow{x'} Jw \xrightarrow{y'} Y)$$

**Lemma 6.5.** *In* WLTS*, we have projection maps* X ÐÝÝ πX Rr πY ÝÝÑ Y *given by* πX : pX x ÐÝ Jv y ÝÑ Y q Ñ *end*pxq *and* πY : pX x ÐÝ Jv y ÝÑ Y q Ñ *end*pyq*. For every strong morphism* r : Jv Ñ Rr *(i.e.* r P LTS*),*

$$\operatorname{lend}(r)\text{ is of the form }(X \xleftarrow{\pi\_X \cdot r} Jv \xrightarrow{\pi\_Y \cdot r} Y).$$

Remark that in this statement, we require r to be strong and not just a morphism of WLTS. With a morphism of WLTS, the statement would become that there is s: v1 Ñ v P S such that πX ¨ r " x ¨ JSs instead. For the characterization of open maps in WLTS, it suffices for our needs to restrict to strong morphisms:

**Lemma 6.6.** *For* f : X Ñ Y *in* WLTS *to be* pE, Sq*-open, it is sufficient to verify the lifting in Definition 4.1 in the special case of* x *being a strong morphism.*

We use this simplification to prove that the projection maps πX, πY are open:

**Proposition 6.7.** *For a strong path bisimulation* R *from* X *to* Y *, the projections* X ÐÝÝ πX Rr πY ÝÝÑ Y *are both* pE, Sq*-open.*

The next step is to prove the equivalence between strong path and stuttering branching bisimulations.

**Table 1.**  Conversely, if* R *is a strong path bisimulation, then*

Rq " tp*end*pxq, *end*pyqq | pX x ÐÝ Jv y ÝÑ Y q P Ru

*is a stuttering branching bisimulation.*

The same reasoning can be made for weak and path bisimulations:

**Theorem 6.9.** *If* R *is a weak bisimulation from* X *to* Y *, then*

$$\text{During can be made for weak and path bisim}$$

$$\text{If } R \text{ is a weak bisimulation from } X \text{ to } Y, \text{ then}$$

$$\hat{R} = \{ X \xleftarrow{x} Jv \xrightarrow{y} Y \mid (end(x), end(y)) \in R \}$$

*is a path bisimulation. If* R *is a path bisimulation, then* Rq *is a weak bisimulation.*

In total, we can describe branching and weak bisimilarity by categorical bisimilarity notions, as summarized in Table 1.

## **7 Conclusions and Future Work**

In this paper, we investigate bisimilarities of weighted and probabilistic systems through the theory of open maps. After showing that the usual theory cannot capture weights, we provide a faithful extension of the theory by the notion of mergings. The new theory has similar properties (equivalence relation, characterization as sets of spans, restriction to generators) as classical open maps but also captures bisimilarity of weighted systems and even branching bisimilarity.

The new instances come at the cost of more parameters to the theory. It remains for future work whether the parameters E, S can be combined in a single path category with two morphism classes and morphism factorizations. It would also be illuminating to know whether this new theory satisfies the axioms of a *class of open maps* from [15], in particular for toposes of coalgebras [14].

For the framework as presented, we would like to formally relate it to coalgebra – as this has been done for non-deterministic systems [19,25]. Furthermore, we would like to investigate how system semantics of true concurrency, such as Higher Dimensional Automata [21] can be integrated. Designing open maps for them turned out to be complicated (see [8]), but a hope would be that the addition of mergings would allow modeling homotopy more naturally.

Finally, it would be interesting to see whether our theory capture quantitative extensions of systems classically modeled by open maps, such as probabilistic and quantum extensions of petri nets and event structures (see [24] for example).

## **References**

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

## Preservation and Reflection of Bisimilarity via Invertible Steps

Ruben Turkenburg()1 , Clemens Kupke2 , Jurriaan Rot1 , and Ezra Schoen2

1 Institute for Computing and Information Sciences (iCIS), Radboud University, Nijmegen, The Netherlands

####<EMAIL_ADDRESS>
2 Department of Computer and Information Sciences, Strathclyde University, Glasgow, UK

Abstract. In the theory of coalgebras, distributive laws give a general perspective on determinisation and other automata constructions. This perspective has recently been extended to include so-called weak distributive laws, covering several constructions on state-based systems that are not captured by regular distributive laws, such as the construction of a belief-state transformer from a probabilistic automaton, and ultrafilter extensions of Kripke frames.

In this paper we first observe that weak distributive laws give rise to the more general notion of what we call an invertible step: a pair of natural transformations that allows to move coalgebras along an adjunction. Our main result is that part of the construction induced by an invertible step preserves and reflects bisimilarity. This covers results that have previously been shown by hand for the instances of ultrafilter extensions and belief-state transformers.

Keywords: Coalgebra · Bisimulations · Weak distributive laws

## 1 Introduction

Distributive laws between a monad T and a functor B are ubiquitous in the theory of coalgebras. They capture various forms of interaction between algebras and coalgebras, including structural operational semantics [45,33], efficient proof techniques [9] and a general coalgebraic determinisation procedure which applies to a wide range of automata and other state-based systems [43,15,29].

The central idea of this general determinisation procedure is to interpret coalgebras in the Eilenberg-Moore category EM(T), as coalgebras for a lifting of B that arises from the distributive law. Behavioural equivalence in EM(T) then amounts to desired notions of equivalence. For instance: language equivalence of non-deterministic automata; weighted automata [7]; Mealy and Moore machines with side-effects [43]; or various types of trace equivalence of transition systems [8].

An illustrative *non-example* of this general determinisation procedure is in a natural construction of belief-state transformers from probabilistic automata, which feature both non-determinism and probabilities. From a categorical perspective, the problem is related to the classical result that there is no suitable distributive law of the probability distribution monad D over the powerset monad

P [46] (also see [47,34] for other non-existence results of distributive laws). Hence, general determinisation via distributive laws seems not applicable here.

Nevertheless, in [12] a concrete coalgebraic account of the construction of belief-state transformers is given, in terms of a two-stage process:

A key result in op. cit. is that the second stage preserves and reflects behavioural equivalence. This shows that behavioural equivalence of coalgebras in EM(D) coincides with distribution bisimilarity on the belief-state transformer.

In [12,21] it was shown that this construction, in fact, arises from a canonical weak distributive law of D over P [22]. Weak distributive laws correspond to so-called weak liftings [19], and—as shown in [22]—these yield a new generalised determinisation procedure which covers the above example, and precisely instantiates to the two stages above. Further examples are the treatment of alternating automata via weak distributive laws in [23], and weak distributive laws for combining non-determinism with semimodules in [10].

However, the result for probabilistic automata that the second stage above preserves and reflects behavioural equivalence has not yet been accounted for in the abstract theory of determinisation via weak distributive laws.

In this paper we provide such an account, starting from a more general setting than weak distributive laws: what we call invertible steps. These basically replace the Eilenberg-Moore adjunction inherent in the weak liftings approach by a general adjunction. In this context, a step allows one to lift the left adjoint to coalgebras—this is a widely occurring phenomenon, for instance in the semantics of coalgebraic modal logic, testing semantics and trace semantics (see [41] for an overview). The key idea here is to assume a right inverse, allowing the lifting of the right adjoint, such that we generalise the two-stage construction above.

We show that, in this setting of an invertible step, the second stage of the two-stage construction preserves and reflects bisimilarity, under mild conditions. As a consequence, we recover the above-mentioned results on preservation and reflection of behavioural equivalence for probabilistic automata [12] for free from the abstract theory.3 Another motivating example is that of coalgebras for the Vietoris functor on the category of Stone spaces: we obtain that bisimilarity is preserved and reflected by the forgetful functor, recovering the main result in [5].

In fact, the latter example is related to a coalgebraic presentation [36] of ultrafilter extensions, a standard construction in modal logic [6]. It fits within the general setting of invertible steps, but not directly in weak liftings, as it involves the category of Stone spaces (for the duality with Boolean algebras). However, if we move from Stone spaces to compact Hausdorff spaces, then the relevant weak lifting (or invertible step) arises precisely from the weak distributive law

3 We focus on bisimilarity, but our setting allows for an easy argument that this coincides with behavioural equivalence in this and many related examples.

constructed by Garner [19]. The weak distributive law in *loc. cit.* thus gives rise to ultrafilter extensions in modal logic.

Finally, we include an example of an invertible step involving Setop instead of an Eilenberg-Moore category. Steps for adjunctions with opposite categories are a standard way of presenting the semantics of coalgebraic modal logic [40,32]. The included example shows the generality of the approach.

*Outline.* Section 2 presents (invertible) steps, the relation to weak liftings and distributive laws, and a range of examples. In Section 3 we recall the standard notion of coalgebraic bisimilarity, defined via relation lifting. Section 4 contains the main results on preservation and reflection of bisimilarity. In Section 5 we discuss applications and instances of these results. We discuss other notions of bisimulation, and future work, in Section 6.

## 2 Forward and Backward Steps

We briefly present the required theory of steps, first termed as such in [41]. This structure occurs already in work on coalgebraic modal logic [35,14,40,32,17,38] where a step gives the one-step semantics of a logic. In existing work, only what we call a *forward* step is considered. Here, we also speak of *backward* steps, being arrows in the opposite direction. In the sequel, such forward and backward steps will usually be each other's (one-sided) inverses, referred to as *invertible steps*.

Next, we recall how such steps give rise to liftings of functors between categories of coalgebras and further, when the adjunction underlying the steps can also be lifted to coalgebras [27]. Finally, we present examples of invertible steps from the literature, which we return to in later sections.

For a functor B : C→C, a *coalgebra* is a pair (X, f) consisting of an object X and an arrow f : X → BX. A homomorphism from (X, f) to (Y,g) is an arrow h: X → Y such that g ◦ h = Bh ◦ f. Coalgebras and homomorphisms between them form a category, denoted by Coalg(B), or CoalgC(B) if we wish to make the underlying category explicit.

The category of sets and functions is denoted by Set. For a monad T, we write EM(T) for the category of Eilenberg-Moore algebras. The powerset monad is denoted by P : Set → Set, given on objects by P(X) = {S | S ⊆ X}, and the finitely-supported distribution monad by D: Set → Set, given by D(X) = {ϕ: X → [0, 1] | - x∈X ϕ(x)=1, supp(ϕ) finite} (see also [12]).

## 2.1 Invertible Steps

The basic setting of interest in this work consists of the following:

Definition 2.1. *Given an adjunction* P Q: D→C *and endofunctors* B : C → C *and* L: D→D *as in the diagram*

$$\mathfrak{a}\_B \underbrace{\mathfrak{C} \mathfrak{C} \xleftarrow{P} \mathfrak{D}}\_Q \mathfrak{D}^L,\tag{1}$$

*a* (forward) step *is a natural transformation* δ : BQ → QL*. A* backward step *is simply a natural transformation* ι: QL → BQ *going the other way. If, moreover,* δ ◦ ι = id *then we call* δ *an* invertible step *(with right inverse* ι*). Finally, if* δ *witnesses an isomorphism then we call it an* isomorphic step*.*

Notice the asymmetry in the definition of invertible step: ι is always assumed to be a *right* inverse of δ. These invertible steps are the main focus of this paper. Examples are given below in Section 2.2.

Step-induced liftings There is a bijective correspondence between a step and its *mate* ˆδ : P B → LP given by P B P BQP P QLP LP PBη P δP εLP (see [37,31]). This mate and the backward step allow us to define liftings of P and Q to the categories of coalgebras for B and L.

Definition 2.2.  This is well-defined due to functoriality of* P *and* Q *and naturality of* ˆδ *and* ι*.*

It is shown in [27, Theorem 2.14] that, when δ and ι form an isomorphism, the adjunction P Q lifts to an adjunction P Q between the step-induced liftings. For our purposes it will be useful to split the isomorphism condition into the cases where ι is the left or right inverse of δ.

Lemma 2.3. *If* δ ◦ ι = id*, then the counit* ε: P Q → Id *of the adjunction* P Q *lifts to a natural transformation* ε: P Q → Id*. If* ι ◦ δ = id*, then the unit* η : Id → QP *of the adjunction lifts to a natural transformation* η : Id → Q P*.*

The combination of these two liftings gives us the lifting of the adjunction.

Corollary 2.4. *If* δ *and* ι *form an isomorphism, then* P Q*.*

In such a situation, Q (being a right adjoint) preserves the final coalgebra for L (the limit of the empty diagram) when this exists. However, there are a number of known examples where the step is not an isomorphism; instead we only have a one-sided inverse. We consider, in particular, these invertible steps, and in the next subsection give a number of examples of this setting.

## 2.2 Steps from weak liftings, and other examples

*Example 2.5.* Our first example arises from the work of Garner, who shows that the Vietoris monad V on the category CHaus of compact Hausdorff spaces arises as a so-called *weak lifting* of the powerset monad [19] (we discuss weak liftings in general after this example). For the definition of the Vietoris monad the reader is referred to [19, Sec. 2.3]. The category CHaus is equivalent to the Eilenberg-Moore category EM(β) of the ultrafilter monad β [39]. The weak lifting provided by Garner consists of natural transformations ι, δ, satisfying δ ◦ ι = id:

$$\iota^{\mathcal{P}} \square \mathsf{Set} \xleftarrow{\mathcal{F}} \widehat{\mathcal{E}\mathcal{M}(\beta)} \square \nu \qquad \qquad U\mathcal{V} \xrightarrow{\iota} \mathcal{P}U \xrightarrow{\delta} U\mathcal{V} \tag{4}$$

where F U is the Eilenberg-Moore adjunction of β. Notice that δ is an invertible step, with right inverse ι. As shown by Garner, a component δX : PUX → UVX, sends each subset S ∈ PUX to its topological closure. The components of ι simply include the closed subsets into the powerset.

It turns out that this invertible step gives rise to ultrafilter extensions of Kripke frames. In modal logic, ultrafilter extensions [6,20,4] are a construction taking a Kripke frame (which we can see as a coalgebra for the powerset functor P) with state space W and forming a new Kripke frame with states being ultrafilters over W. The central motivation for this is in "bisimilarity-somewhere-else" results: two states are modally equivalent iff they are bisimilar in the ultrafilter extension.

Now, the composition of the step-induced coalgebra liftings F : Coalg(P) → Coalg(V) and U : Coalg(V) → Coalg(P), precisely yields the ultrafilter extension of a Kripke frame. The first stage β is the actual extension, which turns the Kripke frame into a V-coalgebra. The second stage U turns this back into a Kripke frame, i.e., a powerset coalgebra in Set.

In [36], ultrafilter extensions are developed more generally for coalgebras for a functor B : Set → Set, via the duality between Boolean algebras and Stone spaces. In fact, since both V and the left adjoint F restrict to the category Stone of Stone spaces, the invertible step δ, ι restricts to an invertible step in the restriction of the above adjunction to Stone.

In general, for monads S, T on a category C, Garner [19] defines S˜: EM(T) → EM(T) to be a weak lifting of S if there are natural transformations

$$U\ddot{S} \stackrel{\iota}{\longrightarrow} SU \stackrel{\delta}{\longrightarrow} U\ddot{S} \tag{5}$$

with δ ◦ ι = id and satisfying further axioms, where U denotes the forgetful functor from EM(T) to C. They show that there is a bijective correspondence between weak distributive laws of T over S, and weak liftings of S to EM(T), in case idempotents in C split (which holds for Set). Here, we do not assume a monad structure on S (which is why the additional axioms are not relevant). In this case, a weak lifting is precisely an invertible step, where the underlying adjunction is an Eilenberg-Moore adjunction.

*Example 2.6.* In [11,12], a procedure is given for "determinising" probabilistic automata (PAs), which model systems with both non-determinism and probabilities, into belief state transformers. It was shown in [22] that this is an instance

of a more general determinisation procedure induced by a weak lifting, which in turn corresponds to a canonical weak distributive law.

Stated for a general monad T with the usual Eilenberg-Moore adjunction F - U : EM(T) → C, this general determinisation procedure thus starts from an invertible step (weak lifting) δ : BU → UB. This gives rise to a two-step process:

$$\mathsf{Coalg}\_{\mathcal{C}}(BT) \xrightarrow{\overline{\mathcal{F}}} \mathsf{Coalg}\_{\mathcal{E}\mathcal{M}(T)}(\overline{B}) \xrightarrow{\overline{U}} \mathsf{Coalg}\_{\mathcal{C}}(B) \tag{6}$$

where the second functor U is simply the step-induced lifting of U. The first is a variation of a step-induced lifting (notice that it takes BT-coalgebras rather than B-coalgebras as input), mapping a coalgebra f : X → BTX to FX FBUFX BFUFX BFX Ff δ ˆUFX BεFX , where ε is the counit of the Eilenberg-Moore adjunction. In fact, this can be viewed as a step-induced lifting for BT which arises by composing δ and the counit, see [41].

We instantiate this to the Eilenberg-Moore adjunction of the distribution monad D, where Pc is the convex powerset monad:

$$\mathcal{P}\underbrace{\mathsf{C}\mathsf{Set}}\_{U}\xleftarrow{\mathcal{F}}\_{\mathcal{LM}(\mathcal{D})}\mathsf{C}\mathcal{M}(\mathcal{D})\xleftarrow{\mathcal{F}}\mathcal{P}\_{c}\tag{7}$$

We take Pc(X) to have as underlying set {S ⊆ X | S convex} following [22]. This matches the usage of Pne + 1 and Pc + 1 in [12], where Pne and Pc are defined to exclude the empty set. A subset is convex if it is closed under convex combinations (see [12] for details). Further, the category EM(D) is equivalent to the category of convex algebras and convex maps.

It is explained in [22, Sec. 5] that we have an invertible step in the setting of Eq. (7), which sends a subset X to its convex hull (the smallest convex set containing X) and that the lifting F of (6) then gives the transformation of a probabilistic automaton into a belief state transformer in the category EM(D). The second step is then to transfer the obtained belief state transformer back to Set with the step-induced lifting of U. As shown in [12] and later recovered from our abstract theory (Section 5), this yields a system with the same behaviour. In fact, this is done for automata with labels, i.e., for the functors PL and PL c with L a set of labels. The weak lifting we will require in this context is given in [21].

*Example 2.7.* The following example from automata and languages considers a dual adjunction P - Q: Dop → C. One motivation to discuss this kind of example stems from coalgebraic modal logic where C commonly is some category of 'spaces' and D commonly is a category of 'algebras' [32]. The setup is as follows:

$${}^{B}\widehat{\text{C}}\text{Set}\xleftarrow{\text{2-}}\text{Set}^{\text{2-}}\text{Set}^{\text{op}}\xleftarrow{} {}^{L}\text{}\underline{\qquad}2^{L}\stackrel{\iota}{\longrightarrow}B(2^{-})\xrightarrow{\delta}2^{L}\tag{8}$$

Here, we have BX = 2 × (PX)Σ and LX =1+ Σ × X for a fixed alphabet Σ. The step δ is given by

$$\delta(i,\xi) = \{\mathsf{inl}(\*) \mid i = 1\} \cup \{\mathsf{inr}(a, x) \mid a \in \Sigma, x \in \bigcup \xi(a)\}\tag{9}$$

334 R. Turkenburg et al.

This step δ is invertible, e.g., by ι as in Eq. (10).

$$\iota(u) = (1 \text{ iff } \text{inl}(\*) \in u, a \mapsto \{v \mid \{(a, x) \mid x \in v\} \subseteq u\}) \tag{10}$$

A B-coalgebra is a non-deterministic automaton. An L-coalgebra in Setop is an algebra X ← 1 + Σ × X in Set, which can be seen as specifying the initial state and transition structure of a deterministic automaton. From this point of view, the coalgebra lifting Q: Coalg(L) → Coalg(B) can be seen as first reversing, and then performing a powerset construction. The specific powerset construction might depend on the chosen right inverse ι, as it is not unique. For ι as in (10), for example, u a → v in Q(A) if and only if each state in v is reachable from a state in u via an a-transition in the reverse of A.

In Section 5 we return to these examples and show how we can apply the techniques from Section 4 to obtain preservation and reflection of bisimilarity.

## 3 Relations, Liftings and Coalgebraic Bisimulations

We recall the standard notion of coalgebraic bisimulation defined via relation lifting, broadly following [30,28]. Note, we will use some terminology from the theory of fibrations to allow us to be more concise and many of the coming results can be generalised to a larger class of fibrations, but knowledge of fibrations is not required as we give a self-contained presentation of the fibration of relations.

We make the following assumptions for the remainder of the paper:

Assumption 3.1. *We assume categories* C, D *with all finite limits, and factorisation systems* (E1,M1)*,* (E2,M2) *respectively for which* M1 = MonoC,M2 = MonoD *and for any left adjoint functor* P : C→D *we have* P(E1) ⊆ E2*.*

We assume finite limits mainly for binary products and pullbacks to allow the definitions of relations and inverse images. The assumptions that maps in M are mono means that pullbacks of abstract monos and factorisation both yield monos, which represent subobjects. The final condition specifies that left adjoints preserve abstract epis. This is required in Section 4.2 and holds, e.g., when the involved categories possess a (RegEpi, Mono)-factorisation system [16,2], as in all our examples from Sections 2.2 and 5.

For a category C satisfying the above, the category Rel(C) consists of:

$$\bigcup\_{X \times X}^{R} \xrightarrow{\cdots \xrightarrow{\cdots \xrightarrow{\cdots} \xrightarrow{\cdots} S}} \bigcup\_{Y \times Y}^{S} \tag{11}$$

In Set, these are subsets of the binary product of underlying sets as usual, and maps between relations constitute maps between the products sending R to S, i.e., xRy implies u(x) S u(y). Objects of Rel(Stone) are closed relations, as the image of a mono representing a subobject is homeomorphic to its domain, and images of continuous functions are compact and thus closed. In the case of an Eilenberg-Moore category for a monad T, objects of Rel(EM(T)) are congruences, as the map into the product is an algebra morphism.

Remark 3.2. A note on notation: we use for epis and for monos and the subobjects they represent. We use for abstract epis and for abstract monos, i.e., maps in E and M respectively.

Using the factorisation system on D, we lift a functor F : C→D to a functor Rel(F): Rel(C) → Rel(D). The action on objects is given by the factorisation

$$\begin{array}{c} FR \xrightarrow{Fr} F(X \times X) \xrightarrow{\langle F\pi\_1, F\pi\_2\rangle} FX \times FX\\ \underbrace{\begin{array}{c} e \end{array} \text{ } \mathsf{Rel}(F)(R) \xleftarrow{m} \end{array} \tag{12}$$

The action on arrows is defined by orthogonality. The resulting functor Rel(F) is a lifting in the sense that the following diagram commutes

$$\begin{array}{c} \mathsf{Rel}(\mathcal{C}) \xrightarrow{\mathsf{Rel}(F)} \mathsf{Rel}(\mathcal{D}) \\ \Downarrow \\ \mathcal{C} \xrightarrow{\mathcal{P}} \xrightarrow{F} \mathcal{D} \end{array} \tag{13}$$

where p: Rel(C) → C sends a relation R - X × X to the object X, and similarly for q. We say (following the terminology of fibrations) that the relation R is above the object X and a map between relations is above the map u from Eq. (11). Note that commutativity of diagram (13) expresses that Rel(F), applied to a relation R -X × X on X, yields a relation on F X.

Given a category of relations Rel(C), called the total category, the subcategory (also called a fibre) RelX consists of objects R - X × X and maps above the identity on X. For relations in Set, such maps are inclusions of relations. In general, these maps are unique, and writing R ≤ S iff there is an arrow from R to S turns the fibre into a poset. A relation lifting Rel(F) can be restricted to the fibres to give a functor Rel(F)X : RelX → RelFX. Since RelX and RelFX are posetal categories, Rel(F)X can be viewed as a monotone map.

For a map f : X → Y in C, we have the direct image and inverse image functors - f : RelX → RelY and f ∗ - : RelY → RelX. For relations on sets, we have f (R ⊆ X × X) = {(f(x), f(y)) | (x, y) ∈ R} and f ∗(S ⊆ Y × Y ) = {(x, y) ∈ X × X | (f(x), f(y)) ∈ S}. More generally, they are obtained as the factorisation and pullback in the left and right diagram below respectively

$$\begin{array}{ccc} R \xrightarrow{R} \begin{array}{c} \coprod\_{f}(R) \\ \coprod\_{f}(R) \\ \coprod\_{f\times f}(r) \end{array} & \begin{array}{c} f^\*(S) \\ \xrightarrow{f^\*(s)} \end{array} & \begin{array}{c} \xrightarrow{S} \\ \xrightarrow{f^\*(s)} \end{array} \\\ X\times X & \xrightarrow{f\times f} X\times Y \end{array} \tag{14}$$

It can further be shown that - f f ∗. We say that Rel(F): Rel(C) → Rel(D) preserves inverse images if Rel(F)X ◦ f ∗ = (F f)∗ ◦ Rel(F)Y .

In this context, *a bisimulation for a* B*-coalgebra* f : X → BX is a post-fixed point of the endofunctor f ∗ ◦Rel(B)X : RelX → RelX, i.e., a relation R - X ×X such that R ≤ f ∗ ◦ Rel(B)X(R). Bisimilarity is then obtained as the greatest fixed point ν(f ∗ ◦ Rel(B)X), if it exists. In Set a bisimulation is a relation R such that R ⊆ (f × f)−1(Rel(B)(R)), i.e., if xRy then f(x) Rel(B)(R) f(y).

# 4 Preserving and Reflecting Bisimilarity

In this section we show that, in the presence of an invertible step, bisimilarity is preserved and reflected by the step-induced lifting of the right adjoint, given some further mild conditions. This allows us to recover a number of existing results for concrete instances (Section 5).

Our approach is as follows:

Throughout this section we assume categories C and D as in Assumption 3.1, and an invertible step δ : BQ → QL with right inverse ι: QL → BQ (and P, Q, B, L as in Definition 2.1).

## 4.1 Preservation and reflection

We now make precise what it means for a monotone map h to preserve and reflect bisimulations. This will be instantiated to bisimulations, captured abstractly as post-fixed points of a monotone map f : Γ → Γ on a poset Γ, which typically consists of relations (Section 3). These are compared against a second type of bisimulations, modelled as post-fixed points of another monotone map g : Δ → Δ. This motivates the following definition.

Definition 4.1. *Let* Γ *and* Δ *be posets, and* f : Γ → Γ*,* g : Δ → Δ *monotone maps. A monotone map* h: Γ → Δ preserves post-fixed points *if* x ≤ f(x) *implies* h(x) ≤ g(h(x))*. It* reflects post-fixed points *if the converse implication holds.*

In the step setting of Eq. (1), bisimulations for B- and L-coalgebras can be represented as post-fixed points of monotone maps on posets of relations as in Section 3. More concretely:

The two can be compared via the restriction Rel(Q)X : RelX → RelQX of the functor Rel(Q). Indeed, our main objective is to show that in the presence of an invertible step, Rel(Q)X preserves and reflects post-fixed points representing bisimulations, and that it maps the greatest fixed point in RelX (bisimilarity on f) to the greatest fixed point in RelQX (bisimilarity on ιX ◦ Qf). In this context we speak about *preservation and reflection of bisimulations/bisimilarity*.

#### 4.2 Proof of preservation and reflection

We are now ready to prove preservation and reflection of bisimilarity, in the sense described in the previous subsection. First, the following basic lemma provides a method of showing preservation and reflection of post-fixed points, which will be useful for our purposes.

Lemma 4.2. *Let* Γ *and* Δ *be posets, and* f : Γ → Γ*,* g : Δ → Δ *and* h: Γ → Δ *monotone maps. Suppose that* h *has a left (lower) adjoint* k : Δ → Γ*, and the equality* gh = hf *holds. Then* h *maps the greatest fixed point of* f *to the greatest fixed point of* g*, when these exist;* h *preserves post-fixed points; and if* h *is order-reflecting, then* h *reflects post-fixed points.*

Categorically speaking, the equality gh = hf is an isomorphic step. Instantiated to our setting of interest, Lemma 4.2 gives us a method for proving preservation and reflection of bisimilarity: it suffices to show each of the following.

To obtain the required adjunction between the fibres RelX and RelQX, we first establish the adjunction Rel(P) Rel(Q) between the total relation categories. Given Theorem 3.1, we can lift the unit and counit of the adjunction P Q, using the transformations constructed in the following lemma.

Lemma 4.3. *Let* F : C→D *and* G: D→E *be functors, with* Rel(F): Rel(C) → Rel(D) *and* Rel(G): Rel(D) → Rel(E) *the corresponding relation liftings. Then we have a natural transformation* Rel(GF) → Rel(G) Rel(F)*. Further, if* G *preserves abstract epis, then there is also a natural transformation* Rel(G) Rel(F) → Rel(GF)*. Also, the constructed transformations are above the identity.*

We note that the first part is in [28, Exercise 4.4.6] and the result is proved for Set endofunctors in [9, Lemma 14.1]. This allows the lifting of the adjunction, which we note may also be obtainable from results on fibred adjunctions in [30,26], but a direct proof is quite straightforward; the main idea is to use Lemma 4.3 together with preservation of abstract epis by P.

Lemma 4.4. *The adjunction* P - Q: D→C *lifts to relations, i.e., the following diagram is commutative, and the unit and counit of the upper adjunction are above the unit and counit of* P -Q*.*

$$\mathop{\mathrm{Rel}}\limits\_{p} \underbrace{\mathop{\mathrm{Rel}}\limits\_{p} \left(\mathcal{D}\right)}\_{\mathcal{P}} \underbrace{\mathop{\mathrm{Rel}}\limits\_{p} \mathrm{Rel}(\mathcal{D})}\_{\mathcal{P}} $$

The relation lifting defined in Section 3 allows us to define endofunctors Rel(B), Rel(L) in the context of the above adjunction:

$$\operatorname{Rel}(B)\coprod\operatorname{Rel}(\mathcal{C})\xleftarrow{\operatorname{Rel}(P)}\operatorname{Rel}(\mathcal{D})\xrightarrow{\operatorname{Rel}(P)}\operatorname{Rel}(L)\tag{16}$$

In this setting, we may try to lift the step δ or its converse ι to this adjunction. It turns out that δ always lifts. For ι, there is a sufficient condition which is independent of ι itself: that Q preserves abstract epis. In both cases, this result follows essentially from Lemma 4.3.

Proposition 4.5. *For a forward step* δ *and backward step* ι*, we have:*

The condition that Q preserves abstract epis holds, e.g., in case it is the forgetful functor in an adjunction monadic over Set. This is because Eilenberg-Moore categories of monads on Set have (RegEpi, Mono)-factorisation systems, and the forgetful functor sends regular epis to epis in Set as discussed in [13, Example 2.3]. It also holds in the Stone-Set case, as Stone is a reflective subcategory of CHaus (which is equivalent to the category of algebras for the ultrafilter monad).

The lifted steps δ and ι give step-induced liftings of Rel(P) and Rel(Q) between Coalg(Rel(B)) and Coalg(Rel(L)). Since bisimulations can be equivalently presented as coalgebras for Rel(B) and Rel(L), these liftings can be used to capture preservation of bisimulations. But it is less obvious what reflection means in this context and how to prove it. For reflection of bisimulations by Rel(Q), we turn our attention to the fibres, as described in the beginning of this section.

As a consequence of Proposition 4.5 and of δ ◦ ι = id, we obtain the following result, which will later be used in the construction of a step on the fibres.

Lemma 4.6. *Let* δ *be an invertible step with right inverse* ι*, and suppose* Q *preserves abstract epis. Then* Rel(Q)LX ◦ Rel(L)X = ι ∗ X ◦ Rel(B)QX ◦ Rel(Q)X*.*

Adjoining the fibres Next, we construct an adjunction between the fibres RelX and RelQX. The usual restriction Rel(Q)X of Rel(Q) to the fibre RelX will be the right adjoint, similarly to the adjunction obtained earlier. To map back into the fibre RelX, we post-compose Rel(P)QX with - ε, the direct image functor obtained from the counit of the adjunction Rel(P) - Rel(Q). We note the similarity with results on fibred adjunctions in [30], where only adjunctions over a single base category are considered.

#### Lemma 4.7. We have an adjunction - ε ◦ Rel(P)QX -Rel(Q)X : RelX → RelQX.

The above lemma fulfils the first proof obligation stated in the beginning of Section 4.2. It now remains to show the second proof obligation, i.e., that we have an isomorphic step in the following setting: -

$$(\iota\_X \circ Qf)^\* \circ \operatorname{Rel}(B)\_{QX} \subsetneq \bigoplus\_{\mathbf{Rel}\_{QX}} \underbrace{\operatorname{Rel}\_{QX} \xleftarrow{\bullet \operatorname{Rel}(P)\_{QX}} \operatorname{Rel}\_X}\_{\operatorname{Rel}(Q)\_X} \uplus f^\* \circ \operatorname{Rel}(L)\_X} \times \tag{17}$$

To this end, we first show that Rel(Q) preserves inverse images, using the fact that we can obtain inverse images as pullbacks inside the category of relations. Since Rel(Q) is a right adjoint, it preserves these pullbacks.

Lemma 4.8. Rel(Q) preserves inverse images.

We are now ready to show the existence of the required isomorphic step.

Theorem 4.9. If Q preserves abstract epis, then for any L-coalgebra (X, f):

$$(\iota\_X \circ Qf)^\* \circ \operatorname{Rel}(B)\_{QX} \circ \operatorname{Rel}(Q)\_X = \operatorname{Rel}(Q)\_X \circ f^\* \circ \operatorname{Rel}(L)\_X \tag{18}$$

Proof. We have

$$(\iota\_X \circ Qf)^\* \circ \text{Rel}(B)\_{QX} \circ \text{Rel}(Q)\_X = (Qf)^\* \circ \iota\_X^\* \circ \text{Rel}(B)\_{QX} \circ \text{Rel}(Q)\_X \tag{19}$$

$$=(Qf)^{\*} \circ \operatorname{Rel}(Q)\_{LX} \circ \operatorname{Rel}(L)\_{X} \tag{20}$$

$$=\operatorname{Rel}(Q)\_X \circ f^\* \circ \operatorname{Rel}(L)\_X \tag{21}$$

where Eq. (19) is an application of a basic fact on inverse images (technically, that the poset fibration of relations is split), Eq. (20) holds by Lemma 4.6, and Eq. (21) holds by Lemma 4.8.

We now reach our main result on preservation and reflection of bisimulations and bisimilarity by Rel(Q)X.

Theorem 4.10. Let (X, f) be an L-coalgebra. Suppose that Q preserves abstract epis. Then Rel(Q)X maps bisimilarity on (X, f) (when it exists) to bisimilarity on Q(X, f). Further, Rel(Q)X preserves bisimulations and, if it is order-reflecting, also reflects bisimulations.

Proof. We have seen in Lemma 4.7, that Rel(Q)X has a left adjoint, and in Theorem 4.9, that in this setting we have an isomorphic step. The result now follows from Lemma 4.2.

While this result is formulated in terms of Rel(Q)X, we will also speak of simply Q preserving and reflecting both bisimulations and bisimilarity.

As a special case of Theorem 4.10, we recover (a version of) the following existing result found in [42,3,11,12].

Lemma 4.11. Assume functors B,L: C→C, and a natural transformation ι: L → B. Then the functor Id: Coalg(L) → Coalg(B) defined by (X, f) → (X, σX ◦ f) on objects and identity on morphisms, preserves bisimulations. If additionally ι has a left inverse, Id reflects bisimulations.

We briefly turn to the condition of order-reflectingness. As we are often interested in cases where the right adjoint is a forgetful functor in the context of an Eilenberg-Moore adjunction, it is useful to state the following.

Lemma 4.12. For a monad T with forgetful functor U : EM(T ) → C, the (restricted) lifting Rel(U)X is an order-reflecting map.

If C = Set in the above lemma, then Rel(U)X is just the inclusion of the poset of congruences RelX on an algebra X into the poset of all relations on its carrier.

In that case, we can also use the above to show preservation and reflection of behavioural equivalence. Two states of a coalgebra (in Set) are behaviourally equivalent if they can be identified by some coalgebra homomorphism. This can be captured more abstractly using kernel bisimulations (see, e.g., [44]). Since U is assumed to be a forgetful functor to Set, we simply define preservation and reflection of behavioural equivalence by U to mean that for any two states x, y of an L-coalgebra (X, f), x and y are behaviourally equivalent (for (X, f)) if and only if they are behaviourally equivalent for U(X, f).

It turns out that, in our setting, coincidence of bisimilarity and behavioural equivalence for L-coalgebras reduces to coincidence for B-coalgebras. This is stated in the following lemma; the essence is that U is easily shown to preserve behavioural equivalence.

Lemma 4.13. For a monad T, consider the Eilenberg-Moore adjunction F U : EM(T) → Set with functors L: EM(T) → EM(T) and B : Set → Set, and an invertible step δ : BU → UL. Further suppose that U preserves and reflects bisimilarity, and that B preserves weak pullbacks. Then bisimilarity and behavioural equivalence for L-coalgebras coincide (and hence, U preserves and reflects behavioural equivalence).

Remark 4.14. We conclude with a brief exploration of preservation and reflection by the restriction of the left adjoint Rel(P)X, in the setting of

$$f^\* \circ \mathsf{Rel}(B) \times \bigoplus\_{\mathsf{T}} \mathsf{Rel}\_X \xrightarrow{\mathsf{Rel}(P)\_X} \mathsf{Rel}\_{PX} \xrightarrow{\mathsf{L}} (\hat{\delta}\_X \circ Pf)^\* \circ \mathsf{Rel}(L)\_{PX} \tag{22}$$