Revisiting the Expressiveness of Metric Temporal Logic : A tale of "Je t'aime, moi non plus."
This addresses a foundational problem in formal verification for researchers, clarifying expressiveness in temporal logic, though it is incremental as it revises prior work.
The paper disproves a long-standing result by showing that the interval-based and pointwise semantics of Metric Temporal Logic are incomparable under standard models of timed executions, and proposes a new mixed semantics that embeds both.
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. % suggesting otherwise. % We then propose a new \emph{mixed} semantics that embeds both the pointwise and the interval-based ones.