Chapter 6 时态逻辑时态逻辑 o（一）（一）模态逻辑模态逻辑 （1） 基本概念基本概念 （2） Kripke结构结构 （3）模态逻辑的类型模态逻辑的类型 o（二）线性时态逻辑（二）线性时态逻辑 （1）命题线性时态逻辑命题线性时态逻辑 （2）一阶线性时态逻辑一阶线性时态逻辑 o（三）（三） 计算树逻辑计算树逻辑 （1） CTL （2） CTL* o（四）四）模型模型检验 （1）标记算法标记算法 （2）资源共享协议问题资源共享协议问题 1（一）（一） 模态逻辑模态逻辑 o自然语言中有一类用于表示事物的“势态”，人的“情态”，以及过程的“变迁”（历史或未来）的词，称之为模态词。例如，“必然、可能”，“应该、允许”，“知道、认可”，“一贯、偶然”等。o模态词和命题连接可以生成新的命题。例如，“火星上可能有生命”就是“可能”与“火星上有生命”所组成的复合命题。o早期，由于模态词的语义不清楚，认为模态词不是逻辑概念，只把它们看作文学修辞，主张“必然A”与“A”相同，“不可能A”与“A”相同。2（一）（一） 模态逻辑模态逻辑o如果说这种做法在数学中勉强行得通，那么在日常推理中就寸步难行，因为“A真但是未必A必然为真”之类的说法，几乎是常识。例如，“张三是年级第1名”未必有“张三必然是年级第1名”。o模态逻辑起源于亚里斯多德（Aristole）将“必然、可能”这一对模态词看作逻辑概念，并详细讨论了它们的逻辑性质。3（一）（一） 模态逻辑模态逻辑 （1） 基本概念o模态词: 模态（modal）词，也称为模模态态算算子子，是构成模态逻辑中复合命题的基本运算。常用基本模态词包括：必然必然（）和可能可能（）。o模态逻辑:模态逻辑是经典命题逻辑和一阶谓词逻辑模态逻辑是经典命题逻辑和一阶谓词逻辑的扩展形式的扩展形式。基于命题逻辑的扩展称为模态命题逻辑，基于一阶谓词逻辑的扩展称为模态一阶逻辑。o模态逻辑通过引入 “可能”和“必然”两个模态词，从而能够对可能世界中的命题进行描述和演算。4o例如，对于命题 P：火星上有生命，那么，P表示火星上必然有生命；P表示火星上可能有生命。 o模模态态逻逻辑辑中中的的模模态态词词必必然然（ ）和和可可能能（ ）存在如下关系存在如下关系：n P = P （PP）n P = P （PP） 5（1） 基本概念基本概念 模 态 命 题 逻 辑 公 式 :简 称 为 MPL（ Modal Propositional Logic）公式，定义如下： 原子命题（命题常元或命题变元）是MPL公式； 如果A、B是MPL公式，那么(A)、(AB)、(AB)、 (AB)、(AB)是MPL公式； 如果A是MPL公式，那么(A)和(A)是MPL公式； 当且仅当有限次地使用所组成的符号串是MPL公式。MPL公式的巴科斯范式（BNF:Backus normal form）表示为：（p是原子命题公式） : = p|()|()|()|()|()|()|() 6一些反映模态词性质的一些反映模态词性质的MPLMPL公式：公式：AA 必然A真则A真；AA A真则可能A真；AA 必然A真则可能A真；AA 必然A当且仅当不可能不可能A A；AA 可能A当且仅当并非必然并非必然A A；AA 可能A或者可能可能A A；(A A) 不会既有必然A，又有必然A；(AA) 必然有A成立或者A成立；(AA) 不可能A与A同时成立；(AB)AB 必然有A并且B等价于必然A并且必然B；AB(AB) 如果必然A和必然B有一为真，那么必然有A真或B真；(AB)AB 可能A或者B当且仅当可能A或者可能B；(AB)AB 如果可能有A并且B那么可能A并且可能B. 7项: 项的定义如下： 变量x是项； 常量c是项； 如果t1,t2,tn是项，f是n元函词，那么f(t1,t2,tn)是项； 当且仅当有限次地使用所组成的符号串是项。项的项的BNFBNF表示为表示为：t : = x | c| f(t,t,t)原子谓词公式: 对于n元谓词P，项t1,t2,tn，称P(t1,t2,tn)为原子谓词公式。（0元原子谓词公式是原子命题公式）8模态一阶逻辑公式: 模态一阶谓词逻辑公式，简称为MFOL（Modal first order logic）公式，定义如下： 原子谓词公式是MFOL公式； 对于MFOL公式A、B，(A)、(AB)、(AB)、(AB)、(AB)是MFOL公式； 对于MFOL公式A，x是A中的变量（个体变元），则xA、xA是MFOL公式； 对于MFOL公式A ，(A)、(A)也是MFOL公式； 当且仅当有限次地使用所组成的符号串是MFOL公式。9（1） 基本概念基本概念 MFOL公式的公式的BNF表示为：表示为： : = p|()|()|()|()|()|(x)|(x)|()|()MFOL公式，除了具有MPL公式的性质外，还具有如下量词相关的性质： xP (xP) xP (xP) (xP) xP xP (xP)在模态逻辑公式中，同样规定了联接词、模态算子的优先级别：（非）、（必然）、（可能）均为一元算子，具有最高的优先级；（与）、（或）的优先级次之；其次是（蕴涵）、（等值）。 10（2） Kripke结构结构 oKripke结构: 三元组M = (W, R, L)称为Kripke （克里普克）结构（模型），其中W是可能世界的非空集合；R WW是可能世界W上的二元关系；L：W2P (P为原子公式集合)是标记函数，它是对各可能世界的真值指派，即对每个原子公式，指明它在每个可能世界中取真值还是假值。o在Kripke结构模型中，对于sW，R(s) = tW| R，称为可可能能世世界界s的的1步步可可达达可能世界集合可能世界集合。11（2） Kripke结构结构o约定：oR0(s) = soR1(s) = R(s)oR2(s) = R(R(s) = tW | u R1(s) 且 RoRk+1(s) = R(Rk(s) = tW | u Rk(s) 且 Ro则称Rk(s) 为可能世界s的k（k0）步可达可能世界集合。o对于skW且R （1 k n），序列, , , , , , 建立了可能世界s0到sn的n步可达关系，并称之为可能世界s0到sn的一条长度为n的路径，简记为s0s1s2sk-1sk sk+1sn-1sn。12 Kripke结构的有向图表示结构的有向图表示o用圆圈表示可能世界、有向弧线表示可能世界之间的关系、标记函数标识在圆圈内（即每一圆圈内标注了该可能世界中成立的原子公式）。o例例：下下图图中中，可可能能世世界界集集W=s0, s1, s2、二二元元关关系系R= , ,、标标记记函函数数L(s0)=p, q, L(s1)=q, r,L(s2)=r。s0q,rrp,qs2s1s0s1s2s2和和s0s1s0s1s2分别为可能世界分别为可能世界s0到到s2的长度为的长度为3和和4的路径的路径 s1s2s2s2和和s1s0s1s0s1s2分别为可能世界分别为可能世界s1到到s2的长度为的长度为3和和5的路径的路径13o在模型M的可能世界s中为真的公式，表示为M,s 或s o在模型M的所有可能世界中为真的公式，表示为M 或 ，并称为满足关系。o基于模态逻辑的Kripke结构模型，可以考察模态逻辑公式的解释或语义。o对于M = (W, R, L)，p, qP和s, tW有， M,s p 当且仅当 p L(s) M,sp 当且仅当 p L(s) M,s pq 当且仅当 p L(s) 或者q L(s) M,s pq 当且仅当 p L(s) 且q L(s) M,s p 当且仅当 t Rk(s)（k0），pL(t) M,s p 当且仅当 t Rk(s)（k0），pL(t) 14（3） 模态逻辑的类型模态逻辑的类型 o模态逻辑中模态词的各种引伸，产生了多种模态逻辑。例如，n把“可能”解释为“将来某个时刻”、把“必然”解释为“将来所有时刻”，就得到时态（时态（temporal）逻辑逻辑；n把“可能”解释为“信念” 或“相信”、把“必然”解释为“知道”，就得到知道逻辑或者信念（知道逻辑或者信念（belief）逻辑逻辑；n把“可能”解释为“应该”、把“必然”解释为“必须”，就得到义务（义务（ought）逻辑逻辑。o在时态逻辑中，Kripke结构模型M = (W, R, L)的可能世界W解释为不同时刻（或状态），可能世界联系R解释为时间（或状态）的先后关系。Kripke结构模型又称为时态结构模型或时序结构模型。o基于对时间的不同描述，产生了时态逻辑的多种不同形式：分支或线性；离散或连续。 15（3 3） 模态逻辑的类型模态逻辑的类型 o分支或线性：任一当前时刻仅存在唯一的可能未来时刻，时间的推进是线性的，称之为线线性性时时间间；时间具有分支或者树结构性质：任一当前时刻可能分叉为多种可能未来时刻，称之为分支时间分支时间。o采用了分支（或线性）时间结构的时态逻辑，称为分分支支（或或线线性性）时时态态逻逻辑辑。o线性时态逻辑中提供了用以描述事件沿着单一时间轴演化的模态算子（词）；o分支时态逻辑中则需要提供对分支时间特性下多种未来行为描述的量化词。分支时态逻辑可以较好地处理不确定性。 线性时间分支时间16（3 3） 模态逻辑的类型模态逻辑的类型 o连续：当某种计算或活动需要描述成随时间连续变化时，需要采用一个稠密时间模型，即，时间对应于实数或实数域上的一个子集；o离散:当系统行为出现在一系列特定的时刻，就可以采用一个离散时间模型，即，时间对应于非负整数或非负整数的一个子集。o系统的时间特征行为可能会出现在一系列时间区间上，那么就需要使用一些连续时间区间，称之为区间时间模型。由此，时间模型又可分为点时间模型和区间时间模型。o常用时态逻辑包括： 命题线性时态（时序）逻辑(PLTL：propositional linear temporal logic)、一阶线性时态（时序）逻辑(FOLTL：first order linear temporal logic)、命题分支时态逻辑或计算树逻辑(CTL：computation tree logic、CTL*)等。 17（二）（二） 线性时态（时序）逻辑线性时态（时序）逻辑 命题线性时态逻辑(PLTL)和一阶线性时态逻辑(FOLTL)是对命题逻辑和一阶逻辑扩展增加一些模态词（或时态算子）的模态逻辑，统称为线性时态（时序）逻辑（LTL：linear temporal logic）。增加的时态算子如下： always算子，A表示A总是为真或者A永远为真； sometimes算子，A表示A最终为真或者A有时为真； next算子，A表示A在下一时刻为真； until算子，AB表示A一直为真直到B为真。 18（二）（二） 线性时态逻辑线性时态逻辑 s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s0 s1 s2 s3 s4 s5 s6 s7 s8 s9s0 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 - - q p - - pppp,qppppp,qs0s1s2s3s4s5s6s7s8ppppqp,qs0s1s2s3s4s5s6s7s8qs9pppppp,qs0s1s2s3s4s5s6s7s8ps9p19（二）（二） 线性时态逻辑线性时态逻辑 命题线性时态逻辑公式: 简称PLTL公式，定义如下： 原子命题（命题常元或者命题变元）是PLTL公式； 如果A、B是PLTL公式，那么(A)、(AB)、(AB)、(AB)、(A B)是PLTL公式； 如果A是PLTL公式，那么(A)、(A)、(A)是PLTL公式； 如果A、B是PLTL公式，那么(AB)是PLTL公式； 当且仅当有限次地使用所组成的符号串是PLTL公式。命题线性时态逻辑公式的BNF表示为：:= p|()|()|()|()|()|()| ()|()|() 20（二）（二） 线性时态逻辑线性时态逻辑一阶线性时态逻辑公式: 简称FOLTL公式，定义如下： 原子谓词公式是FOLTL公式； 如果A、B是FOLTL公式，那么(A)、(AB)、(AB)、(AB)、(AB)是FOLTL公式； 如果A是FOLTL公式，x是A中出现的变量（个体变元），则xA、xA是FOLTL公式； 如果A、B是FOLTL公式，那么(A)、(A)、(A)、(AB)是FOLTL公式； 当且仅当有限次地使用所组成的符号串是FOLTL公式。一阶线性时态逻辑公式的BNF表示为：:=p|()|()|()|()|()|(x)|(x)|()|()| ()|()PLTL公式和FOLTL公式统称为LTL公式。在LTL公式中，规定了联接词、时态算子的优先级别：（非）、均为一元算子，具有最高的优先级；（与）、（或）的优先级次之；其次是（蕴涵）、（等值）；的优先级最低。21（二）（二） 线性时态逻辑线性时态逻辑 pq s0 s1 s2 s3 s4 s5 s0 s1 s2 s3 s4 s5 s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s0 s1 s2 s3 s4 s5 s6 s7 s0 s1 s2 s3 s4 s5 s6 s7(pq) s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s0 s1 s2 s3 s4 s5 s6 s7 s8 s9p s0 s1 s2 s3 s4 s5 s6 s7 s8 s0 s1 s2 s3 s4 s5 s6 s7 s8 s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s0 s1 s2 s3 s4 s5 s6 s7 s8 s9p s0 s1 s2 s3 s4 s5 s6 s7 s8 s0 s1 s2 s3 s4 s5 s6 s7 s8 s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s0 s1 s2 s3 s4 s5 s6 s7 s8 s9(p p) s0 s1 s2 s3 s4 s5 s6 s7 s0 s1 s2 s3 s4 s5 s6 s7 s0 s1 s2 s0 s1 s2pppp,qppppp,qs0s1s2s3s4s5s6s7s8ppppqp,qs0s1s2s3s4s5s6s7s8qs9pppppp,qs0s1s2s3s4s5s6s7s8ps9p一些一些LTL公式及其解释：公式及其解释：pq 若当前状态若当前状态p为真为真，则最终会出现则最终会出现q为真的状态；为真的状态； (pq) 从当前状态开始，使从当前状态开始，使p为真的状态为真的状态后终将有使后终将有使q为真的状态；为真的状态；p 从某一状态开始从某一状态开始p永远为真；永远为真；p 对今后任何状态而言，其后都将有状态对今后任何状态而言，其后都将有状态使使p为真；为真； (p p) 终将有一状态，在该状态中终将有一状态，在该状态中p为为真，并且下一状态中真，并且下一状态中p为假；为假；22（二）（二） 线性时态逻辑线性时态逻辑(pq)s7 s8 s9 s7 s8 s9 p(p q) s0 s1 s2 s3 s4 s5 s6 s7 s8 s0 s1 s2 s3 s4 s5 s6 s7 s8 s4 s5 s6 s7 s8 s9 s4 s5 s6 s7 s8 s9 s4 s5 s6 s7 s8 s9 s4 s5 s6 s7 s8 s9 p(pq) s3 s5 s3 s5 s7 s8 s9 s7 s8 s9 s7 s7pp s0 s1 s2 s3 s4 s5 s6 s7 s8 s0 s1 s2 s3 s4 s5 s6 s7 s8 s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s0 s1 s2 s3 s4 s5 s6 s7 s8 s9s0 s1 s2 s3 s4 s5 s6 s7 s8 s9pqq s0 s1 s2 s3 s4 s5 s6 s7 s8 s0 s1 s2 s3 s4 s5 s6 s7 s8 s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s0 s1 s2 s3 s4 s5 s6 s7 s8 s9s0 s1 s2 s3 s4 s5 s6 s7 s8 s9pppp,qppppp,qs0s1s2s3s4s5s6s7s8ppppqp,qs0s1s2s3s4s5s6s7s8qs9pppppp,qs0s1s2s3s4s5s6s7s8ps9p (pq) 对今后状态而言，对今后状态而言， p真将导致真将导致q从从此永远真；此永远真； p (p q) 从此从此p永远真，或者永远真，或者p从此一直从此一直真直到使真直到使q真的状态出现；真的状态出现； p ( p q) 若有状态使若有状态使p为真，则将有一为真，则将有一状态使状态使q为真，为真， p在此状态前一直为假；在此状态前一直为假； p p 如果如果p从此永远真。那么下一状态从此永远真。那么下一状态中看，中看， p仍然将永远为真；仍然将永远为真；(p q) q 如果有状态使如果有状态使p在此之前一直真，在此之前一直真，而在其中而在其中q为真，那么为真，那么q有时会为真；有时会为真；23（二）（二） 线性时态逻辑线性时态逻辑(pp)(pp) s0 s1 s2 s3 s4 s5 s6 s7 s8 s0 s1 s2 s3 s4 s5 s6 s7 s8 s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s0 s1 s2 s3 s4 s5 s6 s7 s8 s9(pq)(q(p(pq) s0 s1 s2 s3 s4 s5 s6 s7 s8 s0 s1 s2 s3 s4 s5 s6 s7 s8 s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s0 s1 s2 s3 s4 s5 s6 s7 s8 s9pppp,qppppp,qs0s1s2s3s4s5s6s7s8ppppqp,qs0s1s2s3s4s5s6s7s8qs9pppppp,qs0s1s2s3s4s5s6s7s8ps9p (p p)(pp) 若在今后状态若在今后状态中中p真蕴涵下一状态后真蕴涵下一状态后p总为真，则总为真，则p一旦真便永远真；一旦真便永远真；(p q) (q (p (p q) 一直一直p真真到到q真等同于现在真等同于现在q真或者现在真或者现在p真真且下一时刻起且下一时刻起p一直真到一直真到q真。真。 p s0 s1 s2 s3 s4 s5 s6 s7 s8p s0 s1 s2 s3 s4 s5 s6 s7 s8p s0 s1 s2 s3 s4 s5 s6 s7 s8pp s0 s1 s2 s3 s4 s5 s6 s7 s8(pp) s0 s1 s2 s3 s4 s5 s6 s7 s8 pp s0 s1 s2 s3 s4 s5 s6 s7 s8 s0 s1 s2 s3 s4 s5 s6 s7 s8 (pp)(pp) (1) p s4 s5 s6 s7 q s7 s8 s9 pq s4 s5 s6 s7 s8 s9 (pq) s4 s5 s6 s7 s8 p(pq) s4 s5 s6 s7 q(p(pq) s4 s5 s6 s7 s8 s9 s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 (pq)(q(p(pq) (2)24 寄存器电路（略）寄存器电路（略） 电位状态变化(设P表示p点的电位为高位，P表示p点的电位为低位，算子P表示p点的电位从低位到高位的状态变化，算子P表示p点的电位从高位到低位的状态变化。状态的改变还具有性质：如果p点的电位为高（低）位，则保持该电位直到发生状态改变 ) P = PP P = PP (P (PP) (P (PP) 通路晶体管(当v3门的输入信号激活时，v1门的信号将被传送到v2门。即，如果v2门的电位为低而v1门的电位为高，则v3门的电位变为高位时，v2门的电位将变为高位；如果v2门的电位为高而v1门的电位为低，则v3门的电位变为高位时，v2门的电位将变为低位) (v3(v1v2 v2) (v3(v1v2 v2)反向器(当v1门的电位为高时，下一时刻v2门的电位也将为高；当v1门的电位为低时，下一时刻v2门的电位也将为低) (v1 v2) (v1 v2)时钟(一个周期为4的时钟) = 234 lT2yT1zz1xlI2I1v2v3v2v1v1动态寄存器电路 T1和T2为通路晶体管，I1和I2为反向器，x是输入信号，l是负载信号，是时钟信号。寄存器的作用是：在时钟信号和负载信号l都是触发的情况下将一个输入数据x存储到单元中，并且保证在没有新的负载信号到来期间数据x不被通路晶体管T2改变。25寄存器电路（略）寄存器电路（略）晶体管T1：(l)(x z z) (l)(x z z)晶体管T2：(l)(z y y) (l)(z y y)组合反向器 (z y) (z y)电位状态变化 (z (z z)； (z (z z) (y (y y)； (y (y y)负载信号 l l 2l 3 l输入信号 x x 2x时钟信号 时间点时间点 0 1 2 3 4 5 6 7 8输入信号输入信号 x x x 时钟信号时钟信号 负载信号负载信号 l l l l l l l l l l z点电位点电位 z z z z z z y点电位点电位 y y y y y 在时间点3以后y都为真，所以满足y通路晶体管通路晶体管(v3(v1v2 v2) (v3(v1v2 v2)反向器反向器 (v1 v2) (v1 v2)电位电位状态变化状态变化 P = PP P = PP(P (PP) (P (PP)时钟时钟 = 234 lT2yT1zz1xlI2I126 队列及其操作队列及其操作 o队队列列是是一一种种常常用用的的抽抽象象数数据据类类型型，服服从从先先进进先先出出FIFO (first -in-first-out)规则。在某个时刻一个队列可以为空或非空。规则。在某个时刻一个队列可以为空或非空。o队队列列状状态态的的改改变变归归于于两两个个操操作作：PUT，插插入入一一个个元元素素到到队队尾尾；GET，从队列头部移出一个元素。从队列头部移出一个元素。o队队列列是是一一个个共共享享数数据据类类型型，PUT和和GET操操作作就就可可能能被被多多个个进进程程同同时执行。要求在任何时刻队列上只能发生一个时执行。要求在任何时刻队列上只能发生一个PUT或或GET操作。操作。o函词cur_queue 队列的当前状态oputval和getval PUT操作和GET操作的参数oputval nil PUT操作的前置条件oputval=nil PUT操作的后置条件ogetval= nil GET操作的前置条件ogetval nil GET操作的后置条件o通过对原变量添加“”后缀来区分原变量和经过操作之后的变量值27 队列及其操作队列及其操作 o谓词enter(PUT)、enter(GET) 相应操作的开始o谓词exit(GET)、exit(PUT) 相应操作的终止o活性活性oPUT操作的活性（用符号“*”表示在队列末尾插入后继元素）PUT操操作作的的活活性性就就是是要要求求其其能能够够终终止止。元素putval的插入只能在不引起溢出的情况下才能进行。nenter(PUT) (length(cur_queue)max)(exit(PUT) (cur_queue =cur_queue*putval)；nenter(PUT) (length(cur_queue)=max)(exit(PUT) (cur_queue =cur_queue)oGET操作的活性 GET操操作作的的活活性性特特征征是是其其只只有有在在从从队队列列取取出出一一个个值值之之后后才才能能终终止止。即，如果队列为空，则该操作将一直等到某个值被放进队列，然后再取出这个值。nenter(GET) empty(cur_queue)(exit(GET) (getval*cur_queue = cur_queue)；nenter(GET) empty(cur_queue) (enter(GET) exit(PUT)；nempty(cur_queue) enter(PUT)28队列及其操作队列及其操作o安安全全性性 设(enter(PUT)putvalnil)在cur_queue下成立，则如果当前队列为满，其下一个状态cur_queue将与cur_queue一 样 ； 如 果 当 前 队 列 不 为 满 ， 将 有cur_queue= cur_queue*putval。设(enter(GET)getval = nil)在cur_queue下成立，则如果当前队列为空，其下一个状态cur_queue将与cur_queue一样；如果当前队列不为空，将有cur_queue = getval *cur_queue。 o (enter(PUT) putvalnil)(length(cur_queue)= max) (cur_queue =cur_queue) (length(cur_queue) max) (cur_queue = cur_queue*putval)；o (enter(GET) getval=nil)(empty(cur_queue) empty(cur_queue ) (empty(cur_queue) (cur_queue = getval*cur_queue )29（三）（三） 计算树逻辑计算树逻辑 o计算树逻辑（CTL：computation tree logic）是一种离散、分支时间、命题时态逻辑。CTL是由Clarke和Emerson于80年代初提出，后经对CTL文法中路径量词及其它时态算子的组合使用规则扩展，建立了CTL*。一般地，CTL和CTL*统称为计算树逻辑。o在 CTL中 ， 除 了 具 有 时 态 算 子 always()、 sometimes ()、next()和until ()外，还增加了路径量词：所有未来路径(A)、至少某一路径(E)。o计算树逻辑公式：简称为CTL公式，定义如下： 原子命题（命题常元或者命题变元）是CTL公式； 、 是 CTL公 式 ， 那 么 ( )、 ()、 ()、 ()、()是CTL公式； 、是CTL公式，那么(A)、(E)、(A()、 (E()、(A)、(E)、(A)、(E)是CTL公式； 当且仅当有限次地使用所组成的符号串是CTL公式。30（三）（三） 计算树逻辑计算树逻辑CTL公式的BNF表示为： : = p |()|()|()|()|()|(A)|(E)|(A)| (E)| (A)|(E)|(A() |(E()A(p Eq)； EE(pq)； EE pAq； A(pEq)；AA(p A(p(pA(pq)为CTL公式。 p； E(pq)； A(pq)(pt)不是CTL公式（、必须紧接着A或E之后；必须紧接着A或E之后；(pq)、(pt)或(pq)(pt)的前面必须是A或E）31CTL公式的解释或语义：公式的解释或语义： M,s p 当且仅当当且仅当 p L(s)； M,s p 当且仅当当且仅当 p L(s)； M,s Ap 当且仅当当且仅当 t R(s)，p L(t)； M,s Ep 当且仅当当且仅当 t R(s)，p L(t)； M,s A p 当当且且仅仅当当所所有有s0= s的的路路径径s0s1s2s3上上均均存存在在si满满足足p L(si)； M,s E p 当当且且仅仅当当存存在在s0=s的的路路径径s0s1s2s3，该该路路径径上上某某些些si满满足足p L(si)； M,s A p 当且仅当所有当且仅当所有s0= s的路径的路径s0s1s2s3上的所有上的所有si满足满足p L(si)； M,s E p当且仅当存在当且仅当存在s0=s的路径的路径s0s1s2s3上的所有上的所有si满足满足p L(si)； M,sA(p q) 当当且且仅仅当当所所有有s0= s的的路路径径s0s1s2s3满满足足p L(sk)（0 k i）且）且q L(si)； M,s E(p q) 当当且且仅仅当当存存在在s0= s的的路路径径s0s1s2s3，满满足足p L(sk)（0 k i）且）且q L(si).上上述述满满足足关关系系式式中中，和和是是命命题题逻逻辑辑公公式式的的解解释释，只只需需要要考考察察当当前前状状态态下下公公式式的的满满足足；和和的的解解释释，要要考考察察除除了了当当前前状状态态外外，还还有有所所有有与与当当前前状状态态有有关关系系的的直直接接后后继继状状态态（1步步可可达达状状态态）；、和和，不不仅仅要要考考察察当当前前状状态态及及其其所所关关联联的的直直接接后后继继状状态态，而而且且还还要要考察与当前状态所关联的间接后继状态。考察与当前状态所关联的间接后继状态。路径量词路径量词 A全称路径量词；全称路径量词；E存在路径量词存在路径量词状态量词状态量词 全称状态量词；全称状态量词； 存在状态量词存在状态量词32M,s0 p q p和和q均位于状态均位于状态s0；M,s0 r r不在状态不在状态s0；M,s0 E(q r) 路径路径s0s1中的结点中的结点s1包含包含q与与r；M,s0 A(q r) 路径路径s0s1中的结点中的结点s1仅包含仅包含r但不包含但不包含q；M,s0 E (p r) 不存在同时包含不存在同时包含p和和r的结点；的结点；M,s2 E r 路径路径s2s3中的所有结点均包含中的所有结点均包含r；M,s2 A r 所有所有s0= s2路径中的结点均包含路径中的结点均包含r；M,s0 E(p q) r) 路径路径s0s2中结点中结点s2含含r而结点而结点s0包含包含p与与q；M,s0 A(p r) 结点结点s0包含包含p且其所有后继结点包含且其所有后继结点包含r.p,q s0r s2q,r s1p,q s0r s2 r s2q,r s1r s2r s2s0q,rrp,qs2s1Kripke结构模型在状态s0下的路径树 33（三）（三） 计算树逻辑计算树逻辑 A E A E 34（三）（三） 计算树逻辑计算树逻辑AEA( )E( )35（三）（三） 计算树逻辑计算树逻辑在计算树逻辑中，时时态态算算子子、路路径径量量词词可可以以通通过过等等值值公公式式相相互互转转换换。下面给出了一些CTL等值公式： A = EE = AA = EA = A(true)E = E(true)A = AAE = EEA = AAE = EEA()= (AA()E()= (EE()计算树逻辑是命题逻辑的扩展，所以命题逻辑中联结词之间的等值公式同样适用于计算树逻辑。在命题逻辑中，, 和, 分别构成了完备联结词集，因为完备联结词集之外的其他联结词均可用完备联结词集中的联结词来表示。在计算树逻辑中，A, A, A、 A, E, E、E, E, E等分别构成了时态算子和路径量词的完备集。36（三）（三） 计算树逻辑计算树逻辑CTL*公式- CTL*公式分为状态公式和路径公式，状状态态公公式式定义如下： 原子命题是状态公式， 如果、是状态公式，那么()、()是状态公式， 如果是路径公式，那么(A)、(E)是状态公式， 当且仅当有限次地使用所组成的符号串是状态公式；路径公式定义如下：路径公式定义如下： 状态公式是路径公式， 如果、是路径公式，那么()、()是路径公式， 如果、是路径公式，那么 ()、()、()、()是路径公式， 当且仅当有限次地使用所组成的符号串是路径公式。37（三）（三） 计算树逻辑计算树逻辑CTL*公式中状态公式公式中状态公式 和路径公式和路径公式 的的BNF表示表示为：为： : = p | ()| () | ()| ()| ()|(A )| (E ) : = | ()| () | ()| ()| ()|()| ( )| ()| ()CTL和和PLTL都都可可以以看看作作为为CTL*的的子子类类。下面给出一些CTL*公式：AE p CTL公式但不是PLTL公式；Ep 不是CTL公式也不是PLTL公式；p q 不是CTL公式但是PLTL公式。38（四）（四） 模型检验模型检验 o系系统统的的计计算算树树逻逻辑辑规规格格可可通通过过模模型型检检查查得得到到验验证。证。o模模型型检检验验主主要要是是在在软软件件系系统统的的Kripke结结构构模模型型下下，对对以以CTLCTL* *公公式式给给出出的的软软件件性性能能进进行行正正确确性性验证。验证。o标标记记算算法法（labelling algorithm）是是模模型型检检验验的的一一个简单算法个简单算法o标标记记算算法法：对于给定的计算树逻辑公式，将其写成由A、E、E、nil（假）连接的等值CTL公式；对Kriple结构模型中的子公式满足的状态进行标记，直到得到标记；所有标记为的状态就是得到满足的状态。39标记规则标记规则假假定定 是是 的的子子公公式式，满满足足 的的子子公公式式的的状状态态都都已已得得到到标标记记，则则子子公公式式 的的状态标记为：状态标记为： = nil 无标记状态；无标记状态； = p 如果如果p L(s)，用，用p标记状态标记状态s； = 12 如果如果s已标记已标记 1和和 2，那么用，那么用 12标记该状态；标记该状态； = 1 如果如果s没有标记没有标记 1，那么用，那么用1标记该状态；标记该状态； = A1 对对于于已已标标记记 1的的s，用用A1标标记记该该状状态态；对对于于所所有后继状态已标记有后继状态已标记A1的的s，用，用A1标记该状态；标记该状态； = E( 1 2) 对对于于已已标标记记 2的的s，用用E( 1 2)标标记记该该状状态态；对对于于已已标标记记 1，且且至至少少一一个个后后继继状状态态已已标标记记E( 1 2) 的的s，用用E( 1 2)标记该状态；标记该状态； = E 1 对对于于后后继继状状态态之之一一已已标标记记 1的的s，用用E 1标标记记该该状态状态。A = E E = AA = E E = E(true ) A( )= (E( ( ) A )40（四）（四） 模型检验模型检验 o下下图图是是右右图图CTLCTL* *公公式式E(pE(p q)q) r r) )的的模模型型检验 oE(pE(p q)q) r r) )在在KripkeKripke结结构构中中的的所所有有状状态态得得到到满满足足，所所以以公公式式的的正正确确性性得得证。证。s0s1s20: p,q0: r0: q,r1:pq2: E(pq)r) 2: E(pq)r) 3: E(pq)r) s0q,rrp,qs2s141 资源共享协议问题资源共享协议问题 资源共享协议问题需要满足如下性质：安全性(safety)：任意时刻至多有一个进程访问资源；活性(liveness)： 进程对资源提出的访问请求，总会被允许；无阻塞性(non-blocking)：进程会不断提出对资源的访问请求；无次序性(no strict sequencing)：进程对资源的访问没有严格的次序。两个进程的资源共享问题：每一个进程具有3种状态：请求（r）访问（w）和闲置（i），并具有状态转移。两个进程交替对资源进行访问。资源共享协议1的Kriple结构模型安全性：1 = A(w1w2)活性： 21 = A (r1 Aw1) 22 = A (r2 Aw2)无阻塞性：31 = A (i1 Er1) 32 = A (i2 Er2) 无次序性：41 = E(w1 E(w1 (w1E(w2 w1) 41 = E(w2 E(w2 (w2E(w1 w2) s0s6s5s4s3s2s1s7w1,i2r1,i2i1,w2i1,r2w1,r2r1,r2i1,i2r1,w242 资源共享协议问题资源共享协议问题 为为了了对对资资源源共共享享协协议议的的性性能能要要求求进进行行模模型型检检验验验验证证，需需要要对对这这些些CTL公公式式变变换换为为完完备备算算子子集集A , E , E, , 上的等值公式。上的等值公式。具体过程如下：1 = A(w1w2) = E(w1w2) = E11= E(true11)= 12 安全性21 = A (r1 Aw1)=A(r1Aw1)= A(r1Aw1)= E(r1Aw1) =E (r1 211) = E 212 = E(true212) = 213 活性22 = A(r2Aw2)= A(r2Aw2)= A(r2Aw2) = E (r2 Aw2)=E(r2 221) = E 222 = E(true222) = 223 活性31 = A(i1Er1) = A(i1Er1)=A(i1Er1)= E(i1 Er1)=E(i1311) = E 312 = E(true312) =313 无阻塞性32 = A(i2Er2)= A(i2Er2)=A(i2Er2) = E(i2 Er2)=E (i1 321) = E 322 = E(true322) = 323 无阻塞性41 = E(w1 E(w1 (w1E(w2 w1) = E(w1 E(w1 (w1411) =E(w1 E(w1 412) = E(w1 413) = E414= E(true414) 无次序性42 = E(w2 E(w2 (w2E(w1 w2) = E(w2 E(w2 (w2421) = E(w2 E(w2 422) = E(w2 423) = E424= E(true424) 无次序性A = E E = A A = E A = A(true)E = E(true) A()= (E() A)43资源共享协议问题资源共享协议问题活性活性 2121、 2222的模型检验的模型检验s0s6s5s4s3s2s1s70:w1,i20:r1,i20:i1,w20:i1,r20:w1,r20:r1,r20:i1,i20:r1,w21: Aw11: Aw12: 212 2: 212 2: 212 s0s6s5s4s3s2s1s70:w1,i20:r1,i20:i1,w20:i1,r20:w1,r20:r1,r20:i1,i20:r1,w2212 =r1Aw1213 = E(true212)21 = 213 222 =r2Aw2223 = E(true222)22 = 223 安全性的模型检验安全性的模型检验?1 = A(w1w2) 3: 213 3: 213 3: 213 3: 213 3: 213 3: 213 3: 213 3: 213 1: Aw21: Aw22: 2222: 2222: 2223: 2233: 2233: 2233: 2233: 2233: 2233: 2233: 22344资源共享协议问题资源共享协议问题无阻塞性无阻塞性 3131、 3232的模型检验的模型检验s0s6s5s4s3s2s1s70:w1,i20:r1,i20:i1,w20:i1,r20:w1,r20:r1,r20:i1,i20:r1,w21: Er11: Er11: Er11: Er11: Er1s0s6s5s4s3s2s1s70:w1,i20:r1,i20:i1,w20:i1,r20:w1,r20:r1,r20:i1,i20:r1,w231 =E(true(i1Er1)32 =E(true(i2Er2)2: 312: 312: 312: 312: 312: 312: 312: 311:Er21:Er21:Er21:Er21:Er22: 322: 322: 322: 322: 322: 322: 322: 3245资源共享协议问题资源共享协议问题无次序性无次序性 4141、 4242的模型检验的模型检验s0s6s5s4s3s2s1s70:w1,i20:r1,i20:i1,w20:i1,r20:w1,r20:r1,r20:i1,i20:r1,w21: 411 s0s6s5s4s3s2s1s70:w1,i20:r1,i20:i1,w20:i1,r20:w1,r20:r1,r20:i1,i20:r1,w2411 = E(w2 w1) 412 = w1411 413 = E(w1 412)414 = w1413 41 = E(true414) 421 = E(w1 w2) 422 = w2421 423 = E(w2 422)424 = w2423 42 = E(true424) 1: 411 1: 411 1: 411 1: 411 1: 411 2: 412 2: 412 2: 412 2: 412 3: 413 3: 413 3: 413 3: 413 3: 413 3: 413 4: 414 4: 414 5: 41 5: 41 5: 41 5: 41 5: 41 5: 41 5: 41 5: 41 1: 421 1: 421 1: 421 1: 421 1: 421 1: 421 2: 422 2: 422 2: 422 2: 422 3: 423 3: 423 3: 423 3: 423 3: 423 3: 423 4: 424 4: 424 5: 425: 425: 425: 425: 425: 425: 425: 4246资源共享协议问题资源共享协议问题资源共享协议2的Kripke结构模型s0s6s5s4s8s2s1s7w1,i2r1,i2i1,w2i1,r2w1,r2r1,r2i1,i2r1,w2r1,r2s9安全性的模型检验安全性的模型检验?1 = A(w1w2) 47资源共享协议问题资源共享协议问题活性活性 2121的模型检验的模型检验s0s6s5s4s8s2s1s70:w1,i20:r1,i20:i1,w20:i1,r20:w1,r20:r1,r20:i1,i20:r1,w20:r1,r2s91: Aw11: Aw11: Aw11: Aw11: Aw11: Aw1212 =r1Aw1213 = E(true212)21 = 213 2: 212: 212: 212: 212: 212: 212: 212: 212: 2148资源共享协议问题资源共享协议问题活性活性 2222的模型检验的模型检验s0s6s5s4s8s2s1s70:w1,i20:r1,i20:i1,w20:i1,r20:w1,r20:r1,r20:i1,i20:r1,w20:r1,r2s91: Aw21: Aw21: Aw21: Aw21: Aw21: Aw22: 222: 222: 222: 222: 222: 222: 222: 222: 21222 =r2Aw2223 = E(true222)21 = 213 49资源共享协议问题资源共享协议问题无阻塞性无阻塞性 3131、 3232的模型检验的模型检验1: Er11: Er11: Er11: Er11: Er131 =E(true(i1Er1)32 =E(true(i2Er2)s0s6s5s4s8s2s1s70:w1,i20:r1,i20:i1,w20:i1,r20:w1,r20:r1,r20:i1,i20:r1,w20:r1,r2s9s0s6s5s4s8s2s1s70:w1,i20:r1,i20:i1,w20:i1,r20:w1,r20:r1,r20:i1,i20:r1,w20:r1,r2s91: Er21: Er21: Er21: Er21: Er250资源共享协议问题资源共享协议问题无次序性无次序性 4141的模型检验的模型检验411 = E(w2 w1) 412 = w1411 413 = E(w1 412)414 = w1413 41 = E(true414) 1: 411 1: 411 1: 411 1: 411 1: 411 2: 412 2: 412 2: 412 3: 413 3: 413 3: 413 3: 413 4: 414 5: 41 5: 41 5: 41 5: 415: 41 5: 41 s6s0s5s4s8s2s1s70:w1,i20:r1,i20:i1,w20:i1,r20:w1,r20:r1,r20:i1,i20:r1,w20:r1,r2s95: 41 5: 41 5: 41 51资源共享协议问题资源共享协议问题无次序性无次序性 4242的模型检验的模型检验1: 421 1: 421 1: 421 1: 421 1: 421 2: 422 2: 422 2: 422 3: 423 3: 423 3: 423 3: 423 4: 424 5: 42s6s0s5s4s8s2s1s70:w1,i20:r1,i20:i1,w20:i1,r20:w1,r20:r1,r20:i1,i20:r1,w20:r1,r2s9421 = E(w1 w2) 422 = w2421 423 = E(w2 422)424 = w2423 42 = E(true424) 5: 425: 425: 425: 425: 425: 425: 425: 4252