Closure Under Stuttering


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.