This tutorial focuses on efficient methods to predictive monitoring (PM), the problem of detecting at runtime future violations of a given requirement from the current state of a system. While performing model checking at runtime would offer a precise solution to the PM problem, it is generally computationally expensive. To address this scalability issue, several lightweight approaches based on machine learning have recently been proposed. These approaches work by learning an approximate yet efficient surrogate (deep learning) model of the expensive model checker. A key challenge remains to ensure reliable predictions, especially in safety-critical applications. We review our recent work on predictive monitoring, one of the first to propose learning-based approximations for CPS verification of temporal logic specifications and the first in this context to apply conformal prediction (CP) for rigorous uncertainty quantification. These CP-based uncertainty estimators offer statistical guarantees regarding the generalization error of the learning model, and they can be used to determine unreliable predictions that should be rejected. In this tutorial, we present a general and comprehensive framework summarizing our approach to the predictive monitoring of CPSs, examining in detail several variants determined by three main dimensions: system dynamics (deterministic, non-deterministic, stochastic), state observability, and semantics of requirements' satisfaction (Boolean or quantitative).
翻译:本教程聚焦于预测监控(Predictive Monitoring, PM)的高效方法,该问题旨在运行时从系统当前状态检测给定需求是否会在未来被违反。尽管在运行时进行模型检查可为PM问题提供精确解,但通常计算开销巨大。为解决这一可扩展性问题,近期提出了多种基于机器学习的轻量级方法。这些方法通过训练一个近似的、但高效的替代(深度学习)模型来模拟昂贵的模型检查器。然而,在安全关键应用中,确保预测的可靠性仍是一项核心挑战。我们回顾了自身在预测监控方面的最新研究——这是最先提出基于学习近似方法用于信息物理系统(CPS)时序逻辑规约验证的工作之一,也是该领域中首个应用共形预测(Conformal Prediction, CP)进行严格不确定性量化的研究。这些基于CP的不确定性估计器可为学习模型的泛化误差提供统计保证,并能用于识别应被拒绝的不可靠预测。在本教程中,我们提出一个通用且全面的框架,系统总结针对CPS预测监控的方法,并详细考察由三个主要维度决定的若干变体:系统动态性(确定性、非确定性、随机性)、状态可观性,以及需求满足的语义(布尔型或定量型)。