Alternating timed automata are a powerful extension of classical
Alur-Dill timed automata that are closed under all Boolean
operations. They have played a key role, among others, in providing
verification algorithms for prominent specification formalisms such as
Metric Temporal Logic. Unfortunately, when interpreted over an
infinite dense time domain (such as the reals), alternating timed
automata have an undecidable language emptiness problem.
The main result of this paper is that, over bounded time domains,
language emptiness for alternating timed automata is decidable (but
nonelementary). The proof involves showing decidability of a class of
parametric McNaughton games that are played over timed words and that
have winning conditions expressed in the monadic logic of order
augmented with the distance-one relation.
As a corollary, we establish the decidability of the time-bounded
model-checking problem for Alur-Dill timed automata against
specifications expressed as alternating timed automata.
Proceedings of LICS 10, 2010. 10 pages.
PDF
© 2010 IEEE Computer Society Press.