Joël Ouaknine: Digitisation Techniques for Timed Systems

 

Abstract: This talk presents an overview of digitisation techniques and their applicability to the verification problem for timed systems (mostly timed automata). The basic question is this: Suppose that the integral behaviours of a system meet a given specification; under which conditions does this guarantee that the dense-time (or continuous) behaviours of the system also meet this specification?

Digitisation techniques answering this question were first introduced by Henzinger, Manna, and Pnueli in 1992. In practice, they are a very useful tool both for practical and theoretical (e.g., decidability) purposes. I would like to conclude the talk by presenting what I think are some interesting open problems for further research.

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.