On the expressiveness and monitoring of metric temporal logic

HO, H.M., OUAKNINE, J and WORRELL, J (2019). On the expressiveness and monitoring of metric temporal logic. Logical Methods in Computer Science, 15 (2), 13:1-13:52.

[img]
Preview
PDF
1803.02653.pdf - Published Version
Creative Commons Attribution.

Download (950kB) | Preview
Official URL: https://lmcs.episciences.org/5447
Open Access URL: https://arxiv.org/pdf/1803.02653.pdf (Published)
Related URLs:

    Abstract

    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 ∈ 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.

    Item Type: Article
    Uncontrolled Keywords: 0101 Pure Mathematics; 0803 Computer Software; 0802 Computation Theory and Mathematics
    Identification Number: https://doi.org/10.23638/LMCS-15(2:13)2019
    Page Range: 13:1-13:52
    SWORD Depositor: Symplectic Elements
    Depositing User: Symplectic Elements
    Date Deposited: 09 Oct 2019 16:32
    Last Modified: 14 Oct 2019 09:46
    URI: http://shura.shu.ac.uk/id/eprint/25236

    Actions (login required)

    View Item View Item

    Downloads

    Downloads per month over past year

    View more statistics