Portal de Periódicos da CAPES

Time-Bounded Verification

2009; Springer Science+Business Media; Linguagem: Inglês

10.1007/978-3-642-04081-8_33

1611-3349

Joël Ouaknine, Alexander Rabinovich, James Worrell,

VLSI and Analog Circuit Testing

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 be undecidable.