問題タブ [binary-decision-diagram]

私はプログラムの修正/合成プロジェクトに取り組んでいます。私のタスクは、エラー トレース (反例) を取得し、それを完全な状態空間で見つけて、その場所でモデルを修復することです。これを NuSMV 拡張機能として実装したいと考えています。

NuSMV をデバッグして、そのソース コードを理解し、調査しています。ここまでで、BDD FSM を作成する方法を見つけました (compile.c の 520 行目)。状態空間へのプログラムによるアクセスを取得し、モデルに対して修正作業を実行するために、bdd をトラバースする方法を見つけようとしています。NuSMV が bdd fsm を介してプロパティを検証するために使用する再帰的な探索関数をまだ理解できていません。

ドットなどのツールを使用して視覚化できるように、bdd 構造をトラバースする方法を知りたいです。また、そのようなまたは類似のビジュアライゼーションがすでに作成されているかどうかも知りたいです (検索しましたが、空になります)。第二に、私が取り上げた方向が正しいかどうか、または特定のモデルの完全な状態空間を取得するためのより良い方法があるかどうかを確認し、特に得られた反例に関して、それを調査したいと思いますNuSMV を介して。

この質問は、シンボリック モデル チェッカーのシンボリック状態空間を生成する方法に関するものです。最初に、MDD に対してこれを実行したいと思うようになった背景について説明し、次にその質問について詳しく説明します。

Edmund M. Clarke (Model Checking の創設者の 1 人) によるこの講義では、Symbolic Model Checking について紹介します。それは、「産業力」モデルチェッカーがブールエンコーディング（二分決定図、またはBDD）を使用して状態爆発問題を処理すると述べています。ただし、通常のモデル チェックよりも 1 桁多くの状態しか許可されません。プログラムの状態遷移グラフを直接構築する通常のモデル チェックをスキップしました。

より多くの状態を処理する1 (状態空間の爆発問題を回避?!)、一般的なスピードアップ2 (境界のあるモデルのチェック)、状態マッチング手法を使用して状態空間検索を制限するなど、BDD の品質よりも優れていることを説明しているいくつかの論文を見てきました。(制限されたモデル チェックを超えて) 3、および既存の BDD より数桁高速に実行する MDD を使用する[4][5]。

BDDは、サポートされる状態の数を平均で約 10^6 から 10^20 に増やしました。その紙には次のようにも書かれています。

残念ながら、シンボリック手法は、特に状態空間の爆発に悩まされる通信プロトコルなどの非同期システムではうまく機能しないことが知られています。

そのため、MDD または EDD でさえ、モデルのチェックに適しているようです。エッジ値 BDD (EVBDD) もあります。しかし、私の質問は、~MDD のシンボリック状態空間をどのように構築するか (またはどちらが最適か) です。このドキュメントでは紹介していますが、実際に生成する方法については説明していないようです。彼らは次のように述べています。

準縮小、順序付け、非負エッジ値、多値決定図を使用します。

高レベルでの MDD の状態空間生成アルゴリズムと、nodeオブジェクトのプロパティ (C 構造体など) など、システムに関与するデータ構造を説明できるかどうか疑問に思っています。データ構造がどのようなものか、大まかにアルゴリズムがどのように機能するかの全体像が理解できれば、それで十分実装できると考えています。

また、最初のプログラムと仕様で何をする必要があるのか​​ わかりません。したがって、説明が中間オブジェクトを生成する方法をすばやく説明/紹介できれば、それは役に立ちます。これを追加するのは、ある論文で彼らがプログラムをペトリネット形式で持っていて、それを MDD に変換しているのを見たからです。プログラムをペトリネットに変換する方法、またはそれが必要かどうかさえわかりません。基本的に、ソース コードから MDD に移行する方法を大まかに説明します。

この画像が状態空間生成のアルゴリズムだと思いますが、その詳細がよく分からず困っています。具体的には、関連するデータ構造と、「状態」がどこから来ているか、つまり、これらが他のモデルのブール述語であるかどうかなどです。

これも近いようです：

これは同じ論文からの詳細です：

(1)この論文では、Stalmarck の方法 [16] や Davis & Putnam の手順 [7] などのブール決定手順が BDD をどのように置き換えることができるかを示します。この新しい手法は、二分決定グラフの空間爆発を回避し、反例をはるかに高速に生成し、場合によっては検証を高速化します。

(2)この論文の主な結果は、時間制限付きのフォーミュラをチェックする時間の複雑さを O(N) 改善することです。ここで、N は検討中の CTMC の状態の数です。

(3)複雑な入力を持つプログラムを分析するためのシンボリック実行とモデル チェックの組み合わせを提案した以前の研究に基づいています [14,19]。その作業では、モデル チェッカーの入力サイズおよび (または) 検索深度に制限を設けました。ここでは、有界モデル チェックの先を見据え、状態空間検索を制限するための状態マッチング手法を研究します。シンボリック状態が別のシンボリック状態に包含されるタイミングをチェックする手法を提案します。

(4)多値決定グラフを用いて非同期システムの状態空間を生成するための新しいアルゴリズムを提示します。関連する作業とは対照的に、システムの次の状態関数を単一のブール関数としてではなく、整数関数の外積としてエンコードします。これにより、さまざまな反復戦略を適用してシステムの状態空間を構築できます。特に、飽和と呼ばれる新しいエレガントな戦略を導入し、ツール SMART に実装します。通常、既存の BDD ベースの状態空間ジェネレーターよりも数桁高速に実行されることに加えて、アルゴリズムの必要なピーク メモリは、多くの場合、状態空間全体を格納するために必要な最終メモリに近くなります。

(5)二分決定図 (BDD) に基づくシンボリック手法は、ハードウェア回路と同期コントローラーの時間的特性を推論するために広く使用されています。ただし、共有イベントを介して通信する独立して動作するサブシステムで構成される通信プロトコルや分散ソフトウェアなど、インターリーブ セマンティクスに基づくシステムの基礎となる巨大な状態空間を扱う場合、パフォーマンスが低下することがよくあります。デシジョン ダイアグラムを使用した状態空間探索手法は、多くのイベント ベースおよびコンポーネント ベースのシステム モデルの基礎となるインターリーブ セマンティクスを活用することで大幅に改善できます。

これに近づく：

到達可能な状態空間 X_reach は、固定点方程式 X ⊆ X_init ∪ T(X) の最小解として特徴付けることができます。アルゴリズムBfsはこの固定点計算を正確に実装します。ここで、集合と関係はそれぞれ L レベルと 2L レベルの MDD を使用して格納されます。つまり、ノード p は、特性関数 v_p を満たす集合 X_p をエンコードします。

v_p(i_L,...,i_1) = 1 ⇔ (i_L,...,i_1) ∈ X_p.

セットの和集合は Or 演算子をそれらの特性関数に適用することで簡単に実装され、1 ステップで到達可能な状態の計算は関数 RelProd を使用して実装されます (もちろん、MDD を使用する場合はこれらの関数の MDD バージョンを使用する必要があります)。 BDD の代わりに)。幅優先のシンボリック検索を実行するため、アルゴリズム Bfs は、初期状態から到達可能な状態までの最大距離とまったく同じ回数の反復で停止します。

次のブール関数があるとします。

ここで、それらから二分決定図を作成したいと思います。私はいくつかの論文を調べましたが、これらのようなネストされた論理式からそれらを構築する方法を見つけることができませんでした.

ブール関数は根付き有向非巡回グラフであると言われています。いくつかの非ターミナル ノードとターミナル ノードがあります。次に、各非終端ノードが、2 つの子ノードを持つブール変数(関数ではない) によってラベル付けされていることを示しています。上記の関数定義から、ブール変数が何であるかわかりません。ノードから子aまたはノードへのエッジは、それぞれノードの 0 または 1 への割り当てbを表します。同形サブグラフがマージされ、2 つの子が同形であるノードが削除された場合、縮小されたと呼ばれます。これは縮小順序二分決定図 (ROBDD) です。

それから、そして私が遭遇したすべてのリソースから、これらの関数をBDD/ROBDDに変換する方法を理解できませんでした:

あるいは、変換する必要があるのは次のようなものかもしれません:

これを根付き有向非循環グラフにするために何をする必要があるかについての説明を探しています。データ構造がどのように見えるかを知ることも役に立ちます。これだけのようです：

しかし、問題は、これらの関数foo、bar、およびからグラフを構築する方法bazです。