**Smart Reduction**

*Pepijn Crouzen and Frédéric Lang*

Proceedings of Fundamental Approaches to Software Engineering FASE'2011 (Saarbrücken, Germany)

**Abstract:**

Compositional aggregation is a technique to palliate
state explosion - the phenomenon that the behaviour graph of a
parallel composition of asynchronous processes grows
exponentially with the number of processes - which is the main
drawback of explicit-state verification. It consists in building
the behaviour graph by incrementally composing and minimizing
parts of the composition modulo an equivalence relation.
Heuristics have been proposed for finding an appropriate
composition order that keeps the size of the largest
intermediate graph small enough. Yet the underlying composition
models are not general enough for systems involving elaborate
forms of synchronization, such as multiway and/or
nondeterministic synchronizations. We overcome this by proposing
a generalization of compositional aggregation that applies to an
expressive composition model based on synchronization vectors,
subsuming many composition operators. Unlike some algebraic
composition models, this model enables any composition order to
be used. We also present an implementation of this approach
within the CADP verification toolbox in the form of a new
operator called *smart reduction*, as well as experimental results
assessing the efficiency of smart reduction.

15 pages | PostScript |

Slides of F. Lang's lecture at FASE'2011: |