# zbMATH — the first resource for mathematics

On the expressiveness and monitoring of metric temporal logic. (English) Zbl 07056237
Summary: It is known that Metric Temporal Logic ($$\mathsf{MTL}$$) is strictly less expressive than the Monadic First-Order Logic of Order and Metric ($$\mathsf{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 $$\mathsf{MTL}$$ with the same expressive power as $$\mathsf{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 $$\mathsf{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 $$\mathsf{MTL}$$, the first such procedure in a dense real-time setting.
##### MSC:
 03B70 Logic in computer science 68 Computer science
##### Keywords:
computer science; logic in computer science
CESAR; SPIN
Full Text: