International Symposium On Leveraging Applications of Formal Methods, Verification and Validation • Crete, Greece
Time: Thursday, 31.10
Room: Room 4
Authors: Francesca Cairoli
Abstract: Predictive monitoring (PM) aims at predicting at runtime the satisfaction of a desired property from the current state of the system under analysis. PM methods need to be e!cient, to enable timely interventions against predicted violations, and reliable, given the safetycriticality of the problem. Quantitative predictive monitoring (QPM) focuses on stochastic processes, supports rich specifications expressed in Signal Temporal Logic (STL) and provides a quantitative measure of satisfaction by predicting the quantitative (a.k.a. robust) STL semantics, either spatial or temporal. Our solution to QPM integrates machine learning and conformal inference to derive prediction intervals that are highly e!cient to compute and with probabilistic guarantees of covering the STL robustness values relative to the stochastic evolution of the system. Conformal guarantees are in general only marginal. However, conditional guarantees can significantly enhance the consistency and reliability of the resulting monitor. To this end, we equip QPM with conformal techniques to ensure conditional validity of the prediction intervals, i.e., such that the probabilistic guarantees hold given some conditions of the system, e.g. the current state or the dynamical mode of the system.
Paper: Download