model-checking - モデルの LTL 式を満たす

Question

AG(~q ∨ Fp)以下のモデルで LTL 式は満たされていますか? なぜ、またはなぜではないのですか？

モデル？

Answer 1

演算子は LTL に属していないため、まずLTL式ではAG(~q ∨ Fp)ありません。という意味だったと思います。AGG(~q v Fp)

---

モデリング: NuSMVでシステムをエンコードしましょう:

MODULE main ()
VAR
  state : { S0, S1, S2, S3 };
  p : boolean;
  q : boolean;

ASSIGN
  init(state) := S0;
  next(state) := case
    state = S0 : {S1, S2};
    state = S1 : {S0, S3};
    state = S2 : {S0};
    state = S3 : {S3};
  esac;

INVAR state = S0 <-> (!p & !q);
INVAR state = S1 <-> ( p &  q);
INVAR state = S2 <-> (!p &  q);
INVAR state = S3 <-> ( p & !q);


LTLSPEC G(!q | F p)

そしてそれを確認してください：

~$ NuSMV -int
NuSMV > reset; read_model -i f.smv; go; check_property
-- specification  G (!q |  F p)  is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample 
Trace Type: Counterexample 
-- Loop starts here
-> State: 2.1 <-
  state = S0
  p = FALSE
  q = FALSE
-> State: 2.2 <-
  state = S2
  q = TRUE
-> State: 2.3 <-
  state = S0
  q = FALSE

---

説明: そのため、モデルは LTL 式を満たしていません。なんで？

• G到達可能なすべて~q v F pの状態によって が検証された場合にのみ、式が満たされることを意味します。
• State S2is st~qは FALSE であるため、それを満たすためには、それが TRUE である~q v F p必要があります。つまり、遅かれ早かれTRUE になる必要があります。F pp
• S2stから始まる無限パスpが常に FALSE であることが存在します。つまり、 と の間でジャンプしS2、S0と のどちらにも決して触れないパスS1ですS3。
• 矛盾: LTL式が満たされていません。