满足模型中的LTL公式答案

【问题标题】：satisfying the LTL formula in model满足模型中的LTL公式
【发布时间】：2016-06-11 17:16:39
【问题描述】：

AG(~q ∨ Fp) LTL 公式是否满足以下模型？为什么或为什么不？

型号？

【问题讨论】：

不要依赖附加链接。当链接断开时，这个问题会变糟。在问题中写下要点。或者，如果那是一张图片，请正确附上。这不是怎么做的
@Aminah Nuraini 谢谢，我改了。

标签： model-checking nusmv

【解决方案1】：

首先AG(~q ∨ Fp) 不是 LTL 公式，因为运算符AG 不属于LTL。我假设您的意思是G(~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 被每个可达状态验证时，公式才成立。
状态 S2 是 s.t. ~q 是 FALSE，所以为了满足 ~q v F p，它必须保持 F p 是 TRUE，即 这必然是迟早 p 变为 TRUE 的情况。
存在从S2 s.t. 开始的无限路径。 p 始终为 FALSE：从S2 跳转到S0 并返回且从未触及S1 或S3 的路径。
矛盾：LTL 公式不满足。

【讨论】：

非常感谢。