In this paper we reason about the notion of proportional lumpability, that generalizes the original definition of lumpability to cope with the state space explosion problem inherent to the computation of the performance indices of large stochastic models. Lumpability is based on a state aggregation technique and applies to Markov chains exhibiting some structural regularity. Proportional lumpability formalizes the idea that the transition rates of a Markov chain can be altered by some factors in such a way that the new resulting Markov chain is lumpable. It allows one to derive exact performance indices for the original process. We prove that the problem of computing the coarsest proportional lumpability which refines a given initial partition is well-defined, i.e., it has always a unique solution. Moreover, we introduce a polynomial time algorithm for solving the problem. This provides us further insights on both the notion of proportional lumpability and on generalizations of partition refinement techniques.
