Abstract: The algorithmic analysis of timed automata is fundamentally limited by the undecidability of the language inclusion problem (given two timed automata A and B, are all the timed traces accepted by B also accepted by A?). In this talk, we show that, if A is restricted to having a single clock, the problem becomes decidable. This is somewhat surprising, since it is well-known that there exist timed automata with a single clock that cannot be complemented. The crux of our proof consists in reducing the language inclusion problem to a reachability question on an infinite labeled transition system; we then construct a suitable well-quasi-ordering on this state space, which ensures the termination of our search algorithm.

One interesting potential application of this work is the ability to produce timed interface specifications for timed automata. We also discuss how our algorithm could be used to efficiently verify safety properties of networks of timed automata, via a compositional abstraction and refinement approach.

Finally, we complete the picture by showing that our restriction to timed automata with a single clock is essentially the only restriction making the language inclusion problem decidable.

(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.