Journal article icon

Journal article

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 th...

Expand abstract
Publication status:
Published

Actions


Access Document


Authors


Ouaknine, J More by this author
Rabinovich, A More by this author
More by this author
Institution:
University of Oxford
Department:
Oxford, MPLS, Computer Science
Journal:
CONCUR 2009 - CONCURRENCY THEORY, PROCEEDINGS
Volume:
5710
Pages:
496-510
Publication date:
2009
DOI:
EISSN:
1611-3349
ISSN:
0302-9743
URN:
uuid:659e01d6-59ae-4325-8d9a-7d23e627afa4
Source identifiers:
296470
Local pid:
pubs:296470
Language:
English

Terms of use


Metrics



If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP