Joel Ouaknine ( Oxford University Computing Laboratory )
- 12:00 3rd June 2009 ( week 6, Trinity Term 2009 )Rom 478, Oxford University Computing Laboratory
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.