滿足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公式不滿意。