Distributionally Robust Predictive Runtime Verification under Spatio-Temporal Logic Specifications

要約

シミュレータで設計されたサイバーフィジカルシステムは、多くの場合、複数の相互作用するエージェントで構成されるが、実世界では異なる挙動を示す。我々は、このようなシステムを実運用時に検証したいと考えている。そこで我々は、以下のようなロバストな実行時予測検証（RPRV）アルゴリズムを提案する：(1)信号時間論理(STL)タスクの下での一般的確率的CPS、および(2)時空間論理タスクの下での確率的マルチエージェントシステム(MAS)。RPRV問題には以下の課題がある：(1)配備されたCPSの挙動に関する十分なデータが存在しない可能性がある、(2)設計段階のシステム軌道に基づく予測モデルは、実世界の配備中に分布シフトに遭遇する可能性がある、(3)アルゴリズムはMASの複雑性に対応し、時空間論理タスクに適用可能である必要がある。これらの課題に対処するために、我々は、配備時と設計時のシステムの軌道分布の間の統計的距離（f-ダイバージェンス）の上界についての知識を前提とする。我々は、一般的なCPSのための正確で解釈可能なRPRVアルゴリズムを提案した先行研究[1, 2]に動機付けられ、ここではそれをMAS設定と時空間論理タスクに拡張する。具体的には、学習された予測モデルを用いて実行時のシステム動作を推定し、ロバストな適合予測を用いて分布のシフトを考慮することで確率的保証を得る。1]を基に、時空間リーチ＆エスケープ論理（STREL）のロバストなセマンティクス上でロバストな適合予測を行い、MASのための集中型RPRVアルゴリズムを得る。我々は、ドローン群シミュレータにおいて、我々の結果を実証的に検証し、MASに対する我々のRPRVアルゴリズムのスケーラビリティを示し、検証結果に対する異なる軌道予測器の影響を分析する。我々の知る限り、これらは分布シフト下におけるMASのための最初の統計的に有効なアルゴリズムである。

要約(オリジナル)

Cyber-physical systems designed in simulators, often consisting of multiple interacting agents, behave differently in the real-world. We would like to verify these systems during runtime when they are deployed. Thus, we 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 these challenges, we assume knowledge of an upper bound on the statistical distance (in terms of an f-divergence) 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.

arxiv情報

提供元, 利用サービス

arxiv.jp, DeepL