Adventures in monitorability

I will present recent work on runtime monitorability for the Hennessy-Milner logic with recursion (recHML), a very expressive variant of the modal mu-calculus. We investigate the monitorability of recHML with a linear-time semantics and then compare the obtained results with previous results for the branching-time setting. We observe that the class of monitorable properties exhibits different phenomena for linear time than for branching time. Our work establishes an expressiveness hierarchy of monitorable fragments of recHML in a linear-time setting and exactly identifies what kinds of guarantees can be given using runtime monitors for each fragment in the hierarchy. The proposed framework supports the automatic, compositional synthesis of correct monitors from monitorable properties.

Joint work with Luca Aceto, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen