A General Verification Framework for Dynamical and Control Models via Certificate Synthesis

要約

制御理論の新たな分野は、自律モデルまたは制御モデルに必要な (おそらく複雑な) システム動作の仕様に関する証明書学習に特化しており、機能ベースの証明によって分析的に検証されます。
ただし、これらの複雑な要件を満たすコントローラーの合成は一般に簡単な作業ではなく、最も専門的な制御エンジニアでも困難な場合があります。
そのため、コントローラーを設計し、広範囲にわたる精緻な仕様を分析できる自動技術が必要になります。
このペーパーでは、システム仕様をエンコードし、対応する証明書を定義するための一般的なフレームワークを提供し、コントローラーと証明書を正式に合成するための自動化されたアプローチを紹介します。
私たちのアプローチは、SMT ソルバーを使用して正確性の正式な保証を提供しながら、ニューラル ネットワークの柔軟性を利用して候補制御および証明書機能を提供し、制御のための安全な学習の広範な分野に貢献します。
私たちはプロトタイプのソフトウェア ツールを開発することでフレームワークをテストし、大規模で多様なベンチマーク スイートに対する制御と証明書の合成を介した検証でその有効性を評価します。

要約(オリジナル)

An emerging branch of control theory specialises in certificate learning, concerning the specification of a desired (possibly complex) system behaviour for an autonomous or control model, which is then analytically verified by means of a function-based proof. However, the synthesis of controllers abiding by these complex requirements is in general a non-trivial task and may elude the most expert control engineers. This results in a need for automatic techniques that are able to design controllers and to analyse a wide range of elaborate specifications. In this paper, we provide a general framework to encode system specifications and define corresponding certificates, and we present an automated approach to formally synthesise controllers and certificates. Our approach contributes to the broad field of safe learning for control, exploiting the flexibility of neural networks to provide candidate control and certificate functions, whilst using SMT-solvers to offer a formal guarantee of correctness. We test our framework by developing a prototype software tool, and assess its efficacy at verification via control and certificate synthesis over a large and varied suite of benchmarks.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google