第6章时态逻辑

1,Chapter 6 时态逻辑,（一）模态逻辑 （1） 基本概念 （2） Kripke结构 （3）模态逻辑的类型 （二）线性时态逻辑 （1）命题线性时态逻辑 （2）一阶线性时态逻辑 （三） 计算树逻辑 （1） CTL （2） CTL* （四）模型检验 （1）标记算法 （2）资源共享协议问题,2,（一） 模态逻辑,自然语言中有一类用于表示事物的“势态”，人的“情态”，以及过程的“变迁”（历史或未来）的词，称之为模态词例如，“必然、可能”，“应该、允许”，“知道、认可”，“一贯、偶然”等 模态词和命题连接可以生成新的命题例如，“火星上可能有生命”就是“可能”与“火星上有生命”所组成的复合命题 早期，由于模态词的语义不清楚，认为模态词不是逻辑概念，只把它们看作文学修辞，主张“必然A”与“A”相同，“不可能A”与“﹁A”相同3,（一） 模态逻辑,如果说这种做法在数学中勉强行得通，那么在日常推理中就寸步难行，因为“A真但是未必A必然为真”之类的说法，几乎是常识例如，“张三是年级第1名”未必有“张三必然是年级第1名” 模态逻辑起源于亚里斯多德（Aristole）将“必然、可能”这一对模态词看作逻辑概念，并详细讨论了它们的逻辑性质。

4,（一） 模态逻辑,（1） 基本概念 模态词: 模态（modal）词，也称为模态算子，是构成模态逻辑中复合命题的基本运算常用基本模态词包括：必然（）和可能（） 模态逻辑:模态逻辑是经典命题逻辑和一阶谓词逻辑的扩展形式基于命题逻辑的扩展称为模态命题逻辑，基于一阶谓词逻辑的扩展称为模态一阶逻辑 模态逻辑通过引入 “可能”和“必然”两个模态词，从而能够对可能世界中的命题进行描述和演算5,,例如，对于命题 P：火星上有生命，那么，P表示火星上必然有生命；P表示火星上可能有生命 模态逻辑中的模态词必然（）和可能（）存在如下关系： P = ﹁﹁P （P﹁﹁P） P = ﹁﹁P （P﹁﹁P）,6,（1） 基本概念,模态命题逻辑公式:简称为MPL（Modal Propositional Logic）公式，定义如下： ① 原子命题（命题常元或命题变元）是MPL公式； ② 如果A、B是MPL公式，那么(﹁A)、(AB)、(AB)、 (AB)、(AB)是MPL公式； ③ 如果A是MPL公式，那么(A)和(A)是MPL公式； ④ 当且仅当有限次地使用①②③所组成的符号串是MPL公式。

MPL公式的巴科斯范式（BNF:Backus normal form）表示为：（p是原子命题公式）  :: = p|()|()|()|()|()|()|(),一些反映模态词性质的MPL公式： AA 必然A真则A真； AA A真则可能A真； AA 必然A真则可能A真； A﹁﹁A 必然A当且仅当不可能﹁A； A﹁﹁A 可能A当且仅当并非必然﹁A； A﹁A 可能A或者可能﹁A； ﹁(A ﹁A) 不会既有必然A，又有必然﹁A； (A﹁A) 必然有A成立或者﹁A成立； ﹁(A﹁A) 不可能A与﹁A同时成立； (AB)AB 必然有A并且B等价于必然A并且必然B； AB(AB) 如果必然A和必然B有一为真，那么必然有A真或B真； (AB)AB 可能A或者B当且仅当可能A或者可能B； (AB)AB 如果可能有A并且B那么可能A并且可能B.,8,,项: 项的定义如下： ① 变量x是项； ② 常量c是项； ③ 如果t1,t2,…,tn是项，f是n元函词，那么f(t1,t2,…,tn)是项； ④ 当且仅当有限次地使用①②③所组成的符号串是项。

项的BNF表示为：t :: = x | c| f(t,t,…,t) 原子谓词公式: 对于n元谓词P，项t1,t2,…,tn，称P(t1,t2,…,tn)为原子谓词公式 （0元原子谓词公式是原子命题公式）,模态一阶逻辑公式: 模态一阶谓词逻辑公式，简称为MFOL（Modal first order logic）公式，定义如下： ① 原子谓词公式是MFOL公式； ② 对于MFOL公式A、B，(﹁A)、(AB)、(AB)、(AB)、(AB)是MFOL公式； ③ 对于MFOL公式A，x是A中的变量（个体变元），则xA、xA是MFOL公式； ④ 对于MFOL公式A ，(A)、(A)也是MFOL公式； ⑤ 当且仅当有限次地使用①②③④所组成的符号串是MFOL公式10,（1） 基本概念,MFOL公式的BNF表示为：  :: = p|()|()|()|()|()|(x)|(x)|()|() MFOL公式，除了具有MPL公式的性质外，还具有如下量词相关的性质： xP  (xP) xP  (xP) (xP)  xP xP  (xP) 在模态逻辑公式中，同样规定了联接词、模态算子的优先级别： （非）、（必然）、（可能）均为一元算子，具有最高的优先级；（与）、（或）的优先级次之；其次是（蕴涵）、（等值）。

11,（2） Kripke结构,Kripke结构: 三元组M = (W, R, L)称为Kripke （克里普克）结构（模型），其中W是可能世界的非空集合；R  WW是可能世界W上的二元关系；L：W2P (P为原子公式集合)是标记函数，它是对各可能世界的真值指派，即对每个原子公式，指明它在每个可能世界中取真值还是假值 在Kripke结构模型中，对于sW，R(s) = {tW| R}，称为可能世界s的1步可达可能世界集合12,（2） Kripke结构,约定： R0(s) = {s} R1(s) = R(s) R2(s) = R(R(s)) = {tW | u  R1(s) 且 R} Rk+1(s) = R(Rk(s)) = {tW | u  Rk(s) 且 R} 则称Rk(s) 为可能世界s的k（k0）步可达可能世界集合 对于skW且R （1 k  n），序列, , …, , , …, 建立了可能世界s0到sn的n步可达关系，并称之为可能世界s0到sn的一条长度为n的路径，简记为s0s1s2…sk-1sk sk+1…sn-1sn13,Kripke结构的有向图表示,用圆圈表示可能世界、有向弧线表示可能世界之间的关系、标记函数标识在圆圈内（即每一圆圈内标注了该可能世界中成立的原子公式）。

例：下图中，可能世界集W={s0, s1, s2}、二元关系R= {,,, ,}、标记函数L(s0)={p, q}, L(s1)={q, r},L(s2)={r}s0s1s2s2和s0s1s0s1s2分别为可能世界s0到s2的长度为3和4的路径 s1s2s2s2和s1s0s1s0s1s2分别为可能世界s1到s2的长度为3和5的路径,在模型M的可能世界s中为真的公式，表示为M,s╞ 或╞s  在模型M的所有可能世界中为真的公式，表示为M╞ 或╞ ，并称╞为满足关系 基于模态逻辑的Kripke结构模型，可以考察模态逻辑公式的解释或语义 对于M = (W, R, L)，p, qP和s, tW有， ① M,s╞ p 当且仅当 p L(s) ② M,s╞p 当且仅当 p L(s) ③ M,s╞ pq 当且仅当 p L(s) 或者q L(s) ④ M,s╞ pq 当且仅当 p L(s) 且q L(s) ⑤ M,s╞ p 当且仅当 t Rk(s)（k0），pL(t) ⑥ M,s╞ p 当且仅当 t Rk(s)（k0），pL(t),15,（3） 模态逻辑的类型,模态逻辑中模态词的各种引伸，产生了多种模态逻辑。

例如， 把“可能”解释为“将来某个时刻”、把“必然”解释为“将来所有时刻”，就得到时态（temporal）逻辑； 把“可能”解释为“信念” 或“相信”、把“必然”解释为“知道”，就得到知道逻辑或者信念（belief）逻辑； 把“可能”解释为“应该”、把“必然”解释为“必须”，就得到义务（ought）逻辑 在时态逻辑中，Kripke结构模型M = (W, R, L)的可能世界W解释为不同时刻（或状态），可能世界联系R解释为时间（或状态）的先后关系Kripke结构模型又称为时态结构模型或时序结构模型 基于对时间的不同描述，产生了时态逻辑的多种不同形式：分支或线性；离散或连续16,（3） 模态逻辑的类型,分支或线性：任一当前时刻仅存在唯一的可能未来时刻，时间的推进是线性的，称之为线性时间；时间具有分支或者树结构性质：任一当前时刻可能分叉为多种可能未来时刻，称之为分支时间 采用了分支（或线性）时间结构的时态逻辑，称为分支（或线性）时态逻辑 线性时态逻辑中提供了用以描述事件沿着单一时间轴演化的模态算子（词）； 分支时态逻辑中则需要提供对分支时间特性下多种未来行为描述的量化词分支时态逻辑可以较好地处理不确定性。

线性时间,分支时间,17,（3） 模态逻辑的类型,连续：当某种计算或活动需要描述成随时间连续变化时，需要采用一个稠密时间模型，即，时间对应于实数或实数域上的一个子集； 离散:当系统行为出现在一系列特定的时刻，就可以采用一个离散时间模型，即，时间对应于非负整数或非负整数的一个子集 系统的时间特征行为可能会出现在一系列时间区间上，那么就需要使用一些连续时间区间，称之为区间时间模型由此，时间模型又可分为点时间模型和区间时间模型 常用时态逻辑包括： 命题线性时态（时序）逻辑(PLTL：propositional linear temporal logic)、一阶线性时态（时序）逻辑(FOLTL：first order linear temporal logic)、命题分支时态逻辑或计算树逻辑(CTL：computation tree logic、CTL*)等18,（二） 线性时态（时序）逻辑,命题线性时态逻辑(PLTL)和一阶线性时态逻辑(FOLTL)是对命题逻辑和一阶逻辑扩展增加一些模态词（或时态算子）的模态逻辑，统称为线性时态（时序）逻辑（LTL：linear temporal logic）。

增加的时态算子如下：  always算子，A表示A总是为真或者A永远为真；  sometimes算子，A表示A最终为真或者A有时为真； ○ next算子，○A表示A在下一时刻为真； ▷ until算子，A▷B表示A一直为真直到B为真二） 线性时态逻辑,s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 p          - q          -                                         p          - q          -                                         ○p          - ○q          -                                         p▷q。