满足LTL公式

Question

是AG(~q ∨ Fp) LTL公式在下面的模型中满足吗？为什么或者为什么不？

model？

Answer 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是假的，所以为了满足~q v F p它必须认为F p是TRUE，即它必然是早晚p变成TRUE的情况。
• 存在从S2 s.t.开始的无限路径。 p总是FALSE：从S2跳转到S0并返回的路径，从未触及S1或S3。
• 矛盾：LTL公式不满意。