Timed regular expressions

In this article, we define tinned regular expressions, a formalism for specifying discrete behaviors augmented with timing information, and prove that its expressive power is equivalent to the tinned automata of Alur and Dill. This result is the timed analogue of Kleene Theorem and, similarly to that result, the hard part in the proof is the translation from automata to expressions. This result is extended from finite to infinite (in the sense of Buchi) behaviors. In addition to these fundamental results, we give a clean algebraic framework for two commonly accepted formalisms for timed behaviors, time-event sequences and piecewise-constant signals.