arXiv:2504.02964eess.SYcs.LO2025-04被引 3

针对部署后系统行为偏差,提出可验证的实时运行时监控方法。

Distributionally Robust Predictive Runtime Verification under Spatio-Temporal Logic Specifications

  • 基于鲁棒置信预测,融合时空逻辑建模系统行为
  • 在无人机集群仿真中实现多智能体系统的可扩展验证
  • 适用于真实部署中分布偏移场景,适合安全关键系统

在模拟器中设计的网络物理系统(CPS),如多智能体编队,在实际部署中表现可能不同。本文提出鲁棒预测式运行时验证(RPRV)算法,用于一般随机型CPS在信号时间逻辑(STL)任务下的验证,以及随机多智能体系统(MAS)在时空逻辑任务下的验证。面对部署阶段数据不足、模型分布偏移及复杂度高等挑战,假设已知部署与设计阶段轨迹分布间的统计距离上界。基于前期工作[1,2],扩展至多智能体场景与时空逻辑,利用学习的预测模型估计运行时行为,并通过鲁棒置信预测提供概率保证。在时空可达与逃逸逻辑(STREL)的鲁棒语义基础上进行鲁棒置信预测,构建了中心化RPRV算法。在无人机群仿真中验证了算法的可扩展性,并分析了不同轨迹预测器对验证结果的影响。据我们所知,这是首个在分布偏移下对多智能体系统具有统计有效性的验证算法。

原文摘要 · Abstract (English)

Cyber-physical systems (CPS) designed in simulators, often consisting of multiple interacting agents (e.g. in multi-agent formations), behave differently in the real-world. We want to verify these systems during runtime when they are deployed. We thus propose robust predictive runtime verification (RPRV) algorithms for: (1) general stochastic CPS under signal temporal logic (STL) tasks, and (2) stochastic multi-agent systems (MAS) under spatio-temporal logic tasks. The RPRV problem presents the following challenges: (1) there may not be sufficient data on the behavior of the deployed CPS, (2) predictive models based on design phase system trajectories may encounter distribution shift during real-world deployment, and (3) the algorithms need to scale to the complexity of MAS and be applicable to spatio-temporal logic tasks. To address the challenges, we assume knowledge of an upper bound on the statistical distance between the trajectory distributions of the system at deployment and design time. We are motivated by our prior work [1, 2] where we proposed an accurate and an interpretable RPRV algorithm for general CPS, which we here extend to the MAS setting and spatio-temporal logic tasks. Specifically, we use a learned predictive model to estimate the system behavior at runtime and robust conformal prediction to obtain probabilistic guarantees by accounting for distribution shifts. Building on [1], we perform robust conformal prediction over the robust semantics of spatio-temporal reach and escape logic (STREL) to obtain centralized RPRV algorithms for MAS. We empirically validate our results in a drone swarm simulator, where we show the scalability of our RPRV algorithms to MAS and analyze the impact of different trajectory predictors on the verification result. To the best of our knowledge, these are the first statistically valid algorithms for MAS under distribution shift.

运行时验证多智能体时空逻辑鲁棒性

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。