Stephen F. Siegel, Reexamining Two Results in Partial Order Reduction,
Technical Report UD-CIS-2011/06,
Department of Computer & Information Sciences, University of
Delaware, June 10, 2011

This paper reexamines two results dealing with ample-set-based
Partial Order Reduction (POR) for explicit-state model checking.
The first is a theorem asserting that POR and ``on-the-fly'' model
checking can be safely combined. It is shown that the proof of this
theorem contains a gap, though I am not aware of a counterexample to
the theorem itself. The second result asserts that a specific
relation between the reduced and full state spaces is a visible
simulation. This result is incorrect: the posited relation is not a
simulation, and a counterexample is given.

- por_tr_2011.pdf (paper)

@TechReport{siegel:2011:por-tr, author = "Stephen F.\ Siegel", title = "Reexamining Two Results in Partial Order Reduction", institution = {Department of Computer and Information Sciences, University of Delaware}, year = {2011}, number = {UDEL-CIS-2011/06} }

VSL | Publications