Document Open Access Logo

A Theory of (Linear-Time) Timed Monitors (Artifact)

Authors Mouloud Amara, Giovanni Bernardi , Mohammed Aristide Foughali , Adrian Francalanza

PDF

Artifact Description

Thumbnail PDF
PDF
DARTS.11.2.8.pdf
  • Filesize: 0.57 MB
  • 3 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Timed logics
  • Runtime verification
  • Monitorability

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Artifact

Artifact Evaluation Policy

The artifact has been evaluated as described in the ECOOP 2025 Call for Artifacts and the ACM Artifact Review and Badging Policy.

Abstract

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.

Cite As Get BibTex

Mouloud Amara, Giovanni Bernardi, Mohammed Aristide Foughali, and Adrian Francalanza. A Theory of (Linear-Time) Timed Monitors (Artifact). In Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025). Dagstuhl Artifacts Series (DARTS), Volume 11, Issue 2, pp. 8:1-8:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/DARTS.11.2.8

Author Details

Mouloud Amara
  • Université Paris Cité, CNRS, IRIF, F-75013 Paris, France
Giovanni Bernardi
  • Université Paris Cité, CNRS, IRIF, F-75013 Paris, France
Mohammed Aristide Foughali
  • Université Paris Cité, CNRS, IRIF, F-75013 Paris, France
Adrian Francalanza
  • Dept. of Computer Science, ICT, University of Malta, Msida, Malta

Funding

This work received support under the program "Investissement d’Avenir" launched by the French Government and implemented by ANR, with the reference "ANR-18-IdEx-000" as part of its program "Émergence". Other fundings include the ANR-JST Grant CyPhAI as well as the ANR project MAVEriQ.

Related Article

  • Mouloud Amara, Giovanni Bernardi, Mohammed Aristide Foughali, and Adrian Francalanza, "A Theory of (Linear-Time) Timed Monitors", in 39th European Conference on Object-Oriented Programming (ECOOP 2025), LIPIcs, Vol. 333, pp. 1:1-1:30, 2025. https://doi.org/10.4230/LIPIcs.ECOOP.2025.1
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact