Transparent partial order reduction
Partial Order Reduction (POR) techniques improve the basic model checking algorithm by reducing the numbers of states and transitions explored in verifying a property of the model. In the "ample set" POR framework for the verification of an LTL-X formula phi, one associates to each state s a subset T (s) of the set of all transitions enabled at s. The approach requires that whenever T (s) is a proper subset, the transitions in T (s) must be invisible, i.e., their execution can never change the truth values of the atomic propositions occurring in phi. In this paper, we show that the invisibility restriction can be relaxed: for propositions that only occur negatively in phi, it suffices that the transitions in T (s) merely never change the truth value from true to false, and for those that occur only positively, from false to true. This opens up opportunities for reduction, in many commonly occurring scenarios, that would not be allowed by the stricter invisibility criterion.
transparent partial order reduction model checking verification invisibility