CTL fomula直到包含暗示

當我使用NuSMV工具來驗證我的CTL是否正確時，我遇到一個讓我如此困惑的問題。CTL fomula直到包含暗示

我的模型是

和這裏的NuSMV代碼：

MODULE main 
VAR 
    state : {ROOT, A1, B1, C1, D1, F1, M1}; 

ASSIGN 
    init(state) := ROOT; 

    next(state) := case 
    state = ROOT : A1; 
    state = A1 : {B1, C1}; 
    state = B1 : D1; 
    state = D1 : F1; 
    TRUE : state; 
    esac; 

CTLSPEC 
    AG(state=A1 -> AX (A [ state=B1 U (state=D1 -> EX state=F1) ])); 
CTLSPEC 
    AG(state=A1 -> AX (A [ state=B1 U (state=F1 -> EX state=C1) ])); 
CTLSPEC 
    AG(state=A1 -> AX (A [ state=M1 U (state=F1 -> EX state=C1) ]));

我CTL公式如下：

"AG(A1 -> AX (A [ B1 U (D1 -> EX (F1) ) ]))"
"AG(A1 -> AX (A [ B1 U (F1 -> EX (C1) ) ]))"
"AG(A1 -> AX (A [ M1 U (F1 -> EX (C1) ) ]))"

NuSMV驗證了上述三個公式所有這些都被證明是正確的。

所以我的問題是爲什麼公式2和公式3是真的？

來源

2015-04-23 victoroverflow

這個問題很舊，但我認爲它仍然值得回答，因爲這個問題可能會讓其他人產生誤解。

對於所有路徑（s，s2，s3，s4，... s），M，s？A [φUψ] iff。 si Rt si + 1存在狀態sj s.t. M，sj⊨ψ和M，si⊨φ對於所有i < j。

所以，要驗證的屬性，φ必須是真實的，直到當ψ火災。

說明：A [ FALSE U TRUE ]總是被驗證。

現在，你的屬性有什麼問題？

首先是平凡驗證。
第二公式要求開始B1和C1驗證A [ B1 U (F1 -> EX (C1) ) ]兩者的路徑。後一個公式意味着B1應該爲TRUE，直到當我們達到一個狀態，其中F1 - > EX C1成立。該子公式可以翻譯成！F1或EX C1，這意味着我們需要打要麼在A.F1是假的狀態或在B.F1是一種境界TRUE，並存在下一個狀態，其中C1爲真。
- 讓我們考慮的路徑開始B1第一：
  - 不存在其中B.驗證狀態，因爲F1沒有一個繼任
  - 狀態D1確實驗證條件答：爲B1開始的路徑。
- 我們還需要驗證從開始的路徑上的相同屬性C1。在這裏，狀態C1不驗證φ，但它確實驗證ψ因爲條件A.這種狀態是千真萬確的。因此，A [ B1 U (F1 -> EX (C1) ) ]成立。
由於A [ B1 U (F1 -> EX (C1) ) ]被驗證爲狀態A1的兩個後繼者，第二個公式驗證。
第三個公式完全一樣。這兩個周圍的路徑的時間開始在B1和C1驗證屬性A [ M1 U (F1 -> EX (C1) ) ]因爲在既不是兩種狀態F1是立即真實的，因爲每個條件A.我先前提到的。

來源

2016-04-01 15:59:23

CTL fomula直到包含暗示

回答

相關問題