形式化方法ppt课件.ppt

第四章 时态逻辑,时态逻辑,引入,命题逻辑和谓词逻辑表达的可能性真和假不能表达的可能性必然为真知道为真将来为真相信为真,例,奥巴马是美国总统太阳系有九大行星27的立方根是3,模态逻辑,本章内容,模态逻辑时态逻辑命题线性时态逻辑一阶线性时态逻辑计算树逻辑（CTL，CTL*）,模态逻辑相关概念,模态（Modal）谓词逻辑的扩展形式。基于命题逻辑的扩展称为模态命题逻辑，基于一阶谓词逻辑的扩展称为模态一阶逻辑。特点是通过引入“可能”和“必然”两个模态词，从而能够对可能世界中的命题进行描述和演算。模态词必然（）；可能（）例如,对于命题P:火星上有生命，P：火星上必然有生命P：火星上可能有生命；,模态逻辑公式,原子命题是模态逻辑公式；如果A是模态逻辑公式。那么A和A是模态逻辑公式；如果A,B是模态逻辑合适公式，那么（A），（AB），（AB），AB），（AB）是模态逻辑公式；当且仅当有限次地使用（1）（2）（3）所组成的符号串是模态逻辑公式。,考察（1),AA 必然A真则A真；AA A真则可能A真；AA 必然A真则可能A真；AA 必然A真当且仅当不可能A；AA 可能A当且仅当并非必然 A；AA 可能A或者可能A；,考察（2）,（AA）不会既有必然A，又有必然A； (AA) 必然有A成立或者A成立； （AA） 不可能A与 A同时成立； （AB） AB 必然A并且B等价于必然A并且必然B；,考察（3）,AB（AB） 如果必然A和必然B有一个为真，那么必然有A真或者B真； （AB） AB 可能A或者B当且仅当可能A或者可能B； （AB） AB 如果可能有A并且B，那么可能A并且B 。,模态一阶逻辑公式,原子谓词公式是模态逻辑公式；如果A,B是模态一阶逻辑公式，那么（A），（A），（A），（AB），（AB），（AB），（AB）是模态逻辑公式；如果A是模态一阶逻辑公式，x是A中出现的变量（个体变量），则x.A, x.A是模态逻辑公式;当且仅当有限次地使用（1）（2）（3）所组成的符号串是模态一阶逻辑公式.,与量词相关的性质,xP(x. P)xP(x. P)(xP) (xP)xP(xP),模态词之间的关系,P PP P,模态逻辑语义,要区分真值的不同模式或程度基本模态逻辑的模型（Kripke）：三元组M=（W,R,L）W：可能世界的非空集合；R包含于 W W：可能世界W上的二元关系，L：W2p(P为原子公式集合)：标记函数，对可能世界的真值指派。例：R(w,w):世界w可从世界w到达,s1,s2,s0,用图来表现Kripke结构,圆圈：可能世界有向线段：可能世界之间的关系圆圈内：标记函数标识（该可能世界中成立的原子公式）,p.q,q,r,r,标准模型,满足下面条件的三元组M=(W,R,L):对于p，q P和s，t W有：L(p,s) = 10L(p,s) = L(p,s)L(pq,s) = L(p,s)L(q,s)L(pq,s) = L(p,s) L(q,s)L(p,s) = (t)(sRtL(p,t)=1L(p,s) = (t)(sRtL(p,t)=1,定义的真值,设M=(W,R,L)是基本模态逻辑的一个模型。假设xW且是模态逻辑公式。通过对结构归纳，定义满足关系x|- 来定义在世界x中,的真值：x|-p当且仅当pL(x)x|-当且仅当x |= x|-当且仅当x |= 并且x|=x|-当且仅当x |= 或x|=x|-当且仅当只要x |= 则x|=x|- 当且仅当对R(x,y)的每一yW,有y|=x|- 当且仅当存在yW,使得R(x,y)且y|=,定义,如果该模型中每个世界都满足该公式，称基本模态逻辑的模型M(W,R,L)满足一个公式。写M|=当且仅当对每个xW,x|-,x6,x5,x4,例,x1 |- qx1 |- qx1 |- qx5 |- p x5 |- qx5 |- pqx5 |- (pq)x2,x3,x4,x5,x6 |-pp,x1,x3,x2,p.q,q,p,q,q,q,模态公式之间的等价,基本模态逻辑的一个公式集语义导出基本模态逻辑公式，如果对任何模型M=（W,R,L）中的任何世界x，只要对所有均满足x|-,就有x|- 。在这种情况下,|=成立。和是语义等价，如果|=和|=成立。记为,模态公式之间的等价（续）,命题逻辑中的任何等价也是模态逻辑中的等价。取命题逻辑中的任何等价，将原子一致地代换成任意的模态逻辑公式，结果还是模态逻辑中的等价。例：pq, (pq)p: p (qp) q: r(qp)p (qp)(r(qp) (p (qp) (r(qp),有效公式,基本模态公式称为有效，如果它在任何模型的任何世界中都为真任何命题逻辑重言式是有效公式，它的任何代换实例也是有效公式 () ) () ,有效公式,K公式：() 证明：x|- () 当且仅当x|- () 且x|- 当且仅当对所有满足R(x,y)的y，有y|- 和y|- 蕴涵对所有满足R(x,y)的y，有y|- 当且仅当 x|- .,时态逻辑,模态逻辑的种类,必然,可能,将来所有时刻,将来某个时刻,知道或信念逻辑,必然,可能,知道,信念相信,义务逻辑,必然,可能,必须,应该,时态逻辑,一种特殊类型的模态逻辑将Kripke结构M=(W,R,L)中的R解释为时间的先后关系的模态逻辑基于对时间的不同描述，产生了多种不同形式的时态逻辑。分支时态逻辑线性时态逻辑,分支时态逻辑,分支时间时间具有分支或者树形结构性质：任一当前时刻可能分叉为多种可能未来时间。分支时态逻辑采用分支时间结构的时态逻辑。需要提供对分支时间特性下多种未来行为描述的量化词。可以很好地处理不确定性。,线性时态逻辑,线性时间：任一当前时刻仅存在唯一的可能未来时刻，时间的推进；线性时态逻辑：采用线性时间结构的时态逻辑。提供了用于描述事件沿着单一时间轴演化的模态演算子。,常用时态逻辑,命题线性时态逻辑（PLTL）一阶线性时态逻辑（FOLTL）命题分支时态逻辑或计算树逻辑（CTL，CTL*）,命题线性时态逻辑（PLTL）,在命题逻辑中增加4类模态词(G)演算子： A：A总是为真或者永远为真；(F)演算子A：A最终为真或者有时为真；(X)演算子A：A在下一时刻为真；(U)演算子 AB：A一直为真直到B为真；,PLTL公式的定义,原子命题是PLTL；如果A,B是PLTL公式，那么（A），（AB），（AB），（AB），（AB）是命题线性时态逻辑公式；如果A是PLTL公式，那么（A），（A），（A）是命题线性时态逻辑公式；如果A，B是PLTL公式，那么（AB）是命题线性时态逻辑公式；当且仅当有限次地使用（1）（2）（3）所组成的符号串是PLTL公式。,考察（1）,给出下面一些PLTL公式的解释AB如果当前状态A为真，则最终能出现B为真的状态；（AB）从当前状态开始，使A为真的状态后终将有使B为真的状态；A从某一状态开始A永远为真；,考察（2）,（AA）终将有一状态，在该状态中A为真，并且下一状态中A为假；A对今后任何状态而言，其后都将有状态使A为真；（ AB）对今后状态而言，A真将导致B从此永远真；,考察（3）,A（AB）或者A从此永远真，或者A从此一直真直到使B真的状态出现；A（AB）如果有状态使A为真，那么必将有一状态，使A在此状态前一直为假，而B在此状态中为真；AA如果A从此永远真，那么下一状态中，A将永远为真；,考察（4）,AB B如果有状态使A在此之前一直真，而在其中B为真，那么B有时会为真；（AA（AA）如果在今后的状态中，A真蕴涵下一状态A为真，那么A一旦真便永远真；AB（B（A（AB）从现在起A一直真到B真，等同于出现B真，或者现在A真，而下一时刻起A一直真到B真,例：LSI动态寄存器电路单元的命题线性时态逻辑规格,T1和T2为通路晶体管，I1和I2为反相器，x是输入信号，I是负载信号，是时钟信号。寄存器的作用:在时钟信号和负载信号I都是触发的情况下，将一个输入数据x存储到单元中.保证在没有新的负载信号到来期间，数据x不被通路晶体管T2改变,x,1 I,2 I,T1,T2,z,y,I2,I1,基本元素规格p：p点的电位为高位p：p点的电位为地位p：p点电位从地位到高位的状态变化P：p点的电位从高位到低位的状态变化电位的变化可规格为p=PPP=PP,例：LSI动态寄存器电路单元的命题线性时态逻辑规格(续),状态的改变还具有的性质：如果p点的电位为高（低）位，则一直保持该电位直到发生状态变化。相应的时态逻辑规格为（P（PP） （P（PP）,例：LSI动态寄存器电路单元的命题线性时态逻辑规格(续),通路晶体管当v3门的输入信号激活时，v1门的信号将被传送到v2门.如果v2门的电位为低而v1门的电位为高，则当v3门的电位变为高位时，v2门的电位将变为高位；如果v2门的电位为高而v1门的电位为低，则当v3门的电位变为高位时，v2门的电位将变为低位。引入算子PF来规格该功能：PF（v1,v2,v3）=(v3(v1v2v2) (v3（v1v2v2）),例：LSI动态寄存器电路单元的命题线性时态逻辑规格(续),v1,v3,v2,反向器的特征当v1门的电位为高时，下一时刻v2门的电位也将为高；当v1门的电位为低时，下一时刻v2门的电位也将为低。描述：(v1v2)(v1v2),例：LSI动态寄存器电路单元的命题线性时态逻辑规格(续),v1,v2,时钟引入算子y来描述时钟的循环一个周期为4的时钟可描述为：y= y,例：LSI动态寄存器电路单元的命题线性时态逻辑规格(续),电位行为规格晶体管T1: PF(x,z,I)，T2: PF(z,y,I)组合反相器(zy)(zy )电位状态变化(z(zz) ，(z(zz)(y(yy)， (y(yy),例：LSI动态寄存器电路单元的命题线性时态逻辑规格(续),电路性能的推演行为描述为：行为规格+输入信号 电路性能 负载信号根据如下序列进行周期变化：低位，高位，高位，低位，IIII输入信号 输入信号按如下序列产生：低位，高位，高位：xxx时钟信号 时钟信号根据如下序列产生：开始为高位，然后根据y所描述的序列变化：y,例：LSI动态寄存器电路单元的命题线性时态逻辑规格(续),输入信号x，时钟信号，负载信号I，以及z和y点的电位用表表示：y,例：LSI动态寄存器电路单元的命题线性时态逻辑规格(续),一阶线性时态逻辑,阶线性一时态逻辑（FOLTL）是一阶谓词逻辑的扩展。它是在一阶谓词逻辑中增加了模态词 演算子 A表示A总是为真或者永远为真； 演算子 A表示A最终为真或者有时为真； 演算子 A表示A在下一时刻为真； 演算子： AB表示A一直为真直到B为真。,FOLTL公式的定义,原子谓词公式是FOLTL；如果A,B是FOLTL公式，那么（A），（AB），（AB），（AB），（AB）是一阶线性时态逻辑公式；如果A是FOLTL公式，x是A中出现的变量，则则xA, xA是FOLTL公式；如果A是FOLTL公式，那么（A），（A），（A），（AB）是一阶线性时态逻辑公式；当且仅当有限次地使用（1）（2）（3）（4）所组成的符号串是FOLTL公式。,FOLTL的应用,队列及其操作操作规划问题,队列及其操作,是一种常用的抽象数据类型，服从先进先出FIFO规则在某个时刻从一个队列可以为空或非空队列状态的改变归因于两个操作PUT：插入一个元素到队尾GET：从队列头部移动一个元素。,队列及其操作（续）,设所讨论的队列是一个共享数据类型，PUT和GET操作就可以被多个进程同时执行。要求：在具体的任何一个时刻队列上只能发生一个操作，给定队列的当前内容，则只能有一个进程在该状态下执行PUT或GET操作一个进程使用GET操作来取出当前的队列头部的值；如果当前队列为空，则该进程等待，直到另一进程将一个值放进队列。,用函词cur_queue：队列的当前状态putval：PUT操作的参数getval：GET操作的参数PUT操作的前置条件：putvalnil， 后置条件为：putval=nil GET操作的前置条件：getval=nil 后置条件：getvalnil 谓词enter(PUT),enter(GET),exit(GET),exit(PUT),表示相应操作的开始和终止。,队列及其操作（续）,活性PUT操作的活性就是要求其能够终止。元素putval的插入只有在不引起溢出的情况下才能进行Enter(PUT)(length(cur_queue)max)(exit(PUT)(cur_queue=cur_queue*putval);Enter(PUT)(length(cur_queue)=max)(exit(PUT)(cur_queue=cur_queue);（用符号“*”表示在队列末尾插入后继元素）,队列及其操作（续）,GET操作的活性特征是：其中只有在从队列中取出一个值后才能终止如果队列为空，则该操作将一直等到某个值被放进队列，然后再取出这个值。enter(GET)empty(cur_queue)max) (exit(GET)(getval*cur_queue=cur_queue);enter(GET)empty(cur_queue) enter(GET) exit(PUT)如果队列为空，则某些进程将最终加入一个值到队列中。 empty(cur_queue) enter（PUT）,队列及其操作（续）,安全性设（enter(PUT)putvalnil）在cur_queue下成立。则如果当前队列为满，其下一个状态cur_queue将与cur_queue一样；如果当前队列不为满，cur_queue=cur_queue*putval相应的时态逻辑公式为（enter(PUT)putvalnil）(length(cur_queue)=max)(cur_queue=cur_queue)(length(cur_queue)max)(cur_queue=cur_queue*putval)）,队列及其操作（续）,设（enter(GET)putval=nil）在cur_queue下成立。则如果当前队列为空，其下一个状态cur_queue将与cur_queue一样；如果当前队列不为空，将有cur_queue=getval*cur_queue.相应的时态逻辑公式为(enter(GET)getval=nil)(empty(cur_queue)empty(cur_queue)(empty(cur_queue)(cur_queue=getval*cur_queue),队列及其操作（续）,操作规划问题,有三个柱子P1,P2,P3和3个盘子A,B,C开始时三个盘子放在p1上，并且最小的盘子A在最上面，最大的盘子C在最下面要求设计一种操作方案将三个盘子从p1移到p3,在移动过程中可使用p2作为暂时的存放位置在每次移动盘子之后，要求在各柱子上的盘子总是上小下大。,操作活动定义谓词：Move(X,p) 将盘子X移动到柱子p；On(X,Y) 盘X在Y上；Smaller(X,Y) 盘X比盘Y小；Top(X,p) 盘X在柱子p的最上面；Free(X) 盘X可以被移动。,操作规划问题（续）,操作的约束条件：如果盘子上面没有其他的盘子，则该盘子是可以被移动的。free(X) Z.on(X,Z).如果盘子X在柱子p的最上面，则该盘子可以自由移动top(X,p) free(X).,操作规划问题（续）,比较盘子大小的谓词满足传递关系：Smaller(X,Y)smaller(Y,Z) smaller(X,Z).任何时候一个盘子不可能在不同的两个盘子上（Y1Y2）(on(X,Y1)on(X,Y2).,操作规划问题（续）,规格假设：设一个为空的柱子上有一个空盘子，该空盘子比任何一个给定的盘子都大。即p.top(emptydisk,p)X.(top(X,p)on(X,emptydisk);X.smaller(X,emptydisk).,操作规划问题（续）,操作活动的前置条件和后置条件： 活动move(X,p)的前置条件precond(X,p)： 盘X是自由的；盘X比柱子p的最上面的盘子Y小precond(X,p)=free(X)top(Y,p)smaller(X,Y).,操作规划问题（续）,活动move(X,p)的后置条件postcond(X,p)：盘X在柱子p的最上面；原来柱子p最上面的盘子Y不再是自由的;X在Y上;在前置条件中使on(X,Z)为真的盘子Z现在成为自由的。postcond(X,p)是：top(X,p)top(Y,p) (on(X,Y)top(X,p)free(Y), On(X,Z)top(X,p) (top(Z,p)on(X,Z)free(Z),操作规划问题（续）,如果移动的盘子X到柱子p的活动的前置条件成立，并且移动的动作也得到了执行，则后置条件以及持续性都应该成立：precond(X,p)move(X,p) (postcond(X,p)persistent_free(X,p)persistent_on(Y,p).,操作规划问题（续）,操作的持续性：没有受到任何后置条件影响的自由盘子将保持为自Persistent_free(X,p) (X)free(X)(postcond(X,p) (Z)on(Z,X) free(X)没有受任何后置条件影响的在另一盘子上的盘子保持相同状态Persistent_free(X,p) (X) (Y) on(X,Y)(postcond(X,p) on(X,Y) on(X,Y),操作规划问题（续）,操作规划任务初始状态：在起始时刻，盘子A,B,C在柱子p1上，并且A在最上面，C在最下面。盘子A，柱子p2,p3都是自由的。（disk(A)disk(B) disk (C),（smaller(A,B)smaller(B,C),Top(emptydisk,p2)top(emptydisk,p3)top(A,p1)on(A,B)on(B,C)on(C,emptydisk);,操作规划问题（续）,目标状态：目标状态是让A,B,C以初始时同样的顺序叠放在p3上(on(C,emptydisk)on(B,C)on(A,B)top(A,p3)。,操作规划问题（续）,操作规划求取存在一个与规格相一致的活动序列：move(A,p3)move(B,p2)2move(A,p2)3move(C,p3)4move(A,p1)5move(B,p3)6move(A,p3).,操作规划问题（续）,逻辑推演对于该活动序列中的每个移动，证明其前置条件是满足的，并且其后置条件将会使系统处于下一个新状态，而在新的状态下，下一个移动的前置条件是满足的。,操作规划问题（续）,第一次移动证明：前置条件precond(X,p)free(A)top(emptydisk,p3)smaller(A,emptydisk);将盘A移动到柱子p3,便有precond(A,p3)move(A,p3);,操作规划问题（续）,根据移动公理，移动的后置条件变为真在postcond(X,p)top(A,p3)Top(emptydisk,p3) (on(A,emptydisk)top(A,p3)On(A,B)top(A,p1)(top(B,p1)on(A,B);后置条件改变了初始状态，改变后的状态为disk(A)disk(B)disk(C),Top(emptydisk,p2)top(A,p3)top(B,p1)on(A,emptydisk)on(B,C)on(C,emptydisk);,操作规划问题（续）,第二次移动证明：第二次移动是move(B,p2).只有当precond(B,p2)为真时，该移动才是可执行的。将B移动到p2后，该移动所产生的影响由后置条件和持续性公理给出。对后置条件的求值需要步骤：,操作规划问题（续）,top(B,p2)top(emptydisk,p2) (on(B,emptydisk) top(B,p2),on(B,Z)top(B,p1)(top(C,p1)on(B,C),操作规划问题（续）,其他的盘子未受后置条件的影响：Disk(A)disk(B)disk(C),Top(B,p2)on(B,emptydisk)top(A,p3)top(C,p1)on(A,emptydisk)on(C,emptydisk).类似地，可以得到其他各次移动的证明，从而完成该操作规划问题的逻辑演算。,操作规划问题（续）,LTL的模型,一个迁移系统M=(S,L)是一个状态的集合S，带有迁移关系，使得每个sS有某个sS,满足ss，以及一个标记函数L：S2p(p是原子式原子式),s1,s2,s0,p.q,q,r,r,s1,s1,s2,s2,s2,s2,s2,s0,路径,模型M=(S,L)中的一条路径是S中状态的无限序列s1, s2, s3, ,对每个i1，有sisi+1。写为： s1s2。,s1,s2,s0,p.q,q,r,r,s0,p.q,q,r,r,p.q,q,r,r,r,r,r,i :从si 开始的路径3 :从s3 , s4 ,LTL公式的语义,设M=(S,L)是一个模型， =s1是M中的一条路径|= 【路径 满足LTL公式】|= p pLb(t0)|= | |= |= 或者|= |= |= 并且|= |= X 1 |= |= F 存在k0，k|= |= G 对于任意的i1，i|= |= U 存在i1，使得i|=且对于所有的j=1,i-1,有j|=,LTL公式的语义（续）,设M=(S,L)是一个模型，sS,且每条始于s的执行路径，都有|=。记为W.s|=,LTL公式的语义（续）,设M=(S,L)是一个模型，sS,且是一个LTL公式。如果对M的每条始于s的执行路径，都有|= ，记为M,s|= 。M,s0 |= pqM,s0 |= rM,s0 |=XrM,s0 |=X(qr)不成立M,s0 |=G(pr)M,s2 |=GrM,s|=F(qr)FGr M,s0 |=GFpGFr,s1,s2,s2,s2,s2,s2,s0,s0,p.q,q,r,r,p.q,q,r,r,r,r,r,规范的实际模式,在started成立但在ready不成立时，不可能到达的状态G (started ready)对任何状态，如果一个请求发生，那么它将最终被确认G(requestedF acknowledged)在每一条计算路径上，一个特定的使能无限多次GF enabled,规范的实际模式,不管发生什么情况，一个特定过程的最终被永远死锁FG deadlock如果该过程被使能无限次，则它运行无限次GF enabledGF running如果乘客想去五层，一个上行的电梯在第二层不改变方向G(floor2directionupButtonPressed5(directionupUfloor5),LTL不能表达的性质,从任何状态出发，都可能到达一个重启状态电梯可以闲置在第三层不开门,LTL公式之间的重要等价,两个LTL公式和是等价的，如果对所有模型M及M中的所有路径:|= 当且仅当|= 。G FF GX XF() FFG() GG,LTL公式之间的重要等价,U ( U( )F,计算树逻辑,计算树逻辑一种离散，分支时间命题时态逻辑。由E.Clark和A. Emerson于二十世纪八十年代提出的后来经过对CTL文法中的路径量词及其他时态算子的组合使用进行扩展，建立了CTL*一般把CTL和CTL*统称为计算树逻,计算树逻辑演算子,除了时态演算子G，F，X，U外，还增加了路径量词A：所有未来路径E：至少一条路径,CTL公式定义,原子命题（命题常元或者命题变元）是CTL；如果，是CTL公式，那么（），（），（），（），（）是CTL公式；如果，是CTL公式，那么(AX)，(EX)，(A(U)，(E(U)，(AF)，(EF)，(AG)，(EG)CTL公式；且仅当有限次地使用（1）（2）（3）所组成的符号串是CTL公式。,属于CTL公式的符号串,AG(pEGq)EFE(pUq)EFEGpAFqA(pUEFq)AGAF(pA(pU(pA(pUq),不属于CTL公式的符号串,EFGp F，G后面必须紧接A或者E； EF（pUq） U必须接A或者E；AF(pUq)(pUt) (pUq)，(pUt)前面必须是A或E。A(pUq)(pUt) A后面的括号里边不能有,CTL公式的语义（1）,设M=(S,L)是关于CTL的一个模型，sS，是一个CTL公式，关系M,s|=由对做结构归纳定义：M,s p当且仅当pL(s)M,s |=当且仅当 M,s | M,s |= 当且仅当 M,s |= 或者M,s |= M,s |= 当且仅当 M,s |= 并且M,s |= M,s |= 当且仅当M,s | 或者M,s |= ,CTL公式的语义（2）,6. M,s AX当且仅当对所有使ss1的s1有M, s1 |=。7.M,s EX当且仅当对某个使ss1的s1有M, s1 |=。8.M,s AG当且仅当对所有满足s=s1的路径s1s2 ,及该路径上所有的si有M, si |=。9.M,s EG当且仅当存在一条满足s=s1的路径s1s2 ,及该路径上所有的si有M, si |=。,CTL公式的语义（3）,10. M,s AF当且仅当对所有满足s=s1的路径s1s2 ,，有某个si，使得M, si |=。11. M,s EF当且仅当存在一条满足s=s1的路径s1s2 ,，并且该路径存在某个si，使得M, si |=。12. M,s A(1U2)当且仅当对所有满足s=s1的路径s1s2 ,，该路径满足1U2，即沿着该路径存在某个si，使得M, si |=2；对于每个ji,有M, sj |=1。13. M,s E(1U2)当且仅当存在一条满足s=s1的路径s1s2 ,，该路径满足1U2，即沿着该路径存在某个si，使得M, si |=2,对于每个jI,有M, sj |=1。,CTL公式的语义（4）,上述满足关系式中，(1)(2)(3)(4)(5)是命题逻辑公式的解释，只需要考察当前状态下公式的满足；(6)(7)(8)(9)(10)(11)(12)的解释，不仅要考虑当前状态及所关联的直接有序状态，而且要考虑与当前状态所关联的间接后续状态,模型的有向图,AG , EG 的路径图,模型的有向图,AF, EF的路径图,例的Kripke结构满足的CTL公式,M,s0 pqM,s0 rM,s0 EX(qr)M,s0 AX(qr)M,s0 EF(pr)M,s2 EGr M,s2 AGrM,s0 E(pq)Ur)M,s0 A(pUr),s1,s2,s2,s2,s2,s2,s0,s0,p.q,q,r,r,p.q,q,r,r,r,r,r,使用CTL公式描述简单的规格模式,EF(startready)一个启动started成立但就绪ready不成立的状态；AG(requestedAFacknowledged)对于一个状态，如果请求requesed出现，则终将出现应答acknowledged；AG(AFenabled) 某一进程在所有路径上都会是使能enable无限次；,使用CTL公式描述简单的规格模式,AF(AGdeadlock) 一进程将最终进入死锁AG(EFrestart)任一状态都能进入重启状态AG（floor=2direction=upButtonPressed5 A(direction=upUfloor=5)）一步上行电梯中在第二层不改变方向，如果有乘客想去第五层,使用CTL公式描述简单的规格模式,AG(floor=3 idledoor=close EG(floor=3idledoor=closed)电梯可以在第三层关着门保持闲置AG(n1EXt1)一个进程总可以进入其关键段EF(c1E(c1U(c1E(c2Uc1) 进程无需按严格顺序进入其关键段,CTL公式间的重要等价,AFEGEFAGAXEX,CTL连接词的适当集,AFEGEFAG AU,EU,EX是一个适当集合 AFA(U)A(U)(E(U( )EG )证明: A(U) A ( U( )F)E( U( )F)E( U( )G)(E( U( )EG),其他等价,AG AXAGEG EXEGAF AXAFEF EX EFA(U) (AXA (U) )E(U) (EXE (U) ),LTL和CTL,CTL使用路径量词，在路径描述中比LTL有更强的表达能力CTL不允许像LTL那样，通过公式描述来选择一个路径范围FpF q：对所有这样的路径，沿该路径有p的话也有q.AFpAFqAG(pAFq),CTL和CTL*,在CTL的文法中，对路径量词及其他时态演算子，命题连接词的组合使用进行了一定的限制，从而也就限制了其描述能力。CTL*的描述能力超过CTL。除去CTL对每个时态演算子必须与唯一路径量词伴随使用的约束,CTL*状态公式定义,原子命题是状态公式如果，是状态公式，那么（），（）是CTL公式；如果是路径公式，那么（A），（E）是状态公式；且仅当有限次地使用（1）（2）（3）所组成的符号串是状态公式。,CTL*路径公式定义,状态公式是路经公式；如果，是路径公式，那么（），（）是路径公式；如果，是路径公式，那么（F），（G），（X），（U）是路径公式；且仅当有限次地使用（1）（2）（3）所组成的符号串是路径公式。,CTL*允许的公式,A(pUr)(qUr) A(pq)Ur) A(XpXXp) AXpAXAXpE(GFp) EGEFp,CTL*，CTL和LTL的表达能力,从上述定义不难看出，不包含路径量词A和E的CTL*公式就是LTL公式。因此，CTL和LTL都可以看为CTL*的子类。,3,1,2,4,LTL,CTL,CTL*,1=AGEFp,2=AG(pAFq),3=A(GFpFp）,4=E(GFp）,CTL*公式的例,AGEFp 是CTL公式但不是LTL公式；EGFp 不是CTL公式也不是LTL公式；GFpFq 不是CTL公式但是是LTL公式；AG(pAFq) G(pFq) 是CTL公式也是LTL公式；,本章重点,模态逻辑公式，语义命题线性时态逻辑公式，语义一阶线性时态逻辑公式，语义计算树逻辑公式，语义,练习,下图中系统M确定M,s0|=和M,s2|=是否成立,r,p,q,q,r,p,t,r,s0,s1,s2,s3,1pr2Ft3EGr4E(tUq)5Eq6EFq7EGr8G(rq),