## Expressive completeness for Metric Temporal Logic

*Paul Hunter*,
*Joël
Ouaknine*, and *James Worrell*
Metric Temporal Logic (MTL) is a generalisation of Linear
Temporal Logic in which the Until and Since modalities are
annotated with intervals that express metric constraints. A
seminal result of Hirshfeld and Rabinovich shows that over the
reals, first-order logic with binary order relation < and unary
function +1 is strictly more expressive than MTL with integer
constants. Indeed they prove that no temporal logic whose
modalities are definable by formulas of bounded quantifier depth
can be expressively complete for FO(<, +1). In this paper we show
the surprising result that if we allow unary functions +*q*, for
rational *q*, in first-order logic and correspondingly allow
rational constants in MTL, then the two logics have the same
expressive power. This gives the first generalisation of Kamp's
theorem on the expressive completeness of LTL for FO(<) to the
quantitative setting. The proof of this result involves a
generalisation of Gabbay's notion of separation.

*Proceedings of LICS 13*, 2013. 9 pages.

PDF
© 2013 IEEE Computer Society Press.

Imprint / Data Protection