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.