《时态逻辑》PPT课件.ppt

《《时态逻辑》PPT课件.ppt》由会员分享，可在线阅读，更多相关《《时态逻辑》PPT课件.ppt（52页珍藏版）》请在三一办公上搜索。

1、1,Chapter 6 时态逻辑,（一）模态逻辑（1）基本概念（2）Kripke结构（3）模态逻辑的类型（二）线性时态逻辑（1）命题线性时态逻辑（2）一阶线性时态逻辑（三）计算树逻辑（1）CTL（2）CTL*（四）模型检验（1）标记算法（2）资源共享协议问题,2,（一）模态逻辑,自然语言中有一类用于表示事物的“势态”，人的“情态”，以及过程的“变迁”（历史或未来）的词，称之为模态词。例如，“必然、可能”，“应该、允许”，“知道、认可”，“一贯、偶然”等。模态词和命题连接可以生成新的命题。例如，“火星上可能有生命”就是“可能”与“火星上有生命”所组成的复合命题。早期，由于模态词的语义不清楚，认为

2、模态词不是逻辑概念，只把它们看作文学修辞，主张“必然A”与“A”相同，“不可能A”与“A”相同。,3,（一）模态逻辑,如果说这种做法在数学中勉强行得通，那么在日常推理中就寸步难行，因为“A真但是未必A必然为真”之类的说法，几乎是常识。例如，“张三是年级第1名”未必有“张三必然是年级第1名”。模态逻辑起源于亚里斯多德（Aristole）将“必然、可能”这一对模态词看作逻辑概念，并详细讨论了它们的逻辑性质。,4,（一）模态逻辑,（1）基本概念模态词:模态（modal）词，也称为模态算子，是构成模态逻辑中复合命题的基本运算。常用基本模态词包括：必然（）和可能（）。模态逻辑:模态逻辑是经典命题逻辑和一

3、阶谓词逻辑的扩展形式。基于命题逻辑的扩展称为模态命题逻辑，基于一阶谓词逻辑的扩展称为模态一阶逻辑。模态逻辑通过引入“可能”和“必然”两个模态词，从而能够对可能世界中的命题进行描述和演算。,5,例如，对于命题 P：火星上有生命，那么，P表示火星上必然有生命；P表示火星上可能有生命。模态逻辑中的模态词必然（）和可能（）存在如下关系：P=P（PP）P=P（PP）,6,（1）基本概念,模态命题逻辑公式:简称为MPL（Modal Propositional Logic）公式，定义如下：原子命题（命题常元或命题变元）是MPL公式；如果A、B是MPL公式，那么(A)、(AB)、(AB)、(AB)、(AB)是

4、MPL公式；如果A是MPL公式，那么(A)和(A)是MPL公式；当且仅当有限次地使用所组成的符号串是MPL公式。MPL公式的巴科斯范式（BNF:Backus normal form）表示为：（p是原子命题公式）:=p|()|()|()|()|()|()|(),一些反映模态词性质的MPL公式：AA 必然A真则A真；AA A真则可能A真；AA 必然A真则可能A真；AA 必然A当且仅当不可能A；AA 可能A当且仅当并非必然A；AA 可能A或者可能A；(A A)不会既有必然A，又有必然A；(AA)必然有A成立或者A成立；(AA)不可能A与A同时成立；(AB)AB 必然有A并且B等价于必然A并且必然B；

5、AB(AB)如果必然A和必然B有一为真，那么必然有A真或B真；(AB)AB 可能A或者B当且仅当可能A或者可能B；(AB)AB 如果可能有A并且B那么可能A并且可能B.,8,项:项的定义如下：变量x是项；常量c是项；如果t1,t2,tn是项，f是n元函词，那么f(t1,t2,tn)是项；当且仅当有限次地使用所组成的符号串是项。项的BNF表示为：t:=x|c|f(t,t,t)原子谓词公式:对于n元谓词P，项t1,t2,tn，称P(t1,t2,tn)为原子谓词公式。（0元原子谓词公式是原子命题公式）,模态一阶逻辑公式:模态一阶谓词逻辑公式，简称为MFOL（Modal first order log

6、ic）公式，定义如下：原子谓词公式是MFOL公式；对于MFOL公式A、B，(A)、(AB)、(AB)、(AB)、(AB)是MFOL公式；对于MFOL公式A，x是A中的变量（个体变元），则xA、xA是MFOL公式；对于MFOL公式A，(A)、(A)也是MFOL公式；当且仅当有限次地使用所组成的符号串是MFOL公式。,10,（1）基本概念,MFOL公式的BNF表示为：:=p|()|()|()|()|()|(x)|(x)|()|()MFOL公式，除了具有MPL公式的性质外，还具有如下量词相关的性质：xP(xP)xP(xP)(xP)xP xP(xP)在模态逻辑公式中，同样规定了联接词、模态算子的优先级

7、别：（非）、（必然）、（可能）均为一元算子，具有最高的优先级；（与）、（或）的优先级次之；其次是（蕴涵）、（等值）。,11,（2）Kripke结构,Kripke结构:三元组M=(W,R,L)称为Kripke（克里普克）结构（模型），其中W是可能世界的非空集合；R WW是可能世界W上的二元关系；L：W2P(P为原子公式集合)是标记函数，它是对各可能世界的真值指派，即对每个原子公式，指明它在每个可能世界中取真值还是假值。在Kripke结构模型中，对于sW，R(s)=tW|R，称为可能世界s的1步可达可能世界集合。,12,（2）Kripke结构,约定：R0(s)=sR1(s)=R(s)R2(s)=R

8、(R(s)=tW|u R1(s)且 RRk+1(s)=R(Rk(s)=tW|u Rk(s)且 R则称Rk(s)为可能世界s的k（k0）步可达可能世界集合。对于skW且R（1 k n），序列,建立了可能世界s0到sn的n步可达关系，并称之为可能世界s0到sn的一条长度为n的路径，简记为s0s1s2sk-1sk sk+1sn-1sn。,13,Kripke结构的有向图表示,用圆圈表示可能世界、有向弧线表示可能世界之间的关系、标记函数标识在圆圈内（即每一圆圈内标注了该可能世界中成立的原子公式）。例：下图中，可能世界集W=s0,s1,s2、二元关系R=,、标记函数L(s0)=p,q,L(s1)=q,r,

9、L(s2)=r。,s0s1s2s2和s0s1s0s1s2分别为可能世界s0到s2的长度为3和4的路径 s1s2s2s2和s1s0s1s0s1s2分别为可能世界s1到s2的长度为3和5的路径,在模型M的可能世界s中为真的公式，表示为M,s 或s 在模型M的所有可能世界中为真的公式，表示为M 或，并称为满足关系。基于模态逻辑的Kripke结构模型，可以考察模态逻辑公式的解释或语义。对于M=(W,R,L)，p,qP和s,tW有，M,s p 当且仅当 p L(s)M,sp 当且仅当 p L(s)M,s pq 当且仅当 p L(s)或者q L(s)M,s pq 当且仅当 p L(s)且q L(s)M,s

10、 p 当且仅当 t Rk(s)（k0），pL(t)M,s p 当且仅当 t Rk(s)（k0），pL(t),15,（3）模态逻辑的类型,模态逻辑中模态词的各种引伸，产生了多种模态逻辑。例如，把“可能”解释为“将来某个时刻”、把“必然”解释为“将来所有时刻”，就得到时态（temporal）逻辑；把“可能”解释为“信念”或“相信”、把“必然”解释为“知道”，就得到知道逻辑或者信念（belief）逻辑；把“可能”解释为“应该”、把“必然”解释为“必须”，就得到义务（ought）逻辑。在时态逻辑中，Kripke结构模型M=(W,R,L)的可能世界W解释为不同时刻（或状态），可能世界联系R解释为时间（或

11、状态）的先后关系。Kripke结构模型又称为时态结构模型或时序结构模型。基于对时间的不同描述，产生了时态逻辑的多种不同形式：分支或线性；离散或连续。,16,（3）模态逻辑的类型,分支或线性：任一当前时刻仅存在唯一的可能未来时刻，时间的推进是线性的，称之为线性时间；时间具有分支或者树结构性质：任一当前时刻可能分叉为多种可能未来时刻，称之为分支时间。采用了分支（或线性）时间结构的时态逻辑，称为分支（或线性）时态逻辑。线性时态逻辑中提供了用以描述事件沿着单一时间轴演化的模态算子（词）；分支时态逻辑中则需要提供对分支时间特性下多种未来行为描述的量化词。分支时态逻辑可以较好地处理不确定性。,线性时间,分

12、支时间,17,（3）模态逻辑的类型,连续：当某种计算或活动需要描述成随时间连续变化时，需要采用一个稠密时间模型，即，时间对应于实数或实数域上的一个子集；离散:当系统行为出现在一系列特定的时刻，就可以采用一个离散时间模型，即，时间对应于非负整数或非负整数的一个子集。系统的时间特征行为可能会出现在一系列时间区间上，那么就需要使用一些连续时间区间，称之为区间时间模型。由此，时间模型又可分为点时间模型和区间时间模型。常用时态逻辑包括：命题线性时态（时序）逻辑(PLTL：propositional linear temporal logic)、一阶线性时态（时序）逻辑(FOLTL：first order

13、 linear temporal logic)、命题分支时态逻辑或计算树逻辑(CTL：computation tree logic、CTL*)等。,18,（二）线性时态（时序）逻辑,命题线性时态逻辑(PLTL)和一阶线性时态逻辑(FOLTL)是对命题逻辑和一阶逻辑扩展增加一些模态词（或时态算子）的模态逻辑，统称为线性时态（时序）逻辑（LTL：linear temporal logic）。增加的时态算子如下：always算子，A表示A总是为真或者A永远为真；sometimes算子，A表示A最终为真或者A有时为真；next算子，A表示A在下一时刻为真；until算子，AB表示A一直为真直到B为真。

14、,（二）线性时态逻辑,s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 p-q-p-q-p-q-pq-qp-,20,（二）线性时态逻辑,命题线性时态逻辑公式:简称PLTL公式，定义如下：原子命题（命题常元或者命题变元）是PLTL公式；如果A、B是PLTL公式，那么(A)、(AB)、(AB)、(AB)、(A B)是PLTL公式；如果A是PLTL公式，那么(A)、(A)、(A)是PLTL公式；如果A、B是PLTL公式，那么(AB)是PLTL公式；当且仅当有限次地使用所组成的符号串是PLTL公式。命题线性时态逻辑公式的BNF表示为

15、：:=p|()|()|()|()|()|()|()|()|(),21,（二）线性时态逻辑,一阶线性时态逻辑公式:简称FOLTL公式，定义如下：原子谓词公式是FOLTL公式；如果A、B是FOLTL公式，那么(A)、(AB)、(AB)、(AB)、(AB)是FOLTL公式；如果A是FOLTL公式，x是A中出现的变量（个体变元），则xA、xA是FOLTL公式；如果A、B是FOLTL公式，那么(A)、(A)、(A)、(AB)是FOLTL公式；当且仅当有限次地使用所组成的符号串是FOLTL公式。一阶线性时态逻辑公式的BNF表示为：:=p|()|()|()|()|()|(x)|(x)|()|()|()|()

16、PLTL公式和FOLTL公式统称为LTL公式。在LTL公式中，规定了联接词、时态算子的优先级别：（非）、均为一元算子，具有最高的优先级；（与）、（或）的优先级次之；其次是（蕴涵）、（等值）；的优先级最低。,（二）线性时态逻辑,pq s0 s1 s2 s3 s4 s5 s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s0 s1 s2 s3 s4 s5 s6 s7(pq)s0 s1 s2 s3 s4 s5 s6 s7 s8 s9p s0 s1 s2 s3 s4 s5 s6 s7 s8 s0 s1 s2 s3 s4 s5 s6 s7 s8 s9p s0 s1 s2 s3 s4 s5 s6

17、 s7 s8 s0 s1 s2 s3 s4 s5 s6 s7 s8 s9(p p)s0 s1 s2 s3 s4 s5 s6 s7 s0 s1 s2,一些LTL公式及其解释：pq 若当前状态p为真，则最终会出现q为真的状态；(pq)从当前状态开始，使p为真的状态后终将有使q为真的状态；p 从某一状态开始p永远为真；p 对今后任何状态而言，其后都将有状态使p为真；(p p)终将有一状态，在该状态中p为真，并且下一状态中p为假；,（二）线性时态逻辑,(pq)s7 s8 s9 p(p q)s0 s1 s2 s3 s4 s5 s6 s7 s8 s4 s5 s6 s7 s8 s9 s4 s5 s6 s7

18、s8 s9 p(pq)s3 s5 s7 s8 s9 s7pp s0 s1 s2 s3 s4 s5 s6 s7 s8 s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s0 s1 s2 s3 s4 s5 s6 s7 s8 s9pqq s0 s1 s2 s3 s4 s5 s6 s7 s8 s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s0 s1 s2 s3 s4 s5 s6 s7 s8 s9,(pq)对今后状态而言，p真将导致q从此永远真；p(p q)从此p永远真，或者p从此一直真直到使q真的状态出现；p(pq)若有状态使p为真，则将有一状态使q为真，p在此状态前一直为假；

19、pp 如果p从此永远真。那么下一状态中看，p仍然将永远为真；(pq)q 如果有状态使p在此之前一直真，而在其中q为真，那么q有时会为真；,（二）线性时态逻辑,(pp)(pp)s0 s1 s2 s3 s4 s5 s6 s7 s8 s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s0 s1 s2 s3 s4 s5 s6 s7 s8 s9(pq)(q(p(pq)s0 s1 s2 s3 s4 s5 s6 s7 s8 s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s0 s1 s2 s3 s4 s5 s6 s7 s8 s9,(pp)(pp)若在今后状态中p真蕴涵下一状态后p总为真

20、，则p一旦真便永远真；(pq)(q(p(pq)一直p真到q真等同于现在q真或者现在p真且下一时刻起p一直真到q真。,p s0 s1 s2 s3 s4 s5 s6 s7 s8p s0 s1 s2 s3 s4 s5 s6 s7 s8p s0 s1 s2 s3 s4 s5 s6 s7 s8pp s0 s1 s2 s3 s4 s5 s6 s7 s8(pp)s0 s1 s2 s3 s4 s5 s6 s7 s8 pp s0 s1 s2 s3 s4 s5 s6 s7 s8 s0 s1 s2 s3 s4 s5 s6 s7 s8(pp)(pp)(1),p s4 s5 s6 s7 q s7 s8 s9 pq s4

21、 s5 s6 s7 s8 s9(pq)s4 s5 s6 s7 s8 p(pq)s4 s5 s6 s7 q(p(pq)s4 s5 s6 s7 s8 s9 s0 s1 s2 s3 s4 s5 s6 s7 s8 s9(pq)(q(p(pq)(2),寄存器电路（略）,电位状态变化(设P表示p点的电位为高位，P表示p点的电位为低位，算子P表示p点的电位从低位到高位的状态变化，算子P表示p点的电位从高位到低位的状态变化。状态的改变还具有性质：如果p点的电位为高（低）位，则保持该电位直到发生状态改变)P=PP P=PP(P(PP)(P(PP)通路晶体管(当v3门的输入信号激活时，v1门的信号将被传送到v2门

22、。即，如果v2门的电位为低而v1门的电位为高，则v3门的电位变为高位时，v2门的电位将变为高位；如果v2门的电位为高而v1门的电位为低，则v3门的电位变为高位时，v2门的电位将变为低位)(v3(v1v2 v2)(v3(v1v2 v2)反向器(当v1门的电位为高时，下一时刻v2门的电位也将为高；当v1门的电位为低时，下一时刻v2门的电位也将为低)(v1 v2)(v1 v2)时钟(一个周期为4的时钟)=234,动态寄存器电路 T1和T2为通路晶体管，I1和I2为反向器，x是输入信号，l是负载信号，是时钟信号。寄存器的作用是：在时钟信号和负载信号l都是触发的情况下将一个输入数据x存储到单元中，并且保

23、证在没有新的负载信号到来期间数据x不被通路晶体管T2改变。,寄存器电路（略）,晶体管T1：(l)(x z z)(l)(x z z)晶体管T2：(l)(z y y)(l)(z y y)组合反向器(z y)(z y)电位状态变化(z(z z)；(z(z z)(y(y y)；(y(y y)负载信号 l l 2l 3 l输入信号 x x 2x时钟信号 时间点 0 1 2 3 4 5 6 7 8输入信号 x x x 时钟信号 负载信号 l l l l l l l l l l z点电位 z z z z z z y点电位 y y y y y,在时间点3以后y都为真，所以满足y,通路晶体管(v3(v1v2 v

24、2)(v3(v1v2 v2)反向器(v1 v2)(v1 v2)电位状态变化 P=PP P=PP(P(PP)(P(PP)时钟=234,27,队列及其操作,队列是一种常用的抽象数据类型，服从先进先出FIFO(first-in-first-out)规则。在某个时刻一个队列可以为空或非空。队列状态的改变归于两个操作：PUT，插入一个元素到队尾；GET，从队列头部移出一个元素。队列是一个共享数据类型，PUT和GET操作就可能被多个进程同时执行。要求在任何时刻队列上只能发生一个PUT或GET操作。函词cur_queue 队列的当前状态putval和getval PUT操作和GET操作的参数putval n

25、il PUT操作的前置条件putval=nil PUT操作的后置条件getval=nil GET操作的前置条件getval nil GET操作的后置条件通过对原变量添加“”后缀来区分原变量和经过操作之后的变量值,28,队列及其操作,谓词enter(PUT)、enter(GET)相应操作的开始谓词exit(GET)、exit(PUT)相应操作的终止活性PUT操作的活性（用符号“*”表示在队列末尾插入后继元素）PUT操作的活性就是要求其能够终止。元素putval的插入只能在不引起溢出的情况下才能进行。enter(PUT)(length(cur_queue)max)(exit(PUT)(cur_qu

26、eue=cur_queue*putval)；enter(PUT)(length(cur_queue)=max)(exit(PUT)(cur_queue=cur_queue)GET操作的活性 GET操作的活性特征是其只有在从队列取出一个值之后才能终止。即，如果队列为空，则该操作将一直等到某个值被放进队列，然后再取出这个值。enter(GET)empty(cur_queue)(exit(GET)(getval*cur_queue=cur_queue)；enter(GET)empty(cur_queue)(enter(GET)exit(PUT)；empty(cur_queue)enter(PUT),

27、29,队列及其操作,安全性 设(enter(PUT)putvalnil)在cur_queue下成立，则如果当前队列为满，其下一个状态cur_queue将与cur_queue一样；如果当前队列不为满，将有cur_queue=cur_queue*putval。设(enter(GET)getval=nil)在cur_queue下成立，则如果当前队列为空，其下一个状态cur_queue将与cur_queue一样；如果当前队列不为空，将有cur_queue=getval*cur_queue。(enter(PUT)putvalnil)(length(cur_queue)=max)(cur_queue=cu

28、r_queue)(length(cur_queue)max)(cur_queue=cur_queue*putval)；(enter(GET)getval=nil)(empty(cur_queue)empty(cur_queue)(empty(cur_queue)(cur_queue=getval*cur_queue),30,（三）计算树逻辑,计算树逻辑（CTL：computation tree logic）是一种离散、分支时间、命题时态逻辑。CTL是由Clarke和Emerson于80年代初提出，后经对CTL文法中路径量词及其它时态算子的组合使用规则扩展，建立了CTL*。一般地，CTL和CTL

29、*统称为计算树逻辑。在CTL中，除了具有时态算子always()、sometimes()、next()和until()外，还增加了路径量词：所有未来路径(A)、至少某一路径(E)。计算树逻辑公式：简称为CTL公式，定义如下：原子命题（命题常元或者命题变元）是CTL公式；、是CTL公式，那么()、()、()、()、()是CTL公式；、是CTL公式，那么(A)、(E)、(A()、(E()、(A)、(E)、(A)、(E)是CTL公式；当且仅当有限次地使用所组成的符号串是CTL公式。,31,（三）计算树逻辑,CTL公式的BNF表示为：:=p|()|()|()|()|()|(A)|(E)|(A)|(E)

30、|(A)|(E)|(A()|(E()A(p Eq)；EE(pq)；EE pAq；A(pEq)；AA(p A(p(pA(pq)为CTL公式。p；E(pq)；A(pq)(pt)不是CTL公式（、必须紧接着A或E之后；必须紧接着A或E之后；(pq)、(pt)或(pq)(pt)的前面必须是A或E）,CTL公式的解释或语义：M,s p 当且仅当 p L(s)；M,sp 当且仅当 p L(s)；M,s Ap 当且仅当 t R(s)，p L(t)；M,s Ep 当且仅当 t R(s)，p L(t)；M,s Ap 当且仅当所有s0=s的路径s0s1s2s3上均存在si满足p L(si)；M,s Ep 当且仅当

31、存在s0=s的路径s0s1s2s3，该路径上某些si满足p L(si)；M,s Ap 当且仅当所有s0=s的路径s0s1s2s3上的所有si满足p L(si)；M,s Ep当且仅当存在s0=s的路径s0s1s2s3上的所有si满足p L(si)；M,sA(pq)当且仅当所有s0=s的路径s0s1s2s3满足p L(sk)（0 k i）且q L(si)；M,s E(pq)当且仅当存在s0=s的路径s0s1s2s3，满足p L(sk)（0 k i）且q L(si).上述满足关系式中，和是命题逻辑公式的解释，只需要考察当前状态下公式的满足；和的解释，要考察除了当前状态外，还有所有与当前状态有关系的直

32、接后继状态（1步可达状态）；、和，不仅要考察当前状态及其所关联的直接后继状态，而且还要考察与当前状态所关联的间接后继状态。路径量词 A全称路径量词；E存在路径量词状态量词 全称状态量词；存在状态量词,M,s0 pq p和q均位于状态s0；M,s0 r r不在状态s0；M,s0 E(qr)路径s0s1中的结点s1包含q与r；M,s0 A(qr)路径s0s1中的结点s1仅包含r但不包含q；M,s0 E(pr)不存在同时包含p和r的结点；M,s2 Er 路径s2s3中的所有结点均包含r；M,s2 Ar 所有s0=s2路径中的结点均包含r；M,s0 E(pq)r)路径s0s2中结点s2含r而结点s0包

33、含p与q；M,s0 A(pr)结点s0包含p且其所有后继结点包含r.,Kripke结构模型在状态s0下的路径树,34,（三）计算树逻辑,35,（三）计算树逻辑,A,E,（三）计算树逻辑,在计算树逻辑中，时态算子、路径量词可以通过等值公式相互转换。下面给出了一些CTL等值公式：A=EE=AA=EA=A(true)E=E(true)A=AAE=EEA=AAE=EEA()=(AA()E()=(EE()计算树逻辑是命题逻辑的扩展，所以命题逻辑中联结词之间的等值公式同样适用于计算树逻辑。在命题逻辑中，,和,分别构成了完备联结词集，因为完备联结词集之外的其他联结词均可用完备联结词集中的联结词来表示。在计算

34、树逻辑中，A,A,A、A,E,E、E,E,E等分别构成了时态算子和路径量词的完备集。,（三）计算树逻辑,CTL*公式-CTL*公式分为状态公式和路径公式，状态公式定义如下：原子命题是状态公式，如果、是状态公式，那么()、()是状态公式，如果是路径公式，那么(A)、(E)是状态公式，当且仅当有限次地使用所组成的符号串是状态公式；路径公式定义如下：状态公式是路径公式，如果、是路径公式，那么()、()是路径公式，如果、是路径公式，那么()、()、()、()是路径公式，当且仅当有限次地使用所组成的符号串是路径公式。,38,（三）计算树逻辑,CTL*公式中状态公式和路径公式的BNF表示为：:=p|()|

35、()|()|()|()|(A)|(E):=|()|()|()|()|()|()|()|()|()CTL和PLTL都可以看作为CTL*的子类。下面给出一些CTL*公式：AE p CTL公式但不是PLTL公式；Ep 不是CTL公式也不是PLTL公式；p q 不是CTL公式但是PLTL公式。,39,（四）模型检验,系统的计算树逻辑规格可通过模型检查得到验证。模型检验主要是在软件系统的Kripke结构模型下，对以CTL*公式给出的软件性能进行正确性验证。标记算法（labelling algorithm）是模型检验的一个简单算法标记算法：对于给定的计算树逻辑公式，将其写成由A、E、E、nil（假）连接的

36、等值CTL公式；对Kriple结构模型中的子公式满足的状态进行标记，直到得到标记；所有标记为的状态就是得到满足的状态。,40,标记规则,假定是的子公式，满足的子公式的状态都已得到标记，则子公式的状态标记为：=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 对于后

37、继状态之一已标记1的s，用E1标记该状态。A=E E=AA=E E=E(true)A()=(E()A),41,（四）模型检验,下图是右图CTL*公式E(pq)r)的模型检验 E(pq)r)在Kripke结构中的所有状态得到满足，所以公式的正确性得证。,资源共享协议问题,资源共享协议问题需要满足如下性质：安全性(safety)：任意时刻至多有一个进程访问资源；活性(liveness)：进程对资源提出的访问请求，总会被允许；无阻塞性(non-blocking)：进程会不断提出对资源的访问请求；无次序性(no strict sequencing)：进程对资源的访问没有严格的次序。两个进程的资源共享问

38、题：每一个进程具有3种状态：请求（r）访问（w）和闲置（i），并具有状态转移。两个进程交替对资源进行访问。,资源共享协议1的Kriple结构模型,安全性：1=A(w1w2)活性：21=A(r1 Aw1)22=A(r2 Aw2)无阻塞性：31=A(i1 Er1)32=A(i2 Er2)无次序性：41=E(w1 E(w1(w1E(w2 w1)41=E(w2 E(w2(w2E(w1 w2),资源共享协议问题,为了对资源共享协议的性能要求进行模型检验验证，需要对这些CTL公式变换为完备算子集A,E,E,上的等值公式。具体过程如下：1=A(w1w2)=E(w1w2)=E11=E(true11)=12 安

39、全性21=A(r1 Aw1)=A(r1Aw1)=A(r1Aw1)=E(r1Aw1)=E(r1 211)=E 212=E(true212)=213 活性22=A(r2Aw2)=A(r2Aw2)=A(r2Aw2)=E(r2 Aw2)=E(r2 221)=E 222=E(true222)=223 活性31=A(i1Er1)=A(i1Er1)=A(i1Er1)=E(i1 Er1)=E(i1311)=E 312=E(true312)=313 无阻塞性32=A(i2Er2)=A(i2Er2)=A(i2Er2)=E(i2 Er2)=E(i1 321)=E 322=E(true322)=323 无阻塞性41=

40、E(w1 E(w1(w1E(w2 w1)=E(w1 E(w1(w1411)=E(w1 E(w1 412)=E(w1 413)=E414=E(true414)无次序性42=E(w2 E(w2(w2E(w1 w2)=E(w2 E(w2(w2421)=E(w2 E(w2 422)=E(w2 423)=E424=E(true424)无次序性,A=E E=A A=E A=A(true)E=E(true)A()=(E()A),资源共享协议问题,活性21、22的模型检验,1:Aw1,1:Aw1,2:212,2:212,2:212,212=r1Aw1213=E(true212)21=213,222=r2Aw2

41、223=E(true222)22=223,安全性的模型检验?1=A(w1w2),3:213,3:213,3:213,3:213,3:213,3:213,3:213,3:213,1:Aw2,1:Aw2,2:222,2:222,2:222,3:223,3:223,3:223,3:223,3:223,3:223,3:223,3:223,资源共享协议问题,无阻塞性31、32的模型检验,1:Er1,1:Er1,1:Er1,1:Er1,1:Er1,31=E(true(i1Er1)32=E(true(i2Er2),2:31,2:31,2:31,2:31,2:31,2:31,2:31,2:31,1:Er2,1

42、:Er2,1:Er2,1:Er2,1:Er2,2:32,2:32,2:32,2:32,2:32,2:32,2:32,2:32,资源共享协议问题,无次序性41、42的模型检验,1:411,411=E(w2 w1)412=w1411 413=E(w1 412)414=w1413 41=E(true414),421=E(w1 w2)422=w2421 423=E(w2 422)424=w2423 42=E(true424),1:411,1:411,1:411,1:411,1:411,2:412,2:412,2:412,2:412,3:413,3:413,3:413,3:413,3:413,3:413

43、,4:414,4:414,5:41,5:41,5:41,5:41,5:41,5:41,5:41,5:41,1:421,1:421,1:421,1:421,1:421,1:421,2:422,2:422,2:422,2:422,3:423,3:423,3:423,3:423,3:423,3:423,4:424,4:424,5:42,5:42,5:42,5:42,5:42,5:42,5:42,5:42,47,资源共享协议问题,资源共享协议2的Kripke结构模型,安全性的模型检验?1=A(w1w2),资源共享协议问题,活性21的模型检验,1:Aw1,1:Aw1,1:Aw1,1:Aw1,1:Aw1,

44、1:Aw1,212=r1Aw1213=E(true212)21=213,2:21,2:21,2:21,2:21,2:21,2:21,2:21,2:21,2:21,资源共享协议问题,活性22的模型检验,1:Aw2,1:Aw2,1:Aw2,1:Aw2,1:Aw2,1:Aw2,2:22,2:22,2:22,2:22,2:22,2:22,2:22,2:22,2:21,222=r2Aw2223=E(true222)21=213,资源共享协议问题,无阻塞性31、32的模型检验,1:Er1,1:Er1,1:Er1,1:Er1,1:Er1,31=E(true(i1Er1)32=E(true(i2Er2),1:

45、Er2,1:Er2,1:Er2,1:Er2,1:Er2,资源共享协议问题,无次序性41的模型检验,411=E(w2 w1)412=w1411 413=E(w1 412)414=w1413 41=E(true414),1:411,1:411,1:411,1:411,1:411,2:412,2:412,2:412,3:413,3:413,3:413,3:413,4:414,5:41,5:41,5:41,5:41,5:41,5:41,s6,5:41,5:41,5:41,资源共享协议问题,无次序性42的模型检验,1:421,1:421,1:421,1:421,1:421,2:422,2:422,2:422,3:423,3:423,3:423,3:423,4:424,5:42,s6,421=E(w1 w2)422=w2421 423=E(w2 422)424=w2423 42=E(true424),5:42,5:42,5:42,5:42,5:42,5:42,5:42,5:42,