A study on shuffle, stopwatches and independently evolving clocks (joint work with Ruggero Lanotte)

We show that stopwatch automata are equivalent with timed shuffle expressions, an extension of timed regular expressions with the shuffle operation. Since the emptiness problem is undecidable for stopwatch automata, and hence also for timed shuffle expressions, we introduce a decidable subclass of stopwatch automata called partitioned stopwatch automata. We give for this class an equivalent subclass of timed shuffle expressions and investigate closure properties by showing that partitioned stopwatch automata are closed under union, concatenation, star, shuffle and renaming, but not under intersection. We also show that partitioned stopwatch automata are equivalent with distributed timed automata, which are asynchronous compositions of timed automata in which time may evolve independently.

In "Proceedings of the 7th International Conference on Formal Modelling and Analysis of Timed Systems" (FORMATS'09), Lecture Notes in Computer Science vol 5813, p. 118-132, Springer Verlag.

 gzipped postscript file.
 
See also the Technical Report, LACL, 2009.