On the Expressiveness of TPTL and MTL

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 in [4] 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.

• Type: Conference
• Year: 2005
• Where: FSTTCS
• Authors: Patricia Bouyer, Fabrice Chevalier, Nicolas Markey
• Keywords: 15-year-old Conjecture, Classical Timed Extensions, FSTTCS 2005, TPTL Formula