基于鲁棒预测与时空逻辑的自主系统实时验证方法及其在分布偏移下的统计保证

《ACM Transactions on Cyber-Physical Systems》：Distributionally Robust Predictive Runtime Verification under Spatio-Temporal Logic Specifications

本综述系统性地介绍了鲁棒预测运行时验证（RPRV）方法，该方法结合鲁棒预测（基于LSTM等模型）与时空逻辑（STL/STREL），为自主系统（如多智能体系统MAS）在存在分布偏移（Df(D,D0)≤ε）的场景下提供统计验证保证（Prob(ρ?(X,τ0)≥ρ*)≥1?δ）。通过非共形预测（CP）与鲁棒语义的融合，实现了对时态属性（如G[0,105]h≥60）和空间交互（如M[0,2]π）的可信验证。

　　

2.1 STL for General CPS

信号时序逻辑（STL）用于表达一般信息物理系统（CPS）的时序规约。STL基于谓词函数h:Rⁿ→R构建原子命题π，其语法包含布尔运算符（?,∧）和时序运算符（U_I,F_I,G_I）。鲁棒语义ρ^?(x,τ₀)∈R^∞定量评估轨迹x在时间τ₀满足公式?的程度，其中正值表示满足，负值表示违反。有界STL公式的满足性可通过有限长度轨迹（L^?）判定。

2.2 STREL for MAS

时空时序逻辑（STREL）扩展STL以处理多智能体系统（MAS）的空间交互。通过权重函数w:{1,…,L}²×T×R^N×T→R_≥0^∞描述智能体间的连接关系（如欧氏距离），并引入空间运算符：可达（R_[d1,d2]）、逃逸（E_[d1,d2]）和包围（S_≤d）。鲁棒语义ρ^ψ(x,τ₀,l)评估智能体l在时间τ₀满足空间属性ψ的程度，其声音性保证ρ^ψ>0时语义满足。

2.3 RPRV

鲁棒预测运行时验证（RPRV）核心问题是在测试分布D相对训练分布D₀存在f-散度有界偏移（D_f(D,D₀)≤ε）时，基于观测轨迹X_obs和预测轨迹X?（通过LSTM等预测器μ生成），以概率1-δ计算鲁棒语义下界ρ^*。预测 horizon H=τ₀+L^?-t确保覆盖公式?的时序需求。

2.4 Robust CP

鲁棒非共形预测（CP）处理分布偏移下的不确定性量化。通过校准数据集S计算非共形评分R⁽ⁱ⁾=ρ^?(X?⁽ⁱ⁾,τ₀)-ρ^?(X⁽ⁱ⁾,τ₀)，进而基于分位数函数C?=Quantile_1-δ?(R⁽¹⁾,…,R^(K))获得统计边界。数据处理不等式（Lemma 2）保证诱导分布偏移受控，即D_f(R,R₀)≤ε。

3.1 Accurate Robust STL Predictive RV

直接对鲁棒语义应用鲁棒CP：通过校准轨迹的非共形评分分布，计算测试轨迹的鲁棒语义下界ρ^?(X,τ₀)≥ρ^?(X?,τ₀)-C?，概率保证≥1-δ。以F-16高度控制为例（?=G_[0,105]h≥60），在噪声分布偏移（N(x_c(t),3²)→N(x_c(t),3.5²)）下，该方法有效提供验证结果。

该方法通过融合时空逻辑的形式化表达能力、机器学习的前瞻预测能力以及统计学的分布鲁棒性保证，为自主系统在动态不确定环境中的可信验证提供了系统化解决方案。