2

この質問は、シンボリック モデル チェッカーのシンボリック状態空間を生成する方法に関するものです。最初に、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 は、初期状態から到達可能な状態までの最大距離とまったく同じ回数の反復で停止します。

mdd Bfs(mdd Xinit) is
local mdd p;
  p ← Xinit;
  repeat
    p ← Or(p, RelProd(p, T ));
  until p does not change;
  return p;

bdd Or(bdd a, bdd b) is
local bdd r, r0, r1;
local level k;
  if a = 0 or b = 1 then return b;
  if b = 0 or a = 1 then return a;
  if a = b then return a;
  if Cache contains entry hORcode, {a, b} : ri then return r;
  if a.lvl < b.lvl then
    k ← b.lvl;
    r0 ← Or(a, b[0]);
    r1 ← Or(a, b[1]);
  else if a.lvl > b.lvl then
    k ← a.lvl;
    r0 ← Or(a[0], b);
    r1 ← Or(a[1], b);
  else • a.lvl = b.lvl
    k ← a.lvl;
    r0 ← Or(a[0], b[0]);
    r1 ← Or(a[1], b[1]);
  r ← UniqueTableInsert(k, r0, r1);
  enter hORcode, {a, b} : ri in Cache;
  return r;

bdd RelProd(bdd x, bdd2 t) is • quasi-reduced version
local bdd r, r0, r1;
  if x = 0 or t = 0 then return 0;
  if x = 1 and t = 1 then return 1;
  if Cache contains entry hRELPRODcode, x, t : ri then return r;
  r0 ← Or(RelProd(x[0], t[0][0]), RelProd(x[1], t[1][0]));
  r1 ← Or(RelProd(x[0], t[0][1]), RelProd(x[1], t[1][1]));
  r ← UniqueTableInsert(x.lvl, r0, r1);
  enter hRELPRODcode, x, t : ri in Cache;


mdd Saturation(mdd Xinit) is
  return Saturate(L, Xinit);

mdd Saturate(level k, mdd p) is
local mdd r, r0, ..., rnk−1;
  if p = 0 then return 0;
  if p = 1 then return 1;
  if Cache contains entry hSATcode, p : ri then return r;
  for i = to nk − 1 do
  ri ← Saturate(k − 1, p[i]);
  repeat
  choose e ∈ Ek, i, j ∈ Xk, such that ri 6= 0 and Te[i][j] 6= 0;
  rj ← Or(rj , RelProdSat(k − 1, ri, Te[i][j]));
  until r0, ..., rnk−1 do not change;
  r ← UniqueTableInsert(k, r0, ..., rnk−1);
  enter hSATcode, p : ri in Cache;
  return r;

mdd RelProdSat(level k, mdd q, mdd2 f) is
local mdd r, r0, ..., rnk−1;
  if q = 0 or f = 0 then return 0;
  if Cache contains entry hRELPRODSATcode, q, f : ri then return r;
  for each i, j ∈ Xk such that q[i] 6= 0 and f[i][j] 6= 0 do
  rj ← Or(rj , RelProdSat(k − 1, q[i], f[i][j]));
  r ← Saturate(k, UniqueTableInsert(k, r0, ..., rnk−1));
  enter hRELPRODSATcode, q, f : ri in Cache;
  return r.
4

1 に答える 1