Online Monitoring of Metric Temporal Logic
Hsi-Ming Ho ( University of Oxford )
Recently it has been proved that over the real line, Metric Temporal Logic (MTL) with past modalities and rational constants is expressively complete for the monadic first-order logic of order augmented with unary functions +q, q \in Q. In this paper we show that this result does not extend to the pointwise semantics. However, a normal form used in the proof of expressive completeness over the real line turns out to be useful for online monitoring of MTL in the pointwise setting. This normal form rewrites an arbitrary MTL formula into an LTL formula over a set of atoms comprising bounded MTL formulas. We show that under a natural assumption that "consecutive events are not too far apart", it is possible to derive a similar normal form result under the pointwise semantics. Using this we obtain the first trace-length independent online monitoring procedure for MTL.