2026-07-25T02:34:10Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23351 2025-06-25T13:23:37Z ddc:004 open_access

A Theory of (Linear-Time) Timed Monitors (Artifact) Amara, Mouloud Bernardi, Giovanni Foughali, Mohammed Aristide Francalanza, Adrian Timed logics Runtime verification Monitorability We provide an OCaml implementation of the logics MTL and T^lin, as well as monitors. Our artefact includes a compiler that translates T^lin formulae into monitors. The generation of a monitor M from some formula ϕ is decorated with a warning whenever ϕ is not in the syntax of the maximally-expressive monitorable fragment. The resulting monitors being reactive and deterministic, we also implement their semantics, and provide further a pseudo-monitoring prototype where the monitor incrementally consumes an infinite timed word and reaches a verdict whenever possible. For convenience, for users that prefer to use MTL (bearing in mind the loss of expressivity), we also provide a compiler from MTL to T^lin. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Mouloud Amara and Giovanni Bernardi and Mohammed Aristide Foughali and Adrian Francalanza 2025 Is Part Of DARTS, Volume 11, Issue 2, Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025) Article Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/DARTS.11.2.8 urn:nbn:de:0030-drops-233517 https://drops.dagstuhl.de/entities/document/10.4230/DARTS.11.2.8 eng https://creativecommons.org/licenses/by/4.0/legalcode