线性时间逻辑(LTL)

linear-time logic，提供了一种非常直观但是在数学上又很精确的表示方法来描述线性时间性质。在70年代后期，Pnueli提出将线性时序逻辑应用于验证复杂计算机系统。LTL一般通过对程序建模来描述交错序列的属性，但不能描述不同状态间的变化。

LTL的语法

TL在静态逻辑u基础之上定义，利用一阶命题作为u的一个实例，定义为：

φ::= true | a | φ 1 ∧ φ 2 | ¬φ | ◯φ | φ 1 U φ 2

LTL公式的基本成分是原子命题，同时LTL公式一般通过一个无限状态序列x0x1x2…来解释：

上图所示的无限状态序列解释如下，a表示a在当前时刻成立，在轨迹表现为在第一个位置成立

• a表示a在下一个时刻成立，在轨迹表现为第二个位置成立；

• ◯a表示a在下一个时刻成立，在轨迹表现为第二个位置成立；

• aUb表示直到b成立前，a一直成立；

• ◊a=True U a，表示的是a最终(eventually)能够成立，在轨迹上表现为，在某一个时刻的时候a成立；

• □a表示a总是(always)成立，即在全部的时刻都成立，在轨迹上表现为每个位置都成立，□ a=¬◊¬a ；

LTL在无限字上的语义

用ζk表示以xk开始的序列ζ=x0x1x2…的后缀序列LTL在无限字上的语义可以表示为：

• ζk⊨true

• ζk⊨a当且仅当x0⊨a，即a∈x0

• ζk⊨φ1∧φ2当且仅当ζk⊨φ1 and ζk⊨φ2

• ζk⊨¬ φ当且仅当σ ⊭ φ

• ζk⊨ ◯φ当且仅当ζk+1⊨φ

• ζk⊨ ◊φ当且仅当存在i≥k满足ζi⊨φ

• ζk⊨□φ当且仅当对于每个i≥k均有ζi⊨φ

• ζk ⊨□◊φ当且仅当对每一个ζ的后缀ζ’ ◊φ都成立

• ζk ⊨◊□φ当且仅当后缀ζ’满足□φ

在此基础上，再定义一个额外的模态运算符V，称为释放（release），书上的定义为当φ1永远满足或φ1保持满足直到（后缀上）某个点使φ1和φ2都成立，则φ1Vφ2对于序列ζk都成立。

LTL规约连接规则

• φ v μ = ¬( (¬φ) ∧ (¬μ) )
• φ → μ = (¬φ) v μ
• φ ↔ μ = (φ → μ) ∧ (μ→ φ)
• ◊ φ = true **U **φ
• □ φ = ¬ ◊ ¬ φ
• φ V μ = ¬( (¬φ) U (¬μ) )

LTL简单示例

如下图，展示了一个简单的弹簧模型：

我们能够拉伸这个弹簧然后释放掉。拉伸弹簧过后，弹簧有三种可能的状态：失去弹性、保持拉伸状态或者恢复原来的形状。所以系统中设置三个状态，s1：初始状态（弹簧原态）、s2：拉伸状态、s3：拉伸且失去弹性状态。同时将每个状态用集合AP={extended（拉伸），malfunction(失效)}进行标记。

• s1没有用上述任何状态标记，则s1⊨¬extended∧¬malfunction。
• s2被标记为extend，则s2⊨extended∧¬malfunction。
• s3被标记为extended，malfunction，则s3⊨extended∧malfunction。

假设此系统拥有无限数目的序列如下所示：

下面给出几个LTL公式，分析ζ2是否满足。

• ζ2 ⊭extended：公式extended并没有使用任何时序运算符，因此在ζ2的第一个状态对它进行解释。S1并没有被extended所标记，因此公式extended在ζ2中不成立。
• ζ2⊨◯extended。下一时刻运算符在公式中被用来断言序列中的第二个状态，也就是s2满足命题extended。
• ζ2⊨◊extended。右边公式读作“终将被拉伸”，断言序列中存在某个状态满足extended，ζ2显然满足此断言。
• ζ2⊭（¬extended）。右边公式读作“总是会被拉伸”，断言序列每个状态extended都会成立。ζ2的一三状态都不满足extended，所以此LTL公式对ζ2不成立。
• ζ2⊨□◊extended。右边公式读作“最终总是会被拉伸”，断言序列在某一状态后的所有状态extended都会成立。显然，ζ2的第四个状态之后，extended总会被满足。所以此LTL公式对ζ2成立。
• ζ2⊭(¬extended)U malfunction。右边公式读作“直到弹簧失效才会被拉伸。言外之意就是，为了让此公式成立，ζ2需要有一个状态满足malfunction，且在这个状态前的所有状态又必须满足¬extended。我们查看ζ2序列第五个状态s3满足malfunction，而二四状态显然不满足¬extended，所以此LTL公式对ζ2不成立。

LTL公理化

为了证明给定时序公式φ是有效的，为命题化线性时序逻辑给定一组公理。需要注意的是在此证明系统下，释放运算符V会被去除(例如：μVφ=¬((¬μ)U(¬φ))。

• 公理系统的第一部分由八条公理组成，如下所示：

• 第二部分由一个对命题逻辑充分完备的公理系统组成。在系统中，允许用命题公式来实例化公理和证明规则中 的模板变量，在可以用任意命题LTL公式进行替换。
• 第三部分是一个证明规则：
  
  一个证明规则可以表示为：将一条前提写在横线上面，将结论写在下面。那么这条证明规则大致意思就是如果μ成立，那么□μ也成立。

交通灯实例

一个交通灯能在绿色、黄色、红色之间变换，其底层逻辑u是一个命题逻辑。命题re、ye、gr分别对应红灯、黄灯和绿灯。交通灯的颜色按如下顺序变换，并可以无限变换下去：
g r e e n → y e l l o w → r e d → g r e e n green→yellow→red→green green→yellow→red→green
交通灯在任意时刻仅亮一种颜色，这是系统的一个不变量，用LTL语言可以描述为：
□ ( ¬ ( g r ∧ y e ) ∧ ¬ ( g r ∧ y e ) ∧ ¬ ( g r ∧ y e ) ∧ ( g r ∨ y e ∨ r e ) ) □(¬(gr∧ye)∧¬(gr∧ye)∧¬(gr∧ye)∧(gr∨ye∨re)) □(¬(gr∧ye)∧¬(gr∧ye)∧¬(gr∧ye)∧(gr∨ye∨re))
灯在绿灯状态时，他在变成黄灯之前会一直保持绿灯状态，用LTL可以表示为：
□ ( g r → ( g r U y e ) ) □(gr→(gr U ye)) □(gr→(grUye))
则变化规则用LTL语言表示为：
□ ( ( g r U y e ) ∨ ( y e U r e ) ∨ ( r e U g r ) ) □((gr U ye) ∨(ye U re) ∨(re U gr)) □((grUye)∨(yeUre)∨(reUgr))

互斥进程实例

假设有一对共享某资源的互斥进程P1、P2，他们不能同时使用某资源，我们使用一个特殊机制对他们进行控制，在该机制中，为每个进程设置一临界区，进程进入临界区之后才能使用资源且一次仅供一个进程进入；再为它们设置尝试区，在进入临界区之前，每个进程首先进入尝试区，表明进入临界区的目的。首先，我们定义一些描述需求的命题：

tryCSi：进程pi进入它的尝试区（试图进入临界区）。
inCSi：进程pi在它的临界区CSi中。

其次，利用上面的命题和LTL语言定义系统属性：

1. 互斥性：任何时间里只有一个进程能够在它的临界区里。
   □ ¬ ( i n C S 1 ∧ i n C S 2 ) □¬(inCS1∧inCS2) □¬(inCS1∧inCS2)
2. 响应能力属性：每个尝试进入临界区的进程最终都能够获取资源进入临界区。
   □ ( t r y C S i → ◊ i n C S i ) □(tryCSi→◊inCSi) □(tryCSi→◊inCSi)
3. 互斥协议属性：当一个进程进入它的尝试区时他将会停留在里面直到它进入自己的临界区。
   □ ( t r y C S i → （ （ t r y C S i U i n C S i ） ∨ □ t r y C S i ） □(tryCSi→（（tryCSi U inCSi）∨ □tryCSi） □(tryCSi→（（tryCSiUinCSi）∨□tryCSi）

标签：状态,逻辑,extended,gr,ye,线性,成立,LTL
来源： https://blog.csdn.net/weixin_43824169/article/details/121302430