Thomas A. Henzinger, Jean-Francois Raskin and Pierre-Yves Schobbens
EECS Department
University of California, Berkeley
Technical Report No. UCB/CSD-99-1074
November 1999
http://www2.eecs.berkeley.edu/Pubs/TechRpts/1999/CSD-99-1074.pdf
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 the full 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.
BibTeX citation:
@techreport{Henzinger:CSD-99-1074,
Author = {Henzinger, Thomas A. and Raskin, Jean-Francois and Schobbens, Pierre-Yves},
Title = {Temporal Logics, Automata, and Classical Theories for Defining Real-Time Languages},
Institution = {EECS Department, University of California, Berkeley},
Year = {1999},
Month = {Nov},
URL = {http://www2.eecs.berkeley.edu/Pubs/TechRpts/1999/5711.html},
Number = {UCB/CSD-99-1074},
Abstract = {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). <p>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. <p>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 the full 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.}
}
EndNote citation:
%0 Report %A Henzinger, Thomas A. %A Raskin, Jean-Francois %A Schobbens, Pierre-Yves %T Temporal Logics, Automata, and Classical Theories for Defining Real-Time Languages %I EECS Department, University of California, Berkeley %D 1999 %@ UCB/CSD-99-1074 %U http://www2.eecs.berkeley.edu/Pubs/TechRpts/1999/5711.html %F Henzinger:CSD-99-1074