形式化方法课件4.ppt
- 【下载声明】
1. 本站全部试题类文档,若标题没写含答案,则无答案;标题注明含答案的文档,主观题也可能无答案。请谨慎下单,一旦售出,不予退换。
2. 本站全部PPT文档均不含视频和音频,PPT中出现的音频或视频标识(或文字)仅表示流程,实际无音频或视频文件。请谨慎下单,一旦售出,不予退换。
3. 本页资料《形式化方法课件4.ppt》由用户(三亚风情)主动上传,其收益全归该用户。163文库仅提供信息存储空间,仅对该用户上传内容的表现方式做保护处理,对上传内容本身不做任何修改或编辑。 若此文所含内容侵犯了您的版权或隐私,请立即通知163文库(点击联系客服),我们立即给予删除!
4. 请根据预览情况,自愿下载本文。本站不保证下载资源的准确性、安全性和完整性, 同时也不承担用户因使用这些下载资源对自己和他人造成任何形式的伤害或损失。
5. 本站所有资源如无特殊说明,都需要本地电脑安装OFFICE2007及以上版本和PDF阅读器,压缩文件请下载最新的WinRAR软件解压。
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- 形式化 方法 课件
- 资源描述:
-
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(
展开阅读全文