Nicolas Markey

Abstract

TPTL and MTL are two classical timed extensions of LTL. In this paper, we prove the 20-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 modality F can be translated into MTL.

@article{icomp208(2)-BCM,
  author =              {Bouyer, Patricia and Chevalier, Fabrice and Markey,
                         Nicolas},
  title =               {On the Expressiveness of {TPTL} and {MTL}},
  publisher =           {Elsevier},
  journal =             {Information and Computation},
  volume =              {208},
  number =              {2},
  pages =               {97-116},
  year =                {2010},
  month =               feb,
  doi =                 {10.1016/j.ic.2009.10.004},
  abstract =            {TPTL and MTL are two classical timed extensions
                         of~LTL. In~this paper, we prove the 20-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 \emph{can} be expressed
                         in~MTL. More generally, we show that TPTL formulae
                         using only modality~F can be translated into~MTL.},
}