2

基本的に、モデル チェックでは、モデル 'm' (システムの動作記述) と、システムが満たすプロパティ 'p' を扱います。どちらのアーティファクトでも、モデル チェッカーはモデルがプロパティを満たすかどうかを判断します。

私の質問は、モデル 'm' を LTL 式として指定し、LTL 'm' としてのモデルがプロパティ 'p' を満たすかどうかを確認できるかどうかです。

理論的には、LTL 式 'p' 用とモデル 'm' を記述する LTL プロパティ用の 2 つの Büchi オートマトンを生成できるため、このアプローチはうまくいくと思います。2 つの非決定性オートマトンの共通部分が空の場合、LTL としてのモデル 'm' はプロパティを満たします。

誰かが私にヒントを与えることができますか？出来ますか？

4

1 に答える 1

1

興味深い質問です。短い答えはおそらくノーです。

https://en.wikipedia.org/wiki/Linear_temporal_logic_to_B%C3%BCchi_automaton

通常、モデルのチェック中に、LTL から Buchi Automata への変換が実行されます。これが可能なのは、LTL が Buchi Automata よりも表現力がはるかに低いためです。ただし、既存の設計がある場合、LTL でキャプチャできる可能性は低いです。たとえば、設計に多くの状態が含まれている場合、LTL で問題になる可能性があります。

于 2015-02-05T00:09:12.690 に答える