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.
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). There are various versions of the method, the so-called stubborn set method (Valmari 1990), ample set method (Peled 1993), and persistent set method (Godefroid 1994).
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
...
Wikipedia