The regular real-time languages

Abstract. A speci cation formalism for reactive systems de nes a class of!-languages. We call a speci cation formalism fully decidable if it is constructively closed under boolean operations and has a decidable satis ability (nonemptiness) problem. There are two important, robust classes of!-languages that are de nable by fully decidable formalisms. The!-regular languages are de nable by nite automata, or equivalently,by the Sequential Calculus. The counter-free!-regular languages are de nable by temporal logic, or equivalently,by the rst-order fragmentoftheSequential Calculus. The gap between both classes can be closed by nite counting (using automata connectives), or equivalently,by projection (existential second-order quanti cation over letters). A speci cation formalism for real-time systems de nes a class of timed!-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 satis ability problems, and nite automata with clocks (so-called timed automata) are not closed under complement. Therefore, two fully decidable restrictions of these formalismshave bee