Joël Ouaknine: Some decidability and undecidability results for timed automata

 

Abstract: Timed automata were introduced in the early 1990s by Alur and Dill. They are probably the most widely used paradigm to model real-time systems. Using a regions graph construction, Alur and Dill showed that the language-emptiness problem for timed automata is decidable, but that the language-universality problem, and hence also language inclusion, is undecidable.

In this talk, I will discuss the language-universality problem for open timed automata (timed automata for which all invariant and enabling clock constraints are "open", as in x < 3 rather than x <= 3, etc.). This question (whether the problem is decidable or not) is described as open by Henzinger and Raskin in a 2000 paper. Surprisingly, it turns out that language-universality for open timed automata is decidable if the (dense) time domain is "weakly monotonic" (several events are allowed at the same time), and undecidable otherwise.

Time permitting, I will also present some related decidability and undecidability results for open and closed timed automata, as well as for robust timed automata. The interest in considering these more restricted classes is that, when certain conditions are met, digitisation algorithms can be invoked which significantly accelerate model checking.

This is joint work with James Worrell.

CV: Joël Ouaknine has recently joined Ed Clarke's group as a postdoc. Prior to that he spent a couple of years as a postdoc/writing-up student with Mike Mislove at Tulane University. He received his PhD last year from Oxford, working with Mike Reed and Bill Roscoe on the relationship between discrete and continuous models for timed systems in CSP. His research interests include real-time and probabilistic systems, model checking, concurrency, semantics, and security.