On the expressiveness of TPTL and MTL (Q2266987)

The paper is about two extensions of Linear-time Temporal Logic LTL: Metric Temporal Logic MTL and Timed Propositional Temporal Logic TPTL. In MTL the temporal `until' operator \textbf{U} of LTL is generalised to an operator \(\mathbf{U}_I\) where \(I\) is an interval of the rational numbers. In TPTL the until operator of LTL is complemented by constraints of the form \(x\leq c\), \(x< c\), \(x= c\), \(x> c\), and \(x\geq c\), where \(x\) is a temporal variable and \(c\) is a rational number. Furthermore, there is an operator `\(x\cdot\)' where \(x\) is a temporal variable whose role is to bind \(x\) to the current time point in a way similar to the binder `\(\downarrow \! x\)' of hybrid modal logics; see, e.g., the special issue on hybrid logics introduced by \textit{C. Areces} and \textit{P. Blackburn} [J. Log. Comput. 11, No. 5, 657--669 (2001; Zbl 0993.03011)]. As the domain of rational numbers is dense, both TPTL and MTL allow for both a pointwise and an interval-based semantics. The authors recall that TPTL is at least as expressive as MTL (the MTL operator \(\mathbf{U}_I\) being definable in TPTL) and that the conjecture that TPTL is strictly more expressive than MTL was stated in 1992 and has not been proved yet. They provide a proof by exhibiting for each of the semantics a TPTL formula that cannot be expressed in MTL.