## 1 Introduction  
Markov chains serve as the fundamental semantic model for a multitude of modeling formalisms employed in the reliability analysis and performance evaluation of complex systems, including Stochastic Petri nets [1, 2], Stochastic Automata Networks [3, 4], queuing networks [5, 6], and Markovian process algebras [7, 8]. Although the utilization of high-level specification formalisms greatly simplifies the creation of compositional and hierarchical quantitative models, even seemingly straightforward models can pose challenges due to a large number of states, making analysis a daunting task. To tackle this problem, exploring models with extensive state spaces without resorting to approximation or simulation techniques involves reducing the state space of the underlying Markov chain by aggregating states that exhibit equivalent behaviors [9, 10]. This state-based reduction technique is known as _lumping_. Various notions of lumping, including strong and weak lumping [11], exact lumping [9, 12], and strict lumping [13], have been introduced in the literature. The lumpability method enables efficient computation of exact performance indices [14] when the model is lumpable. It is widely recognized that not all Markov chains are inherently lumpable, particularly those originating from real-world applications. To overcome this limitation, the notion of _quasi-lumpability_ was introduced in [15], suggesting that transforming a quasi-lumpable Markov chain into a lumpable one allows for the application of steady state probability bounding methods [15; 16; 17; 18; 19] to obtain bounds on the performance indices of the original model. In [20], the concept of _proportional lumpability_ was introduced, expanding upon the original notion of lumpability. Unlike the broader definition of quasi-lumpability, proportional lumpability allows for the derivation of precise performance indices for the original process. Building on this foundation, our research in [21] delves deeper into the topic by juxtaposing proportional lumpability with other lumping definitions, such as weak lumpability [11; 22], and the concept of exact lumpability for ordinary differential equations (ODEs) [23; 24]. The definition of proportional lumpability entails identifying a function that assigns a positive coefficient to each state of the system. However, given the infinite set of potential functions, devising an efficient algorithmic technique to check or compute proportional lumpability is not immediately evident. This paper explores the properties of proportional lumpability and elaborates on three alternative characterizations. The first, proven in [21], enables efficient verification of whether a partition of the state space is induced by an equivalence relation representing proportional lumpability. The second, proven in [25], is used to design an algorithm to calculate the coarsest proportional lumpability of a given Markov chain in time \(O(|\mathcal{S}|^{4})\) with \(|\mathcal{S}|\) being the cardinality of the state space of the analyzed model. The third characterization is a novel contribution, and it allows us to improve on the above complexity by obtaining an algorithm for proportional lumpability running in \(O(|\mathcal{S}|^{2}\log|\mathcal{S}|)\). Similar to partition refinement algorithms used for the traditional concept of strong (or ordinary) lumpability, our approach demonstrates that computing the coarsest proportional lumpability refining a given initial partition is well defined, always yielding a unique solution. Furthermore, we demonstrate that the maximum proportional lumpability over an initial Markov chain, within a specified equivalence relation, can be interpreted as ordinary lumpability over a perturbation of the original chain. Consequently, we can leverage efficient algorithms for calculating the maximum lumpability over a Markov chain. The effectiveness of proportional lumpability is illustrated through the presentation of a comprehensive case study.