Conformal Quantitative Predictive Monitoring of STL Requirements for Stochastic Processes

• URL: http://arxiv.org/abs/2211.02375v2
• Date: Thu, 6 Apr 2023 09:22:28 GMT
• Title: Conformal Quantitative Predictive Monitoring of STL Requirements for Stochastic Processes
• Authors: Francesca Cairoli, Nicola Paoletti, Luca Bortolussi
• Abstract summary: We introduce textitquantitative predictive monitoring (QPM), the first PM method to support processes and rich specifications given in Signal Temporal Logic (STL) QPM provides a quantitative measure of satisfaction by predicting the quantitative (aka robust) STL semantics of $phi$. We show how our monitors can be combined in a compositional manner to handle composite formulas.
• Score: 4.279881803310469
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• DASA: Delay-Adaptive Multi-Agent Stochastic Approximation [64.32538247395627]
  We consider a setting in which $N$ agents aim to speedup a common Approximation problem by acting in parallel and communicating with a central server. To mitigate the effect of delays and stragglers, we propose textttDASA, a Delay-Adaptive algorithm for multi-agent Approximation.
  arXiv  Detail & Related papers  (2024-03-25T22:49:56Z)
• Learning-Based Approaches to Predictive Monitoring with Conformal Statistical Guarantees [2.1684857243537334]
  This tutorial focuses on efficient methods to predictive monitoring (PM) PM is the problem of detecting future violations of a given requirement from the current state of a system. We present a general and comprehensive framework summarizing our approach to the predictive monitoring of CPSs.
  arXiv  Detail & Related papers  (2023-12-04T15:16:42Z)
• SMURF-THP: Score Matching-based UnceRtainty quantiFication for Transformer Hawkes Process [76.98721879039559]
  We propose SMURF-THP, a score-based method for learning Transformer Hawkes process and quantifying prediction uncertainty. Specifically, SMURF-THP learns the score function of events' arrival time based on a score-matching objective. We conduct extensive experiments in both event type prediction and uncertainty quantification of arrival time.
  arXiv  Detail & Related papers  (2023-10-25T03:33:45Z)
• Score Matching-based Pseudolikelihood Estimation of Neural Marked Spatio-Temporal Point Process with Uncertainty Quantification [59.81904428056924]
  We introduce SMASH: a Score MAtching estimator for learning markedPs with uncertainty quantification. Specifically, our framework adopts a normalization-free objective by estimating the pseudolikelihood of markedPs through score-matching. The superior performance of our proposed framework is demonstrated through extensive experiments in both event prediction and uncertainty quantification.
  arXiv  Detail & Related papers  (2023-10-25T02:37:51Z)
• Robust Control for Dynamical Systems With Non-Gaussian Noise via Formal Abstractions [59.605246463200736]
  We present a novel controller synthesis method that does not rely on any explicit representation of the noise distributions. First, we abstract the continuous control system into a finite-state model that captures noise by probabilistic transitions between discrete states. We use state-of-the-art verification techniques to provide guarantees on the interval Markov decision process and compute a controller for which these guarantees carry over to the original control system.
  arXiv  Detail & Related papers  (2023-01-04T10:40:30Z)
• Conformal Prediction Intervals for Markov Decision Process Trajectories [10.68332392039368]
  This paper provides conformal prediction intervals over the future behavior of an autonomous system executing a fixed control policy on a Markov Decision Process (MDP) The method is illustrated on MDPs for invasive species management and StarCraft2 battles.
  arXiv  Detail & Related papers  (2022-06-10T03:43:53Z)
• Sampling-Based Robust Control of Autonomous Systems with Non-Gaussian Noise [59.47042225257565]
  We present a novel planning method that does not rely on any explicit representation of the noise distributions. First, we abstract the continuous system into a discrete-state model that captures noise by probabilistic transitions between states. We capture these bounds in the transition probability intervals of a so-called interval Markov decision process (iMDP)
  arXiv  Detail & Related papers  (2021-10-25T06:18:55Z)
• Quantifying Uncertainty in Deep Spatiotemporal Forecasting [67.77102283276409]
  We describe two types of forecasting problems: regular grid-based and graph-based. We analyze UQ methods from both the Bayesian and the frequentist point view, casting in a unified framework via statistical decision theory. Through extensive experiments on real-world road network traffic, epidemics, and air quality forecasting tasks, we reveal the statistical computational trade-offs for different UQ methods.
  arXiv  Detail & Related papers  (2021-05-25T14:35:46Z)
• Predictive Monitoring with Logic-Calibrated Uncertainty for Cyber-Physical Systems [2.3131309703965135]
  We develop a novel approach for monitoring sequential predictions generated from Bayesian Recurrent Neural Networks (RNNs) We propose a new logic named emphSignal Temporal Logic with Uncertainty (STL-U) to monitor a flowpipe containing an infinite set of uncertain sequences. We evaluate the proposed approach via experiments with real-world datasets and a simulated smart city case study.
  arXiv  Detail & Related papers  (2020-10-31T23:18:15Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.