《标号迁移系统》PPT课件

1、标号迁移系统,自动售茶机,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,初始状态 s0 t0 x=0 y=0 t=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,抽象

2、状态变化图:,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 ,Bchi自动机,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

3、,z12,z35,z67,z97,z46,z20,z24,z47,抽象状态变化图:,z78,z55,b,a,b,a,a: 进程A的运行 b: 进程B的运行,a,a,b,a,b,b,Bchi自动机,动作信息 系统状态 状态变化 初始状态 公平性约束,符号 抽象状态 三元组 状态集合 状态集合,Bchi自动机,Bchi自动机：例子,标号集合： 状态集合： 迁移关系： 初始状态集： 接受状态集：, a, b z0, z1, z2, z3, (z0,a,z35), (z0,b,z12), z0 z12, z20, z46, ,Bchi自动机：运行/语言,z0 z35 z67 z97 z0 z35 z4

4、6 z78 ,a a a a b b ,语言：(a|b)的子集,扩展Bchi自动机,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,扩展Bchi自动机,动作信息 系统状态 状态变化 初始状态 多元公平性,符号 抽象状态 三元组 状态集合 状态集合的集合,扩展Bchi自动机,扩展B

5、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

6、,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), ,基于迁移的扩展Bchi自动机,z0,z12,z35,z67,z97,z46,z20,z24,z47,抽象状态变化图:,z78,z55,b,a,b,a,a: 进

7、程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,基于迁移的扩展Bchi自动机,动作信息 系统状态 状态变化 初始状态 多元公平性,符号 抽象状态 三元组 状态集合 迁移集合的集合,基于迁移的扩展Bchi自动机,标号集合： 状态集合： 迁移关系(T)： 初始状态集： 迁移集合的集合：, a, b z0, z1, z2, z3, (z0,a,z35), (z0,b,z12), z0 (x,a,y) | (x,

8、a,y)T , (x,b,y) | (x,b,y)T ,交错迁移系统,z0,z12,z35,z67,z97,z46,z20,z24,z47,抽象状态变化图:,z78,z55,pqr,p: a=s0 q: b=t0 r: t=0 s: a=s0b=t0,pqr,pqr,pqr,pqr,pqr,pqr,pqr,pqr,pq,迁移关系,(z35,z67) (z35,z46/z47),(z35,z67) (z35,z46,z47),(z35,a,z67) (z35,b,z46,z47),交错迁移系统,动作信息 系统状态 状态变化 初始状态,符号 抽象状态 三元组(S,2S) 状态集合,交错迁移系统,交

9、错迁移系统：例子,标号集合： 状态集合： 迁移关系： 初始状态集：, 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,pq,交错迁移系统：例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,

10、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,

11、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 = ; for each initial state s I, if (s is not in A) add s to W; dfs1(); ,Buchi自动机非空判定,dfs1() q = last element from W; add q to A; for each successor 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; ,Buchi自动机非空判定,dfs2() q = last ele