In computer science

Computer science

Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...

, partial order reduction is a technique for reducing the size of the state-space

State transition system

In theoretical computer science, a state transition system is an abstract machine used in the study of computation. The machine consists of a set of states and transitions between states, which may be labeled with labels chosen from a set; the same label may appear on more than one transition...

 to be searched by a model checking

Model checking

In computer science, model checking refers to the following problem:Given a model of a system, test automatically whether this model meets a given specification....

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 .
There are various versions of the method, the so-called stubborn set method , ample set method , and
persistent set method .

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 .

Stubborn sets

Stubborn sets make no use of an explicit independence relation. Instead they are defined solely through commutativity over
sequences of actions. A set is (weakly) stubborn at s, if the following hold.

D0 , if execution of the sequence is possible and leads to the state , then execution of the sequence is possibe and will lead to state

D1 Either is a deadlock, or such that , the execution of is possible.

These conditions are sufficient for preserving all deadlocks, just like C0 and C1 are in the ample set method.
They are, however, somewhat weaker, and as such may lead to smaller sets. The conditions C2 and C3 can also be
further weakened from what they are in the ample set method, but the stubborn set method is compatible with C2 and C3.

Others

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 .

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