Technische Universiteit Eindhoven (THE NETHERLANDS)
CADP (Construction and Analysis of Distributed Processes)
117,879 compositional generations
Compositional state space generation is a prominent approach to fight
the state space explosion problem. The basic principle is to generate
the state space of a system consisting of a number of parallel
components by iteratively adding a component and minimising the
result. To make the minimisation steps more effective, some actions
might be hidden. The idea of compositional state space generation is
that incremental minimisation leads to a lower maximum memory use than
composing and minimising the system monolithically. For a number of
cases, compositional state space generation has shown to perform
better than monolithical generation. However, there are also cases
where monolithical state space generation is more effective.
A crucial parameter for compositional state space generation is the order in which the components are added. Unfortunately, the number of possible orders is exponential in the number of parallel components, and the selection of an efficient order is still an unsolved issue. Several heuristics (such as root leaf reduction or smart reduction, both implemented in SVL) have been proposed, but unfortunately it is unpredictable whether the heuristics are an improvement over monolithic generation.
To better understand characteristics that help decide for or against compositional state space generation, this study considers 8 scalable models with varying network topologies (client-server, pipes, ring, shared variables, and peer-to-peer). For each model, for each number of parallel components (up to seven), and for several sets of actions to be hidden, the performance of all possible generation orders is measured. In total, this amounts to 117,879 compositional generations, requiring 2.5 CPU years of computation time.
In some cases, the authors observed differences of several orders of
magnitude for different orders. They found that root leaf reduction is
slightly more efficient, because smart (respectively, root leaf)
reduction requires fewer transitions in memory than the monolithic
approach in 80 (respectively, 94) out of 119 cases, and smart
reduction (respectively, root leaf) reduction finds an optimal
aggregation order for 29 (respectively, 40) cases.
Finally, they observed that "among the five network topologies we considered, none of them fundamentally rule out compositional aggregation as an effective technique."
Sander de Putter and Anton Wijs.
"To Compose, or Not to Compose, That Is the Question: An Analysis of
Compositional State Space Generation".
Proceedings of the 22nd International Symposium on Formal Methods
(FM'2018), Oxford, UK, LNCS vol. 10951, pages 485-504, Springer
Verlag, July 2018.
Available on-line at: https://www.win.tue.nl/~awijs/articles/composeornot-fm18.pdf
or from the CADP Web site in PDF or PostScript
Technische Universiteit Eindhoven
Software Engineering and Technology
Den Dolech 2
5612 AZ Eindhoven
Tel: +49 (0)241 80 21206
|Further remarks:||This case-study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|