Ho, Hsi-Ming and Ouaknine, Joël and Worrell, James - On the Expressiveness and Monitoring of Metric Temporal Logic

lmcs:4366 - Logical Methods in Computer Science, May 10, 2019, Volume 15, Issue 2
On the Expressiveness and Monitoring of Metric Temporal Logic

Authors: Ho, Hsi-Ming and Ouaknine, Joël and Worrell, James

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 \in \mathbb{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.

DOI : 10.23638/LMCS-15(2:13)2019
Volume: Volume 15, Issue 2
Published on: May 10, 2019
Submitted on: March 13, 2018
Keywords: Computer Science - Logic in Computer Science