In computer science, partial order reduction is a method used to make the process of searching through a set of possible situations easier for tools like model checking or planning and scheduling systems. It uses the fact that certain actions can be done in different orders without changing the final result.

When exploring the set of possible situations, partial order reduction often involves looking at a smaller group of actions that represent all possible choices. This method is sometimes called "model checking with representatives." There are several ways to apply this technique, including the stubborn set method, the ample set method, and the persistent set method.

Ample sets

Ample sets are an example of model checking using representatives. They depend on a separate idea of dependency. Two transitions are considered independent only if they do not prevent each other from happening when both are allowed to occur. When both transitions happen, they always lead to the same final state, no matter the order. Transitions that are not independent are considered dependent. In practice, dependency is estimated using static analysis.

Ample sets can be defined for different purposes by setting rules that determine when a group of transitions is "ample" in a specific state.

C0: ample(s) is empty if and only if enabled(s) is empty.
C1: If a transition α depends on a transition in ample(s), it cannot occur until a transition in the ample set is executed.

Rules C0 and C1 are enough to ensure all deadlocks in the state space are preserved. Additional rules are needed to preserve more detailed properties. For example, to preserve properties of linear temporal logic, the following two rules are required:

C2: If enabled(s) is not equal to ample(s), every transition in the ample set must be invisible.
C3: A cycle is not allowed if it includes a state where a transition α is enabled but is never part of ample(s) for any states on the cycle.

These rules are sufficient for defining an ample set, but they are not the only possible conditions.

Stubborn sets

Stubborn sets do not rely on explicit independence relations. Instead, they are defined only by how actions can be rearranged in sequences. A set T(s) is (weakly) stubborn at state s if the following conditions are met.

D0: For every action a in T(s), and for every sequence of actions b₁, …, bₙ not in T(s), if performing the sequence b₁, …, bₙ, a is possible and leads to a new state s', then performing the sequence a, b₁, …, bₙ is also possible and leads to the same state s'.

D1: Either s is a deadlock (a state where no actions can proceed), or there exists at least one action a in T(s) such that performing any sequence of actions b₁, …, bₙ not in T(s) followed by a is possible.

These conditions ensure that all deadlocks are preserved, similar to conditions C0 and C1 in the ample set method. However, they are slightly less strict, which may result in smaller sets. Conditions C2 and C3 can also be relaxed compared to their use in the ample set method, but the stubborn set method works with the same C2 and C3 conditions.

Others

Other ways to describe partial order reduction include the persistent set / sleep set algorithm. More details about this method are described in Patrice Godefroid's thesis.

In symbolic model checking, partial order reduction can be done by adding more constraints, known as guard strengthening. Additional uses of partial order reduction include tasks related to automated planning.