Expressiveness of Metric modalities for continuous time

TL;DR

This paper proves that certain counting modalities in metric temporal logic cannot be expressed by simpler modalities, demonstrating the limitations of finite metric temporal logics in capturing all temporal properties over the real line.

Contribution

It proves a conjecture by Pnueli, showing an infinite hierarchy of counting modalities not expressible in simpler temporal logics over the real line.

Findings

No finite metric temporal logic can express all counting modalities.

A sequence of counting modalities is not expressible in the temporal logic generated by previous ones.

The result holds over both the real line and positive reals.

Abstract

We prove a conjecture by A. Pnueli and strengthen it showing a sequence of "counting modalities" none of which is expressible in the temporal logic generated by the previous modalities, over the real line, or over the positive reals. Moreover, there is no finite temporal logic that can express all of them over the real line, so that no finite metric temporal logic is expressively complete.