Flow-Based Synthesis of Reactive Tests for Discrete Decision-Making Systems with Temporal Logic Specifications

要約

特定の自律システムが複雑な仕様を満たしているかどうかを評価するテストを設計することは、これらのシステムが複雑であるため困難です。
この研究では、時相論理仕様からのリアクティブなテスト合成のためのフローベースのアプローチを提案し、静的およびリアクティブな障害物と動的テスト エージェントで構成されるテスト環境の合成を可能にします。
時相論理仕様は、システム要件やシステムには明らかにされないテスト目標など、望ましいテスト動作を記述します。
合成テスト戦略は、システム状態に応じてシステムの動作に制限を設けます。
テストは最小限の制限で、システムの目的を支援することなく実現可能性を確保しながらテストの目的を達成します (半協力設定)。
オートマトン理論とフロー ネットワークを活用して、混合整数線形プログラム (MILP) を定式化し、テスト戦略を合成します。
動的テスト エージェントの場合、エージェント戦略は MILP のソリューションから構築された GR(1) 仕様に合わせて合成されます。
仕様がテスト エージェントのダイナミクスによって実現できない場合は、戦略が見つかるまで、反例に基づくアプローチを使用して MILP を解決します。
このフローベースのリアクティブなテスト合成はオフラインで実行され、システム コントローラーに依存しません。
最後に、結果として得られるテスト戦略が、さまざまな仕様の 1 対の四足ロボット上でシミュレーションおよび実験で実証されます。

要約(オリジナル)

Designing tests to evaluate if a given autonomous system satisfies complex specifications is challenging due to the complexity of these systems. This work proposes a flow-based approach for reactive test synthesis from temporal logic specifications, enabling the synthesis of test environments consisting of static and reactive obstacles and dynamic test agents. The temporal logic specifications describe desired test behavior, including system requirements as well as a test objective that is not revealed to the system. The synthesized test strategy places restrictions on system actions in reaction to the system state. The tests are minimally restrictive and accomplish the test objective while ensuring realizability of the system’s objective without aiding it (semi-cooperative setting). Automata theory and flow networks are leveraged to formulate a mixed-integer linear program (MILP) to synthesize the test strategy. For a dynamic test agent, the agent strategy is synthesized for a GR(1) specification constructed from the solution of the MILP. If the specification is unrealizable by the dynamics of the test agent, a counterexample-guided approach is used to resolve the MILP until a strategy is found. This flow-based, reactive test synthesis is conducted offline and is agnostic to the system controller. Finally, the resulting test strategy is demonstrated in simulation and experimentally on a pair of quadrupedal robots for a variety of specifications.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google