Stephen F. Siegel, Transparent Partial Order Reduction,
Formal Methods in System Design 40(1):1–19,
2012.

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 f, 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 f. In
this paper, we show that the invisibility restriction can be
relaxed: for propositions that only occur negatively in f, 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_tr_2011.pdf (preprint)
- tmc-repo.tgz (experimental archive with TMC source code)

@article{siegel:2012:transparent, Author = {Stephen F. Siegel}, Doi = {10.1007/s10703-011-0126-0}, Journal = {Formal Methods in System Design}, Number = {1}, Pages = {1--19}, Title = {Transparent Partial Order Reduction}, Volume = {40}, Year = {2012}} }

VSL | Publications