## 5 Conclusions  
In this study, we have delved into the concept of proportional lumpability and have introduced three distinct characterizations of this novel notion. These characterizations have laid the groundwork for the development of an efficient algorithm designed to automatically check the property of proportional lumpability for, even complex, CTMCs. The first characterization, as outlined in [21], provides a streamlined method for verifying whether a given relation aligns with proportional lumpability. Building upon this, a second characterization presented in [25] enables the creation of an algorithm for computing proportional lumpability by iteratively refining an initial relation. In this paper, we introduced a novel characterization that significantly enhances computational efficiency, leading to the development of an algorithm for proportional lumpability with a time complexity of \(O(|\mathcal{S}|^{2}\log|\mathcal{S}|)\). Figure 8: (**a**) Markov chain underlying the model presented in Table 2 and (**b**) its aggregation according to proportional lumpability. To demonstrate the efficacy of proportional lumpability, we conducted an extensive case study akin to the approach outlined in [26]. Specifically, we expanded upon the findings in [26] by analyzing a strongly lumpable model meticulously designed to probe selfish mining behaviors within the context of a public blockchain. The model examined in this paper represents an extended, more general version of the one presented in [26], tailored to capture a more realistic depiction of the blockchain state under investigation. Unlike the assumptions in [26], where all miners are assumed to possess identical computational capabilities for both mining and verification phases, our extended model acknowledges variations in miners' computational powers. This adjustment offers a more authentic portrayal of the blockchain state, enabling a deeper exploration of real-world scenarios with enhanced accuracy and relevance. It is crucial to emphasize that the case study presented in this paper diverges from the one discussed in [26]. Our primary focus revolves around investigating how verification time influences the efficacy of the selfish mining strategy. This examination assumes particular importance in the context of the dynamic landscape of blockchain technology, especially with the emergence of smart contracts. As highlighted in seminal work such as [45], the impact of verification time on selfish mining strategies cannot be underestimated, thereby rendering our model applicable to a wider array of scenarios. Our objective is to offer valuable insights into the concept of proportional lumpability and highlight the broader applications of partition refinement techniques. As part of our future research endeavors, we aim to explore the possibility of further relaxing the definition of proportional lumpability by introducing approximated semantics, aligning with the spirit of the proposed approaches, e.g., in [49; 50; 51; 52; 53]. This future direction aims to enhance the flexibility and applicability of proportional lumpability in various modeling scenarios. Furthermore, we aim to delve into the concept of _component substitution_ as outlined in [54], specifically for approximating solutions of stochastic models expressed within the framework of Performance Evaluation Process Algebra (PEPA). This approach is introduced to tackle the computational complexity inherent in analyzing PEPA models. The proposed method involves substituting certain components within the models to simplify the analysis process, potentially leading to more efficient and scalable solutions. This methodology hinges upon the notion of _behavioral independence_[55] to delineate specific restricted classes of models. Essentially, this property affirms that the actions of a specific group of components within a model are unaffected by the actions of other components. This characteristic serves as a valuable means of discerning independent and semi-independent behaviors.