Time-Bounded Verification

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.