Cluster-Based Partial-Order Reduction

13 years 5 months ago
Cluster-Based Partial-Order Reduction
The verification of concurrent systems through an exhaustive traversal of the state space suffers from the infamous state-space-explosion problem, caused by the many interleavings of actions of different processes in the system. Partialorder reduction is a well-known technique to tackle this problem. In this paper, we present an enhancement of the partial-order-reduction scheme of Holzmann and Peled that uses the hierarchical structure of concurrent systems. Our technique tries to contain dependencies between actions within clusters of processes, capitalizing on the independence of actions in different clusters to reduce the state space to be verified while preserving properties of interest. The paper starts with a formalization of the partial-order-reduction technique and continues with a presentation of our enhanced technique, including a correctness argument. The new technique has been implemented in the verification tool SPIN. We present implementation details, some small experimen...
Twan Basten, Dragan Bosnacki, Marc Geilen
Added 16 Dec 2010
Updated 16 Dec 2010
Type Journal
Year 2004
Where ASE
Authors Twan Basten, Dragan Bosnacki, Marc Geilen
Comments (0)