Conformal Quantitative Predictive Monitoring of STL Requirements for Stochastic Processes

DOI10.1145/3575870.3587113MaRDI QIDQ6202073zbMATH OpenOpenAlexFDO

Authors Francesca Cairoli, Nicola Paoletti, Luca Bortolussi

Publication date 21 February 2024

Published in Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2211.02375

zbMATH Keywords

stochasticconformal quantile regressionpredictive monitoring

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30)

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 extit{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.

Cites work

• scientific article; zbMATH DE number 2168212 (Why is no real title available?)
• scientific article; zbMATH DE number 6306019 (Why is no real title available?)
• Approximate model checking of stochastic hybrid systems
• Clairvoyant monitoring for signal temporal logic
• Electric load model synthesis by diffusion approximation of a high-order hybrid-state stochastic system
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Hybrid Systems: Computation and Control
• Predictive monitoring for signal temporal logic with probabilistic guarantees
• Robust satisfaction of temporal logic over real-valued signals
• Smoothed model checking for uncertain continuous-time Markov chains
• Stochastic hybrid models of gene regulatory networks -- a PDE approach
• System design of stochastic models using robustness of temporal properties
• Tools and Algorithms for the Construction and Analysis of Systems
• Verisig
• Weakness monitors for fail-aware systems

This page was built for publication: Conformal Quantitative Predictive Monitoring of STL Requirements for Stochastic Processes

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6202073)