第8讲模型检测.ppt

* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * 构造自动机A?? 若?(?1U ?2)在s 中，那么??2在s 中 因为：?(?1U ?2) = ??2 ?(??1 ? …) s2 ?ab? s1 ?a ?b ?? s4 ab? a ?b ? s3 a ?b ?? s?3 ? =a U b 构造自动机A?? 初始状态是包含?? (即a U b )的状态 s2 ?ab? s1 ?a ?b ?? s4 ab? a ?b ? s3 a ?b ?? s?3 ? =a U b 构造自动机A?? 构造状态迁移关系 s2 ?ab? s1 ?a ?b ?? s4 ab? a ?b ? s3 a ?b ?? s?3 ? =a U b 构造自动机A?? ( s, s? )属于状态迁移关系，当且仅当 若X? ?s，则? ?s? 若?X? ?s，则?? ?s? s2 ?ab? s1 ?a ?b ?? s4 ab? a ?b ? s3 a ?b ?? s?3 ? =a U b 构造自动机A?? ( s, s? )属于状态迁移关系，当且仅当 若?1U ?2 ?s且?2?s，则?1U ?2 ?s? s2 ?ab? s1 ?a ?b ?? s4 ab? a ?b ? s3 a ?b ?? s?3 ? =a U b 构造自动机A?? ( s, s? )属于状态迁移关系，当且仅当 若?(?1U ?2) ?s且?1 ?s，则：?(?1U ?2) ?s? s2 ?ab? s1 ?a ?b ?? s4 ab? a ?b ? s3 a ?b ?? s?3 ? =a U b 构造自动机A?? 可接受路径的条件 含?1U ?2的状态必有含?2的状态在后面出现 例：路径不能以s3, s3, …结尾 s2 ?ab? s1 ?a ?b ?? s4 ab? a ?b ? s3 a ?b ?? s?3 ? =a U b * Any question? 人有了知识，就会具备各种分析能力， 明辨是非的能力。 所以我们要勤恳读书，广泛阅读， 古人说“书中自有黄金屋。 ”通过阅读科技书籍，我们能丰富知识， 培养逻辑思维能力； 通过阅读文学作品，我们能提高文学鉴赏水平， 培养文学情趣； 通过阅读报刊，我们能增长见识，扩大自己的知识面。 有许多书籍还能培养我们的道德情操， 给我们巨大的精神力量， 鼓舞我们前进。 * * * * * * * * * * * * * * CTL的形式语义 M,s |= AF? iff ?s1, s2, … ? Path(M), s =s1, ? i ? 1?M,si |= ? M,s |= EF? iff ? s1, s2, … ? Path(M), s =s1, ? i ? 1?M,si |= ? M,s |= A[?1 U ?2] iff ?s1, s2, … ? Path(M), s =s1, ? i ? 1?M,si |= ?2 ? ?j i ? M,sj |= ?1 M,s |= E[?1 U ?2] iff ? s1, s2, … ? Path(M), s =s1, ? i ? 1?M,si |= ?2 ? ?j i ? M,sj |= ?1 * 实例 1) 不可能到达一个状态：started成立ready 不成立 2) 可能到达一个状态：started成立ready 不成立 3) 如果一个请求发生，它最终会被确认 4) 乘客要到5楼，2楼的向上电梯不会改变运行方向 CTL LTL 1) AG ?(started ? ? ready) G ?(started ? ? ready) 2) EF (started ? ?ready) 3) AG (requested → AF acknowledged) G (requested → F acknowledged) 4) AG(f2 ? up ? p5 → A(up U f5)) G(f2 ? up ? p5 → (up U f5)) LTL与CTL的比较 直观比较 CTL较强 LTL不能表达：任何状态可以到达 restart 状态 CTL表达：AG EF restart LTL较强 LTL可以描述在所有路径上选择一个范围 F p ? F q：每条有p的路径，也有q AF p ? AF q和AG( p ? AF q )含义都与之不同 CTL的模型检验算法 给定M = (S,