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.

翻译：我们考虑预测监控（PM）问题，即根据系统当前状态在运行时预测期望属性的满足情况。由于其在运行时安全保证和在线控制中的重要性，PM方法不仅需要高效以实现对预测违规的及时干预，同时需提供正确性保证。本文提出**定量预测监控（QPM）**，这是首个支持随机过程与信号时序逻辑（STL）中丰富规约的PM方法。与现有多数仅预测某属性φ是否满足的PM技术不同，QPM通过预测φ的定量（即鲁棒）STL语义，提供满足程度的定量度量。QPM推导的预测区间计算效率极高且具有概率保证——这些区间以任意概率覆盖系统随机演化对应的STL鲁棒性值。为此，我们采用机器学习方法，并利用分位数回归中共形推断的最新进展，从而避免运行时通过昂贵的蒙特卡洛模拟来估计区间。我们还展示了如何以组合方式集成监控器以处理复合公式，既无需重新训练预测器，也不牺牲保证性。通过在四个复杂度各异的离散时间随机过程基准上的实验，我们验证了QPM的有效性和可扩展性。