1

2 つの LTL を比較して、一方が互いに矛盾する可能性があるかどうかを確認するにはどうすればよいですか? 階層的なステート マシンと、各ステートの動作を説明する LTL があるためです。ローカル LTL がグローバル LTL と矛盾する可能性があるかどうかを知る必要があります。「機能仕様と自動競合検出」という記事で、L(f) の交差 L(g) が空である場合、2 つの LTL プロパティ f と g が矛盾することを見ました。そして、これはまさに、プログラムとして f とプロパティとして ¬g を使用したモデル チェックの問題です。誰でもこれで私を助けることができますか？LTL f を SPIN/Promela のプログラムに変換するにはどうすればよいですか??

ありがとう。

4

1 に答える 1

1

以下は私にとってはうまくいきます。(警告: 私はこれを公式文書で見たことがありません。これは、これを行うための他のより良い方法があることを意味する可能性があります。または、私が十分に調べていないことを意味します。)

[] <> p && [] <> qを意味するかどうかを確認し <> (p && q)ます。（そうではありません。）

すべての遷移を実行できる簡単なプロセスPを記述し、クレームを LTL プロパティとして記述しますA。

bool p; bool q;

active proctype P () {
  do :: d_step { p = false; q = false } 
     :: d_step { p = false; q = true }  
     :: d_step { p = true; q = false } 
     :: d_step { p = true; q = true }  
  od
}

ltl A { (([] <> p) && ([] <> q)) -> <> (p && q) }

(2016 年 11 月 1 日編集: 初期状態が隠されているためにいくつかの遷移が欠落している可能性があるため、これは正しくない可能性があります。Spinで初期化されていない変数を作成する方法を参照してください。 )

次に、これをファイルcheck.pmlに入れて、

spin -a check.pml
cc     pan.c   -o pan
./pan -a -n
./pan -r check.pml.trail -v

p主張の否定のモデルを示します (とqが無限に頻繁に真であるが、決して真ではない最終的に周期的なトレイルp && q)。

ダブルチェック: クレームの結論を に変更すると<> (p || q)、反例がなく、含意が有効であることを証明できます。

あなたの場合、主張は ! (f && g)（同時に真実であってはなりません）です。

些細なプロセスのコードを小さくする賢い方法がおそらくあるでしょう。

また、3 番目のコマンドは実際には./pan -a -i -n(-i最短の例を見つけるため) ですが、警告が表示されます。そして、それはより短いサイクルを見つけます。

于 2015-11-05T19:26:13.417 に答える