软件理论基础——第四章时态逻辑

4.1线性时态逻辑系统LTL

定义4.1.1 LTL公式的定义

{~,∧}{~，∨}{~，->}

pure future formates

与之对应的有pure past formaces

T，什么意思？

定义4.1.2 迁移系统的定义

迁移关系是S上的连续关系（连续关系是指有出边）

定义4.1.3路

无限状态序列，通常写成s0-> s1->s2->……用表示π，

πⁱ指从π的第i个状态开始的路，π=π⁰

定义4.1.4 路满足公式

路满足p,指路径的第一个状态满足p

8.π^{2指路的第二个状态}

11在满足ψ之前φ一直满足

12相比11多了若一种情况，所有的状态都满足φ

13把12中的φ和ψ调换位置即可，ψ一直成立，直到φ成立，即φ释放了ψ

定义4.1.5状态满足公式

定义4.1.6语义等价φ≡ψ　　从路的角度定义

定义4.1.7语义等价等价刻画 　　从状态角度定义

定理4.1.8 

德摩根律，幂等律

G可以用F表示

F可以用U表示

X 必不可少

充足集{X,U}

定理4.1.9 连接词相互定义

连接词充分性{U,X},{R,X},{W,X}

4.2计算树逻辑CTL