The two key timed logics studied in literature are TPTL and MTL. Their several sublogics are obtained by placing restrictions such as bounded interval constraints, non-punctual constraints, etc., With such a variety of logics being studied, there is a need to systematically compare them from an expressiveness point-of-view.
About 20 years back, Alur and Henzinger conjectured that TPTL[U,S] is strictly more expressive than MTL[U,S]. Fifteen years later, a result by Bouyer et al. partially resolved this question by showing that MTL[U] is less expressive than TPTL[U]. We proved the original conjecture in its full generality using EF games for MTL.
Ehrenfeucht-Fra\"{\i}ss\'e games have been used in the study of expressiveness of various classical and temporal logics. We extend these to time and define MTL EF games. Essentially
