2

NuSMV でモデル チェック用の有効な CTL または LTL 式を作成しようとしています。

ゲーム内に変数があり、アクターがお互いを捕まえようとして走り回っています。変数は State_Of_Game : {Win,Lose,Playing}

そして、すべての開始状態から、ゲームは勝ったり負けたりする可能性があることを表現したいと思います。

では、これを CTL または LTL でどのように実装すればよいでしょうか?

AG (S_O_G = Win | S_O_G = Lose) のようなものを考えていましたが、すべての開始状態から見られるように実装する方法がわかりません。

4

2 に答える 2

3

私はSMV表記に詳しくないので、これについては推測ですが、重要なポイントは次のとおりです。

  1. 外側のすべての状態を定量化することを避けるために: すべてのゲームが勝敗のどちらかになる可能性があるとは言いたくありませんが、最初のゲームだけです。したがって、最も外側のモダリティのない開始状態で式を作成するだけです

  2. 論理和ではなく論理積を使用するには: 勝者と敗者の両方を主張したい

  3. 各ブランチをラップする個別のモダリティが必要です。勝者、敗者は、条件を達成することが可能であるという実存的な主張です。

必要な式は次のとおりだと思います: (EG SOG=Win) & (EG SOG=Lose) ルートで、これは init/start 句のようなもの、または名前付きルート句でのアサートを意味する可能性があります。SMV が EG モダリティを持っていない場合は、同等の EG p = !(AG !p) を使用して AG に変換できます。この 2 つは De Morgan 双対であるためです。

于 2013-12-13T09:30:55.033 に答える