Time-bounded verification

Joël Ouaknine, Alexander Rabinovich, and James Worrell

We study the decidability and complexity of verification problems for timed automata over time intervals of fixed, bounded length. One of our main results is that time-bounded language inclusion for timed automata is 2EXPSPACE-complete. We also investigate the satisfiability and model-checking problems for Metric Temporal Logic (MTL), as well as monadic first- and second-order logics over the reals with order and the +1 function (FO(<,+1) and MSO(<,+1) respectively). We show that, over bounded time intervals, MTL satisfiability and model checking are EXPSPACE-complete, whereas these problems are decidable but non-elementary for the predicate logics. Nevertheless, we show that MTL and FO(<,+1) are equally expressive over bounded intervals, which can be viewed as an extension of Kamp's well-known theorem to metric logics.

It is worth recalling that, over unbounded time intervals, the various problems listed above are all undecidable.

Proceedings of CONCUR 09 (improved and expanded version), LNCS 5710, 2009. 19 pages.

PostScript / PDF © 2009 Springer-Verlag.

Imprint / Data Protection