Online Monitoring of Metric Temporal Logic
Hsi-Ming Ho ( University of Oxford )
- 11:30 15th May 2013 ( week 4, Trinity Term 2013 )051
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.