形式化方法课件4.ppt

1、第四章 时态逻辑时态逻辑引入n命题逻辑和谓词逻辑表达的可能性真和假n不能表达的可能性必然为真知道为真将来为真相信为真例n奥巴马是美国总统n太阳系有九大行星n27的立方根是3模态逻辑本章内容n模态逻辑n时态逻辑命题线性时态逻辑一阶线性时态逻辑计算树逻辑（CTL，CTL*）模态逻辑相关概念n模态（Modal）谓词逻辑的扩展形式。基于命题逻辑的扩展称为模态命题逻辑，基于一阶谓词逻辑的扩展称为模态一阶逻辑。特点是通过引入“可能”和“必然”两个模态词，从而能够对可能世界中的命题进行描述和演算。n模态词必然（）；可能（）例如,对于命题P:火星上有生命，nP：火星上必然有生命nP：火星上可能有生命；模态逻辑

2、公式n原子命题是模态逻辑公式；n如果A是模态逻辑公式。那么A和A是模态逻辑公式；n如果A,B是模态逻辑合适公式，那么（A），（AB），（AB），AB），（AB）是模态逻辑公式；n当且仅当有限次地使用（1）（2）（3）所组成的符号串是模态逻辑公式。考察（1)nAA 必然A真则A真；nAA A真则可能A真；nAA 必然A真则可能A真；nAA 必然A真当且仅当不可能A；nAA 可能A当且仅当并非必然 A；nAA 可能A或者可能A；考察（2）n（AA）不会既有必然A，又有必然A；n (AA) 必然有A成立或者A成立；n （AA） 不可能A与 A同时成立；n （AB） AB 必然A并且B等价于必然A并且

3、必然B；考察（3）nAB（AB） 如果必然A和必然B有一个为真，那么必然有A真或者B真；n （AB） AB 可能A或者B当且仅当可能A或者可能B；n （AB） AB 如果可能有A并且B，那么可能A并且B 。模态一阶逻辑公式n原子谓词公式是模态逻辑公式；n如果A,B是模态一阶逻辑公式，那么（A），（A），（A），（AB），（AB），（AB），（AB）是模态逻辑公式；n如果A是模态一阶逻辑公式，x是A中出现的变量（个体变量），则x.A, x.A是模态逻辑公式;n当且仅当有限次地使用（1）（2）（3）所组成的符号串是模态一阶逻辑公式.与量词相关的性质xP(x. P)xP(x. P)(xP) (xP)

4、xP(xP)模态词之间的关系nP PnP P模态逻辑语义n要区分真值的不同模式或程度n基本模态逻辑的模型（Kripke）：三元组M=（W,R,L）W：可能世界的非空集合；R包含于 W W：可能世界W上的二元关系，L：W2p(P为原子公式集合)：标记函数，对可能世界的真值指派。例：R(w,w):世界w可从世界w到达s1s2s0用图来表现Kripke结构n圆圈：可能世界n有向线段：可能世界之间的关系n圆圈内：标记函数标识（该可能世界中成立的原子公式）p.qq,rr标准模型n满足下面条件的三元组M=(W,R,L):对于p，q P和s，t W有：nL(p,s) = 10nL(p,s) = L(p,s)

5、nL(pq,s) = L(p,s)L(q,s)nL(pq,s) = L(p,s) L(q,s)nL(p,s) = (t)(sRtL(p,t)=1nL(p,s) = (t)(sRtL(p,t)=1定义的真值n设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|=定义n如

6、果该模型中每个世界都满足该公式，称基本模态逻辑的模型M(W,R,L)满足一个公式。写M|=当且仅当对每个xW,x|- x6x5x4例nx1 |- qnx1 |- qnx1 |- qnx5 |- p nx5 |- qnx5 |- pqnx5 |- (pq)nx2,x3,x4,x5,x6 |-ppx1x3x2p.qqpqqq模态公式之间的等价n基本模态逻辑的一个公式集语义导出基本模态逻辑公式，如果对任何模型M=（W,R,L）中的任何世界x，只要对所有均满足x|-,就有x|- 。在这种情况下,|=成立。n和是语义等价，如果|=和|=成立。记为模态公式之间的等价（续）n命题逻辑中的任何等价也是模态逻辑

7、中的等价。n取命题逻辑中的任何等价，将原子一致地代换成任意的模态逻辑公式，结果还是模态逻辑中的等价。n例：pq, (pq)p: p (qp) q: r(qp)p (qp)(r(qp) (p (qp) (r(qp)有效公式n基本模态公式称为有效，如果它在任何模型的任何世界中都为真n任何命题逻辑重言式是有效公式，它的任何代换实例也是有效公式 () ) () 有效公式K公式：() 证明：x|- () 当且仅当x|- () 且x|- 当且仅当对所有满足R(x,y)的y，有y|- 和y|- 蕴涵对所有满足R(x,y)的y，有y|- 当且仅当 x|- .时态逻辑模态逻辑的种类必然可能 将来所有时刻 将来某

8、个时刻知道或信念逻辑必然可能知道信念相信义务逻辑必然可能 必须 应该时态逻辑n一种特殊类型的模态逻辑n将Kripke结构M=(W,R,L)中的R解释为时间的先后关系的模态逻辑n基于对时间的不同描述，产生了多种不同形式的时态逻辑。分支时态逻辑线性时态逻辑分支时态逻辑n分支时间时间具有分支或者树形结构性质：任一当前时刻可能分叉为多种可能未来时间。n分支时态逻辑采用分支时间结构的时态逻辑。需要提供对分支时间特性下多种未来行为描述的量化词。可以很好地处理不确定性。线性时态逻辑n线性时间：任一当前时刻仅存在唯一的可能未来时刻，时间的推进；n线性时态逻辑：采用线性时间结构的时态逻辑。提供了用于描述事件沿着

9、单一时间轴演化的模态演算子。常用时态逻辑n命题线性时态逻辑（PLTL）n一阶线性时态逻辑（FOLTL）n命题分支时态逻辑或计算树逻辑（CTL，CTL*）命题线性时态逻辑（PLTL）n在命题逻辑中增加4类模态词(G)演算子： A：A总是为真或者永远为真；(F)演算子A：A最终为真或者有时为真；(X)演算子A：A在下一时刻为真；(U)演算子 AB：A一直为真直到B为真；PLTL公式的定义n原子命题是PLTL；n如果A,B是PLTL公式，那么（A），（AB），（AB），（AB），（AB）是命题线性时态逻辑公式；n如果A是PLTL公式，那么（A），（A），（A）是命题线性时态逻辑公式；n如果A，B是P

10、LTL公式，那么（AB）是命题线性时态逻辑公式；n当且仅当有限次地使用（1）（2）（3）所组成的符号串是PLTL公式。考察（1）n给出下面一些PLTL公式的解释nAB如果当前状态A为真，则最终能出现B为真的状态；n（AB）从当前状态开始，使A为真的状态后终将有使B为真的状态；nA从某一状态开始A永远为真；考察（2）n（AA）终将有一状态，在该状态中A为真，并且下一状态中A为假；nA对今后任何状态而言，其后都将有状态使A为真；n（ AB）对今后状态而言，A真将导致B从此永远真；考察（3）nA（AB）或者A从此永远真，或者A从此一直真直到使B真的状态出现；nA（AB）如果有状态使A为真，那么必将有

11、一状态，使A在此状态前一直为假，而B在此状态中为真；nAA如果A从此永远真，那么下一状态中，A将永远为真；考察（4）nAB B如果有状态使A在此之前一直真，而在其中B为真，那么B有时会为真；n（AA（AA）如果在今后的状态中，A真蕴涵下一状态A为真，那么A一旦真便永远真；nAB（B（A（AB）从现在起A一直真到B真，等同于出现B真，或者现在A真，而下一时刻起A一直真到B真例：LSI动态寄存器电路单元的命题线性时态逻辑规格nT1和T2为通路晶体管，nI1和I2为反相器，nx是输入信号，nI是负载信号，是时钟信号。n寄存器的作用:在时钟信号和负载信号I都是触发的情况下，将一个输入数据x存储到单元中

12、.保证在没有新的负载信号到来期间，数据x不被通路晶体管T2改变x1 I2 IT1T2zyI2I1n基本元素规格p：p点的电位为高位p：p点的电位为地位p：p点电位从地位到高位的状态变化P：p点的电位从高位到低位的状态变化电位的变化可规格为p=PPP=PP例：LSI动态寄存器电路单元的命题线性时态逻辑规格(续)n状态的改变还具有的性质：如果p点的电位为高（低）位，则一直保持该电位直到发生状态变化。相应的时态逻辑规格为（P（PP） （P（PP）例：LSI动态寄存器电路单元的命题线性时态逻辑规格(续)n通路晶体管当v3门的输入信号激活时，v1门的信号将被传送到v2门.如果v2门的电位为低而v1门的电

13、位为高，则当v3门的电位变为高位时，v2门的电位将变为高位；如果v2门的电位为高而v1门的电位为低，则当v3门的电位变为高位时，v2门的电位将变为低位。引入算子PF来规格该功能：PF（v1,v2,v3）=(v3(v1v2v2) (v3（v1v2v2）)例：LSI动态寄存器电路单元的命题线性时态逻辑规格(续)v1v3v2n反向器的特征当v1门的电位为高时，下一时刻v2门的电位也将为高；当v1门的电位为低时，下一时刻v2门的电位也将为低。描述：(v1v2)(v1v2)例：LSI动态寄存器电路单元的命题线性时态逻辑规格(续)v1v2n时钟引入算子y来描述时钟的循环一个周期为4的时钟可描述为：ny=

14、y例：LSI动态寄存器电路单元的命题线性时态逻辑规格(续)n电位行为规格n晶体管T1: PF(x,z,I)，T2: PF(z,y,I)n组合反相器(zy)(zy )n电位状态变化(z(zz) ，(z(zz)(y(yy)， (y(yy)例：LSI动态寄存器电路单元的命题线性时态逻辑规格(续)n电路性能的推演行为描述为：行为规格+输入信号 电路性能 负载信号根据如下序列进行周期变化：低位，高位，高位，低位，IIII输入信号 输入信号按如下序列产生：低位，高位，高位：xxx时钟信号 时钟信号根据如下序列产生：开始为高位，然后根据y所描述的序列变化：y例：LSI动态寄存器电路单元的命题线性时态逻辑规格

15、(续)n输入信号x，时钟信号，负载信号I，以及z和y点的电位用表表示：ny例：LSI动态寄存器电路单元的命题线性时态逻辑规格(续)时间点012345678输入信号xx时钟信号负载信号IIIIIIIIZ点电位zzzzzzzY点电位yyyyyy一阶线性时态逻辑n阶线性一时态逻辑（FOLTL）是一阶谓词逻辑的扩展。它是在一阶谓词逻辑中增加了模态词 演算子 A表示A总是为真或者永远为真； 演算子 A表示A最终为真或者有时为真； 演算子 A表示A在下一时刻为真； 演算子： AB表示A一直为真直到B为真。FOLTL公式的定义n原子谓词公式是FOLTL；n如果A,B是FOLTL公式，那么（A），（AB），（

16、AB），（AB），（AB）是一阶线性时态逻辑公式；n如果A是FOLTL公式，x是A中出现的变量，则则xA, xA是FOLTL公式；n如果A是FOLTL公式，那么（A），（A），（A），（AB）是一阶线性时态逻辑公式；n当且仅当有限次地使用（1）（2）（3）（4）所组成的符号串是FOLTL公式。FOLTL的应用n队列及其操作n操作规划问题队列及其操作n是一种常用的抽象数据类型，n服从先进先出FIFO规则n在某个时刻从一个队列可以为空或非空n队列状态的改变归因于两个操作PUT：插入一个元素到队尾GET：从队列头部移动一个元素。队列及其操作（续）n设所讨论的队列是一个共享数据类型，PUT和GET操作

17、就可以被多个进程同时执行。n要求：在具体的任何一个时刻队列上只能发生一个操作，给定队列的当前内容，则只能有一个进程在该状态下执行PUT或GET操作一个进程使用GET操作来取出当前的队列头部的值；如果当前队列为空，则该进程等待，直到另一进程将一个值放进队列。n用函词cur_queue：队列的当前状态nputval：PUT操作的参数ngetval：GET操作的参数nPUT操作的前置条件：putvalnil， 后置条件为：putval=niln GET操作的前置条件：getval=nil 后置条件：getvalnil 谓词enter(PUT),enter(GET),exit(GET),exit(PU

18、T),表示相应操作的开始和终止。队列及其操作（续）n活性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);（用符号“*”表示在队列末尾插入后继元素）队列及其操作（续）nGET操作的活性特征是：其中只有在从队列中取出一个值后才能终止如果队列为空，则该操作将一直等到某个值被放进队列，然后再取

19、出这个值。enter(GET)empty(cur_queue)max) (exit(GET)(getval*cur_queue=cur_queue);enter(GET)empty(cur_queue) enter(GET) exit(PUT)n如果队列为空，则某些进程将最终加入一个值到队列中。 empty(cur_queue) enter（PUT）队列及其操作（续）n安全性设（enter(PUT)putvalnil）在cur_queue下成立。则如果当前队列为满，其下一个状态cur_queue将与cur_queue一样；如果当前队列不为满，cur_queue=cur_queue*putval

20、相应的时态逻辑公式为（enter(PUT)putvalnil）(length(cur_queue)=max)(cur_queue=cur_queue)(length(cur_queue)max)(cur_queue=cur_queue*putval)）队列及其操作（续）n设（enter(GET)putval=nil）在cur_queue下成立。则如果当前队列为空，其下一个状态cur_queue将与cur_queue一样；如果当前队列不为空，将有cur_queue=getval*cur_queue.相应的时态逻辑公式为n(enter(GET)getval=nil)(empty(cur_queue

21、)empty(cur_queue)(empty(cur_queue)(cur_queue=getval*cur_queue)队列及其操作（续）操作规划问题n有三个柱子P1,P2,P3和3个盘子A,B,Cn开始时三个盘子放在p1上，并且最小的盘子A在最上面，最大的盘子C在最下面n要求设计一种操作方案将三个盘子从p1移到p3,在移动过程中可使用p2作为暂时的存放位置在每次移动盘子之后，要求在各柱子上的盘子总是上小下大。n操作活动n定义谓词：Move(X,p) 将盘子X移动到柱子p；On(X,Y) 盘X在Y上；Smaller(X,Y) 盘X比盘Y小；Top(X,p) 盘X在柱子p的最上面；Free(

22、X) 盘X可以被移动。操作规划问题（续）n操作的约束条件：如果盘子上面没有其他的盘子，则该盘子是可以被移动的。free(X) Z.on(X,Z).如果盘子X在柱子p的最上面，则该盘子可以自由移动top(X,p) free(X).操作规划问题（续）n比较盘子大小的谓词满足传递关系：Smaller(X,Y)smaller(Y,Z) smaller(X,Z).n任何时候一个盘子不可能在不同的两个盘子上（Y1Y2）(on(X,Y1)on(X,Y2).操作规划问题（续）n规格假设：设一个为空的柱子上有一个空盘子，该空盘子比任何一个给定的盘子都大。即p.top(emptydisk,p)X.(top(X,p

23、)on(X,emptydisk);X.smaller(X,emptydisk).操作规划问题（续）n操作活动的前置条件和后置条件： 活动move(X,p)的前置条件precond(X,p)： 盘X是自由的；盘X比柱子p的最上面的盘子Y小precond(X,p)=free(X)top(Y,p)smaller(X,Y).操作规划问题（续）n活动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,

24、Y)top(X,p)free(Y), On(X,Z)top(X,p) (top(Z,p)on(X,Z)free(Z),操作规划问题（续）n如果移动的盘子X到柱子p的活动的前置条件成立，并且移动的动作也得到了执行，则后置条件以及持续性都应该成立：precond(X,p)move(X,p) (postcond(X,p)persistent_free(X,p)persistent_on(Y,p).操作规划问题（续）n操作的持续性：没有受到任何后置条件影响的自由盘子将保持为自nPersistent_free(X,p) (X)free(X)(postcond(X,p) (Z)on(Z,X) free(X

25、)没有受任何后置条件影响的在另一盘子上的盘子保持相同状态nPersistent_free(X,p) (X) (Y) on(X,Y)(postcond(X,p) on(X,Y) on(X,Y)操作规划问题（续）n操作规划任务初始状态：在起始时刻，盘子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);操作规划问题（续）

26、n目标状态：目标状态是让A,B,C以初始时同样的顺序叠放在p3上(on(C,emptydisk)on(B,C)on(A,B)top(A,p3)。操作规划问题（续）n操作规划求取存在一个与规格相一致的活动序列：move(A,p3)move(B,p2)2move(A,p2)3move(C,p3)4move(A,p1)5move(B,p3)6move(A,p3).操作规划问题（续）n逻辑推演对于该活动序列中的每个移动，证明其前置条件是满足的，并且其后置条件将会使系统处于下一个新状态，而在新的状态下，下一个移动的前置条件是满足的。操作规划问题（续）n第一次移动证明：前置条件precond(X,p)fr

27、ee(A)top(emptydisk,p3)smaller(A,emptydisk);将盘A移动到柱子p3,便有precond(A,p3)move(A,p3);操作规划问题（续）n根据移动公理，移动的后置条件变为真在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);n后置条件改变了初始状态，改变后的状态为disk(A)disk(B)disk(C),Top(emptydisk,p2)top(A,p3)top(B,p1)on(A,emptydisk)o

28、n(B,C)on(C,emptydisk);操作规划问题（续）n第二次移动证明：第二次移动是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)操作规划问题（续）n其他的盘子未受后置条件的影响：Disk(A)disk(B)disk(C),Top(B,p2)on(B,emptydisk)t

29、op(A,p3)top(C,p1)on(A,emptydisk)on(C,emptydisk).n类似地，可以得到其他各次移动的证明，从而完成该操作规划问题的逻辑演算。操作规划问题（续）LTL的模型n一个迁移系统M=(S,L)是一个状态的集合S，带有迁移关系，使得每个sS有某个sS,满足ss，以及一个标记函数L：S2p(p是原子式原子式)s1s2s0p.qq,rrs1s1s2s2s2s2s2s0路径n模型M=(S,L)中的一条路径是S中状态的无限序列s1, s2, s3, ,对每个i1，有sisi+1。写为： s1s2。s1s2s0p.qq,rrs0p.qq,rrp.qq,rrrrri :从s

30、i 开始的路径3 :从s3 , s4 ,LTL公式的语义n设M=(S,L)是一个模型， =s1是M中的一条路径|= 【路径 满足LTL公式】n|= p pLb(t0)n|= | n|= |= 或者|= n|= |= 并且|= n|= X 1 |= n|= F 存在k0，k|= n|= G 对于任意的i1，i|= n|= U 存在i1，使得i|=且对于所有的j=1,i-1,有j|= LTL公式的语义（续）n设M=(S,L)是一个模型，sS,且每条始于s的执行路径，都有|=。记为W.s|=LTL公式的语义（续）n设M=(S,L)是一个模型，sS,且是一个LTL公式。如果对M的每条始于s的执行路径，

31、都有|= ，记为M,s|= 。1.M,s0 |= pq2.M,s0 |= r3.M,s0 |=Xr4.M,s0 |=X(qr)不成立5.M,s0 |=G(pr)6.M,s2 |=Gr7.M,s|=F(qr)FGr 8.M,s0 |=GFpGFrs1s2s2s2s2s2s0s0p.qq,rrp.qq,rrrrr规范的实际模式n在started成立但在ready不成立时，不可能到达的状态G (started ready)n对任何状态，如果一个请求发生，那么它将最终被确认G(requestedF acknowledged)n在每一条计算路径上，一个特定的使能无限多次GF enabled规范的实际模式

32、n不管发生什么情况，一个特定过程的最终被永远死锁FG deadlockn如果该过程被使能无限次，则它运行无限次GF enabledGF runningn如果乘客想去五层，一个上行的电梯在第二层不改变方向G(floor2directionupButtonPressed5(directionupUfloor5)LTL不能表达的性质n从任何状态出发，都可能到达一个重启状态n电梯可以闲置在第三层不开门LTL公式之间的重要等价n两个LTL公式和是等价的，如果对所有模型M及M中的所有路径:|= 当且仅当|= 。nG FnF GnX XnF() FFnG() GGLTL公式之间的重要等价U ( U( )F

33、F计算树逻辑n计算树逻辑一种离散，分支时间命题时态逻辑。由E.Clark和A. Emerson于二十世纪八十年代提出的后来经过对CTL文法中的路径量词及其他时态算子的组合使用进行扩展，建立了CTL*一般把CTL和CTL*统称为计算树逻计算树逻辑演算子n除了时态演算子G，F，X，U外，还增加了路径量词nA：所有未来路径nE：至少一条路径CTL公式定义n原子命题（命题常元或者命题变元）是CTL；n如果，是CTL公式，那么（），（），（），（），（）是CTL公式；n如果，是CTL公式，那么(AX)，(EX)，(A(U)，(E(U)，(AF)，(EF)，(AG)，(EG)CTL公式；n且仅当有限次地使

34、用（1）（2）（3）所组成的符号串是CTL公式。属于CTL公式的符号串nAG(pEGq)nEFE(pUq)nEFEGpAFqnA(pUEFq)nAGAF(pA(pU(pA(pUq)不属于CTL公式的符号串nEFGp F，G后面必须紧接A或者E；n EF（pUq） U必须接A或者E；nAF(pUq)(pUt) (pUq)，(pUt)前面必须是A或E。nA(pUq)(pUt) A后面的括号里边不能有CTL公式的语义（1）设M=(S,L)是关于CTL的一个模型，sS，是一个CTL公式，关系M,s|=由对做结构归纳定义：1.M,s p当且仅当pL(s)2.M,s |=当且仅当 M,s | 3.M,s

35、|= 当且仅当 M,s |= 或者M,s |= 4.M,s |= 当且仅当 M,s |= 并且M,s |= 5.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

36、 ,，有某个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）n上述满足关系式中，(1)(2)(3)(4)(5)是命题逻辑公式的

37、解释，只需要考察当前状态下公式的满足；n(6)(7)(8)(9)(10)(11)(12)的解释，不仅要考虑当前状态及所关联的直接有序状态，而且要考虑与当前状态所关联的间接后续状态模型的有向图nAG , EG 的路径图模型的有向图nAF, EF的路径图例的Kripke结构满足的CTL公式1.M,s0 pq2.M,s0 r3.M,s0 EX(qr)4.M,s0 AX(qr)5.M,s0 EF(pr)6.M,s2 EGr 7.M,s2 AGr8.M,s0 E(pq)Ur)9.M,s0 A(pUr)s1s2s2s2s2s2s0s0p.qq,rrp.qq,rrrrr使用CTL公式描述简单的规格模式nEF

38、(startready)一个启动started成立但就绪ready不成立的状态；nAG(requestedAFacknowledged)对于一个状态，如果请求requesed出现，则终将出现应答acknowledged；nAG(AFenabled) 某一进程在所有路径上都会是使能enable无限次；使用CTL公式描述简单的规格模式AF(AGdeadlock) 一进程将最终进入死锁AG(EFrestart)任一状态都能进入重启状态AG（floor=2direction=upButtonPressed5 A(direction=upUfloor=5)）一步上行电梯中在第二层不改变方向，如果有乘客想

39、去第五层使用CTL公式描述简单的规格模式nAG(floor=3 idledoor=close EG(floor=3idledoor=closed)电梯可以在第三层关着门保持闲置nAG(n1EXt1)一个进程总可以进入其关键段nEF(c1E(c1U(c1E(c2Uc1) 进程无需按严格顺序进入其关键段CTL公式间的重要等价nAFEGEGnEFAGAGnAXEXEXCTL连接词的适当集AFEGEGEFAGAG AU,EU,EX是一个适当集合 AFA A(U U)nA(U)(E(U( )EGEG )证明: A(U) A ( U( )F F)E( U( )F F)E( U( )G G)(E( U( )

40、EGEG)其他等价nAG AXAGnEG EXEGnAF AXAFnEF EX EFnA(U) (AXA (U) )nE(U) (EXE (U) )LTL和CTLnCTL使用路径量词，在路径描述中比LTL有更强的表达能力nCTL不允许像LTL那样，通过公式描述来选择一个路径范围FpF q：对所有这样的路径，沿该路径有p的话也有q.AFpAFqAG(pAFq)CTL和CTL*n在CTL的文法中，对路径量词及其他时态演算子，命题连接词的组合使用进行了一定的限制，从而也就限制了其描述能力。CTL*的描述能力超过CTL。除去CTL对每个时态演算子必须与唯一路径量词伴随使用的约束CTL*状态公式定义n原

41、子命题是状态公式n如果，是状态公式，那么（），（）是CTL公式；n如果是路径公式，那么（A），（E）是状态公式；n且仅当有限次地使用（1）（2）（3）所组成的符号串是状态公式。CTL*路径公式定义n状态公式是路经公式；n如果，是路径公式，那么（），（）是路径公式；n如果，是路径公式，那么（F），（G），（X），（U）是路径公式；n且仅当有限次地使用（1）（2）（3）所组成的符号串是路径公式。CTL*允许的公式nA(pUr)(qUr) A(pq)Ur) nA(XpXXp) AXpAXAXAXAXpnE(GFp) EGEFpCTL*，CTL和LTL的表达能力n从上述定义不难看出，不包含路径量词A和

42、E的CTL*公式就是LTL公式。因此，CTL和LTL都可以看为CTL*的子类。3 1 24 LTLCTLCTL*1=AGEFp2=AG(pAFq)3=A(GFpFp）4=E(GFp）CTL*公式的例nAGEFp 是CTL公式但不是LTL公式；nEGFp 不是CTL公式也不是LTL公式；nGFpFq 不是CTL公式但是是LTL公式；nAG(pAFq) G(pFq) 是CTL公式也是LTL公式；本章重点n模态逻辑公式，语义n命题线性时态逻辑公式，语义n一阶线性时态逻辑公式，语义n计算树逻辑公式，语义练习n下图中系统M确定M,s0|=和M,s2|=是否成立 rp,qq,rp,t,rs0s1s2s31pr2Ft3EGr4E(tUq)5Eq6EFq7EGr8G(rq)