Partial order reduction
From Wikipedia, the free encyclopedia
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.
In explicit state space exploration, partial order reduction usually refers to the specific technique of expanding a representative subset of all enabled transitions. This technique has also been described as model checking with representatives (Peled 1993).
[edit] Ample sets
Ample sets are an example of model checking with representatives. Their formulation relies on a separate notion of dependency. Two transitions are considered independent only if whenever they are mutually enabled, they cannot disable another and the execution of both results in a unique state regardless of the order in which they are executed. Transitions that are not independent, are dependent. In practice dependency is approximated using static analysis.
Ample sets for different purposes can be defined by giving conditions as to when a set of transitions is "ample" in a given state.
C0 
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.
Conditions C0 and C1 are sufficient for preserving all the deadlocks in the state space. Further restrictions are needed in order to preserve more nuanced properties. For instance, in order to preserve properties of linear temporal logic, the following two conditions are needed:
C2 If 
, 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).
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 symbolic model checking, partial order reduction can be achieved by adding more constraints (guard strengthening).
[edit] References
- _ Doron A. Peled, All from One, One for All: Model Checking Using Representatives, Proceedings of CAV'93, LNCS 697, Springer 1993, pp 409--423
- _ 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.
 |
This formal methods-related article is a stub. You can help Wikipedia by expanding it. |
