Formal Controller Synthesis for Markov Jump Linear Systems with Uncertain Dynamics

要約

セーフティ・クリティカルなシナリオに導入するためには、サイバーフィジカル・システム用の証明可能な正しいコントローラを自動合成することが極めて重要である。しかし、ハイブリッド機能や確率的あるいは未知の動作がこの問題を困難にしている。我々は、サイバーフィジカルシステムの離散時間モデルの一種であるマルコフジャンプ線形システム（MJLS）に対して、確率的計算木論理（PCTL）公式を証明可能に満たすようにコントローラを合成する手法を提案する。MJLSは、マルコフ決定過程(MDP)によって支配される、有限の確率的線形ダイナミクスとこれらのダイナミクス間の離散ジャンプから構成される。我々は、このMDPの遷移確率が区間まで既知である場合と、完全に未知である場合を考える。我々のアプローチは、MJLSの離散（モードジャンプ）と連続（確率的線形）の両方の振る舞いを捉える有限状態の抽象化に基づいている。この抽象化を区間MDP(iMDP)として定式化し、いわゆる「シナリオアプローチ」のサンプリング技術を用いて遷移確率の区間を計算し、確率論的に健全な近似を得る。本手法を複数の現実的なベンチマーク問題、特に温度制御と航空機配送問題に適用する。

要約(オリジナル)

Automated synthesis of provably correct controllers for cyber-physical systems is crucial for deployment in safety-critical scenarios. However, hybrid features and stochastic or unknown behaviours make this problem challenging. We propose a method for synthesising controllers for Markov jump linear systems (MJLSs), a class of discrete-time models for cyber-physical systems, so that they certifiably satisfy probabilistic computation tree logic (PCTL) formulae. An MJLS consists of a finite set of stochastic linear dynamics and discrete jumps between these dynamics that are governed by a Markov decision process (MDP). We consider the cases where the transition probabilities of this MDP are either known up to an interval or completely unknown. Our approach is based on a finite-state abstraction that captures both the discrete (mode-jumping) and continuous (stochastic linear) behaviour of the MJLS. We formalise this abstraction as an interval MDP (iMDP) for which we compute intervals of transition probabilities using sampling techniques from the so-called ‘scenario approach’, resulting in a probabilistically sound approximation. We apply our method to multiple realistic benchmark problems, in particular, a temperature control and an aerial vehicle delivery problem.

arxiv情報

提供元, 利用サービス

arxiv.jp, DeepL