CTL3. temporal logic_960301659

软件形式化验证软件形式化验证第三章时序逻辑贺飞清华大学软件学院2010年3月2011年3月14日星期一1属性规约„为验证系统满足某条性质：1.对系统进行建模，得到系统模型2.对属性进行说明，得到属性公式3执行模型检测算法3.执行模型检测算法如何以一种形式化语言无歧义的描述系统属性？2011年3月14日星期一2时序逻辑„Temporallogicprovidesaformalsystempgpy‰qualitativelydescribingandreasoningabouthowthetruthvaluesofassertionschangeovertimeg‰Itisappropriatefordescribingthetime-varyingbehaviorofsystems(orprograms).y(pg)„Example:Systemcanalwaysrunintoworkingstatusafterbeing„Example:Systemcanalwaysrunintoworkingstatusafterbeingstarted‰AG(Started→AFWorking)‰AG(Started→AFWorking)March14,20113常用的时序逻辑1计算树逻辑（CTL）1.计算树逻辑（CTL）2.线性时序逻辑（LTL）3.扩展的计算树逻辑（CTL*）2011年3月14日星期一4时序逻辑计算树逻辑（CTL）时序辑2011年3月14日星期一5计算树逻辑„计算树逻辑，简称CTL(ComputationTreeLogic)。计算树逻辑，简称CTL(ComputationTreeLogic)。‰是一种分枝时序逻辑‰系统状态变化的可能性被表示成树状结构‰从一个系统状态出发，存在多个可能的后续状态‰从个系统状态出发，存在多个可能的后续状态2011年3月14日星期一6本节内容„CTL语法„CTL语义CTL语义„CTL等价关系„CTL最小联结词集合„CTL属性范例„CTL属性范例2011年3月14日星期一7ComputationTreeLogic(CTL)CTL=Classicalpropositionallogic+temporaloperators„CTL=Classicalpropositionallogic+temporaloperatorsTemporaloperatorsPropositionalLogicLogicMarch14,20118命题逻辑——语法„P,Q,R,...:Propositionalsymbols„¬P:NegationofP„P∧Q:Conjunction:PandQ„P∨Q:Disjunction:PorQQjQ„P→Q:Implication:ifPthenQ„P→Q:Implication:ifPthenQ„P↔Q:Equivalence:PifandonlyifQMarch14,20119命题逻辑——语义PQ¬PP∧QP∨QP→QP↔Q001001100100110110110100010011011111101111March14,201110CTL的时序联结词„CTL以命题逻辑为基础，扩展了新的语法元素‰路径量词„A：对所有路径（All）„A：对所有路径（All）„E：存在一条路径（Exist）时序模态词‰时序模态词„X：下一个状态（neXt）F未来某个状态（Ft）„F：未来某个状态（Future）„G：所有未来状态（Global）直到l）„U：直到（Until）2011年3月14日星期一11CTL语法CTL公式由以下规则递归定义„CTL公式由以下规则递归定义‰每一个原子命题都是CTL公式；‰如果f和g是CTL公式，则¬f,f∧g,AFg,EFg,AGf,EGf,AXf,EXf,A(fUg),E(fUg)也都是CTL公式。„注意在CTL公式中，时序模态词必须与路径量词成对出现出现。2011年3月14日星期一12CTL语法（续）路径量词{A,E}时序模态词{F,X,G,U}2011年3月14日星期一13下面的公式是否符合CTL语法定义？()AEFAEF„A(rUq)„A[pUEFr]„FGr„AEFr„AEFr„FGr„A[pUEFr]„AGAFr„FGr„FGr„A¬G¬p„A¬G¬p„EFE[rUq]A¬G¬pA¬G¬p„F(rUq)„F(rUq)[q](q)(q)2011年3月14日星期一14语法分析树„1.输入：EFE[rUq]„2.前缀形式：EFEU(r,q)EF„3.生成语法树EU„在化简和生成语法树的同时执行语法分析检查。行分析检rq2011年3月14日星期一15本节内容„CTL语法„CTL语义CTL语义„CTL等价关系„CTL最小联结词集合„CTL属性范例„CTL属性范例2011年3月14日星期一16Kripke结构„Kripke结构是一个三元组M=S,R,L，其中Kp结构是个元组M,,L，其中‰S为状态集合；RSS为状态变迁关系‰R⊆S×S为状态变迁关系；‰L:S→2AP为标记函数，将每一个状态映射到在该状态上为真的原子命题集合子命题集合。„Kripke结构的一条路径是S中状态的一个无限序列s0s1s2，其中„Kripke结构的条路径是S中状态的个无限序列s0,s1,s2,…，其中对于每一个i≥0,有(si,si+1)∈R成立。‰记该条路径为：π=s→s→s→‰记该条路径为：π=s0→s1→s2→…‰以πi表示路径π从si开始的后缀，即π=si→si+1→si+2→…2011年3月14日星期一17Kripke结构的计算树模型XXZXYYZXZZ„计算树模型：‰以给定状态为根结点，按照从该结点出发的所有可能计算路径，将Kripke结构展开为一个无穷计算树模型。‰计算树中的每一条路径对应于系统的一条可能执行路径。2011年3月14日星期一18p,qs0rrrq,rs1rs2rrrs2s2s2p,qs0qrsrs2rrs2rs2q,rs1rs2rs2p,qs0q,rs1p,qs0rsq,rrs2s10q,rs1s2rs2rs2p,qs0rs2rs22011年3月14日星期一19CTL语义„设s0是Kripke结构M的一个状态，f和g为CTL公式，根据以下规则„设s0是Kripke结构M的个状态，f和g为CTL公式，根据以下规则定义M,s0|=f(或g):‰Ms0|=piffp∈L(s0)wherepisaatomicproposition‰M,s0|piffp∈L(s0),wherepisaatomicproposition‰M,s0|=¬fiff(M,s0)|≠fMs|fiff(Ms)|fnd(Ms)|‰M,s0|=f∧giff(M,s0)|=fand(M,s0)|=g‰M,s0|=AFfiff∀π:s0→s1→s2→…,∃i≥0,(M,si)|=f‰Ms0|=AGfiff∀π:s0→s1→s2→∀i≥0(Msi)|=f‰M,s0|=EFfiff∃π:s0→s1→s2→…,∃i≥0,(M,si)|=f‰M,s0|=AGfiff∀π:s0→s1→s2→…,∀i≥0,(M,si)|=f‰M,s0|=EGfiff∃π:s0→s1→s2→…,∀i≥0,(M,si)|=f2011年3月14日星期一20CTL语义（续）‰Ms0|=AXfiff∀statet(s0t)∈R(Mt)|=f‰M,s0|AXfiff∀statet,(s0,t)∈R,(M,t)|f‰M,s0|=EXfiff∃statet,(s0,t)∈R,(M,t)|=f‰M,s0|=E(fUg)iff∃π:s0→s1→s2→…,∃k≥0,(M,sk)|=g,and∀i,0≤ik,(M,si)|=f‰M,s0|=A(fUg)iff∀π:s0→s1→s2→…,∃k≥0,(M,sk)|=gand∀i,0≤ik,(M,si)|=f2011年3月14日星期一21CTL语义的直观解释解释M,s|=AFf:如果从s出发的所有路径上都最终存在一个结点，使得f被满足。s点，使得f被满足。M,s|=EFf:如果存在一条从s出发的路径，并且在这条路径上最终存在一个结点，使得f被满足。s存在个结点，使得f被满足。2011年3月14日星期一22CTL语义的直观解释（续）解释续M,s|=AGf:如果从s出发的所有路径上的所有结点，f都被满足s都被满足。M|EGf如果存在条从出M,s|=EGf:如果存在一条从s出发的路径，使得该路径上的所有结点都满足f。s2011年3月14日星期一23CTL语义的直观解释（续）解释续M,s|=AXf:如果从s出发的所有路径的下一个结点都满足fs满足f。M,s|=EXf:如果存在一条M,s|EXf如果存在条从s出发的路径，使得其下一个结点满足f。s2011年3月14日星期一24CTL语义的直观解释（续）解释续fUgfffgfffgM,s|=A[fUg]:如果从s出发的所有路径都满足M,s|=E[fUg]:如果存在一条从出发的路径满足f发的所有路径都满足fUg。条从s出发的路径满足fUg。2011年3月14日星期一25CTL语义的直观解释（续）解释续„理解fUg解g‰公式g必须在未来的某个状态成立，并且在此之前，公式f必须一直成立；直成立；fUgfffg如果在当前状态成立则对公式f没有要求fffg‰如果g在当前状态成立，则对公式f没有要求。fUgg2011年3月14日星期一26WeakUntil„Theweakuntilallowsthepossibilitythatqneverhappensandpremainstrueforever.„ForCTL,the“weak”until:E[pWq]=E[pUq]∨EGpA[pWq]=A[pUq]∨AGp„Usefulforexpressingpropertieslike:¬output(x)Winput(x)‰“Anoutputdoesnotoccurbeforeaninputoccurs.”2011年3月14日星期一27“当前”与“未来”„在上述定义中“未来”包含“当前”„在上述定义中，未来包含当前‰这意味着，当我们说“在所有的未来状态”时，我们将当前状态作为种未来状态也包括了进来作为一种未来状态也包括了进来。‰这只是为了方便处理的一种约定。„采纳该约定的结果：p‰|=(AGp)→p‰|=p→A[qUp]p‰|=p→EFp2011年3月14日星期一28下面的CTL公式是否成立？M,s0|=p∧qp,qs0,0|pqM,s0|=rMs|=TM,s0|=TM,s0|=EX(q∧r)q,rrs2s1M,s0|=AX(q∧r)M,s0|=¬EF(p∧r)Ms|=AGrM,s0|=AFrM,s0|=E[(p∧q)Ur]M,s2|=AGrM,s1|=EGr,0|[(pq)]M,s0|=A[pUr]M,s1|=E[(p∧q)Ur]M,s1|=EG[q∨r]2011年3月14日星期一29本节内容„CTL语法„CTL语义CTL语义„CTL等价关系„CTL最小联结词集合„CTL属性范例„CTL属性范例2011年3月14日星期一30CTL公式的等价关系„给定CTL公式f和g，如果对于任意模型M中的任意状态s，M,s|=f当且仅当M,s|=g成立，则称f和g是语义等价的，简称f等价g，并记为fg并记为f≡g。„根据德·摩尔根定律‰¬AFf≡EG¬f‰¬EFf≡AG¬fXfEXf‰¬AXf≡EX¬f„根据AU和EU的定义，‰AFf≡A[trueUf]EFf≡E[trueUf]‰AGf≡¬E[trueU¬f]EGf≡¬A[trueU¬f]2011年3月14日星期一31CTL公式的其它重要等价关系„AGf≡f∧AXAGfGffXGf„EGf≡f∧EXEGf„AFf≡f∨AXAFf3.29stophere„AFf≡f∨AXAFf„EFf≡f∨EXEFfA[fUg]g∨(f∧AXA[fUg])„A[fUg]≡g∨(f∧AXA[fUg])„E[fUg]≡g∨(f∧EXE[fUg])