Nicolas Markey

Résumé

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 commonly occurring specifications, such as invariance and bounded response, punctuality can be accommodated at no cost.

@inproceedings{icalp2008-BMOW,
  author =              {Bouyer, Patricia and Markey, Nicolas and Ouaknine,
                         Jo{\"e}l and Worrell, James},
  title =               {On Expressiveness and Complexity in Real-time Model
                         Checking},
  editor =              {Aceto, Luca and Damg{\aa}rd, Ivan and Goldberg,
                         Leslie Ann and Halld{\'o}rsson, Magn{\'u}s M. and
                         Ing{\'o}lfsd{\'o}ttir, Anna and Walukiewicz, Igor},
  booktitle =           {{P}roceedings of the 35th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'08)~-- Part~{II}},
  acronym =             {{ICALP}'08},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {5126},
  pages =               {124-135},
  year =                {2008},
  month =               jul,
  doi =                 {10.1007/978-3-540-70583-3_11},
  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 \emph{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
                         commonly occurring specifications, such as
                         invariance and bounded response, punctuality can be
                         accommodated at no cost.},
}