For over a decade, researchers in formal methods tried to create formalisms that permit natural specification of systems and allow mathematical reasoning about their correctness. The availability of fully-automated reasoning tools enables more non-specialists to use formal methods effectively --- their responsibility reduces to just specifying the model and expressing the desired properties. Thus, it is essential that these properties be represented in a language that is easy to use and sufficiently expressive.
Linear-time temporal logic is a formalism that has been extensively used by researchers for program specification and verification. One of the essential properties of LTL formulas is closure under stuttering , i.e. their interpretation is not modified by transitions that leave the system in the same state. This property is important from both practical and theoretical prospectives.
In this paper we present a formal theory of closure under stuttering, give theorems that enable syntactic reasoning about it, introduce the notion of \emph{edges} in LTL formulas, and apply the theory to the pattern-based approach to specifying temporal formulas.