Most parts of this talk are based on joint work with Mouloud Amara and Giovanni Bernardi (IRIF, Université Paris Cité) and Adrian Francalanza (University of Malta).

In runtime verification (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. Monitorability is a central issue in RV that remained unsolved for timed logics, i.e., where formulae can express both the order of events and the quantity of time separating them.

The challenge is to precisely characterise, given some expressive timed logic T interpreted over infinite timed executions, its largest subset of monitorable formulae. Intuitively, a formula φ is monitorable iff there exists a monitor M that is sound and (violation or satisfaction) complete for φ.

• Soundness requires that whenever M reaches a violation (resp. satisfaction) verdict after observing a finite execution ρ, then any infinite extension of ρ violates (resp. satisfies) φ.
• Violation completeness states that for any infinite execution π violating φ, M will inevitably reach a violation verdict after observing a finite prefix of π (satisfaction completeness is defined dually).

The main difficulty underlying the monitorability problem is, therefore, to formally characterise when one can “tell the future based on the present.”

In this keynote, I will go over our recent work that solved the monitorability problem for Tˡⁱⁿ, a new expressive (linear-time) timed μ-calculus that we proposed.

1. First, we show that Tˡⁱⁿ is strictly more expressive than MTL, the de facto timed extension of the well-known LTL.
2. Second, we identify MTˡⁱⁿ, the largest monitorable fragment of Tˡⁱⁿ; and further characterise its largest subsets of formulae that are:

• Violation monitorable
• Satisfaction monitorable
• Complete monitorable (both satisfaction and violation monitorable)

To the best of our knowledge, this is the first work that solves the monitorability problem for such an expressive timed logic.

Our theoretical results are accompanied with compilers: - (i) from MTL to Tˡⁱⁿ, and - (ii) from MTˡⁱⁿ formulae to monitors.

If time allows, I will discuss some challenges in the continuation of this work such as bounded-memory, tight, and overhead-aware monitorability.

Mohammed “Mo” Aristide Foughali is maître de conférences (associate professor) at Université Paris Cité (Paris, France) since 2021. He is a member of the Modelling and Verification team at Laboratoire de Recherche en Informatique Fondamentale (IRIF). His research interests span different approaches of formal verification of real-time and hybrid systems, including model checking and runtime monitoring.

Before, he was a postdoctoral researcher at the VERIMAG laboratory (Grenoble, France) from 2019 to 2021. Between 2018 and 2019, he was a temporary lecturer and researcher at INSA Toulouse and LAAS-CNRS (Toulouse, France). In 2018, he earned his PhD degree from INSA Toulouse in computer science and robotics on the subject of formal verification of robotic and autonomous systems.