DROPS

Document

DOI: 10.4230/LIPIcs.ECOOP.2025.1

A Theory of (Linear-Time) Timed Monitors

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

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract

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.

Cite as

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). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 1:1-1:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{amara_et_al:LIPIcs.ECOOP.2025.1,
  author =	{Amara, Mouloud and Bernardi, Giovanni and Foughali, Mohammed Aristide and Francalanza, Adrian},
  title =	{{A Theory of (Linear-Time) Timed Monitors}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{1:1--1:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.1},
  URN =		{urn:nbn:de:0030-drops-232930},
  doi =		{10.4230/LIPIcs.ECOOP.2025.1},
  annote =	{Keywords: Timed logics, Runtime Verification, Monitorability}
}

Document

Artifact

DOI: 10.4230/DARTS.11.2.8

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

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

Published in: DARTS, Volume 11, Issue 2, Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025)

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

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)

Copy BibTex To Clipboard

@Article{amara_et_al:DARTS.11.2.8,
  author =	{Amara, Mouloud and Bernardi, Giovanni and Foughali, Mohammed Aristide and Francalanza, Adrian},
  title =	{{A Theory of (Linear-Time) Timed Monitors (Artifact)}},
  pages =	{8:1--8:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2025},
  volume =	{11},
  number =	{2},
  editor =	{Amara, Mouloud and Bernardi, Giovanni and Foughali, Mohammed Aristide and Francalanza, Adrian},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.11.2.8},
  URN =		{urn:nbn:de:0030-drops-233517},
  doi =		{10.4230/DARTS.11.2.8},
  annote =	{Keywords: Timed logics, Runtime verification, Monitorability}
}

Search Results

Documents authored by Amara, Mouloud

A Theory of (Linear-Time) Timed Monitors

Abstract

Cite as

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

Abstract

Cite as

Thanks for your feedback!

Could not send message