Time-Bounded Verification

Joel Ouaknine (Oxford University Computing Laboratory)

Info

Date	3rd June 2009 (week 6, Trinity Term 2009)
Time	12:00
Place	Rom 478, Oxford University Computing Laboratory

Abstract

We study the decidability and complexity of verification problems for timed automata over time intervals of fixed, bounded length. In particular, we investigate language inclusion for timed automata as well as model checking Metric Temporal Logic and monadic first- and second-order logics over the reals with order and the +1 function. We also consider the satisfiability problems for these logics and their relative expressiveness over bounded intervals. In the process we answer some long-standing open questions.