This paper presents a partial order reduction algorithm, called Two
phase, that preserves stutter free LTL properties. Two phase
dramatically reduces the number of states visited compared to previous
partial order reduction algorithms on most practical protocols. The
reason can be traced to a step of the previous algorithms, called the
{\em proviso} step, that specifies a condition on how a state that
closes a loop is expanded. Two phase avoids this step, and uses a new
execution approach to obtain the reductions. Two phase can be easily
combined with an on-the-fly model-checking algorithm to reduce the
memory requirements further.  Furthermore a simple but powerful
selective-caching scheme can also be added to Two phase. Two phase has
been implemented in a model-checker called PV (Protocol Verifier) and is
in routine use on large problems.