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 , 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 . 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 .
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).