Bisimulation Learning

要約

非常に大きく、場合によっては無限の状態空間を持つ状態遷移システムの有限バイシミュレーションを計算するためのデータ駆動型アプローチを導入します。
私たちの新しい技術は、決定論的システムのスタッターの影響を受けないバイシミュレーションを計算します。これは、各クラスのランキング関数とともに状態分類器を学習する問題として特徴づけられます。
私たちの手順では、サンプル状態の有限データセットから候補状態分類器と候補ランキング関数を学習します。
次に、充足可能性モジュロ理論の解法を使用して、これらが状態空間全体に一般化するかどうかをチェックします。
肯定的な答えが得られた場合、この手順は、分類器がシステムの有効なスタッターの影響を受けないバイシミュレーションを構成していると結論付けます。
否定的な答えが返されると、ソルバーは分類器が主張に違反する反例状態を生成し、それをデータセットに追加し、有効な二重シミュレーションが見つかるまで反例に基づく帰納合成ループで学習とチェックを繰り返します。
私たちは、リアクティブ検証やソフトウェア モデル チェックに至るまでのさまざまなベンチマークで、実際に私たちの手法が代替の最先端ツールよりも高速な検証結果をもたらすことを実証しています。
私たちの方法は、次の演算子なしで線形時相論理の効果的な検証を可能にし、システム診断用に解釈可能な簡潔な抽象化を生成します。

要約(オリジナル)

We introduce a data-driven approach to computing finite bisimulations for state transition systems with very large, possibly infinite state space. Our novel technique computes stutter-insensitive bisimulations of deterministic systems, which we characterize as the problem of learning a state classifier together with a ranking function for each class. Our procedure learns a candidate state classifier and candidate ranking functions from a finite dataset of sample states; then, it checks whether these generalise to the entire state space using satisfiability modulo theory solving. Upon the affirmative answer, the procedure concludes that the classifier constitutes a valid stutter-insensitive bisimulation of the system. Upon a negative answer, the solver produces a counterexample state for which the classifier violates the claim, adds it to the dataset, and repeats learning and checking in a counterexample-guided inductive synthesis loop until a valid bisimulation is found. We demonstrate on a range of benchmarks from reactive verification and software model checking that our method yields faster verification results than alternative state-of-the-art tools in practice. Our method produces succinct abstractions that enable an effective verification of linear temporal logic without next operator, and are interpretable for system diagnostics.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google