Venue: LRE, EPITA Paris, salle Apprentissage 2
Speaker 1: (present) Mo Foughali, IRIF
Title: A Theory of Linear-Time Timed Monitors
► Abstract:
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.
- First, we show that Tˡⁱⁿ is strictly more expressive than MTL, the de facto timed extension of the
well-known LTL.
- 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, and 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.
Speaker 2: (present) Dietrich Kuske, TU Ilmenau, Germany
Title: Decision problems for infinite Mazurkiewicz traces
► Abstract:
This talk studies decision problems for Boolean combinations of
omega-rational languages of Mazurkiewicz traces. The complexities of
these decision problems (emptiness, regularity, rationality) are
classified depending on properties of the independence alphabets and
of the Boolean combinations allowed. For any of the problems, we
obtain a trichotomy ranging from decidable over a low level of the
arithmetical hierarchy to a low level of the analytical hierarchy.