在模型检测工具NuSMV中，时序逻辑是用来描述系统性质（或形式规约）的形式化语言，包括两类，一类是线性时序逻辑（Linear-time Temporal Logic, LTL）,另一类是分支时序逻辑（也称计算树逻辑，Computing Tree Logic, CTL），二者主要的区别在于采取不同的方式对Kripke结构所对应的计算树分支进行展开。

线性时序逻辑

定义

时态运算符限定于描述从一个给定的状态开始的某条路径上的事件。

特点

• 将时间建模成状态序列，无限延伸到未来，该状态序列称为计算路径（简称“路径”），隐含了整个系统是按着一个路径向前发展演化的，隐含使用全称量词，不适用存在量词（与CTL不同）
• 使用指示未来的连接词（时间操作符），只表达一条路径上的不确定性，而CTL表达多个路径

构成

• 项（terms）：p表示原子命题

• 经典布尔操作

  • ¬(not), v(or), ∧(and)
  • →(imply, if-then): p->q, 如果p发生则会出现q

• 基本时态操作（Basic temporal operators）

  • ☐(G, always), ◇(F, eventually), ○(X, next), U(strong unit)
  • Gp - p holds globally in the future.
  • Fp - p holds sometime（不确定性！）in the future.
  • Xp - p holds next time.
  • pUq - p holds until q holds.

语义

<>p ：p在以后某个时刻会真

[]p ：从当前时刻起，p总是为真

Xp ：p在下一个时刻为真

示例

以红绿灯为例（gr:green ye:yellow re:red）

性质1：信号灯按照“红、黄、绿、红、黄、绿…”的顺序变化
对应的LTL：[] ( (grUye) v (yeUre) v (reUgr) )

性质2：信号灯不能在同一时间出现两种以上的颜色
对应的LTL： [] ( ¬(gr∧ye) ∧ ¬(ye∧re) ∧ ¬(re∧gr) ∧ (gr v ye v re) )

分支时序逻辑

定义

时态运算符限定于从一个给定的状态开始的所有可能路径上。

构成

CTL由路径量词和时态算子构成。

路径量词：

• A（“for all computation paths”，全称量词，将来全部路径）
• E（“exist some computation path” ，存在量词，存在一条将来路径）

时态算子：

• X（next：下一个状态）
• F（future：某个未来的状态）
• G（globally：所有的未来状态）
• U（until：路径上存在某个状态满足性质q，而且它之前的每
  个状态都满足性质p）
• R（release：路径上从第一个状态开始，都要满足性质q，直
  到某个状态满足性质p）

常见表达：

• AX p：在所有未来路径上，公式在下一个状态为真
• AF p：在所有未来路径上，公式在某个状态必然为真
  
• AG p：在所有未来路径上，公式都永远为真
  
• A (p U q)：在所有未来路径都存在：公式p一直为真，直到公式q为真
• EX p：存在一条未来路径，下一状态公式为真
• EF p：存在一条未来路径，公式在某个状态一定为真
  
• EG p：存在一条未来路径，公式永为真
  
• E (p U q)：存在一条未来路径，公式p一直为真，直到公式q为真

示例

以进程访问共享数据为例，假设有两个进程proc1和proc2，当进入“critical”状态表示正在访问共享数据，“entering”状态表示进程请求访问共享数据，当任务调度允许访问后进入“critical”状态访问共享数据。

性质1：不存在进程1和进程2同时进入“critical”状态
对应的CTL：AG ! (proc1.state = critical & proc2.state = critical)

性质2：如果进程1处于“entering”状态（即请求进入“critical”状态），那么最终进程1都会进入“critical”状态
对应的CTL：AG (proc1.state = entering -> AF proc1.state = critical)

参考资料

1. 嵌入式系统的属性与验证
2. NuSMV 2.6 Tutorial

最后

以上就是激动巨人为你收集整理的时序逻辑之线性时序逻辑（LTL）和分支时序逻辑（CTL）对比及典型示例线性时序逻辑分支时序逻辑参考资料的全部内容，希望文章能够帮你解决时序逻辑之线性时序逻辑（LTL）和分支时序逻辑（CTL）对比及典型示例线性时序逻辑分支时序逻辑参考资料所遇到的程序开发问题。

如果觉得靠谱客网站的内容还不错，欢迎将靠谱客网站推荐给程序员好友。