Towards Partial Monitoring: It is Always too Soon to Give Up

TL;DR

This paper revises the concept of monitorability in Runtime Verification, demonstrating how non-monitorable properties can still be used to generate partial monitors, with implications for both theory and practice.

Contribution

It introduces the idea of partial monitors for non-monitorable properties, expanding the practical applicability of Runtime Verification techniques.

Findings

Non-monitorable properties can generate useful partial monitors.

Partial monitors provide partial verification capabilities.

Implications enhance practical runtime verification methods.

Abstract

Runtime Verification is a lightweight formal verification technique. It is used to verify at runtime whether the system under analysis behaves as expected. The expected behaviour is usually formally specified by means of properties, which are used to automatically synthesise monitors. A monitor is a device that, given a sequence of events representing a system execution, returns a verdict symbolising the satisfaction or violation of the formal property. Properties that can (resp. cannot) be verified at runtime by a monitor are called monitorable and non-monitorable, respectively. In this paper, we revise the notion of monitorability from a practical perspective, where we show how non-monitorable properties can still be used to generate partial monitors, which can partially check the properties. Finally, we present the implications both from a theoretical and practical perspectives.