# Events in Linear-Time Properties

### Abstract

For several decades, 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
used extensively for specifying properties of systems. When such
properties are *closed under stuttering*, verification tools can
utilize a partial-order reduction technique to
reduce the size of the model and thus analyze larger systems. If LTL
formulas do not contain the ``next'' operator, the formulas are closed
under stuttering, but the resulting language is not expressive enough
to capture many important properties, e.g., properties involving
events. Determining if an arbitrary LTL formula is closed under
stuttering is hard --- it has been proven to be
PSPACE-complete.

In this paper we relax the restriction on LTL that guarantees closure
under stuttering, introduce the notion of *edges* in the context
of LTL, and provide theorems that enable syntactic reasoning about
closure under stuttering of LTL formulas.