Enhancing Partial-Order Reduction via Process Clustering

Key words: concurrency -- state explosion -- formal verification -- partial-order reduction -- (LTL) model checking -- SPIN

Partial-order reduction is a well-known technique to cope with the state-space-explosion problem in the verification of concurrent systems. Using the hierarchical structure of concurrent systems, we present an enhancement of the partial-order-reduction scheme of [1,2]. A prototype of the new algorithm has been implemented on top of the verification tool SPIN. The first experimental results are encouraging.

  1. G.J. Holzmann and D. Peled. An Improvement in Formal Verification. In D. Hogrefe and S. Leue, editors, Formal Descriptions Techniques VII, FORTE '94, pages 197-211. Chapman & Hall, 1995.

  2. D. Peled. Combining Partial Order Reductions with On-the-fly Model Checking. In D.L. Dill, editor, Computer Aided Verification, CAV '94, LNCS 818, pages 377-390. Springer, 1994.

The full version is not available, because the report is superseded by the following publication:

T. Basten, D. Bošnački, and M.C.W. Geilen. Cluster-Based Partial-Order Reduction. Automated Software Engineering, An International Journal, 11(4):365-402, October 2004. (abstract / pdf) © Kluwer Academic Publishers.

Back to the list of technical reports.