# An Efficient Algorithm to Determine Probabilistic Bisimulation
## 2 Preliminaries  
Let \(S\) be a finite set. A _distribution_\(f\) over \(S\) is a function \(f:S\to[0,1]\) such that \(\sum_{s\in S}f(s)=1\). For each distribution \(f\), its _support_ is the set \(\{s\in S\mid f(s)>0\}\). The size of \(f\) is defined as the number of elements in its support, written as \(|f|\). The set of all distributions over a set \(S\) is denoted by \(\mathcal{D}(S)\). Distributions are lifted to act on subsets \(T\subseteq S\) by \(f[T]=\sum_{s\in T}f(s)\). For an equivalence relation \(R\) on \(S\), we use \(S/R\) to denote the set of equivalence classes of \(R\). We define \(s/R=\{\,t\in S\mid sR\,\}\) and, for a subset \(T\) of \(S\), we define \(T/R=\{\,s\in S\mid\exists t\in T\colon sRt\,\}\). A partition \(\pi=\{\,B_{i}\subseteq S\mid i\in I\,\}\) is a set of non-empty subsets such that \(B_{i}\cap B_{j}=\emptyset\) for all \(i,j\in I\) and \(\bigcup_{i\in I}B_{i}=S\). Each \(B_{i}\) is called a _block_ of the partition. Slightly ambiguously, we use \(S/R\) to denote the set of equivalence classes of \(R\) with respect to \(S\). Clearly, the set of equivalence classes of \(R\) forms a partition of \(S\). Reversely, a partition \(\pi\) of \(S\) induces an equivalence relation \(R_{\pi}\) on \(S\), by \(sR_{\pi}t\) iff \(s,t\in B\) for some block \(B\) of \(\pi\). A partition \(\pi\) is called a _refinement_ of a partition \(\varrho\) if each block of \(\pi\) is a subset of a block of \(\varrho\). Hence, each block in \(\varrho\) is a disjoint union of blocks from \(\pi\). We use probabilistic labeled transition systems as the canonical way to represent the behaviour of systems. Definition 1 (Probabilistic Labeled Transition System): A probabilistic labeled transition system (PLTS) for a set of actions \(Act\) is a pair \(\mathcal{A}=(\,S,\,\to)\) where  
* \(S\) is a finite set of states, and
* \(\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\, \,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\  
We also use the notation \(s\xrightarrow{a}u_{f}\) if \(s\xrightarrow{a}f\) for some \(f\in\mathcal{D}(S)\). As a matter of notation, we write \(u_{f}[T]\) for \(f[T]\) if probabilistic state \(u_{f}\) corresponds to the distribution \(f\). We sometimes use a so-called probabilistic transition \(u_{f}\mapsto_{p}s\) for \(0<p\leqslant 1\) and \(s\in S\) iff \(u_{f}(s)=p\). To stress \(S\cap U=\emptyset\), we refer to states \(s\in S\) as action states. Below, in particular in the complexity analysis, we use \(n_{a}=|S|\) as the number of action states, \(n_{p}=|U|\) as the number of probabilistic states, \(m_{a}=|\rightarrow|\) as the number of action transitions and \(m_{p}=\sum_{u_{f}\in U}|f|\) as the cumulative size of the support of the distributions corresponding to all probabilistic states. Note that \(m_{p}\geqslant n_{p}\) as every distribution has support of at least size \(1\). The following definition for probabilistic bisimulation stems from [1]. Definition 2: (Probabilistic Bisimulation). _Consider a PLTS \(\mathcal{A}=(\ S,\rightarrow)\). An equivalence relation \(R\subseteq S\times S\) is called a probabilistic bisimulation for \(\mathcal{A}\) iff for all states \(s,t\in S\) such that \(sR\) and \(s\xrightarrow{a}f\), for some action \(a\in Act\) and distribution \(f\in\mathcal{D}(S)\), it holds that \(t\xrightarrow{a}g\) for some distribution \(g\in\mathcal{D}(S)\), and \(f[B]=g[B]\) for each \(B\in S/R\)._  
_Two states \(s,t\in S\) are probabilistically bisimilar iff a probabilistic bisimulation \(R\) for \(\mathcal{A}\) exists such that \(sR\,t\), which we write as \(s\simeq_{p}t\). Two distributions \(f,g\in\mathcal{D}(S)\), and similarly two probabilistic states \(u_{f},u_{g}\in U\), are probabilistically bisimilar iff for all \(B\in S/\simeq_{p}\) it holds that \(f[B]=g[B]\), which we also denote by \(f\simeq_{p}g\) and \(u_{f}\simeq_{p}u_{g}\), respectively._  
By definition, probabilistic bisimilarity is the union of all probabilistic bisimulations.