Tags:compositional model checking, explanatory analysis and state space minimisation
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. Our 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. In this presentation we discuss the lessons we have learned from performing this elaborate study on performance results of compositional model checking. We encourage the audience to perform more structured benchmakrs in an controlled setting and to address the multiple measurment problem
To Compose, Or Not to Compose, That is the Question: An Analysis of Compositional State Space Generation