On nested depth first search
Gerard J. Holzmann, Doron Peled, Mihalis Yannakakis · DIMACS series in discrete mathematics and theoretical computer science · 1997
ABSTRACT. We show in this paper that the algorithm for solving the model checking problem with a nested depth-first search can interfere with algorithms that support partial order reduction. We introduce a revised version of the algorithm that guarantees compatibility. The change also improves the performance of the nested depth-first search algorithm when partial order reduction is not used. 1.