《标号迁移系统.ppt》由会员分享，可在线阅读，更多相关《标号迁移系统.ppt（49页珍藏版）》请在三一办公上搜索。
1、标号迁移系统,http:/,自动售茶机,s0,1,1,1,2,1,取茶,s1,s3,s5,2,s2,2,s4,找钱/取钱,2,退钱,s6,s7,出茶,取钱,http:/,http:/,互斥协议：卫式迁移模型,初始状态：,迁移集合：,http:/,互斥协议：示意图,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,http:/,z0,z12,z35,z67,z97,z46,z20,z24,z47,抽象状态变化图:,z78,z55,a:进程A的运行 b:进程B的运行,http:/,z
2、0,z12,z35,z67,z97,z46,z20,z24,z47,抽象状态变化图:,z78,z55,b,a,b,a,a:进程A的运行 b:进程B的运行,a,a,b,a,b,b,http:/,标号迁移系统,http:/,标号迁移系统,动作信息系统状态状态变化初始状态,符号抽象状态三元组状态集合,标号迁移系统,http:/,标号迁移系统：例子,标号集合：状态集合：迁移关系：初始状态集：,a,b z0,z1,z2,z3,(z0,a,z35),(z0,b,z12),z0,http:/,Bchi自动机,http:/,z0,z12,z35,z67,z97,z46,z20,z24,z47,抽象状态变化图:
3、,z78,z55,b,a,b,a,a:进程A的运行 b:进程B的运行,a,a,b,a,b,b,http:/,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,http:/,Bchi自动机,动作信息系统状态状态变化初始状态公平性约束,符号抽象状态三元组状态集合状态集合,Bchi自动机,http:/,Bchi自动机：例子,标号集合：状态集合：迁移关系：初始状态集：接受状态集：,a,b z0,z1,z2,z3,(z0,a,z35),(z0,b,z12),z0 z12,z2
4、0,z46,http:/,Bchi自动机：运行/语言,z0 z35 z67 z97 z0 z35 z46 z78,a a a a b b,语言：(a|b)的子集,http:/,扩展Bchi自动机,http:/,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,http:/,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,http:/,扩
5、展Bchi自动机,动作信息系统状态状态变化初始状态多元公平性,符号抽象状态三元组状态集合状态集合的集合,扩展Bchi自动机,http:/,扩展Bchi自动机：例子,标号集合：状态集合：迁移关系：初始状态集：接受状态集集合：,a,b z0,z1,z2,z3,(z0,a,z35),(z0,b,z12),z0 z12,z20,z35,z67,http:/,Streett自动机,http:/,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,http:/,z0,z12,z3
6、5,z67,z97,z46,z20,z24,z47,抽象状态变化图:,z78,z55,b,a,b,a,a:进程A的运行 b:进程B的运行,a,a,b,a,b,b,http:/,Streett自动机,动作信息系统状态状态变化初始状态强公平性,符号抽象状态三元组状态集合状态集合对的集合,Streett自动机,http:/,Streett自动机：例子,标号集合：状态集合：迁移关系：初始状态集：状态集合对的集合：,a,b z0,z1,z2,z3,(z0,a,z35),(z0,b,z12),z0(z35,z67),(z35,z46),(z35,z12,z97,z24),http:/,基于迁移的扩展Bch
7、i自动机,http:/,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,http:/,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,http:/,基于迁移的扩展Bchi自动机,动作信息系统状态状态变化初始状态多元公平性,符号抽象状态三元组状态集合迁移集合的集合,http:/,基于迁移的扩展Bchi自动机,标号集合：状态集合：迁移关系
8、(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,http:/,交错迁移系统,http:/,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,http:/,迁移关系,(z35,z67)(z35,z46/z47),(z35,z67)(z35,z46,z47),(z35,a
9、,z67)(z35,b,z46,z47),http:/,交错迁移系统,动作信息系统状态状态变化初始状态,符号抽象状态三元组(S,2S)状态集合,交错迁移系统,http:/,交错迁移系统：例子,标号集合：状态集合：迁移关系：初始状态集：,a,b z0,z1,z2,z3,(z0,a,z35),(z35,b,z46,z47),z0,http:/,s01,s0,s1,s2,s11,s02,s12,p,q,p,p,q,pq,交错迁移系统：例2,p,q,q,s2,p,q,http:/,s01,s11,s02,s12,p,q,p,交错迁移系统：例2,p,q,q,s2,p,q,s01,s11,s02,s12,
10、p,q,p,q,s2,p,q,http:/,交错迁移系统：例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,http:/,交错迁移系统：例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),http:/,交错迁移系统：例2,标号集合：状态集合：迁移关系：初始状态集：,p,q,pq,s0,s
11、01,s02,s11,s12,s2(s0,p,s01),(s0,pq,s02),s0,http:/,火车进站控制,S0,S3,og,req,S2,S1,train,ctr,ctr,og,train,og,gr,ig,tr,ctr,ctr,tr,ctr,tr,http:/,非确定型自动机/确定型自动机,http:/,非确定型Buchi自动机,L(A)=(+)*,S0,S1,S1,http:/,确定型Buchi自动机,L(B)=L(A)=(*),S0,S1,S0,http:/,确定型Buchi自动机的补,L(A)(+)*,n1 n1 n2,n1n1 n2n1 n2 n3,无限多个、无限多次经过接受
12、状态,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 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;,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自动机语言非空判定算法的复杂度是线性的,
