The expressiveness of MTL with counting

TL;DR

This paper proves that extending Metric Temporal Logic (MTL) with counting modalities makes it expressively complete for the first-order logic of order and metric, highlighting the importance of counting in temporal logic expressiveness.

Contribution

It demonstrates that MTL extended with counting modalities (MTL+C) is fully expressive for FO(<,+1), resolving a longstanding open problem.

Findings

MTL+C is expressively complete for FO(<,+1)

Counting modalities enable full expressiveness of MTL

Supports the significance of Q2MLO as the most expressive decidable fragment

Abstract

It is well known that MTL with integer endpoints is unable to express all of monadic first-order logic of order and metric (FO(<,+1)). Indeed, MTL is unable to express the counting modalities $C_n$ that assert a properties holds $n$ times in the next time interval. We show that MTL with the counting modalities, MTL+C, is expressively complete for FO(<,+1). This result strongly supports the assertion of Hirshfeld and Rabinovich that Q2MLO is the most expressive decidable fragments of FO(<,+1).