DROPS

Document

DOI: 10.4230/OASIcs.TIME.2026.1

Revisiting the Expressiveness of Metric Temporal Logic

Authors: Mohammed Aristide Foughali

Published in: OASIcs, Volume 146, 33rd International Symposium on Temporal Representation and Reasoning (TIME 2026)

Abstract

The expressiveness of Metric Temporal Logic (MTL) has been extensively studied throughout the last two decades. In particular, it has been shown that the interval-based semantics of MTL is strictly more expressive than the pointwise one. These results may suggest that enabling the evaluation of formulae at arbitrary time points instead of positions of timed events increases the expressive power of MTL. In this paper, we formally argue otherwise. We demonstrate that under standard models of finite or non-Zeno infinite (action-based) timed executions, the interval-based and the pointwise semantics are incomparable. We then propose a new mixed semantics that embeds both the pointwise and the interval-based ones.

Cite as

Mohammed Aristide Foughali. Revisiting the Expressiveness of Metric Temporal Logic. In 33rd International Symposium on Temporal Representation and Reasoning (TIME 2026). Open Access Series in Informatics (OASIcs), Volume 146, pp. 1:1-1:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{foughali:OASIcs.TIME.2026.1,
  author =	{Foughali, Mohammed Aristide},
  title =	{{Revisiting the Expressiveness of Metric Temporal Logic}},
  booktitle =	{33rd International Symposium on Temporal Representation and Reasoning (TIME 2026)},
  pages =	{1:1--1:18},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-448-2},
  ISSN =	{2190-6807},
  year =	{2026},
  volume =	{146},
  editor =	{Orlandini, AndreA and Pinchinat, Sophie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TIME.2026.1},
  URN =		{urn:nbn:de:0030-drops-276970},
  doi =		{10.4230/OASIcs.TIME.2026.1},
  annote =	{Keywords: Timed logics, Metric temporal logic}
}

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 Foughali, Mohammed Aristide

Revisiting the Expressiveness of Metric Temporal Logic

Abstract

Cite as

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