《标号迁移系统》PPT课件.ppt

标号迁移系统 自动售茶机 s0 1 1 1 2 1 取茶 s1 s3 s5 2 s2 2 s4 找钱 取钱 2 退钱 s6 s7 出茶 取钱 互斥协议 卫式迁移模型 初始状态 迁移集合 互斥协议 示意图 x 0 t 0 t0 x 1 t 0 t1 t2 y 0 t 1 t3 x 0 s0 y 1 t 1 s1 s2 s3 y 0 初始状态s0t0 x 0y 0t 0 z0 z12 z35 z67 z97 z46 z20 z24 z47 抽象状态变化图 z78 z55 a 进程A的运行b 进程B的运行 z0 z12 z35 z67 z97 z46 z20 z24 z47 抽象状态变化图 z78 z55 b a b a a 进程A的运行b 进程B的运行 a a b a b b 标号迁移系统 标号迁移系统 动作信息系统状态状态变化初始状态 符号抽象状态三元组状态集合 标号迁移系统 标号迁移系统 例子 标号集合 状态集合 迁移关系 初始状态集 a b z0 z1 z2 z3 z0 a z35 z0 b z12 z0 B chi自动机 z0 z12 z35 z67 z97 z46 z20 z24 z47 抽象状态变化图 z78 z55 b a b a a 进程A的运行b 进程B的运行 a a b a b b z0 z12 z35 z67 z97 z46 z20 z24 z47 抽象状态变化图 z78 z55 b a b a a 进程A的运行b 进程B的运行 a a b a b b B chi自动机 动作信息系统状态状态变化初始状态公平性约束 符号抽象状态三元组状态集合状态集合 B chi自动机 B chi自动机 例子 标号集合 状态集合 迁移关系 初始状态集 接受状态集 a b z0 z1 z2 z3 z0 a z35 z0 b z12 z0 z12 z20 z46 B chi自动机 运行 语言 z0z35z67z97 z0z35z46z78 aaa abb 语言 a b 的子集 扩展B chi自动机 z0 z12 z35 z67 z97 z46 z20 z24 z47 抽象状态变化图 z78 z55 b a b a a 进程A的运行b 进程B的运行 a a b a b b z0 z12 z35 z67 z97 z46 z20 z24 z47 抽象状态变化图 z78 z55 b a b a a 进程A的运行b 进程B的运行 a a b a b b 扩展B chi自动机 动作信息系统状态状态变化初始状态多元公平性 符号抽象状态三元组状态集合状态集合的集合 扩展B chi自动机 扩展B chi自动机 例子 标号集合 状态集合 迁移关系 初始状态集 接受状态集集合 a b z0 z1 z2 z3 z0 a z35 z0 b z12 z0 z12 z20 z35 z67 Streett自动机 z0 z12 z35 z67 z97 z46 z20 z24 z47 抽象状态变化图 z78 z55 b a b a a 进程A的运行b 进程B的运行 a a b a b b z0 z12 z35 z67 z97 z46 z20 z24 z47 抽象状态变化图 z78 z55 b a b a a 进程A的运行b 进程B的运行 a a b a b b Streett自动机 动作信息系统状态状态变化初始状态强公平性 符号抽象状态三元组状态集合状态集合对的集合 Streett自动机 Streett自动机 例子 标号集合 状态集合 迁移关系 初始状态集 状态集合对的集合 a b z0 z1 z2 z3 z0 a z35 z0 b z12 z0 z35 z67 z35 z46 z35 z12 z97 z24 基于迁移的扩展B chi自动机 z0 z12 z35 z67 z97 z46 z20 z24 z47 抽象状态变化图 z78 z55 b a b a a 进程A的运行b 进程B的运行 a a b a b b z0 z12 z35 z67 z97 z46 z20 z24 z47 抽象状态变化图 z78 z55 b a b a a 进程A的运行b 进程B的运行 a a b a b b 基于迁移的扩展B chi自动机 动作信息系统状态状态变化初始状态多元公平性 符号抽象状态三元组状态集合迁移集合的集合 基于迁移的扩展B chi自动机 标号集合 状态集合 迁移关系 T 初始状态集 迁移集合的集合 a b z0 z1 z2 z3 z0 a z35 z0 b z12 z0 x a y x a y T x b y x b y T 交错迁移系统 z0 z12 z35 z67 z97 z46 z20 z24 z47 抽象状态变化图 z78 z55 p q r p a s0q b t0r t 0s a s0 b t0 p q r p q r p q r p q r p q r p q r p q r p q r p q 迁移关系 z35 z67 z35 z46 z47 z35 z67 z35 z46 z47 z35 a z67 z35 b z46 z47 交错迁移系统 动作信息系统状态状态变化初始状态 符号抽象状态三元组 S 2S 状态集合 交错迁移系统 交错迁移系统 例子 标号集合 状态集合 迁移关系 初始状态集 a b z0 z1 z2 z3 z0 a z35 z35 b z46 z47 z0 s01 s0 s1 s2 s11 s02 s12 p q p p q p q 交错迁移系统 例2 p q q s2 p q s01 s11 s02 s12 p q p 交错迁移系统 例2 p q q s2 p q s01 s11 s02 s12 p q p q s2 p q 交错迁移系统 例2 s01 s11 s02 s12 p q p q s2 p q s0 q q q p q p q s01 s11 s02 s12 p q p q s2 p q 交错迁移系统 例2 s0 p s01 s0 pq s02 s01 q s11 s12 s02 q s11 s12 s11 q s11 s12 s11 pq s2 s12 q s11 s12 s12 pq s2 s2 pq s2 交错迁移系统 例2 标号集合 状态集合 迁移关系 初始状态集 p q pq s0 s01 s02 s11 s12 s2 s0 p s01 s0 pq s02 s0 火车进站控制 S0 S3 og req S2 S1 train ctr ctr og train og gr ig tr ctr ctr tr ctr tr 非确定型自动机 确定型自动机 非确定型Buchi自动机 L A S0 S1 S1 确定型Buchi自动机 L B L A S0 S1 S0 确定型Buchi自动机的补 L A n1 n1 n2 n1 n1 n2 n1 n2 n3 无限多个 无限多次经过接受状态 Buchi自动机非空判定 start W A B foreachinitialstates I if sisnotinA addstoW dfs1 Buchi自动机非空判定 dfs1 q lastelementfromW addqtoA foreachsuccessorstatesofq if sisnotinA addstoW dfs1 if accept q addqtoB dfs2 deleteqfromW Buchi自动机非空判定