《标号迁移系统》PPT课件

《《标号迁移系统》PPT课件》由会员分享，可在线阅读，更多相关《《标号迁移系统》PPT课件（49页珍藏版）》请在装配图网上搜索。

1、 标 号 迁 移 系 统 http:/ 自 动 售 茶 机s0111 21 取 茶s1s3 s52 s2 2 s4找 钱 /取 钱2退 钱 s6s7 出 茶取 钱 http:/ http:/ 互 斥 协 议 ： 卫 式 迁 移 模 型 初 始 状 态 ： 迁 移 集 合 ： http:/ 互 斥 协 议 ： 示 意 图x=0 |t=0 t0 x=1 ,t=0t1t2y=0 |t=1 t3x=0s0y=1 ,t=1s1s2s3y=0 初 始 状 态s0t0 x=0y=0t=0 http:/ z0 z1 2z3 5z6 7z9 7 z4 6 z2 0 z2 4z4 7 抽 象 状 态 变 化 图

2、:z7 8 z5 5a: 进 程 A的 运 行 b: 进 程 B的 运 行 http:/ z0 z1 2z3 5z6 7z9 7 z4 6 z2 0 z2 4z4 7 抽 象 状 态 变 化 图 :z7 8 z5 5 ba baa: 进 程 A的 运 行 b: 进 程 B的 运 行aa ba b b http:/ 标 号 迁 移 系 统 http:/ 标 号 迁 移 系 统 动 作 信 息 系 统 状 态 状 态 变 化 初 始 状 态 符 号抽 象 状 态三 元 组状 态 集 合 标 号 迁 移 系 统 http:/ 标 号 迁 移 系 统 ： 例 子 标 号 集 合 ： 状 态 集 合 ：

3、 迁 移 关 系 ： 初 始 状 态 集 ： a, b z0 , z1 , z2 , z3 , (z0 ,a,z3 5 ), (z0 ,b,z1 2 ), z0 http:/ Bchi自 动 机 http:/ z0 z1 2z3 5z6 7z9 7 z4 6 z2 0 z2 4z4 7 抽 象 状 态 变 化 图 :z7 8 z5 5 ba baa: 进 程 A的 运 行 b: 进 程 B的 运 行aa ba b b http:/ z0 z1 2z3 5z6 7z9 7 z4 6 z2 0 z2 4z4 7 抽 象 状 态 变 化 图 :z7 8 z5 5 ba baa: 进 程 A的 运 行

4、 b: 进 程 B的 运 行aa ba b b http:/ Bchi自 动 机 动 作 信 息 系 统 状 态 状 态 变 化 初 始 状 态 公 平 性 约 束 符 号抽 象 状 态三 元 组状 态 集 合状 态 集 合 Bchi自 动 机 http:/ Bchi自 动 机 ： 例 子 标 号 集 合 ： 状 态 集 合 ： 迁 移 关 系 ： 初 始 状 态 集 ： 接 受 状 态 集 ： a, b z0 , z1 , z2 , z3 , (z0 ,a,z3 5 ), (z0 ,b,z1 2 ), z0 z1 2 , z2 0 , z4 6 , http:/ Bchi自 动 机 ： 运

5、行 /语 言 z0 z3 5 z6 7 z9 7 z0 z3 5 z4 6 z7 8 a a a a b b 语 言 ： (a|b) 的 子 集 http:/ 扩 展 Bchi自 动 机 http:/ z0 z1 2z3 5z6 7z9 7 z4 6 z2 0 z2 4z4 7 抽 象 状 态 变 化 图 :z7 8 z5 5 ba baa: 进 程 A的 运 行 b: 进 程 B的 运 行aa ba b b http:/ z0 z1 2z3 5z6 7z9 7 z4 6 z2 0 z2 4z4 7 抽 象 状 态 变 化 图 :z7 8 z5 5 ba baa: 进 程 A的 运 行 b:

6、进 程 B的 运 行aa ba b b http:/ 扩 展 Bchi自 动 机 动 作 信 息 系 统 状 态 状 态 变 化 初 始 状 态 多 元 公 平 性 符 号抽 象 状 态三 元 组状 态 集 合状 态 集 合 的 集 合扩 展 Bchi自 动 机 http:/ 扩 展 Bchi自 动 机 ： 例 子 标 号 集 合 ： 状 态 集 合 ： 迁 移 关 系 ： 初 始 状 态 集 ： 接 受 状 态 集 集 合 ： a, b z0 , z1 , z2 , z3 , (z0 ,a,z3 5 ), (z0 ,b,z1 2 ), z0 z1 2 ,z2 0 , z3 5 ,z6 7 ,

7、 http:/ Streett自 动 机 http:/ z0 z1 2z3 5z6 7z9 7 z4 6 z2 0 z2 4z4 7 抽 象 状 态 变 化 图 :z7 8 z5 5 ba baa: 进 程 A的 运 行 b: 进 程 B的 运 行aa ba b b http:/ z0 z1 2z3 5z6 7z9 7 z4 6 z2 0 z2 4z4 7 抽 象 状 态 变 化 图 :z7 8 z5 5 ba baa: 进 程 A的 运 行 b: 进 程 B的 运 行aa ba b b http:/ Streett自 动 机 动 作 信 息 系 统 状 态 状 态 变 化 初 始 状 态 强

8、 公 平 性 符 号抽 象 状 态三 元 组状 态 集 合状 态 集 合 对 的 集 合Streett自 动 机 http:/ Streett自 动 机 ： 例 子 标 号 集 合 ： 状 态 集 合 ： 迁 移 关 系 ： 初 始 状 态 集 ： 状 态 集 合 对的 集 合 ： a, b z0 , z1 , z2 , z3 , (z0 ,a,z3 5 ), (z0 ,b,z1 2 ), z0 (z3 5 ,z6 7 ), (z3 5 ,z4 6 ), (z3 5 ,z1 2 ,z9 7 ,z2 4 ), http:/ 基 于 迁 移 的 扩 展 Bchi自 动 机 http:/ z0 z1

9、 2z3 5z6 7z9 7 z4 6 z2 0 z2 4z4 7 抽 象 状 态 变 化 图 :z7 8 z5 5 ba baa: 进 程 A的 运 行 b: 进 程 B的 运 行aa ba b b http:/ z0 z1 2z3 5z6 7z9 7 z4 6 z2 0 z2 4z4 7 抽 象 状 态 变 化 图 :z7 8 z5 5 ba baa: 进 程 A的 运 行 b: 进 程 B的 运 行aa ba b b http:/ 基 于 迁 移 的 扩 展 Bchi自 动 机 动 作 信 息 系 统 状 态 状 态 变 化 初 始 状 态 多 元 公 平 性 符 号抽 象 状 态三 元

10、 组状 态 集 合迁 移 集 合 的 集 合 http:/ 基 于 迁 移 的 扩 展 Bchi自 动 机 标 号 集 合 ： 状 态 集 合 ： 迁 移 关 系 (T)： 初 始 状 态 集 ： 迁 移 集 合 的 集 合 ： a, b z0 , z1 , z2 , z3 , (z0 ,a,z3 5 ), (z0 ,b,z1 2 ), z0 (x,a,y) | (x,a,y)T , (x,b,y) | (x,b,y)T http:/ 交 错 迁 移 系 统 http:/ z0 z1 2z3 5z6 7z9 7 z4 6 z2 0 z2 44 7 抽 象 状 态 变 化 图 :z7 8 z5

11、5pqrp: a=s0 q: b=t0 r: t=0 s: a=s0 b=t0pqr pqrpqrpqrpqrpqrpqr pqrpq http:/ 迁 移 关 系(z3 5 ,z6 7 )(z3 5 ,z4 6 /z4 7 )(z3 5 ,z6 7 )(z3 5 ,z4 6 ,z4 7 )(z3 5 ,a,z6 7 )(z3 5 ,b,z4 6 ,z4 7 ) http:/ 交 错 迁 移 系 统 动 作 信 息 系 统 状 态 状 态 变 化 初 始 状 态 符 号抽 象 状 态三 元 组 (S,2 S)状 态 集 合交 错 迁 移 系 统 http:/ 交 错 迁 移 系 统 ： 例 子

12、 标 号 集 合 ： 状 态 集 合 ： 迁 移 关 系 ： 初 始 状 态 集 ： a, b z0 , z1 , z2 , z3 , (z0 ,a,z3 5 ), (z3 5 ,b,z4 6 ,z4 7 ), z0 http:/ s0 1s0s1s2 s1 1 s0 2s1 2 p,qppqpq 交 错 迁 移 系 统 ： 例 2 p,qq s2p,q http:/ s0 1s1 1 s0 2s1 2 p,qp交 错 迁 移 系 统 ： 例 2 p,qq s2p,qs0 1s1 1 s0 2s1 2 p,qpq s2p,q http:/ 交 错 迁 移 系 统 ： 例 2s0 1s1 1 s

13、0 2s1 2 p,qpq s2 p,qs0 qq qp,qp,qs0 1s1 1 s0 2s1 2 p,qpq s2p,q http:/ 交 错 迁 移 系 统 ： 例 2(s0 , p, s0 1 ), (s0 , pq,s0 2 ), (s0 1 ,q, s1 1 ,s1 2 ), (s0 2 ,q, s1 1 ,s1 2 ), (s1 1 ,q, s1 1 ,s1 2 ), (s1 1 ,pq,s2 ), (s1 2 ,q, s1 1 ,s1 2 ), (s1 2 ,pq,s2 ), (s2 , pq,s2 ) http:/ 交 错 迁 移 系 统 ： 例 2 标 号 集 合 ： 状

14、态 集 合 ： 迁 移 关 系 ： 初 始 状 态 集 ： p,q,pq, s0 , s0 1 ,s0 2 ,s1 1 ,s1 2 ,s2 (s0 ,p,s0 1 ), (s0 ,pq,s0 2 ), s0 http:/ 火 车 进 站 控 制S0S3 og, reqS2S1trainctr ctrog trainog, grig trctr ctrtrctr tr http:/ 非 确 定 型 自 动 机 /确 定 型 自 动 机 http:/ 非 确 定 型 Buchi自 动 机 L(A) = (+)*S0 S11 , http:/ 确 定 型 Buchi自 动 机 L(B) = L(A)

15、 = (*)S0 S10 http:/ 确 定 型 Buchi自 动 机 的 补L(A) (+)*n1 n1 n2 n1n1 n2n1 n2 n3 无 限 多 个 、 无 限 多 次 经 过 接 受 状 态 http:/ Buchi自 动 机 非 空 判 定start() W = A = B = ; for each initial state s I, if (s is not in A) add s to W; dfs1 (); http:/ Buchi自 动 机 非 空 判 定dfs1 () q = last element from W;add q to A; for each suc

16、cessor state s of q,if (s is not in A) add s to W; dfs1 (); if (accept(q) add q to B; dfs2 (); delete q from W; http:/ Buchi自 动 机 非 空 判 定dfs2 () q = last element from B;for each successor state s of q, if (s is in W) report(“nonempty”); if (s is not in B) add s to B; dfs2 (); http:/ 算 法 正 确 性 和 复 杂 度 算 法 报 告 “nonempty”当 且 仅 当 自 动 机 的 语言 非 空 Buchi自 动 机 语 言 非 空 判 定 算 法 的 复 杂 度 是线 性 的