计算树逻辑 主讲：王超.ppt

,6.3,计算树逻辑,模型检验,目录/contents,6.4,主讲：王超,6.3计算树逻辑,计算树逻辑（CTL：computationtreelogic）是一种离散、分支时间、命题时态逻辑。CTL是由Clarke和Emerson于80年代初提出，后经对CTL文法中路径量词及其它时态算子的组合使用规则扩展，建立了CTL*。一般地，CTL和CTL*统称为计算树逻辑。在CTL中，除了具有时态算子always()、sometimes()、next()和until()外，还增加了路径量词：所有未来路径(A)、至少某一路径(E)。,02,03,04,01,原子命题（命题常元或者命题变元）是CTL公式；,如果、是CTL公式，那么()、()、()、()、()是CTL公式；,如果、是CTL公式，那么(A)、(E)、(A()、(E()、(A)、(E)、(A)、(E)是CTL公式；,当且仅当有限次地使用所组成的符号串是CTL公式。A(pEq)；EE(pq)；EEpAq；A(pEq)；AA(pA(p(pA(pq)为CTL公式。然而，下列几个不是CTL公式：p；E(pq)；A(pq)(pt)（、必须紧接着A或E之后；必须紧接着A或E之后；(pq)、(pt)或(pq)(pt)的前面必须是A或E）,计算树逻辑公式：简称为CTL公式，定义如下：,CTL公式的满足关系,M,sp当且仅当pL(s)；M,sp当且仅当pL(s)；M,sAp当且仅当tR(s)，pL(t)；M,sEp当且仅当tR(s)，pL(t)；M,sAp当且仅当所有s0=s的路径s0s1s2s3上均存在si满足pL(si)；M,sEp当且仅当存在s0=s的路径s0s1s2s3，该路径上某些si满足pL(si)；M,sAp当且仅当所有s0=s的路径s0s1s2s3上的所有si满足pL(si)；M,sEp当且仅当存在s0=s的路径s0s1s2s3上的所有si满足pL(si)；M,sA(pq)当且仅当所有s0=s的路径s0s1s2s3满足pL(sk)（0ki）且qL(si)；M,sE(pq)当且仅当存在s0=s的路径s0s1s2s3，满足pL(sk)（0ki）且qL(si).,上述满足关系式中，和是命题逻辑公式的解释，只需要考察当前状态下公式的满足；和的解释，要考察除了当前状态外，还有所有与当前状态有关系的直接后继状态（1步可达状态）；、和，不仅要考察当前状态及其所关联的直接后继状态，而且还要考察与当前状态所关联的间接后继状态。路径量词A全称路径量词；E存在路径量词状态量词全称状态量词；存在状态量词,对于与间接后继续状态相关的CTL公式，可以将模型的有向图展开，得到给定状态下相关路径的树结构描述。图1所示是Kripke结构在状态S0下的树径树。,Kripke结构模型在状态s0下的路径树,M,s0pqp和q均位于状态s0；M,s0rr不在状态s0；M,s0E(qr)路径s0s1中的结点s1包含q与r；M,s0A(qr)路径s0s1中的结点s1仅包含r但不包含q；M,s0E(pr)不存在同时包含p和r的结点；M,s2Er路径s2s3中的所有结点均包含r；M,s2Ar所有s0=s2路径中的结点均包含r；M,s0E(pq)r)路径s0s2中结点s2含r而结点s0包含p与q；M,s0A(pr)结点s0包含p且其所有后继结点包含r.,A,E,状态公式：,路径公式：,原子命题是状态公式如果、是状态公式，那么()、()是状态公式如果是路径公式，那么(A)、(E)是状态公式当且仅当有限次地使用所组成的符号串是状态公式；,CTL*公式-CTL*公式分为状态公式和路径公式,状态公式是路径公式如果、是路径公式，那么()、()是路径公式如果、是路径公式，那么()、()、()、()是路径公式当且仅当有限次地使用所组成的符号串是路径公式。,从上述定义不难看出，不包含路径量词A和E的CTL*公式就是PLTL公式。因此，CTL和PLTL都可以看作为CTL*的子类。,下面给出一些CTL*公式：AEpCTL公式但不是PLTL公式；Ep不是CTL公式也不是PLTL公式；pq不是CTL公式但是PLTL公式。A（pAq）是CTL公式也是PLTL公式,6.4模型检验,系统的计算树逻辑规格可通过模型检查得到验证。模型检验主要是在软件系统的Kripke结构模型下，对以CTL*公式给出的软件性能进行正确性验证。标记算法（labellingalgorithm）是模型检验的一个简单算法标记算法：对于给定的计算树逻辑公式，将其写成由A、E、E、nil（假）连接的等值CTL公式；对Kriple结构模型中的子公式满足的状态进行标记，直到得到标记；所有标记为的状态就是得到满足的状态。,假定是的子公式，满足的子公式的状态都已得到标记，则子公式的状态标记为：=nil无标记状态；=p如果pL(s)，用p标记状态s；=12如果s已标记1和2，那么用12标记该状态；=1如果s没有标记1，那么用1标记该状态；=A1对于已标记1的s，用A1标记该状态；对于所有后继状态已标记A1的s，用A1标记该状态；=E(12)对于已标记2的s，用E(12)标记该状态；对于已标记1，且至少一个后继状态已标记E(12)的s，用E(12)标记该状态；=E1对于后继状态之一已标记