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 talk, 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ˡⁱⁿmodulo a rich monitoring framework that we devise; and further characterise its largest subsets of formulae that are:

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

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

If time allows, I’ll give a broad view of ongoing extensions of this work, in particular the monitorability of timed regular languages.