Action prefixes: reified synchronization paths in minimal component interaction automata

Component Interaction Automata provide a fitting model to capture and analyze the temporal facets of hierarchical-structured component-oriented software systems. However, the rules governing composition, as is typical for all automata-based approaches, suffer from combinatorial state explosion, an effect that can have significant ramifications on the successful application of the Component Interaction Automata formalism to real-world scenarios. We must, therefore, find some appropriate means to counteract state explosion – one of which is partition refinement through weak bisimulation. But, while this technique can yield the desired state space reduction, it does not consider synchronization cliques, i.e., groups of states that are interconnected solely by internal synchronization transitions. Synchronization cliques give rise to action prefixes that capture pre-conditions for a component’s ability to interact with the environment. Current practice does not pay attention to these cliques, but ignoring them can result in a loss of valuable information. For this reason we show, in this paper, how synchronization cliques emerge and how we can capture their behavior in order to make state space reduction aware of the presence of synchronization cliques