We are interested in predicting failures of cyber-physical systems during their operation. Particularly, we consider stochastic systems and signal temporal logic specifications, and we want to calculate the probability that the current system trajectory violates the specification. The paper presents two predictive runtime verification algorithms that predict future system states from the current observed system trajectory. As these predictions may not be accurate, we construct prediction regions that quantify prediction uncertainty by using conformal prediction, a statistical tool for uncertainty quantification. Our first algorithm directly constructs a prediction region for the satisfaction measure of the specification so that we can predict specification violations with a desired confidence. The second algorithm constructs prediction regions for future system states first, and uses these to obtain a prediction region for the satisfaction measure. To the best of our knowledge, these are the first formal guarantees for a predictive runtime verification algorithm that applies to widely used trajectory predictors such as RNNs and LSTMs, while being computationally simple and making no assumptions on the underlying distribution. We present numerical experiments of an F-16 aircraft and a self-driving car.

翻译：我们有兴趣预测网络物理系统运行过程中的故障。 特别是, 我们考虑随机系统和信号时间逻辑规格, 我们想要计算当前系统轨迹违反规格的概率。 本文介绍了预测未来系统运行时间的两种预测运行时间核查算法, 该算法根据当前观测的系统轨迹来预测未来系统。 由于这些预测可能不准确, 我们构建了预测区域, 通过使用符合的预测来量化预测不确定性, 这是一种用于不确定性量化的统计工具。 我们的第一个算法直接构建了一个对规格的满意度的预测区域, 以便我们能够以期望的信心预测违反规格的情况。 第二个算法为未来系统构建了预测区域, 首先列出, 并使用这些算法来获取对满意度的预测区域。 据我们所知, 这些是预测运行时间核查算法的第一个正式保障, 适用于广泛使用的轨迹预测器, 如 RNNS 和 LSTMs,, 同时进行简单的计算, 对基本分布不作任何假设。 我们对F-16型飞机和自驾驶车进行数字实验。