Real-time automata and the Kleene algebra of sets of real numbers

We study here the class of so-called real-time automata, which can be seen as timed automata with a single clock which is resetted at each transition. We are concerned with the problem of complementation. We find that in order to adapt the usual subset construction we have to remove "stuttering steps" in the automata. Stuttering steps are transitions between states labeled with the same symbol. To this end we introduce a Kleene algebra of sets of (positive) real numbers where the second operation (the one which in the Kleene algebras of languages is the concatenation) is addition of sets of real numbers. Addition models the process in which a stuttering step is removed by "fusing" the two adjacent states in a single state. We prove a normal form theorem for the subalgebra generated by finite unions of intervals with rational bounds. Then the results are lifted to the matrix level by defining a Kleene algebra of matrices of normal forms. These form the basis for a procedure for removing stuttering steps in which stuttering steps that involve the same symbol are removed simultaneously and the process is iterated for all symbols.

"Proceedings of 17th Annual Symposium on Theoretical Aspects of Computer Science (STACS'2000)", Lille, France, 17-19 February 2000, pages 279-289.

 gzipped postscript file ; also you may find  here  some slides I used.