线性时态逻辑之 实际模式规范

上一篇说了线性时态逻辑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（Ф∧ψ）