Alternating Timed Automata over Bounded Time

13 years 4 months ago
Alternating Timed Automata over Bounded Time
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 non-elementary). 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 monadic logic over the signature with order and the +1 function. As a corollary, we establish the decidability of the time-bounded model-checking problem for Alur-Dill timed automata against specifications expressed as alternating tim...
Mark Jenkins, Joël Ouaknine, Alexander Rabino
Added 29 Jan 2011
Updated 29 Jan 2011
Type Journal
Year 2010
Where LICS
Authors Mark Jenkins, Joël Ouaknine, Alexander Rabinovich, James Worrell
Comments (0)