
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Security and Verification in Computing
