Time-Bounded Verification

13 years 10 months ago
Time-Bounded Verification
Abstract. 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 satisfiability and model-checking problems listed above are all well-known to ...
Joël Ouaknine, Alexander Rabinovich, James Wo
Added 14 Aug 2010
Updated 14 Aug 2010
Type Conference
Year 2009
Authors Joël Ouaknine, Alexander Rabinovich, James Worrell
Comments (0)