Formal Methods for Autonomous Systems

要約

形式的手法とは、システム開発に対する厳密で数学的なアプローチを指し、セーフティ クリティカルなシステムの正確性を確立する上で重要な役割を果たしてきました。
形式的手法の主な構成要素はモデルと仕様です。これらはシステム設計における動作と要件に類似しており、形式的な保証を備えたシステムの動作を検証および統合する手段を提供します。
このモノグラフは、自律システム領域における形式的手法の応用に関する最新技術の概要を提供します。
私たちは、閉鎖系、反応性、確率的設定などのさまざまな定式化の下での正しい構築による合成を検討します。
既知の環境でシステムを合成するだけでなく、不確実性の概念に取り組み、形式的手法を使用した学習を採用するシステムの動作を制限します。
さらに、システムが予期された動作から逸脱した場合に正常に戻る方法を確実に認識するための緩和手法である監視を備えたシステムの統合を検討します。
また、形式的手法自体のいくつかの制限を学習によって克服する方法も示します。
最後に、強化学習における形式手法、不確実性、プライバシー、形式手法の説明可能性、規制と認証の今後の方向性について説明します。

要約(オリジナル)

Formal methods refer to rigorous, mathematical approaches to system development and have played a key role in establishing the correctness of safety-critical systems. The main building blocks of formal methods are models and specifications, which are analogous to behaviors and requirements in system design and give us the means to verify and synthesize system behaviors with formal guarantees. This monograph provides a survey of the current state of the art on applications of formal methods in the autonomous systems domain. We consider correct-by-construction synthesis under various formulations, including closed systems, reactive, and probabilistic settings. Beyond synthesizing systems in known environments, we address the concept of uncertainty and bound the behavior of systems that employ learning using formal methods. Further, we examine the synthesis of systems with monitoring, a mitigation technique for ensuring that once a system deviates from expected behavior, it knows a way of returning to normalcy. We also show how to overcome some limitations of formal methods themselves with learning. We conclude with future directions for formal methods in reinforcement learning, uncertainty, privacy, explainability of formal methods, and regulation and certification.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google