Revisiting the Expressiveness of Metric Temporal Logic : A tale of "Je t'aime, moi non plus."

Mohammed Aristide Foughali

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.

picture_as_pdf flag

Knowledge Graph

arrow_drop_up

Comments

Sign up or login to leave a comment