第8讲模型检测案例.ppt

* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * 构造自动机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? * * * * * * * * * * * * * * * * 实例 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, T, L), s0?S和?，计算M, s0 |= ? 若M不满足? ，产生反例 CTL的一个时态连接词集合是充分的，当且仅当它至少包含{AX, EX}中之一，{EG, AF, AU}中之一以及EU 只考虑：{?, ?, ?} 和{AF, EU, EX} CTL的模型检验算法 算法原理 方法1 输入：M, s0 和? 输出：yes或no 方法2 输入：M和? 输出：满足? 的状态集，检查s0是否在该集合 CTL的模型检验算法 标记算法 SAT(? ) 输入： M和? 输出：满足? 的状态集合 步骤 转换 ? //只包含{?, ?, ?} 和{AF, EU, EX} 从?中的原子命题开始直到?，对每个子公式? ，用? 标记使它满足的所有状态 输出有标记? 的所有状态 CTL的模型检验算法 计算? 能标记状态 ?：没有任何状态能带标记? p：若p ?L(s)，则s 带标记p ?1 ? ?2：如果状态s 同时带标记? 1和? 2，则可用? 1 ? ? 2标记s ??1：如果状态s 不带? 1，则可标记?? 1 CTL的模型检验算法 AF? 1、状态s 带?，则可标记AF ? 2、若状态s的所有后继状态带AF ? ，则可用AF ?标记s 。重复该过程，直到标记无变化 ? AF? AF? AF? … AF? AF? AF? … CTL的模型检验算法 EX? 如果状态s有一个后继状态带?，则s 可标记EX? ? … EX? ? … CTL的模型检验算