Conformal Quantitative Predictive Monitoring of STL Requirements for Stochastic Processes

DOI10.1145/3575870.3587113arXiv2211.02375OpenAlexW4375852289MaRDI QIDQ6202073FDOQ6202073

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)

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.

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)

Cites Work

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

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)