VSL Publications

Reexamining Two Results in Partial Order Reduction

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.
  1. por_tr_2011.pdf (paper)
Related Links
  1. Transparent Partial Order Reduction
  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