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, Google