Reexamining Two Results in Partial Order Reduction

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.

@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}
}