Journal article icon

Journal article

On expressiveness and complexity in real-time model checking

Abstract:

Metric Interval Temporal Logic (MITL) is a popular formalism for expressing real-time specifications. This logic achieves decidability by restricting the precision of timing constraints, in particular, by banning so-called punctual specifications. In this paper we introduce a significantly more expressive logic that can express a wide variety of punctual specifications, but whose model-checking problem has the same complexity as that of MITL. We conclude that for model checking the most commo...

Expand abstract
Publication status:
Published

Actions


Access Document


Authors


Ouaknine, J More by this author
More by this author
Institution:
University of Oxford
Department:
Oxford, MPLS, Computer Science
Journal:
AUTOMATA, LANGUAGES AND PROGRAMMING, PT 2, PROCEEDINGS
Volume:
5126
Issue:
PART 2
Pages:
124-135
Publication date:
2008
DOI:
EISSN:
1611-3349
ISSN:
0302-9743
URN:
uuid:c854a274-a688-468d-bde0-1bb59b2fc4d9
Source identifiers:
291870
Local pid:
pubs:291870
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