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.