《形式化方法幻灯片4》由会员分享，可在线阅读，更多相关《形式化方法幻灯片4（107页珍藏版）》请在金锄头文库上搜索。
1、第四章 时态逻辑,时态逻辑,引入,命题逻辑和谓词逻辑表达的可能性 真和假 不能表达的可能性 必然为真 知道为真 将来为真 相信为真,例,奥巴马是美国总统 太阳系有九大行星 27的立方根是3,模态逻辑,本章内容,模态逻辑 时态逻辑 命题线性时态逻辑 一阶线性时态逻辑 计算树逻辑（CTL，CTL*）,模态逻辑相关概念,模态（Modal） 谓词逻辑的扩展形式。基于命题逻辑的扩展称为模态命题逻辑，基于一阶谓词逻辑的扩展称为模态一阶逻辑。特点是通过引入“可能”和“必然”两个模态词，从而能够对可能世界中的命题进行描述和演算。 模态词 必然（）；可能（） 例如,对于命题P:火星上有生命， P：火星上必然有生
2、命 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）
3、 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.
4、 P) xP(x. P) (xP) (xP) xP(xP),模态词之间的关系,P P P 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
5、 P和s，t W有： L(p,s) = 10 L(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)=1 L(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
6、(x,y)的每一yW,有y|= x|- 当且仅当存在yW,使得R(x,y)且y|=,定义,如果该模型中每个世界都满足该公式，称基本模态逻辑的模型M(W,R,L)满足一个公式。写M|=当且仅当对每个xW,x|-,x6,x5,x4,例,x1 |- q x1 |- q x1 |- q x5 |- p x5 |- q x5 |- pq x5 |- (pq) x2,x3,x4,x5,x6 |-pp,x1,x3,x2,p.q,q,p,q,q,q,模态公式之间的等价,基本模态逻辑的一个公式集语义导出基本模态逻辑公式，如果对任何模型M=（W,R,L）中的任何世界x，只要对所有均满足x|-,就有x|- 。在这种
7、情况下,|=成立。 和是语义等价，如果|=和|=成立。记为,模态公式之间的等价（续）,命题逻辑中的任何等价也是模态逻辑中的等价。 取命题逻辑中的任何等价，将原子一致地代换成任意的模态逻辑公式，结果还是模态逻辑中的等价。 例：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|
8、- 和y|- 蕴涵对所有满足R(x,y)的 y，有y|- 当且仅当 x|- .,时态逻辑,模态逻辑的种类,必然,可能,将来所有时刻,将来某个时刻,知道或信念逻辑,必然,可能,知道,信念 相信,义务逻辑,必然,可能,必须,应该,时态逻辑,一种特殊类型的模态逻辑 将Kripke结构M=(W,R,L)中的R解释为时间的先后关系的模态逻辑 基于对时间的不同描述，产生了多种不同形式的时态逻辑。 分支时态逻辑 线性时态逻辑,分支时态逻辑,分支时间 时间具有分支或者树形结构性质：任一当前时刻可能分叉为多种可能未来时间。 分支时态逻辑 采用分支时间结构的时态逻辑。 需要提供对分支时间特性下多种未来行为描述的量
9、化词。 可以很好地处理不确定性。,线性时态逻辑,线性时间： 任一当前时刻仅存在唯一的可能未来时刻，时间的推进； 线性时态逻辑： 采用线性时间结构的时态逻辑。 提供了用于描述事件沿着单一时间轴演化的模态演算子。,常用时态逻辑,命题线性时态逻辑（PLTL） 一阶线性时态逻辑（FOLTL） 命题分支时态逻辑或计算树逻辑（CTL，CTL*）,命题线性时态逻辑（PLTL）,在命题逻辑中增加4类模态词 (G)演算子： A：A总是为真或者永远为真； (F)演算子 A：A最终为真或者有时为真； (X)演算子 A：A在下一时刻为真； (U)演算子 AB：A一直为真直到B为真；,PLTL公式的定义,原子命题是PL
10、TL； 如果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 对今
11、后任何状态而言，其后都将有状态使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一直真到
12、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=PP P=PP,例：LSI动态寄存器电路单元的命题线性时态逻辑规格(续),状态的改变还具有的性
13、质： 如果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
14、,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，时钟信号，负载信
