FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
To Compose, Or Not to Compose, That is the Question: An Analysis of Compositional State Space Generation

Authors: Sander de Putter and Anton Wijs

Paper Information

Title:To Compose, Or Not to Compose, That is the Question: An Analysis of Compositional State Space Generation
Authors:Sander de Putter and Anton Wijs
Proceedings:FM FMComplete
Editors: Jan Peleska, Klaus Havelund and Bill Roscoe
Keywords:compositional model checking, state space minimisation, explanatory analysis
Abstract:

ABSTRACT. To combat state space explosion several compositional verification approaches have been proposed. One such approach is compositional aggregation, where a given system consisting of a number of parallel components is iteratively composed and minimised. Compositional aggregation has shown to perform better (in the size of the largest state space in memory at one time) than classical monolithic composition in a number of cases. However, there are also cases in which compositional aggregation performs much worse. It is unclear when one should apply compositional aggregation in favor of other techniques and how it is affected by action hiding and the scale of the model. This paper presents a descriptive analysis following the quantitiative experimental approach. The experiments were conducted in a controlled test bed setup in a computer laboratory environment. A total of eight scaleable models with different network topologies considering a number of varying properties were investigated comprising 119 subjects. This makes it the most comprehensive study done so far on the topic. We investigate whether there is any systematic difference in the success of compositional aggregation based on the model, scaling, and action hiding. Our results indicate that both scaling up the model and hiding more behaviour has a positive influence on compositional aggregation.

Pages:18
Talk:Jul 17 10:00 (Session 117B)
Paper: