Formal Synthesis of Controllers for Safety-Critical Autonomous Systems: Developments and Challenges

要約

近年、自律システムの設計には形式的手法が広く使用されています。
数学的に厳密な手法を採用することにより、形式的手法は、連続ダイナミクスと離散ロジックの間の複雑な相互作用を伴う複雑な動的システムに対して、証明可能な安全性保証を備えた完全に自動化された推論プロセスを提供できます。
このペーパーでは、セーフティ クリティカルな自律システム向けのフォーマル コントローラー合成技術の包括的なレビューを提供します。
具体的には、決定論的、非決定論的、確率的などの多様なシステム モデルに基づいて形式的制御合成問題を分類し、論理、リアルタイム、実数値の領域を含むさまざまな形式的安全性が重要な仕様を分類します。
このレビューでは、抽象化ベースのアプローチや抽象化を必要としない手法など、基本的な形式制御合成手法を取り上げます。
私たちは、形式制御合成におけるデータ駆動型合成アプローチの統合を検討します。
さらに、大規模システムにおけるスケーラビリティの課題に対処するためのさまざまなアプローチに特に焦点を当てて、マルチエージェント システム (MAS) に合わせた正式な手法をレビューします。
最後に、いくつかの最近の傾向について説明し、この分野の研究課題に焦点を当てます。

要約(オリジナル)

In recent years, formal methods have been extensively used in the design of autonomous systems. By employing mathematically rigorous techniques, formal methods can provide fully automated reasoning processes with provable safety guarantees for complex dynamic systems with intricate interactions between continuous dynamics and discrete logics. This paper provides a comprehensive review of formal controller synthesis techniques for safety-critical autonomous systems. Specifically, we categorize the formal control synthesis problem based on diverse system models, encompassing deterministic, non-deterministic, and stochastic, and various formal safety-critical specifications involving logic, real-time, and real-valued domains. The review covers fundamental formal control synthesis techniques, including abstraction-based approaches and abstraction-free methods. We explore the integration of data-driven synthesis approaches in formal control synthesis. Furthermore, we review formal techniques tailored for multi-agent systems (MAS), with a specific focus on various approaches to address the scalability challenges in large-scale systems. Finally, we discuss some recent trends and highlight research challenges in this area.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google