Partitioning state spaces of concurrent transition systems

Abstract EN

As the model-checking becomes increasingly used in the industry as an analysis support, there is a big need for efficient new methods to deal with the large real-size of concurrent transition systems.

We propose a new algorithm for partitioning the large state space modeling industrial designs as concurrent transition systems with hundreds of millions of states and transitions.

The produced partitions will be used by distributed processes for parallel system analysis.

The state space is supposed to be represented by a weighted Kripke structure (this is an extension of the Kripke structure where weights are associated with the states and with the transitions).

This algorithm partitions the weighted Kripke structure by performing a combination of abstraction-partition-refinement on this structure.

The algorithm is designed in a way that reduces the communication overhead between the processes.

The experimental results on large real designs show that this method improves the quality of partitions, the communication overhead and then the overall performance of the system analysis.