*
Thomas A. Henzinger,
Jean-Francois Raskin, and Pierre-Yves Schobbens*

A specification formalism for reactive systems defines a class of
omega-languages. We call a specification formalism *fully decidable*
if it is constructively closed under boolean operations and has a decidable
satisfiability (nonemptiness) problem. There are two important, robust
classes of omega-languages that are definable by fully decidable formalisms.
The *omega-regular languages* are definable by finite automata, or
equivalently, by the Sequential Calculus. The *counter-free omega-regular
languages* are definable by temporal logic, or equivalently, by the
first-order fragment of the Sequential Calculus. The gap between both
classes can be closed by finite counting (using automata connectives), or
equivalently, by projection (existential second-order quantification over
letters).

A specification formalism for real-time systems defines a class of
*timed* omega-languages, whose letters have real-numbered time stamps.
Two popular ways of specifying timing constraints rely on the use of clocks,
and on the use of time bounds for temporal operators. However, temporal
logics with clocks or time bounds have undecidable satisfiability problems,
and finite automata with clocks (so-called *timed automata*) are not
closed under complement. Therefore, two fully decidable restrictions of
these formalisms have been proposed. In the first case, clocks are
restricted to *event clocks*, which measure distances to immediately
preceding or succeeding events only. In the second case, time bounds are
restricted to *nonsingular intervals*, which cannot specify the exact
punctuality of events. We show that the resulting classes of timed
omega-languages are robust, and we explain their relationship.

First, we show that temporal logic with event clocks defines the same class
of timed omega-languages as temporal logic with nonsingular time bounds, and
we identify a first-order monadic theory that also defines this class.
Second, we show that if the ability of finite counting is added to these
formalisms, we obtain the class of timed omega-languages that are definable
by finite automata with event clocks, or equivalently, by a restricted
second-order extension of the monadic theory. Third, we show that if
projection is added, we obtain the class of timed omega-languages that are
definable by timed automata, or equivalently, by a richer second-order
extension of the monadic theory. These results identify three robust classes
of timed omega-languages, of which the third, while popular, is not definable
by a fully decidable formalism. By contrast, the first two classes are
definable by fully decidable formalisms from temporal logic, from automata
theory, and from monadic logic. Since the gap between these two classes can
be closed by finite counting, we dub them the *timed omega-regular
languages* and the *timed counter-free omega-regular languages*,
respectively.

*Proceedings of the
25th International Colloquium on Automata, Languages, and Programming*
(ICALP),
Lecture Notes in Computer Science,
Springer, 1998, pp. 580-591.

Download inofficial, sometimes updated PostScript / PDF document. © 1998 Springer.