定义4.1.1 LTL公式的定义
{~,∧}{~，∨}{~，->}
pure future formates
与之对应的有pure past formaces
T，什么意思？
定义4.1.2 迁移系统的定义
迁移关系是S上的连续关系（连续关系是指有出边）
定义4.1.3路
无限状态序列，通常写成s0-> s1->s2->……用表示π，
πi指从π的第i个状态开始的路，π=π0
定义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}