Sciweavers

Share
CONCUR
2009
Springer

Time-Bounded Verification

4 years 2 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
Where CONCUR
Authors Joël Ouaknine, Alexander Rabinovich, James Worrell
Comments (0)
books