This directory contains files for Technical Report CSRG-394, entitled
"On Closure Under Stuttering", by Dimitrie Paun and Marsha Chechik

The contents of the directory are as follows:

0) README       (1 KB -- the ASCII file you are currently reading)
1) tr394.ps	(303 KB -- the PostScript version of the report)
2) tr394.ps.gz	(85 KB -- the PostScript compressed with "gzip")

If you have the UNIX "gunzip" program, get the file "tr394.ps.gz".
Remember to transfer the file in binary mode.  After the transfer, use
"gunzip" to extract the original document, then print it on a
PostScript printer.

If  you do not have  either of the programs  above, get the file "tr394.ps" in
ASCII mode and print it on a PostScript printer.

Should you have any questions or comments about  this technical report, please
contact	 chechik@cs.toronto.edu.



On Closure Under Stuttering

Dimitrie Paun      Marsha Chechik
July 1999

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~\cite{manna89} is a formalism that has been
extensively used by researchers for program specification and
verification.  One of the essential properties of LTL formulas is
\emph{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~\cite{dwyer98a,dwyer99}.