上一篇说了线性时态逻辑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（Ф∧ψ）
版权声明
本文仅代表作者观点，不代表百度立场。
本文系作者授权百度百家发表，未经许可，不得转载。
