Monitoring Algorithms for Metric Temporal Logic Specifications

Prasanna Thati, Grigore Rou

Research output: Contribution to journalArticlepeer-review


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 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. Metric temporal logic (MTL) is an extension of propositional linear temporal logic with discrete-timebounded 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.

Original languageEnglish (US)
Pages (from-to)145-162
Number of pages18
JournalElectronic Notes in Theoretical Computer Science
Issue numberSPEC. ISS.
StatePublished - Jan 3 2005


  • Execution trace
  • Metric temporal logic
  • Runtime verification
  • Specification

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Monitoring Algorithms for Metric Temporal Logic Specifications'. Together they form a unique fingerprint.

Cite this