## 3 Proportional Lumpability
### Three Alternative Characterizations of Proportional Lumpability  
We introduce three alternative characterizations of proportional lumpability. The first one, proven in [21], provides an efficient method to determine if a partition of a Markov chain's state space is induced by proportional lumpability. The second characterization, outlined in [25], has been utilized to describe an algorithm for computing the coarsest proportional lumpability of a given Markov chain in \(O(|\mathcal{S}|^{4})\) time. The third characterization is new, and it allows us to improve on the above complexity of obtaining an algorithm running in \(O(|\mathcal{S}|^{2}\log|\mathcal{S}|)\). First, for a given equivalence relation \(\sim\) over the state space of a CTMC, we denote by \(q_{\sim}(s)\) the sum of all transition rates from the state \(s\) to any state \(t\) such that \(s\
ot\sim t\), i.e., for all \(s\in\mathcal{S}\),  
\[q_{\sim}(s)=\sum_{t\
ot\sim s}q(s,t).\]  
The following theorem shows that proportional lumpability can be characterized in terms of \(q_{\sim}(s)\) by replacing \(\kappa(s)\) with \(q_{\sim}(s)\) in the original definition. **Theorem 3** (Characterization 1 of proportional lumpability [21]). : _Let \(X(t)\) be an ergodic CTMC with state space \(\mathcal{S}\) and \(\sim\) be an equivalence relation over \(\mathcal{S}\). The relation \(\sim\) is a proportional lumpability for \(X(t)\) if and only if for any equivalence classes \(S_{i},S_{j}\in\mathcal{S}/\sim\) with \(S_{i}\
ot=S_{j}\) and \(s,s^{\prime}\in S_{i}\),_  
1. \(q_{\sim}(s)\
ot=0\) _if and only if_ \(q_{\sim}(s^{\prime})\
ot=0\)__
2. _if_ \(q_{\sim}(s)\
ot=0\) _then_ \[\frac{q(s,S_{j})}{q_{\sim}(s)}=\frac{q(s^{\prime},S_{j})}{q_{\sim}(s^{\prime} )}.\]  
While the aforementioned characterization is useful for efficiently verifying whether a given relation conforms to proportional lumpability, its direct application in an algorithm for computing proportional lumpability refinement from an initial relation is not immediately apparent. As we will demonstrate below, if the relation undergoes changes during computation, \(q_{\sim}\) also changes. Consequently, an equality from item 2 that is false in the current step might become true later. Conversely, the following characterization of proportional lumpability is more straightforward to employ in defining a partition refinement algorithm for proportional lumpability. **Theorem 4** (Characterization 2 of proportional lumpability [25]). : _Consider a CTMC \(X(t)\) with a state space \(\mathcal{S}\), and let \(\sim\) denote an equivalence relation over \(\mathcal{S}\). The relation \(\sim\) is a proportional lumpability for \(X(t)\) if and only if for any equivalence classes \(S_{i},S_{j},S_{k}\in\mathcal{S}/\sim\) where \(S_{i}\
ot=S_{j}\), \(S_{i}\
ot=S_{k}\), and \(s,s^{\prime}\in S_{i}\),_  
1. \(q(s,S_{k})\
ot=0\) _if and only if_ \(q(s^{\prime},S_{k})\
ot=0\) _and_
2. _if_ \(q(s,S_{k})\
ot=0\)_, then_ \[\frac{q(s,S_{j})}{q(s,S_{k})}=\frac{q(s^{\prime},S_{j})}{q(s^{\prime},S_{k})}\]  
Figure 2: Aggregated CTMC representing the reliability of the system in Figure 1.  
In order to introduce our new characterization, we need to recall that, as for strong lumpability, also in the case of proportional lumpability the equivalence relation \(\mathcal{S}\times\mathcal{S}\) is always a proportional lumpability. However, this is not useful in the applications. On the other hand, the problem of \"refining\" a given initial equivalence relation in order to obtain a proportional lumpability is a challenging one. **Definition 4** (Maximum Proportional Lumpability Problem). : _Let \(X(t)\) be a CTMC with state space \(\mathcal{S}\) and let \(\mathcal{R}\) be an equivalence relation over \(\mathcal{S}\).