Correct-by-Construction Control for Stochastic and Uncertain Dynamical Models via Formal Abstractions

要約

自律システム用の Correct-by-Construction コントローラーの自動合​​成は、セーフティ クリティカルなシナリオでの導入に不可欠です。
このような自律システムは、確率力学モデルとして自然にモデル化されます。
一般的な問題は、確率的時相論理仕様として表される、指定されたタスクを証明できるコントローラーを計算することです。
ただし、確率的不確実性、不正確に既知のパラメータ、ハイブリッド機能などの要因により、この問題は困難になります。
私たちは、さまざまなモデリング仮定の下でこの問題を解決するために使用できる抽象化フレームワークを開発しました。
私たちのアプローチは、確率間隔のあるマルコフ決定プロセス (iMDP) の形式での確率力学モデルの堅牢な有限状態抽象化に基づいています。
当社は、最先端の検証技術を使用して、指定された仕様を満たすことを保証した iMDP 上の最適なポリシーを計算します。
次に、このポリシーを構築することで、これらの保証が動的モデルに引き継がれるフィードバック コントローラーに改良できることを示します。
この短い論文では、この分野における最近の研究を概観し、進行中の研究で取り組むことを目指している 2 つの課題 (スケーラビリティと非線形ダイナミクスの処理に関連する) に焦点を当てます。

要約(オリジナル)

Automated synthesis of correct-by-construction controllers for autonomous systems is crucial for their deployment in safety-critical scenarios. Such autonomous systems are naturally modeled as stochastic dynamical models. The general problem is to compute a controller that provably satisfies a given task, represented as a probabilistic temporal logic specification. However, factors such as stochastic uncertainty, imprecisely known parameters, and hybrid features make this problem challenging. We have developed an abstraction framework that can be used to solve this problem under various modeling assumptions. Our approach is based on a robust finite-state abstraction of the stochastic dynamical model in the form of a Markov decision process with intervals of probabilities (iMDP). We use state-of-the-art verification techniques to compute an optimal policy on the iMDP with guarantees for satisfying the given specification. We then show that, by construction, we can refine this policy into a feedback controller for which these guarantees carry over to the dynamical model. In this short paper, we survey our recent research in this area and highlight two challenges (related to scalability and dealing with nonlinear dynamics) that we aim to address with our ongoing research.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google