Online monitoring of Metric Temporal Logic

Hsi-Ming Ho, Joël Ouaknine, and James Worrell

Current approaches to monitoring real-time properties suffer either from unbounded space requirements or lack of expressiveness. In this paper, we adapt a separation technique enabling us to rewrite arbitrary MTL formulas into LTL formulas over a set of atoms comprising bounded MTL formulas. As a result, we obtain the first trace-length independent online monitoring procedure for full MTL in a dense-time setting.

Proceedings of RV 14, LNCS 8734, 2014. 15 pages.

PDF © 2014 Springer-Verlag.

Imprint / Data Protection