Timed tree automata with an application to temporal logic

Finite automata on omega -sequenccs and omega -trees were introduced in the sixties by Buchi, McNaughton and Rabin. Finite automata on timed omega -sequences were introduced by Alur and Dill. In this paper we extend the theory of timed omega -sequences to omega -trees. The main motivation is the introduction of a new way to specify real-time systems and to study, using automata-theoretic techniques, branching-time temporal logics with timing constraints. We study closure properties and decision problems for the obtained classes of timed omega -tree languages. In particular, we show the decidability of the emptiness problem. As an application of the introduced theory, we give a new decidable branching time temporal logic (STCTL) whose semantics is based upon timed omega -trees.