Monitoring Algorithms for Metric Temporal Logic

From FSL
Revision as of 12:30, 24 February 2016 by Grosu (Talk | contribs)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

Monitoring Algorithms for Metric Temporal Logic
Prasanna Thati and Grigore Rosu
RV'05, Electronic Notes in Theoretical Computer Science 113, pp 145-162. 2005
Abstract. Program execution traces can be so large in practical testing and monitoring applications that it would be very expensive, if not impossible, to store them for detailed analysis. Monitoring execution traces {\em without storing} them, can be a nontrivial matter for many specification formalisms, because complex formulae may require a considerable amount of information about the past. {\em Metric temporal logic} (MTL) is an extension of propositional linear temporal logic with discrete-time-bounded temporal operators. In MTL, one can specify time limits within which certain temporal properties must hold, thus making it very suitable to express real-time monitoring requirements. In this paper, we present monitoring algorithms for checking timestamped execution traces against formulae in MTL or certain important sublogics of it. We also present lower bounds for the monitoring problem, showing that the presented algorithms are asymptotically optimal.

Personal tools