【大学课件】时间迁移系统.ppt
时间迁移系统,http:/,自动售茶机,s0,1,1,1,2,1,取茶,s1,s3,s5,2,s2,2,s4,找钱/取钱,2,退钱,s6,s7,出茶,取钱,x,x10,x=10,量的变化,http:/,http:/,时间迁移系统,x=0|t=0,http:/,系统运行过程描述：例子,t0,x=1,t=0,t1,t2,y=0|t=1,t3,x=0,s0,y=1,t=1,s1,s2,s3,y=0,无约束,1,5,无约束,无约束,2,8,无约束,http:/,z0,z12,z35,z67,z97,z46,z20,z24,z47,抽象状态变化图:,z78,z55,b,u,true,b,u,u1,b,u5,a,v,true,a,v,true,b,u,u1,http:/,时间变化,5.05.15.75.910.4 ba abbz0 z12z12z12z20z24u=5.0,u=0.1 u=0.7 u=0.9u=4.5u=0.0,u=0.1 u=0.7 u=0.0 u=4.5v=5.0 v=5.1v=0.6v=0.2v=4.7v=5.0 v=0.0v=0.0v=0.2v=4.7,http:/,时间迁移系统,动作信息系统状态时钟变量状态变化初始状态,符号抽象状态变量集合五元组状态集合,时间迁移系统,http:/,时间迁移系统：例子,标号集合：状态集合：时钟变量集合：迁移关系：初始状态集：,a,b z0,z1,z2,z3,u,v(z0,a,v,true,z12),z0,时钟变量相关公式,http:/,时间迁移系统：例子,S0,S1,a,S2,S3,d,y2,x:=0,b,y:=0,c,x1,http:/,时间迁移系统：例子,http:/,时间迁移系统：运行,http:/,时间Buchi自动机1,S1,S0,b,S2,S3,S2,a,a,x:=0,a,x:=0,b,x2,http:/,时间Buchi自动机1,http:/,时间Buchi自动机1：运行/语言,http:/,时间Buchi自动机2,S0,S1,S2,S3,S2,a,y:=0,a,x:=0,x=1,b,y:=0,y1,a,x:=0,x=1,http:/,时间Buchi自动机2,http:/,时间Buchi自动机2：运行/语言,混成迁移系统/混成自动机,http:/,混成迁移系统/混成自动机,水箱,x=2,x=5x:=x+1,x=1x=9,x=-1,on,off,http:/,混成迁移系统/混成自动机,水箱,x=1,x=-1,on,off,on2off,x:=x+1,x=5,off2on,x=2,x=9,http:/,http:/,混成迁移系统/混成自动机,动作信息系统状态变量状态状态变化初始状态,符号抽象状态变量集合五元组混合状态集合,混成自动机,混成自动机,http:/,混成自动机,http:/,http:/,Petri网,x=0|t=0,http:/,系统运行过程描述：例子,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:/,系统资源模型,s0s1s2s3,t0t1t2t3,http:/,系统资源模型,t0t1t2t3,s0s1s2s3,http:/,系统资源模型,t0t1t2t3,s0s1s2s3,http:/,系统资源模型,t0t1t2t3,s0s1s2s3,http:/,Petri网,位置迁移状态变化描述初始状态,抽象元素抽象元素边（两种）位置标号,Petri网,http:/,系统资源模型,t0v0t1v1t2v2t3v3,s0u0s1u1s2u2s3u3,ts,http:/,Petri网：例子,位置集合：迁移集合：边的集合：初始状态：,s0,s3,t0,t3,ts u0,u3,v0,v3(s0,u0),(u0,s1),(s1,u1),(ts,u1),M:M(s0)=1,M(s1)=0,M(s2)=0,http:/,有问题的系统资源模型,s0u0s1u1s2u2,t0v0t1v1t2v2,http:/,通信系统,http:/,系统资源模型,t0v0t1v1t2v2t3v3,s0u0s1u1s2u2s3u3,ts,http:/,系统资源模型,ts!1ts?1,ts!1ts?1,ts,http:/,系统资源模型,ts!1ts?1,ts!1ts?1,ts,http:/,系统资源模型,1,ts!1ts?1,ts!1ts?1,ts,http:/,系统资源模型,ts!1ts?1,ts!1ts?1,ts,http:/,通信系统,状态通道状态变化初始状态,抽象状态二元组三元组给定状态,通信系统,http:/,系统资源模型,t0t1ts!1t2ts?1t3,s0s1ts!1s2ts?1s3,ts,http:/,通信单元：例子,状态集合：通道集合：迁移关系：初始状态：,s0,s3 ts:(s0,s1),(s1,ts?1,s2),s0,通信系统：通信单元的组合,http:/,通信系统：例子,q0,q1,q2,q3,q4,q5,!0,?1,?0,!1,?1,?0,!0,!1,http:/,通信系统：例子,q2,q0,q1,q3,q4,q5,?0,!0,?1,!1,?0,?1,!0,!1,http:/,通信系统：例2,rw()=1,2y+x=(y+x)%4,s0,t1,S!B,t0,B+1=b,B+,B+1!=b,R!(A+rw(),s1,S?A,R?b,http:/,通信系统：例2,s0,s1,m1!1,m1!2,m2?1,m2?2,m2?0,s3,s2,m2?2,m2?3,m2?0,m1!2,m1!3,m2?3,m2?0,m2?1,m1!3,m1!0,m2?0,m2?1,m2?2,m2?3,m1!0,m1!1,m2?1,m2?2,m2?3,http:/,通信系统：例2,t0,t1,m2!0,m1?1,m1?2,m1?0,t3,t2,m1?2,m1?3,m1?0,m2!1,m1?3,m1?0,m1?1,m2!2,m1?0,m1?1,m1?2,m1?3,m2!3,m1?1,m1?2,m1?3,http:/,通信系统：例2,rw()=1,2,W,s0,t1,S!B,t0,B+1=b,B+,B+1!=b,R!(A+rw(),s1,S?A,R?b,http:/,通信系统：例2,Window Protocol InvariantB W Ri B+W for 1 i r,http:/,通信系统：例2,Window Protocol InvariantB W Ri B+W for 1 i r,引理1：A S1 Ss B,引理2：设 R0=B,Rr+1=A+1 则 Ri Rj+W for 0 i r,ij r+1,http:/,有限状态变量与自动机,q0,q1,mi?r,mi?0,mi?0,(mi?2),mi?2,mi?r,q2,mi?1,r0,mo!0,r1,mo!1,mi?r,r2,mo!2,m 0,1,2,
