Resets vs. Aborts in Linear Temporal Logic
==========================================


There has been a major emphasis recently in the semiconductor
industry on designing industrial-strength property specification
languages (PSLs). Two major languages are ForSpecs and Sugar 2.0,
which are both extensions of Pnueli's LTL. Both ForSpecs and
Sugars directly support reset/abort signals, in which a check for
a property \psi may be terminated and declared successful by an
reset/abort signal, provided the check has not yet failed.
ForSpecs and Sugar 2.0, however, differ in their definition of
failure. The definition of failure in ForSpec is syntactic,
while the definition in Sugar 2.0 is semantic.  In this work we
examine the implications of this distinction between the two approaches,
which we refer to as the reset approach (for \ForSpec) and the
abort approach (for Sugar 2.0). In order to focus on the
reset/abort issue, we do not consider the full languages, which
are quite rich, but rather the extensions of LTL with the
reset/abort constructs.

We show that the distinction between syntactic and semantic
failure has a dramatic impact on the complexity of using the
language in a model-checking tool. We prove that Reset-LTL enjoys the
"fast-compilation property": there is a linear translation of
Reset-LTL formulas into alternating Buchi automata, which implies a
linear translation of reset-LTL formulas into a symbolic
representation of nondeterministic Buchi automata. In contrast,
the translation of Abort-LTL formulas into alternating Buchi
automata is nonelementary (i.e., cannot be bounded by a stack of
exponentials of a bounded height); each Abort yields an
exponential blow-up in the translation.  This complexity bounds
also apply to model checking; model checking Reset-LTL formulas is
exponential in the size of the property, while model checking
Abort-LTL formulas is nonelementary in the size of the property (the
same bounds apply to satisfiability checking).