On Expressiveness and Complexity in Real-time Model Checking

International audience 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 \emphpunctual specifications. In~this paper we~introdu...

Full description

Bibliographic Details
Main Authors: Bouyer, Patricia, Markey, Nicolas, Ouaknine, Joël, Worrell, James
Other Authors: Laboratoire Spécification et Vérification Cachan (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Computing Laboratory (OUCL), University of Oxford Oxford, Aceto, Luca and Damgård, Ivan and Goldberg, Leslie~Ann and Halldórsson, Magnús M. and Ingólfsdóttir, Anna and Walukiewicz, Igor
Format: Conference Object
Language:English
Published: HAL CCSD 2008
Subjects:
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Iceland
Online Access:https://hal.archives-ouvertes.fr/hal-01194597
https://hal.archives-ouvertes.fr/hal-01194597/document
https://hal.archives-ouvertes.fr/hal-01194597/file/BMOW-icalp08.pdf
https://doi.org/10.1007/978-3-540-70583-3_11
Description
Summary:International audience 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 \emphpunctual 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 commonly occurring specifications, such as invariance and bounded response, punctuality can be accommodated at no cost.

Similar Items