Checking metric temporal logic with TRACE

M. Hendriks, M.C.W. Geilen, A.R.B. Behrouzian, A.A. Basten, H. Alizadeh, D. Goswami

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

4 Citations (Scopus)
1 Downloads (Pure)


Execution traces' time-stamped sequences of events' provide a general' domain-independent' view on the behavior of systems. They enable analysis of metrics such as latency' pipeline depth and throughput. Often' however' it is not clear what such metrics exactly mean and ad hoc methods are used to compute them. Metric Temporal Logic (MTL) can be used to address this issue: it enables the formal specification of quantitative properties on execution traces. We thus have added an MTL checking capability to the TRACE tool' which is a tool for viewing and analyzing execution traces [1]. We use a recursive memoization algorithm that generates concise explanations of the truth value of the given MTL formula. These explanations can be visualized in the TRACE viewer to aid interpretation by the user.

Original languageEnglish
Title of host publicationProceedings - 2016 16th International Conference on Application of Concurrency to System Design, ACSD 2016, 19-21 June 2016, Turan, Poland
Place of PublicationPiscataway
PublisherInstitute of Electrical and Electronics Engineers
Number of pages6
ISBN (Electronic)978-1-5090-2589-3
ISBN (Print)978-1-5090-0763-9
Publication statusPublished - 3 Feb 2017
Event16th International Conference on Application of Concurrency to System Design (ACSD 2016) - Torun, Poland
Duration: 19 Jun 201621 Jun 2016
Conference number: 16


Conference16th International Conference on Application of Concurrency to System Design (ACSD 2016)
Abbreviated titleACSD 2016
Internet address


  • execution trace
  • explanation
  • informative prefix
  • Metric temporal logic
  • visualization


Dive into the research topics of 'Checking metric temporal logic with TRACE'. Together they form a unique fingerprint.

Cite this