Conformal quantitative predictive monitoring of stochastic systems with conditional validity

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 quantitative predictive monitoring (QPM), a PM method to support stochastic processes and rich specifications given in Signal Temporal Logic (STL). QPM provides a quantitative measure of satisfaction of some property φ by predicting its quantitative (a.k.a. robust) STL semantics, either spatial or temporal. 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 or sacrificing the guarantees. We further equip QPM with techniques to ensure conditional validity of the prediction intervals, i.e., such that the probabilistic guarantees hold relative to any state of the system (or any satisfaction value), thereby significantly enhancing the consistency and reliability of the resulting monitor. We demonstrate the effectiveness and scalability of QPM over a benchmark of five discrete-time stochastic processes with varying degrees of complexity, including a stochastic multi-agent system.