A <EM>stuttering step</EM> is a 
 <A HREF = "step.html">step</A> 
that leaves all relevant variables unchanged.  (The relevant variables
are usually all the free variables of a formula.)  A stuttering step
represents a step in which something else (a variable representing
some part of the universe outside the system under consideration)
changes.  A specification of a system should allow stuttering steps,
since it should allow changes to parts of the universe external to the
system.  All TLA formulas are invariant under stuttering, meaning that
adding or removing stuttering steps does not affect whether or not a
 <A HREF = "behavior.html">behavior</A> 
satisfies a 
 <A HREF = "temporal-formula.html">temporal formula</A>.