## Multi-Head Monitoring of Metric Temporal Logic

#### Abstract

We present a novel approach to the offline monitoring of specifications
expressed in metric temporal logic (MTL). Our monitoring algorithm exploits
multiple one-way reading heads that traverse a trace sequentially. We present
both theoretical and practical results that show this substantially improves
upon the state-of-the-art. In particular, our algorithm is the first offline
monitoring algorithm for MTL with past and bounded-future temporal operators
that is almost trace-length independent and outputs a trace of Boolean verdicts
denoting the monitored formula's satisfaction at every position in the input
trace. In addition, our algorithm's worst-case space complexity is linear in
the formula size, while previous algorithms were exponential. Moreover, we
compare our implementation of the algorithm with another almost trace-length
independent tool that outputs non-standard verdicts to achieve this space
complexity. Our tool used less memory and runs significantly faster, for
example yielding a 10-fold improvement on average on random formulas, while
producing a better output.

Paper draft