## On the expressiveness and monitoring of Metric Temporal Logic

*Hsi-Ming Ho*, *Joël
Ouaknine*, and *James Worrell*
It is known that *Metric Temporal Logic* (MTL) is strictly less
expressive than the *Monadic First-Order Logic of Order and Metric*
(FO[<,+1]) when interpreted over timed words; this remains true even
when the time domain is bounded *a priori*. In this work, we
present an extension of MTL with the same expressive power as FO[<,+1]
over bounded timed words (and also, trivially, over time-bounded
signals). We then show that expressive completeness also holds in the
general (time-unbounded) case if we allow the use of rational
constants *q* ∈ **Q** in formulas. This
extended version of MTL therefore yields a definitive real-time
analogue of Kamp's theorem. As an application, we propose a
*trace-length independent* monitoring procedure for our extension of
MTL, the first such procedure in a dense real-time setting.

*Logical Methods in Computer Science* 15(2), 2019. 52 pages.

PDF
© 2019 Hsi-Ming Ho, Joël Ouaknine, and James Worrell.

Imprint / Data Protection