Skip to Main content Skip to Navigation
Conference papers

Smart Reduction

Pepijn Crouzen 1 Frédéric Lang 2 
2 VASY - System validation - Research and applications
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
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.
Document type :
Conference papers
Complete list of metadata

Cited literature [32 references]  Display  Hide  Download
Contributor : Christine Mckinty Connect in order to contact the contributor
Submitted on : Tuesday, March 1, 2011 - 4:51:17 PM
Last modification on : Sunday, June 26, 2022 - 9:33:38 AM
Long-term archiving on: : Monday, May 30, 2011 - 3:00:00 AM


Files produced by the author(s)


  • HAL Id : inria-00572535, version 1



Pepijn Crouzen, Frédéric Lang. Smart Reduction. Proceedings of Fundamental Approaches to Software Engineering (FASE'2011), Mar 2011, Saarbrucken, Germany. pp.111-126. ⟨inria-00572535⟩



Record views


Files downloads