Abstract: I would like to give a high-level overview of some recent work on timed automata. The abstract of the submitted paper is as follows, but I promise the talk will keep the technical details under the rug and focus on the big picture instead.

We consider several questions related to the use of digitization techniques for timed automata. These very successful techniques reduce dense-time language inclusion problems to discrete time, but are applicable only when the implementation is closed under digitization and the specification is closed under inverse digitization. We show that, for timed automata, the former (whether the implementation is closed under digitization) is decidable, but not the latter. We also investigate digitization questions in connection with the robust semantics for timed automata. The robust modelling approach introduces a timing fuzziness through the semantic removal of equality testing. Since its introduction half a decade ago, research into the robust semantics has suggested that it yields roughly the same theory as the standard semantics. This paper shows that, surprisingly, this is not the case: the robust semantics is significantly less tractable, and differs from the standard semantics in many key respects. In particular, the robust semantics yields an undecidable (non-regular) discrete-time theory, in stark contrast with the standard semantics. This makes it virtually impossible to apply digitization techniques together with the robust semantics. On the positive side, we show that the robust languages of timed automata remain recursive.

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.