Monitorability for the Modal mu-Calculus over Systems with Data: From Practice to Theory

TL;DR

This paper explores the monitorability of an extended modal mu-calculus that incorporates data flow properties, providing a monitor synthesis algorithm and revealing a hierarchy of monitorable properties with implications for deterministic monitors.

Contribution

It introduces a monitorability framework for a data-extended mu-calculus, establishing a monitorability hierarchy and a fragment capturing all monitorable properties.

Findings

Strict hierarchy of monitorable properties established

Deterministic monitors have reduced monitorability

A fragment can express all monitorable properties without greatest fixed-points

Abstract

Runtime verification, also known as runtime monitoring, consists of checking whether a system satisfies a given specification by observing the trace it produces during its execution. It is used as a lightweight verification technique to complement or substitute costlier methods such as model-checking. In the regular setting, Hennessy-Milner logic with recursion, a variant of the modal mu-calculus, provides a versatile formalism for expressing linear- and branching-time specifications of the control flow of the system. In this paper, we shift the focus from control to data and study the monitorability of an extension of this logic that allows one to express properties of the data flow. Data values are modelled as values from an infinite domain. They are stored using data variables and manipulated using predicates and first-order quantification. The resulting logic is closely related to register automata with guessing. This correspondence yields a monitor synthesis algorithm, and allows us to derive a strict monitorability hierarchy between the different fragments of the logic, in stark contrast to the regular setting. In particular, restricting to deterministic monitors strictly reduces the set of monitorable properties. Last, we exhibit a fragment of the logic that can express all monitorable formulae in the logic without greatest fixed-points but not in the full logic. We finally show that this is unavoidable because, in fact, there is no decidable fragment of the logic that captures all monitorable properties.