EF Games for Expressiveness in Time

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, the MTL-EF theorem allows us to establish the inability of an MTL fragment in distinguishing two timed behaviors. This technique gives remarkably simpler proofs for many existing results on expressiveness and it also answers some long-standing questions such as the Alur-Henzinger conjecture.