# An Operational Guide to Monitorability

## TL;DR

This paper introduces a hierarchical framework for monitorability in runtime verification, explicitly linking properties to monitor guarantees, and unifies existing definitions to improve understanding and design of verification tools.

## Contribution

It proposes a monitorability hierarchy with operational and syntactic characterizations, unifying various existing definitions into a rigorous, explicit framework.

## Key findings

- Mapped existing monitorability definitions into the hierarchy
- Provided operational and syntactic characterizations for hierarchy levels
- Established a unified framework for runtime verification monitorability

## Abstract

Monitorability delineates what properties can be verified at runtime. Although many monitorability definitions exist, few are defined explicitly in terms of the guarantees provided by monitors, i.e., the computational entities carrying out the verification. We view monitorability as a spectrum: the fewer monitor guarantees that are required, the more properties become monitorable. We present a monitorability hierarchy and provide operational and syntactic characterisations for its levels. Existing monitorability definitions are mapped into our hierarchy, providing a unified framework that makes the operational assumptions and guarantees of each definition explicit. This provides a rigorous foundation that can inform design choices and correctness claims for runtime verification tools.