模型检验理论基础课件.ppt

《模型检验理论基础课件.ppt》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、模型检验理论基础TheoreticalfoundationsofModelChecking王国俊陕西师范大学数学研究所2010年10月1参考书：(1)C.Baier,J-P.Katoen.PrinciplesofModelChecking.London:TheMITPress,2008.(2)E.M.Clarke,Jr.,O.Grumberg,D.A.Peled.ModelChecking.London:TheMITPress,2000.(3)M.Huth,M.ryan.LogicinComputerScience—Modellingan

2、dReasoningaboutSystems(2nd.Ed.).Cambridge:CambridgeUniversityPress,2004.21.什么是模型检验？1.1模型(model):设S是一组原子命题之集.(1)S的一个子集叫做一个模型;或者等价地说(2)一个赋值v:S--->{0,1}叫做一个模型.31.2满足(satisfaction):设AP是一组原子命题,如AP={p,q,r,s,t,u}设=(uq)r,赋值v的值从p到u依次为0,0,1,1,0,0,则v满足，因为v(r)=1.这时我们也说{r,s}满足,或{r

3、,s}是的模型.还有很多模型,如{r,s,t,u},{p,q,r}和{u}等等.41.3动态满足(dynamicsatisfaction)设公式表示“相互垂直的路口的信号灯永远不能同时为红灯”,或“黄灯之后应为红灯”这类很实用的时态逻辑命题时，静态的模型已经不能用来刻画满足的问题了.因为时态逻辑公式的表达能力比经典逻辑公式的表达能力强得多,所以常用它来描述复杂性质,并称之为规范.相应地,就用动态模型(dynamicmodel)来刻画满足的问题了.51.4模型检验(ModelChecking)设是一个规范(specification)

4、,即,一个时态逻辑公式,TS是一个动态模型(称为迁移系统).简单地说,模型检验就是要通过一种算法,自动地验证TS是否满足的过程.更重要的是：当TS不满足时，找出毛病出在哪里.6美国宇航局1998年的DeepSpace-1宇宙飞船就是经过ModelChecking后发射升空的.72.迁移系统2.1定义1迁移系统(TransitionSystem)TSTS是一个6元组(S,Act,,I,AP,L),这里S是状态之集Act是作用之集⊆SActS是一个迁移关系I⊆S是初始状态之集AP是一组原子命题之集L:S2AP是标记函数，即，在每个

5、状态下都有一个赋值（AP的子集）TS叫有限的，若S，Act，AP都是有限的82.2TS的例子（例1）a,bb,ccs0s1s2s3AP={a,b,c}S={s0,s1,s2,s3}.L(s0)={a,b},L(s1)={b,c},L(s2)={c},L(s3)=.I={s0}.Act=图中箭头之集.=O(ac),sk,k=0,1图1192.3相关概念(1)TS中的状态s叫末端（terminalstate),如果没有从s出发的箭头.如,图1中的TS没有末端,但若去掉其中的s3和进、出s3的箭头，那么s2就是一个末端.(2)“(s,

6、,s’)”常写为“ss’”,其中作用常略去不写.称s’为s的后继.s可以有很多后继.如,在图1的TS中,s1和s2都是s0的后继.s的后继之集记为post(s).所以post(s0)={s1,s2}.(3)称=sisi+1si+2…为以si为起点的无限长的路径(path),这里sk+1是sk的后继(k=0,1,…).103.线性时态逻辑(LinearTimeLogic---LTL)3.1定义2LTL的公式定义如下::=a12O1U2这里aAP，AP是一组原子公式之集.如=O(bUc)a就

7、是一个LTL公式,这里a,b,cAP.但图1中的不是LTL公式.113.2可引入的连接词=12=(12)12=12=U=如,a和(aOa)都是LTL公式123.3定义3LTL的语义定义3设=s0s1s2…是某TS中的以s0为起点的路径，则[i]=sisi+1si+2….规定:(1)(2)aiffaL(s0)(3)iff不成立(4)12iff1且2(5)Oiff[1](6)1U2iff存在k0使[k

8、]2且[i]1(i=1,2,…k-1).133.4推论(7)不成立(8)12iff12不成立iff1不成立，或1不成立if