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

Publication status:
Published

### Authors

More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Computer Science
Role:
Author
Journal:
AUTOMATA, LANGUAGES AND PROGRAMMING, PT 2, PROCEEDINGS
Volume:
5126
Issue:
PART 2
Pages:
124-135
Publication date:
2008-01-01
DOI:
EISSN:
1611-3349
ISSN:
0302-9743
Language:
English
Pubs id:
pubs:291870
UUID:
uuid:c854a274-a688-468d-bde0-1bb59b2fc4d9
Local pid:
pubs:291870
Source identifiers:
291870
Deposit date:
2013-11-17