When is Metric Temporal Logic Expressively Complete?

TL;DR

This paper characterizes when Metric Temporal Logic (MTL) is expressively equivalent to first-order logic, identifying specific sets of constants that determine their equivalence and demonstrating the role of counting modalities in achieving full expressiveness.

Contribution

It provides a precise characterization of constant sets for which MTL matches first-order logic's expressive power and shows how counting modalities extend MTL's expressiveness.

Findings

MTL and FO are equally expressive for certain rational constants.

Full FO expressiveness is achievable with counting modalities.

The paper generalizes previous results on MTL's expressive power.

Abstract

A seminal result of Kamp is that over the reals Linear Temporal Logic (LTL) has the same expressive power as first-order logic with binary order relation < and monadic predicates. A key question is whether there exists an analogue of Kamp's theorem for Metric Temporal Logic (MTL) -- a generalization of LTL in which the Until and Since modalities are annotated with intervals that express metric constraints. Hirshfeld and Rabinovich gave a negative answer, showing that first-order logic with binary order relation < and unary function +1 is strictly more expressive than MTL with integer constants. However, a recent result of Hunter, Ouaknine and Worrell shows that with rational timing constants, MTL has the same expressive power as first-order logic, giving a positive answer. In this paper we generalize these results by giving a precise characterization of those sets of constants for which MTL and first-order logic have the same expressive power. We also show that full first-order expressiveness can be recovered with the addition of counting modalities, strongly supporting the assertion of Hirshfeld and Rabinovich that Q2MLO is one of the most expressive decidable fragments of FO(<,+1).