線性時态邏輯之 實際模式規範

上一篇說了線性時态邏輯LTL。那麼LTL公式能夠檢測那些實際相關的性質呢？

我們可以要求實際的系統具有以下一些性質：

1）在1）started成立但在ready不成立時，不可能到達狀态：

          G ┐（ started ∧┐ ready ）

 2）對任何狀态，如果一個（對某些資源）請求（request）發生，那麼它将最終被确認（acknowledged)：

          G（requested→F acknowledged ）

3）在每一條計算路徑上，一個特定過程常“使能” （enabled）無限多次：

         G F enabled

4）不管發生什麼情況，一個特定過程最終被永久死鎖（deadlock）：

         F G deadlock

5）如果該過程被使能無限次，則它運作無限多次：

         G F enabled →G F running。

例：如果有乘客想去第五層，一個上行的電梯在第二層不改變方向：

           G（floor2∧ directionup ∧ButtonPressed5→（ directionup ∪floor5））

          此處，原子描述是由系統變量構造的布爾表達式，比如floor2.

有些事情LTL不可能表達出來，如：

1.從任何狀态出發，都能達到一個重新開機（restart）狀态（即：從所有狀态出發都存在一條路徑到達一個滿足restart的狀态。

         2.電梯可以閑置在第三層不開門（即：從處于第三層的狀态出發，存在一條路徑，沿着該路徑電梯停留在原地）。

 LTL不能表達這些陳述，因為它不能直接斷定這些路徑的存在性。

兩個LTL公式Ф和ψ是語義等價的（或簡單說是等價的）并寫為Ф≡ψ，如果對所有模型M以及M中的所有路徑π： π╞Ф當且僅當π╞ψ。

Ф與ψ等價意味着Ф與ψ在語義上是可以互換的。

F和G是互相對偶的，而X與其自身對偶：

1）┐GФ≡F┐Ф

2）┐FФ≡G┐Ф

3)  ┐XФ≡X┐Ф。

U和R也是互相對偶的：

1） ┐（ФUψ）≡ ┐ФR┐ψ

2） ┐（ФRψ）≡ ┐ФU┐ψ

F關于∨，G關于∧的配置設定律：

1）F（Ф∨ψ）≡FФ∨Fψ

2）G（Ф∧ψ）≡GФ∧Gψ

此外，還有等價關系：

  1）FФ≡┬UФ

  2）GФ≡┴RФ

  3）ФUψ≡ФWψ∧Fψ

  4）ФWψ≡ФUψ∨GФ

  5）ФWψ≡ψR（Ф∨ψ）

  6）ФRψ≡ψW（Ф∧ψ）