Runtime Consultants

TL;DR

This paper introduces runtime consultants that proactively guide system actions to optimize quantitative objectives and avoid violations, functioning alongside runtime monitors with constant-time computation for common value functions.

Contribution

It formalizes the concept of runtime consultants, shows how to compute them efficiently for various value functions, and extends the approach to $mbda$-regular properties with quantitative semantics.

Findings

Runtime consultants can be computed in constant time for common value functions.

They provide proactive guidance to optimize system behavior.

The approach extends to $mbda$-regular properties with quantitative interpretations.

Abstract

In this paper we introduce the notion of a runtime consultant. A runtime consultant is defined with respect to some value function on infinite words. Similar to a runtime monitor, it runs in parallel to an execution of the system and provides inputs at every step of the run. While a runtime monitor alerts when a violation occurs, the idea behind a consultant is to be pro-active and provide recommendations for which action to take next in order to avoid violation (or obtain a maximal value for quantitative objectives). It is assumed that a runtime-controller can take these recommendations into consideration. The runtime consultant does not assume that its recommendations are always followed. Instead, it adjusts to the actions actually taken (similar to a vehicle navigation system). We show how to compute a runtime consultant for common value functions used in verification, and that almost all have a runtime consultant that works in constant time. We also develop consultants for $\omega$-regular properties, under both their classical Boolean semantics and their recently proposed quantitative interpretation.