Experimental Analysis of Compositional State Space Generation Strategies

Organisation:	Technische Universiteit Eindhoven (THE NETHERLANDS)
Method:	EXP
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Domain:	Distributed Systems
Period:	2018
Size:	129 examples 117,879 compositional generations
Description:	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.
Conclusions:	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."
Publications:	[DePutter-Wijs-18] 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
Contact:	Anton Wijs Technische Universiteit Eindhoven MetaForum 6.077 Software Engineering and Technology Faculteit Informatica Den Dolech 2 5612 AZ Eindhoven THE NETHERLANDS Tel: +49 (0)241 80 21206 Email: [email protected]
Further remarks:	This case-study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page