Nicolas Markey

Résumé

TPTL and MTL are two classical timed extensions of LTL. In this paper, we positively answer a 15-year-old conjecture that TPTL is strictly more expressive than MTL. But we show that, surprisingly, the TPTL formula proposed by Alur and Henzinger for witnessing this conjecture can be expressed in MTL. More generally, we show that TPTL formulae using only the F modality can be translated into MTL.

@inproceedings{fsttcs2005-BCM,
  author =              {Bouyer, Patricia and Chevalier, Fabrice and Markey,
                         Nicolas},
  title =               {On the Expressiveness of {TPTL} and {MTL}},
  editor =              {Ramanujam, R. and Sen, Sandeep},
  booktitle =           {{P}roceedings of the 25th {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'05)},
  acronym =             {{FSTTCS}'05},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {3821},
  pages =               {432-443},
  year =                {2005},
  month =               dec,
  doi =                 {10.1007/11590156_35},
  abstract =            {TPTL and MTL are two classical timed extensions of
                         LTL. In this paper, we positively answer a
                         15-year-old conjecture that TPTL is strictly more
                         expressive than MTL. But we show that, surprisingly,
                         the TPTL formula proposed by Alur and Henzinger for
                         witnessing this conjecture can be expressed in MTL.
                         More generally, we show that TPTL formulae using
                         only the \textbf{F} modality can be translated into
                         MTL.},
}