Not Checking for Closure under Stuttering
-----------------------------------------

The model checker SPIN works better with specifications that are
closed under stuttering. Checking such specifications, SPIN can use
its partial-order reductions. It is hard to check whether a given
specification is closed under stuttering and it is pity to give up
SPIN's partial-order reductions.   
We suggest an algorithm that, given a program P and a specification
N of bad behaviors for P, checks the correctness of P with respect
to an extension N' of N that is guaranteed to be closed under
stuttering. In this check, SPIN can use its partial-order reductions.
If P is correct with respect to N', we conclude that it is correct
also with respect to N. If P is not correct with respect to N', we use
the counter-example that SPIN provides to determine whether the
program is correct with respect to N or that N is not closed under
stuttering.