Timed Shuffle Expressions

We show that stopwatch automata are equivalent to timed shuffle  expressions, an extension of timed regular expressions with the shuffle operation. This implies that the emptiness problem for timed shuffle expressions is undecidable. The result holds for both timed state sequence semantics and timed event sequence semantics of automata and expressions.

Similarly to timed regular expressions, our timed shuffle expressions employ renaming. But we show that even when renaming is not used, shuffle regular expressions still have an undecidable emptiness problem. This solves in the negative a conjecture of Asarin on the possibility to use shuffle to define timed regular languages.

We also define a subclass of timed shuffle expressions which can be used to model preemptive scheduling problems. Expressions in this class are in the form $(E_1 \shuf \ldots \shuf E_n) \wedge E$, where $E_i$ and $E$ do not use shuffle. We show that emptiness checking within this class is undecidable too.

"Proceedings of 16th International Conference on Concurrency Theory (CONCUR'05)", San Francisco, Ca., 23-26 August 2005, Springer Verlag, Lecture Notes in Computer Science, pages 95-109, 2005.

 gzipped postscript file.