显式状态迁移模型内容摘要：
达状态 可达状态 17个 : 18 Kripke模型：安全性质 系统的互斥性质表示为安全性质 19 Kripke模型：响应性质 系统具备的部分性质包括响应性质 (不满足 ) 20 标号 Kripke模型 21 s0,t0,0,0,0 s0,t1,1,0,0 s1,t0,0,1,1 s2,t0,0,1,1 s3,t0,0,0,1 s1,t1,1,1,0 s0,t2,1,0,0 s0,t3,0,0,0 s1,t1,1,1,1 • 状态变化图 : s2,t1,1,1,0 s1,t2,1,1,1 22 z0 z12 z35 z67 z97 z46 z20 z24 z47 • 抽象状态变化图 : z78 z55 a=s0: { z0,z12,…} b=t0: { z0,z35,…} 23 z0 z12 z35 z67 z97 z46 z20 z24 z47 • 抽象状态变化图 : z78 z55 p,q,r p: a=s0 q: b=t0 r: t=0 s: a=s0b=t0 p p p,r q q q r r 24 标号 Kripke模型 • 系统状态 • 状态变化 • 初始状态 • 状态信息 抽象状态 二元组 状态 集合 命题 标号 Kripke模型 25 标号 Kripke模型：例子 • 状态集合： • 迁移关系： • 初始状态集： • 标号函数： { z0, z1, z2, z3, … } { (z0,z35), (z0,z12), … } { z0 } L: L(z0)={p,q,r},L(z12)={p},… 命题集合 { p, q, r } 的子集 26 标号 Kripke模型：命题 定义命题 : 27 标号 Kripke模型：标号函数 可达状态的标号。阅读剩余 0%
本站所有文章资讯、展示的图片素材等内容均为注册用户上传(部分报媒/平媒内容转载自网络合作媒体)，仅供学习参考。
用户通过本站上传、发布的任何内容的知识产权归属用户或原始著作权人所有。如有侵犯您的版权，请联系我们反馈本站将在三个工作日内改正。