Intuitively, a formula is closed under stuttering when its interpretation
is not modified by transitions that leave the system in the same state.
For example, a formula []a is closed
under stuttering because no matter how much we repeat states, we cannot
change the value of a.
On the other hand, the formula oa
is not closed under stuttering. We can see that by considering a state
sequence in which a is true in the
first state and false in the second. Then oa
is
false if we evaluate it on this sequence, and true if we repeat the first
state.
For a more detailed information about this issue, please refer to Closure Under Stuttering in Temporal Formulas, Dimitrie O. Paun, M.Sc. Thesis, DCS, University of Toronto, April 1999.