Conformal Quantitative Predictive Monitoring of STL Requirements for Stochastic Processes

TL;DR

This paper introduces Quantitative Predictive Monitoring (QPM), a novel method for real-time safety assurance of stochastic systems using Signal Temporal Logic, providing efficient, probabilistic satisfaction intervals without costly simulations.

Contribution

QPM is the first predictive monitoring approach supporting stochastic processes and rich STL specifications, offering efficient, probabilistic satisfaction intervals with compositional guarantees.

Findings

QPM effectively predicts STL robustness with probabilistic coverage.

The method scales well on complex stochastic benchmarks.

QPM avoids expensive Monte-Carlo simulations at runtime.

Abstract

We consider the problem of predictive monitoring (PM), i.e., predicting at runtime the satisfaction of a desired property from the current system's state. Due to its relevance for runtime safety assurance and online control, PM methods need to be efficient to enable timely interventions against predicted violations, while providing correctness guarantees. We introduce \textit{quantitative predictive monitoring (QPM)}, the first PM method to support stochastic processes and rich specifications given in Signal Temporal Logic (STL). Unlike most of the existing PM techniques that predict whether or not some property $\phi$ is satisfied, QPM provides a quantitative measure of satisfaction by predicting the quantitative (aka robust) STL semantics of $\phi$. QPM derives prediction intervals that are highly efficient to compute and with probabilistic guarantees, in that the intervals cover with arbitrary probability the STL robustness values relative to the stochastic evolution of the system. To do so, we take a machine-learning approach and leverage recent advances in conformal inference for quantile regression, thereby avoiding expensive Monte-Carlo simulations at runtime to estimate the intervals. We also show how our monitors can be combined in a compositional manner to handle composite formulas, without retraining the predictors nor sacrificing the guarantees. We demonstrate the effectiveness and scalability of QPM over a benchmark of four discrete-time stochastic processes with varying degrees of complexity.