Partial order reduction

In computer science, partial order reduction is a technique for reducing the size of the state-space to be searched by a model checking algorithm. It exploits the commutativity of concurrently executed transitions, which result in the same state when executed in different orders. Thus, this reduction technique is best suited for asynchronous systems.

Additional recommended knowledge

How to quickly check pipettes?

How to ensure accurate weighing results every day?

What is the Correct Way to Check Repeatability in Balances?

C0 ${ample(s)=\empty} \iff {enabled(s)=\empty}$

C1 If a transition $α$ depends on some transition relation in ample(s), this transition cannot be invoked until some transition in the ample set executed.

C2 If $enabled(s) \neq ample(s)$ , each transition in the ample set is invisible

C3 A cycle is not allowed if it contains a state in which some transition $α$ is enabled, but is never included in ample(s) for any states s on the cycle.

These conditions are sufficient for an ample set, but not necessary conditions (Clarke et al. 1999). The premises of cutting a state out is that the state will not lead to some property-violate-states that cannot be uncovered by other states in the ample set. As those erroneous states cannot be known in advance, while exploring the state space, we use those conditions.

There are also other notations for partial order reduction. One of the commonly used is the persistent set/sleep set algorithm. Detailed information can be found in Patrice Godefroid's thesis (Godefroid 1994).

In explicit model checking, partial order reduction can be achieved by discovering the independent transitions. In symbolic model checking, partial order reduction can be achieved by adding more constraints (guard strengthening).

References

^_ Edmund M. Clarke, Jr., Orna Grumberg and Doron A. Peled, Model Checking, MIT Press, 1999.
^_ Patrice Godefroid, Partial-Order Methods for the Verification of Concurrent Systems -- An Approach to the State-Explosion Problem, PhD. thesis, University of Liege, Computer Science Department, 1994, download thesis as PostScript.
The Spin Model Checker: Primer and Reference Manual, Gerard J. Holzmann, Addison-Wesley, ISBN 0-321-22862-6.