Title: Time-Bounded Verification

 Joel Ouaknine (Oxford)


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.

This is joint work with Alex Rabinovich and James Worrell.