BDD for Complete Characterization of a Safety Violation in Linear Systems with Inputs

要約

線形システムの制御設計ツールには通常、安定性を確保するために役立つ極の配置とリアプノフ関数の計算が含まれます。
しかし、制御設計に対するより高い要件を考慮すると、設計者は安全性や時相論理仕様などの他の仕様も満足することが期待され、単純な制御設計ではそのような仕様を満たさない可能性があります。
制御設計者は、安全性をチェックするためのツールとしてモデル チェックを採用し、安全性違反の場合の反例を得ることができます。
線形力学システムの安全性検証のために、いくつかのスケーラブルな検証技術が開発されていますが、そのようなツールはシステムの安全性を評価するための決定手順として機能するだけであり、その結果、安全性違反の証拠として反例が得られます。
ただし、これらのモデル検査方法は、例外的なケースを発見したり、別の次善の安全仕様のために検証アーティファクトを再利用したりすることを目的としたものではありません。
この論文では、線形システムにおける安全違反に対する反例の完全な特徴付けを取得する手法について説明します。
提案された手法は、与えられた時相論理式の安全性検証中に計算された到達可能な集合を使用し、制約伝播を実行し、二分決定図 (BDD) を使用して反例のすべてのモダリティを表します。
大幅に縮小された（サイズの）決定図を取得するために、同型ノードを動的に決定するアプローチを導入します。
さまざまなベンチマークでの徹底的な実験評価により、この削減手法によりノード数が最大 $67\%$ 削減され、デシジョン ダイアグラムの幅が $75\%$ 削減されることがわかりました。

要約(オリジナル)

The control design tools for linear systems typically involves pole placement and computing Lyapunov functions which are useful for ensuring stability. But given higher requirements on control design, a designer is expected to satisfy other specification such as safety or temporal logic specification as well, and a naive control design might not satisfy such specification. A control designer can employ model checking as a tool for checking safety and obtain a counterexample in case of a safety violation. While several scalable techniques for verification have been developed for safety verification of linear dynamical systems, such tools merely act as decision procedures to evaluate system safety and, consequently, yield a counterexample as an evidence to safety violation. However these model checking methods are not geared towards discovering corner cases or re-using verification artifacts for another sub-optimal safety specification. In this paper, we describe a technique for obtaining complete characterization of counterexamples for a safety violation in linear systems. The proposed technique uses the reachable set computed during safety verification for a given temporal logic formula, performs constraint propagation, and represents all modalities of counterexamples using a binary decision diagram (BDD). We introduce an approach to dynamically determine isomorphic nodes for obtaining a considerably reduced (in size) decision diagram. A thorough experimental evaluation on various benchmarks exhibits that the reduction technique achieves up to $67\%$ reduction in the number of nodes and $75\%$ reduction in the width of the decision diagram.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google