Corelab Seminar

Antonis Achilleos
A guide to monitorability

I will present recent work on runtime monitorability. Runtime Verification (RV) is the technique of using a monitor to detect the violation or satisfaction of a property at runtime. One question that we ask is what properties we can monitor for. But even before giving an answer, we must first understand what that question means. Although many monitorability definitions exist, few are defined explicitly in terms of the operational guarantees provided by monitors, ie, the computational entities carrying out the verification. We view monitorability as a spectrum, where the fewer guarantees that are required of monitors, the more properties become monitorable. Accordingly, we present a monitorability hierarchy based on this trade-off. For regular, linear-time specifications, we give syntactic characterisations of the hierarchy in Hennessy-Milner logic with recursion. We then compare the obtained fragments with previous results for the branching-time setting.

This is joint work with Luca Aceto, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen.