模型检测方法

1、模型检测方法中国科学院软件研究所张文辉/zwh/pv(ab)(bc)(ad)2BDDabcdd0000cdd0100bcdd1111cdd1100(ab)(bc)(ad)3BDDabcdd0cddbcdd1cdd(ab)(bc)(ad)4BDDabcdd0cddbcdd1cdd(ab)(bc)(ad)5BDDabcd0cdbcdd1cd(ab)(bc)(ad)6BDDabcd0cdbcdd1cd(ab)(bc)(ad)7BDDabcd0cdbc1cd(ab)(bc)(ad)8BDDabcd0cdbc1cd(ab)(bc)(ad)9BDDabccdbcc01(ab)(bc)(ad)10BDDab

2、ccdbcc01(ab)(bc)(ad)11BDDabcdbc01(ab)(bc)(ad)12BDDabcdd0000cdd0100bcdd1111cdd1100(ab)(bc)(ad)13BDDabcdd0000cdd0100bcdd1111cdd1100(ab)(bc)(ad)14BDDab0cd001b1c10(ab)(bc)(ad)15BDDabcd01bc限界模型检测与验证从模型的局部考察一个性质是否满足对一些不满足的性质可能很快知道问题对一些满足的性质也可能很快知道结论限界模型检测与验证限界模型检测与验证限界模型检测与验证M,s |= ，限界模型 M0, M1, .问题：是否存在k

3、 ，Mk,s |=m ?存在k, Mk,s |=m , 则 M,s |= = 系统满足性质可靠性K 较小时，较快验证系统性质限界模型检测与验证M,s |= ，限界模型 M0, M1, .问题：是否存在k ，Mk,s |=m ?存在k, Mk,s |=m , 则 M,s |= 则 M,s |= = 系统存在问题可靠性K 较小时，较快查出系统问题自动售茶机s0s1s3s5s2s4p0,q0p4,q1p3,q2p2,q0p1,q0p2,q0E(q0 U q2) vs A(q0 R q2)P0:s0 P1:s0 s1; s0 s2; P2:s0 s1 s3; s0 s1 s5; s0 s2 s4; s

4、0 s2 s5; 我们有M2, s0 s1 s5 |= (q0 U q2)因此 M2 满足 E(q0 U q2)M 满足 E(q0 U q2)M0 |= E(q0 U q2), M1 |= E(q0 U q2)M2=(S,P2,s0,L)是最小可确定E(q0 U q2)是否满足的限界模型AG(q0q2) vs EF(q0q2)我们有M2, s0 s2 s4 |= F(q0q2)因此 M2 满足 EF(q0q2)M 不满足 AG(q0q2) M0 |=EF(q0q2), M1 |=EF(q0q2)M2=(S,P2,s0,L)是最小可确定AG(q0q2)是否满足的限界模型P0:s0 P1:s0 s1; s0 s2; P2:s0 s1 s3; s0 s1 s5; s0 s2 s4; s0 s2 s5; 限界模型P4:s0 s1 s3 s4 s5;s0 s1 s3 s5 s0; s0 s1 s5 s0 s1;s0 s1 s5 s0 s2; s0 s2 s4 s5 s0; s0 s2 s5 s0 s1;s0 s2 s5 s0 s2; P3:s0 s1 s3 s4;s0 s1 s3 s5; s0 s1 s5 s0; s0 s2 s4 s5; s0