Hsi-Ming Ho ; Joël Ouaknine ; James Worrell - On the Expressiveness and Monitoring of Metric Temporal Logic

lmcs:4366 - Logical Methods in Computer Science, May 10, 2019, Volume 15, Issue 2 - https://doi.org/10.23638/LMCS-15(2:13)2019
On the Expressiveness and Monitoring of Metric Temporal LogicArticle

Authors: Hsi-Ming Ho ; Joël Ouaknine ; James Worrell

    It is known that Metric Temporal Logic (MTL) is strictly less expressive than the Monadic First-Order Logic of Order and Metric (FO[<, +1]) when interpreted over timed words; this remains true even when the time domain is bounded a priori. In this work, we present an extension of MTL with the same expressive power as FO[<, +1] over bounded timed words (and also, trivially, over time-bounded signals). We then show that expressive completeness also holds in the general (time-unbounded) case if we allow the use of rational constants $q \in \mathbb{Q}$ in formulas. This extended version of MTL therefore yields a definitive real-time analogue of Kamp's theorem. As an application, we propose a trace-length independent monitoring procedure for our extension of MTL, the first such procedure in a dense real-time setting.


    Volume: Volume 15, Issue 2
    Published on: May 10, 2019
    Accepted on: April 10, 2019
    Submitted on: March 13, 2018
    Keywords: Computer Science - Logic in Computer Science
    Funding:
      Source : OpenAIRE Graph
    • Analysis, Verification, and Synthesis for Infinite-State Systems; Funder: European Commission; Code: 648701

    Consultation statistics

    This page has been seen 1266 times.
    This article's PDF has been downloaded 307 times.