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.
The final publication is available at link.springer.com.
Paper draft