Partition refinement of Component Interaction Automata

provide a fitting model to capture and analyze the temporal facets of hierarchically-structured component-oriented software systems. However, the rules governing composition typically suffer from , an effect that can impede modeling languages, like , from being successful in real-world scenarios. We must, therefore, find some appropriate ways to counteract state explosion, one of which is through bisimulation, in particular, weak bisimulation. While this technique can yield the desired state space reduction, it does not consider , that is, groups of states that are interconnected solely by internal synchronization transitions. Synchronization cliques give rise to , local states that encapsulate pre-conditions for a component’s ability to interact with the environment. Furthermore, both the existence and the size of synchronization cliques can be used as an indicator for the success of partition refinement. In particular, the more frequent synchronization cliques are and the more states they entail, the more likely it is that partition refinement can reduce the state space. But, there may be other factors that impact the refinement process. For this reason, we study, in this paper, how partition refinement behaves under weak bisimulation, how synchronization cliques emerge when using weak bisimulation, how we make state space reduction through partition refinement aware of the existence of synchronization cliques, and what other attributes of specifications can provides us with additional cues to forecast the possible outcome of the partition refinement process.