Explainability is a Game
for Probabilistic Bisimilarity Distances

Probabilistic bisimilarity, a fundamental notion introduced by Larsen and Skou [39], captures which states of a model with randomness are considered behaviourally equivalent. As shown by Katoen, Kemna, Zapreev, and Jansen [31], reducing a model by identifying states that are probabilistic bisimilar often speeds up probabilistic model checking. That is, the time it takes to reduce a model and subsequently check a property of the reduced model is often less than the time needed to check the property of the original model.

As shown by Giacalone, Jou, and Smolka [25], behavioural equivalences such as probabilistic bisimilarity are not robust. Even the smallest changes to the probabilities in the model may result in different states being identified as behaviourally equivalent and, hence, may lead to different reduced models. These models may even satisfy different properties.

Giacalone et al.  suggested distances as a robust alternative to equivalences. Desharnais, Gupta, Jagadeesan, and Panangaden [14] proposed a quantitative generalization of probabilistic bisimilarity: probabilistic bisimilarity distances (or distances for short). To each pair of states, a real number in the unit interval $[0,1]$ is assigned that captures the behavioural similarity of the states. The smaller this number, the more alike the states behave. As shown by Desharnais et al., states are probabilistic bisimilar if and only if their distance is zero.

During the last two decades, efficient algorithms have been developed to approximate and compute probabilistic bisimilarity distances (see, for example, the work of Tang [51]). Once we have computed that the distance between two states is, say $\frac{1}{8}$, it begs for an explanation. In this paper we address the question how to explain probabilistic bisimilarity distances.

Logic has been extensively used to explain behavioural equivalences. Logics have been designed such that for each pair of states that is not behaviourally equivalent there exists a formula of the logic such one state satisfies the formula and the other state does not. For example, for models with nondeterminism, such as labelled transition systems, bisimilarity, due to Milner [42] and Park [44], is a key behavioural equivalence. The Hennessy-Milner logic [27] provides a logical characterization of bisimilarity. For labelled Markov chains, which model systems with randomness, probabilistic bisimilarity is logically characterized by the probabilistic modal logic of [39]. Rady and Van Breugel [47] explained the distance of a pair of states by means of an infinite sequence of formulas of a logic. The major drawback of their approach is that the explanation is in general not finitely representable. In this paper, we use games to explain distances. As we will see, these can be finitely represented. Before introducing our game, we first review some related work from the literature as our approach is different from the commonly used Ehrenfeucht-Fraïssé-like games [19, 24], yet uses some ingredients of those games.

We start with formalizing the model of interest, labelled Markov chains, and the probabilistic bisimilarity distances by recalling several results from the literature. Given a finite set $X$, a function $\mu :X\to [0,1]$ is a probability distribution on $X$ if ${\sum }_{x\in X}\mu (x)=1$. We denote the set of probability distributions on $X$ by $𝒟(X)$. For $\mu \in 𝒟(X)$ and $A\subseteq X$, we often write $\mu (A)$ for ${\sum }_{x\in A}\mu (x)$. Similarly, for $\omega \in 𝒟(X\times X)$, $x\in X$, and $A\subseteq X$, we usually write $\omega (x,A)$ for ${\sum }_{a\in A}\omega (x,a)$. For $\mu \in 𝒟(X)$, we define the support of $\mu$ by $\mathrm{support}(\mu )=\{x\in X\mid \mu (x)>0\}$. To avoid clutter, for $\mu \in 𝒟(X)$ and $f:X\to ℝ$ instead of ${\sum }_{x\in X}\mu (x)f(x)$ we write $\mu \cdot f$.

Several examples of labelled Markov chains have already been provided in the introduction. The states are represented by circles, squares, and diamonds, the labels by colours as well as shapes, and the transitions by arrows decorated with the probabilities. For the remainder of this paper, we fix a labelled Markov chain . We define probabilistic bisimilarity by means of the set $\mathrm{\Omega }(\mu ,\nu )$, which is known as the transportation polytope of the probability distributions $\mu$ and $\nu$. The elements of $\mathrm{\Omega }(\mu ,\nu )$ are called couplings.

For each $\mu$, $\nu \in 𝒟(S)$, $\mathrm{\Omega }(\mu ,\nu )$ is a closed convex polytope. We denote the vertices of the transportation polytope by $V(\mathrm{\Omega }(\mu ,\nu ))$.

To define the probabilistic bisimilarity distances, it is convenient to partition the set of state pairs into 0-pairs, 1-pairs, and ?-pairs.

The set $S_0^2$ contains those state pairs that behave the same and, hence, have distance zero (see Theorem 2.6). We call these 0-pairs. The set $S_1^2$ contains those state pairs that have a different label and, therefore, are fundamentally differently and, hence, have distance one (see Definition 2.5). We call these 1-pairs. The set $S_{\mathrm{?}}^2$ contains the remaining state pairs. We call these ?-pairs. Note that some of these state pairs may have distance one, but cannot have distance zero (see Theorem 2.6). The probabilistic bisimilarity distances are defined in terms of the following function.

The functions in $S\times S\to [0,1]$ carry a natural partial order. For $d$, $e\in S\times S\to [0,1]$, we define $d⊑e$ if for all $s$, $t\in S$, $d(s,t)\le e(s,t)$. According to, for example, [16, Lemma 3.2], is a complete lattice. Since the function ${\mathrm{\Delta }}_1$ is monotone (see, for example, [51, Proposition 2.1.13]), we can conclude from the Knaster-Tarski fixed point theorem [32, 52] that ${\mathrm{\Delta }}_1$ has a least fixed point, which we denote by ${\delta }_1$. It maps each pair of states to a real number in the interval $[0,1]$: the probabilistic bisimilarity distance of the states. As we already mentioned, distance zero captures probabilistic bisimilarity.

The 0-pairs are probabilistic bisimilar. This can be explained by means of the games mentioned in Section 1.2. The 1-pairs have different labels, which explains their difference in behaviour. Therefore, the distances of the ?-pairs remain to be explained. Hence, for the remainder of this paper, we assume that $S_{\mathrm{?}}^2\ne \mathrm{\varnothing }$ and, as a result, $S_1^2\ne \mathrm{\varnothing }$.

As we already mentioned, a policy consists of a coupling of the transitions of states $s$ and $t$ for each ?-pair $(s,t)$.

Figure 3 and 4 provide examples of policies. The 0-pairs are blue rectangles, the 1-pairs are red rounded rectangles, and the ?-pairs are purple ellipses. For each ?-pair, its outgoing arrows labelled with probabilities represent a coupling. Given a policy, we can define the probability of reaching a 0- or 1-pair from any state pair as follows.

Since ${\mathrm{\Delta }}_{iP}$ can be shown to be a monotone function from a complete lattice to itself, we can conclude from the Knaster-Tarski fixed point theorem that ${\mathrm{\Delta }}_{iP}$ has a least fixed point. We denote the least fixed point of ${\mathrm{\Delta }}_{iP}$ by ${\delta }_{iP}$. For states $s$ and $t$, ${\delta }_{iP}(s,t)$ is the probability of reaching an $i$-pair with respect to the policy $P$.

The probabilistic bisimilarity distances can be characterized in terms of a policy that minimizes the probability of reaching a 1-pair.

A policy that captures the distances, that is, the probability of reaching a 1-pair from a state pair $(s,t)$ when using policy $P$ equals the distance of $s$ and $t$, we call optimal.

For states $s$ and $t$, the transportation polytope $\mathrm{\Omega }(\tau (s),\tau (t))$ is generally infinite. As a result, our game, if formulated in terms of all couplings, is infinite in general. However, as we will see below, we can restrict our attention to the vertices of the transportation polytope $\mathrm{\Omega }(\tau (s),\tau (t))$, making our game as well as the set of policies finite.

Even if we restrict ourselves to vertex policies, we can still characterize the distances in terms of reachability probabilities.

According to Theorem 3.3 and 3.6, optimal and optimal vertex policies exist. We denote the set of optimal policies by ${𝒫}_{\mathrm{opt}}$ and the set of optimal vertex policies by ${𝒱}_{\mathrm{opt}}$. The policies depicted in Figure 3 and 4 are optimal vertex policies. The following alternative characterization of optimal policies turns out to be very useful in several of our proofs.

For every policy that is not a vertex policy, there exists a vertex policy the support graph of which is a strict subgraph. Hence, the transitions can be matched in such a way that fewer state pairs need to be considered, resulting in a simpler explanation.

Let $i\in \{0,1\}$. Given an optimal policy $P$ and a pair of states $(s,t)$, we are interested in the expected length of paths from $(s,t)$ to $i$-pairs when using $P$. We restrict to only those paths that reach an $i$-pair, that is, it is a conditional expectation. For example, consider the policy in the middle of Figure 4. To reach the 1-pair (5, 6) starting from the state pair (0, 1), there are 2 paths, each with a probability of $\frac{1}{8}$, of length 2, 2 paths, each of probability $\frac{1}{16}$, of length 3, etc. The probability of reaching a 1-pair from state pair (0, 1) is $\frac{1}{2}$. Hence, the conditional expectation is $\frac{\frac{1}{8}2+\frac{1}{8}2+\frac{1}{16}3+\frac{1}{16}3+\mathrm{\cdots }}{\frac{1}{2}}=3$. As we have already seen, ${\delta }_{1P}(s,t)$ captures the probability of all paths that reach an 1-pair from $(s,t)$. However, when we restrict ourselves to optimal policies ${\delta }_{1P}(s,t)={\delta }_1(s,t)$. This represents the denominator of the conditional expectation. Since $P$ is optimal, the denominator is independent of $P$. Therefore, we omit it. Hence, in the following we only consider the numerator.

We define the function ${\delta }_0:S\times S\to [0,1]$ by ${\delta }_0(s,t)=1-{\delta }_1(s,t)$. Since ${\delta }_{iP}(s,t)$ captures the probability of reaching an $i$-pair from $(s,t)$, we can conclude that $(s,t)$ can reach an $i$-pair if and only if ${\delta }_{iP}(s,t)\ne 0$. Because $P$ is optimal, this is equivalent to ${\delta }_i(s,t)\ne 0$.

Note that $S_i^2\subseteq D_i\subseteq S_i^2\cup S_{\mathrm{?}}^2$. The expected lengths are defined in terms of the following function.

Since the set $S$ is finite and, therefore, the set $D_i$ is finite, the set of functions $D_i\to [0,\mathrm{\infty })$ endowed with the sup metric³³3The distance of $k$, $l\in D_i\to [0,\mathrm{\infty })$ is defined as ${\max }_{(s,t)\in D_i}|k(s,t)-l(s,t)|$. forms a nonempty complete metric space (see, for example, [49, Theorem 3.11]). Hence, ${\mathrm{\Lambda }}_{iP}$ is a function from a nonempty complete metric space to itself. To prove that ${\mathrm{\Lambda }}_{iP}$ has a unique fixed point, which we denote by ${\lambda }_{iP}$, we use the following generalization of Banach’s fixed point theorem. This result dates back at least as far as the sixties. Part (a) and (b) are Banach’s original fixed point theorem [4]. Part (c) can already be found in [34] and [12] contains part (d).

We denote $P$ restricted to $S_{\mathrm{?}}^2$ by $P_{\mathrm{?}}$, that is, $P_{\mathrm{?}}\in S_{\mathrm{?}}^2\to (S_{\mathrm{?}}^2\to [0,1])$.

From the above proposition we can conclude that ${\mathrm{\Lambda }}_{iP}$ is a power-contraction and nonexpansive.

As discussed in the introduction and illustrated in Figure 3, an optimal policy that maximizes the expected length of paths to 1-pairs is desirable. This maximal expected length is defined as follows.

An optimal policy that realizes that maximal expected length is called 1-maximal.

We denote the set of optimal 1-maximal policies by ${𝒫}_{\mathrm{opt}}^{\max }$ and the set of optimal 1-maximal vertex policies by ${𝒱}_{\mathrm{opt}}^{\max }$. Similar to Proposition 3.7, we provide an alternative characterization of 1-maximal that we use in several of our proofs.

Below we present a policy iteration algorithm that computes a 1-maximal optimal vertex policy from an optimal vertex policy. In our algorithm we use the following function.

The following theorem is crucial for proving that the vertex policy our algorithm computes is 1-maximal.

Our algorithm starts from an optimal vertex policy $P$, which can be obtained by the policy iteration algorithm of [51, Section 6.2]. It computes ${\lambda }_{1P}$ for that policy $P$ (line 1), which can be done by means of standard algorithms (see, for example, [3, Section 10.1.1]). As long as there is a state pair in $D_1\setminus S_1^2$ that is not locally 1-maximal with respect to the current policy (line 2), the policy at $(s,t)$ is improved to a locally 1-maximal choice (line 3). This boils down to solving a linear programming problem. After this change to the policy $P$, we recompute ${\lambda }_{1P}$ (line 4). The loop maintains the invariant that $P$ is an optimal vertex policy as $\omega$ in line 3 is a vertex and satisfies ${\delta }_1(s,t)=\omega \cdot {\delta }_1$ (see Proposition 3.7). At termination, we have that ${\lambda }_{1P}$ is a fixed point of ${\mathrm{\Lambda }}_1$ and, by Theorem 5.5, equals ${\lambda }_1$ and, therefore, is 1-maximal.

Next, we prove an exponential lower bound for the above algorithm.

Note that $C_n$ has $3n+8$ states and $6n+11$ transitions and, hence, is of size $𝒪(n)$. Applying the above algorithm to the labelled Markov chain $C_n$ results in an exponential number of iterations.

As we discussed in the introduction and Figure 4 illustrates, a 1-maximal optimal policy that minimizes the expected length of paths to 0-pairs is a preferable explanation. As in the previous section, we first capture the minimal expected length.

A 1-maximal optimal policy that matches that minimal expected length is called 0-minimal.

Below we present a policy iteration algorithm that computes a 0-minimal 1-maximal optimal vertex policy from a 1-maximal optimal vertex policy. In our algorithm we use the following function.

The key ingredient of the correctness proof of our algorithm is the following result.

Our algorithm that computes a 0-minimal 1-maximal vertex policy from a 1-maximal vertex policy (Algorithm 2) is very similar in structure to Algorithm 1. Instead of focussing on 1-pairs, we concentrate on 0-pairs. Furthermore, we maintain as a loop invariant that $P$ is not only an optimal vertex policy but also that it is 1-maximal.

Algorithm 1 and 2 both optimize locally in line 3 to obtain a global optimum. This may remind the reader of the “elegance” quote of Fijalkow et al. in the introduction.

Since probabilistic bisimilarity distances are symmetric, that is, ${\delta }_1(s,t)={\delta }_1(t,s)$ for all states $s$ and $t$, one may wonder whether ${\delta }_1(s,t)$ can be explained similarly to ${\delta }_1(t,s)$. We call a policy $P$ symmetric if $P(s,t)$ and $P(t,s)$ are mirror images.

We fix a total order $\prec$ on the set of states $S$. This allows us to turn a policy into a symmetric one as follows.

This construction preserves all the properties of policies in which we are interested.

As a result, once we have computed a 0-minimal 1-maximal optimal vertex policy $P$, we can turn it into a symmetric 0-minimal 1-maximal optimal vertex policy  $P_{\prec }$. Generally, such a symmetric policy is simpler as ${\delta }_1(s,t)$ is explained similarly to ${\delta }_1(t,s)$. In the graphical representation of a symmetric policy, we only need to represent the state pairs $(s,t)$ with $s⪯t$, where an arrow from $(s,t)$ to $(u,v)$ with $u\succ v$ is depicted as a twisted arrow.

We have implemented Algorithm 1 and 2 in Java⁴⁴4The code is available at github.com/antoNanahJi/Explainability. To compute an optimal vertex policy, we used a Java implementation⁵⁵5The code is available at bitbucket.org/discoveri/probabilistic-bisimilarity-distances. of the algorithm presented in [51, Section 6.2]. In our experimental evaluation we used the two examples of [51, Section 9.3], namely an example of two dies due to Knuth and Yao [33] and randomized quick sort, as well as the Miller-Rabin primality test [41, 46], the crowds protocol by Reiter and Rubin in [48], and the leader election protocol by Itai and Rodeh [29].

The experiments were run on an Intel machine with an i7-8700T CPU and 15 GB of RAM. For each of the five examples, we first computed an optimal vertex policy, then a 1-maximal optimal vertex policy, and finally a 0-minimal 1-maximal optimal vertex policy. We timed 55 trails for each of the three stages of the computation and report the average (and standard deviation) in milliseconds in Table 1. Since a Java virtual machine needs to perform just-in-time compilation and optimization, we discarded the first eight trails. Garbage collection was triggered in between trials to minimize its impact on our measurements.

As can be seen, the algorithms tend to perform well in practice despite the exponential lower bound. In most cases, computing the 1-maximal and 0-minimal optimal policies is significantly faster than computing optimal policies. Recall that if policy $P$ is optimal then ${\lambda }_{1P}$ captures the distances. Hence, once we have computed the distances by means of policy iteration, we can construct a symmetric 0-minimal 1-maximal optimal vertex policy that explains the distances, often taking less time than computing the distances.

Our implementation also provides a graphical representation (DOT format) of the policy.

We have shown that explainability is a game in the context of probabilistic bisimilarity distances of labelled Markov chains. More precisely, symmetric 0-minimal 1-maximal optimal vertex policies for the $1⁤\frac{1}{2}$-player games presented in this paper explain the distances.

Apart from the area of probabilistic model checking, distances similar to the ones studied in this paper also play a role in other fields including control theory [26], fault-tolerance [9], privacy [11], quantum computing [20], reinforcement learning [40], and systems-biology [38]. As a consequence, we anticipate that our results are widely applicable.

The main contributions of this paper are the following.

• $\mathrm{■}$

  We provide a unified overview of games related to probabilistic bisimilarity and probabilistic bisimilarity distances in the introduction of the paper.

• $\mathrm{■}$

  We argue that symmetric 0-minimal 1-maximal optimal vertex policies explain these distances.

• $\mathrm{■}$

  We develop algorithms to compute symmetric 0-minimal 1-maximal optimal vertex policies and prove them correct.

• $\mathrm{■}$

  We prove an exponential lower bound for the algorithm that computes a 1-maximal optimal vertex policy from an optimal vertex policy.

• $\mathrm{■}$

  We have implemented all algorithms in Java. The code is open-source.

Several questions remain open. For example, we conjecture that the algorithm that computes a 0-minimal 1-maximal optimal policy from a 1-maximal optimal policy also has an exponential lower bound. Determining upper bounds for both our algorithms is left for future work.

In [53], Vlasman introduced two properties of policies, label conflict and probabilistic bisimilar conflict, argued that policies free of such conflicts are desirable for explaining probabilistic bisimilarity distances, and presented algorithms to remove such conflicts from optimal policies. We have already shown that 1-maximal optimal policies are free of label conflicts (see [43]). It is an open problem whether a 0-minimal 1-maximal optimal policy is free of probabilistic bisimilar conflicts. We conjecture that “transitivity” of policies, which seems closely related to the fact that probabilistic bisimilarity distances satisfy the triangle inequality, may play a role in tackling that problem. Apart from symmetry and “transitivity,” it could be worthwhile exploring other forms of structure of policies to further reduce the complexity of the explanation.

We conjecture that the policy iteration algorithm of [51, Section 6.2], as well as Algorithm 1 and 2 can be modified so that they maintain that the policy is symmetric as a loop invariant. This may allows us to restrict our attention to only half of the state pairs currently being considered in the algorithm.

As we mentioned in the introduction, our game can be viewed as a Markov decision process presented by Tang in [51, Section 5.3]. Several definitions and results can be expressed in the parlance of Markov decision processes. For example, the function ${\mathrm{\Delta }}_1$ presented in Definition 2.5 can be seen as a Bellman equation (see, for example, [45, Section 4.3]) – note that a slight generalization of ${\mathrm{\Delta }}_1$ was already defined in, for example, [7, Definition 15], which predates Tang’s presentation of the Markov decision process by more than a decade. Similarly, for a policy $P$ and a state pair $(s,t)$, $P(s,t)$ can be seen a decision rule and Proposition 3.7 then characterizes a conserving decision rule (see, for example, [45, Section 6.2.4]).

Our results are related to the work of Busatto-Gaston et al. [8]. They consider bi-objective problems on Markov decision processes. In particular, they minimize the (conditional) expected number of steps to a target while guaranteeing the maximal probability of reaching it. In this paper, we consider three objectives (optimal, 1-maximal, and 0-minimal). They propose a simple two-step pruning algorithm. Our algorithms show similarities to their algorithm. For example, Definition 5.4 corresponds to pruning the Markov decision process by restricting to couplings $\omega$ that satisfy ${\delta }_1(s,t)=\omega \cdot {\delta }_1$. Since the size of the Markov decision process representing our game may be exponential in the number of states of the labelled Markov chain, we do not explicitly construct the Markov decision process, nor do we explicitly prune it.

The aim of our work is to provide a human-interpretable explanation of probabilistic bisimilarity distances. According to Theorem 3.3, for a policy $P$ we have that ${\delta }_{1P}$ provides an upper bound for ${\delta }_1$. As a result, a policy can also be viewed as a certificate (see, for example, [2] for work on certificates for Markov decision processes) for an upper bound of the probabilistic bisimilarity distances. In this case, we would aim for a small policy $P$ so that ${\delta }_{1P}$ can be computed quickly. We consider this an interesting line of future work.