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.