2026-07-23T05:50:44Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23293 2025-06-25T13:20:36Z ddc:004 open_access

A Theory of (Linear-Time) Timed Monitors Amara, Mouloud Bernardi, Giovanni Foughali, Mohammed Aristide Francalanza, Adrian Timed logics Runtime Verification Monitorability Runtime Verification (RV) is gaining popularity due to its scalability and ability to analyse block-box systems. Monitoring is at the heart of RV; a logical formula ϕ, formalising some property of interest, is typically translated into a monitor that checks whether the system under scrutiny satisfies ϕ during its execution. A logical formula ϕ is violation (resp. satisfaction) monitorable iff there exists a monitor for ϕ that is both sound and complete w.r.t. its violation (resp. satisfaction). The monitorability problem is thus concerned with determining the largest subset of a logic L that is monitorable. Although this problem has been solved for expressive untimed logics, it remains open for timed logics, where formulae can express both the order of events and the quantity of time separating them. This paper solves the monitorability problem for T^lin, a new expressive (linear-time) timed μ-calculus that we propose. First, we show that T^lin is strictly more expressive than MTL, the de facto timed extension of LTL. Second, we identify MT^lin, the largest monitorable fragment of T^lin: we characterise its largest subsets of formulae that are violation monitorable, satisfaction monitorable, and complete monitorable (both satisfaction and violation monitorable). To wit, this is the first work that answers the monitorability question for such an expressive timed logic. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Mouloud Amara and Giovanni Bernardi and Mohammed Aristide Foughali and Adrian Francalanza 2025 Is Part Of LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ECOOP.2025.1 urn:nbn:de:0030-drops-232930 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.1 eng https://creativecommons.org/licenses/by/4.0/legalcode