Overview

Monitorability underpins the technique of Runtime Verification because it delineates what properties can be verified at runtime. Although many definitions of monitorability exist, few are defined explicitly in terms of the operational guarantees provided by monitors, which are 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 specifications, we give syntactic characterisations in Hennessy–Milner logic with recursion for its levels. Finally, we map existing monitorability definitions into our hierarchy. Our work gives a unified framework that makes the operational asumtions and guarantees of each definition explicit. This provides a rigorous foundation that can inform design choices and correctness claims for runtime verification tools. This presentation is based on joint work with Antonis Achilles (Reykjavik University), Adrian Francalanza (University of Malta), Anna Ingólfsdótt (Reykjavik University) and Karoliina Lehtinen (University of Liverpool).