Revisiting the expressiveness of metric temporal logic : A tale of "Je t'aime, moi non plus."

TL;DR

This paper challenges the long-held belief that interval-based semantics of Metric Temporal Logic (MTL) are strictly more expressive than pointwise semantics, showing they are incomparable under standard models and proposing a mixed semantics.

Contribution

The paper disproves a 20-year-old result by demonstrating the incomparability of interval-based and pointwise MTL semantics and introduces a new mixed semantics combining both.

Findings

Interval-based and pointwise semantics are incomparable under standard models.

Disproves the longstanding belief that interval-based semantics are strictly more expressive.

Proposes a new mixed semantics that integrates both existing semantics.

Abstract

The expressiveness of Metric Temporal Logic (MTL) has been extensively studied throughout the last two decades. In particular, it has been shown that the \emph{interval-based} semantics of MTL is strictly more expressive than the \emph{pointwise} one. These results may suggest that enabling the evaluation of formulae at arbitrary time points \emph{instead of} positions of timed events increases the expressive power of MTL. In this paper, we formally argue otherwise. We demonstrate that under standard models of finite or non-Zeno infinite (action-based) timed executions, the interval-based and the pointwise semantics are incomparable, and therefore disprove a twenty-year-old result. We then propose a new \emph{mixed} semantics that embeds both the pointwise and the interval-based ones.