A Kleene/Büchi-like Theorem for Clock Languages

We propose in this paper a generalization of the famous Kleene/Buchi's theorem on formal languages, one of the cornerstones of theoretical computer science, to the timed model of clock languages. These languages extend the now classical timed languages introduced by Alur and Dill as a suitable model for real-time systems. As a corollary of our main result, we get a simple algebraic characterization of timed languages recognized by (updatable) timed automata.