一种模糊互模拟的局部算法_胡晋玮.pdf

第4 3卷 第1期桂 林 电 子 科 技 大 学 学 报V o l.4 3,N o.1 2 0 2 3年2月J o u r n a l o f G u i l i n U n i v e r s i t y o f E l e c t r o n i c T e c h n o l o g yF e b.2 0 2 3收稿日期:2 0 2 1-0 3-0 7基金项目:国家自然科学基金(6 1 5 6 2 0 1 5);广西自然科学基金(2 0 1 8 G X N S F D A 1 3 8 0 0 3)通信作者:钱俊彦(1 9 7 3-),男,教授,博士,研究方向为软件工程、程序验证与测试、容错技术。E-m a i l:q j y 2 0 0 0 g m a i l.c o m引文格式:胡晋玮,钱俊彦.一种模糊互模拟的局部算法J.桂林电子科技大学学报,2 0 2 3,4 3(1):3 5-4 0.一种模糊互模拟的局部算法胡晋玮,钱俊彦(桂林电子科技大学 计算机与信息安全学院,广西 桂林 5 4 1 0 0 4)摘 要:为了快速地对模糊迁移系统中给定状态是否满足互模拟关系进行验证,提出了一种模糊互模拟的局部算法。该算法将验证与遍历相结合,在对状态是否满足模糊互模拟关系验证的同时,动态地增加状态空间,使得算法只需遍历部分状态空间即可完成验证。在部分情况下,尤其是当2个状态不满足模糊互模拟关系时,模糊互模拟的局部算法可以更快地对给定状态是否满足模糊互模拟关系进行验证。通过J a v a实现了模糊互模拟的局部算法和已有全局算法,并进行了比较实验。实验结果表明,在给定状态对不满足互模拟关系的情况下,本算法比现有模糊互模拟的全局算法的效率更高。关键词:互模拟;模糊集;模糊迁移系统;模糊互模拟;局部算法中图分类号:T P 3 0 1 文献标志码:A 文章编号:1 6 7 3-8 0 8 X(2 0 2 3)0 1-0 0 3 5-0 6A l o c a l a l g o r i t h m o f f u z z y b i s i m u l a t i o nHU J i n w e i,Q I A N J u n y a n(S c h o o l o f C o m p u t e r a n d I n f o r m a t i o n S e c u r i t y,G u i l i n U n i v e r s i t y o f E l e c t r o n i c T e c h n o l o g y,G u i l i n 5 4 1 0 0 4,C h i n a)A b s t r a c t:I n o r d e r t o v e r i f y w h e t h e r t h e g i v e n s t a t e s s a t i s f i y t h e b i s i m u l a t i o n,a l o c a l a l g o r i t h m o f f u z z y b i s i m u l a t i o n i s p r o-p o s e d.T h e a l g o r i t h m t a k e s v e r i f i c a t i o n a n d t r a v e r s a l a t t h e s a m e.W h i l e v e r i f y t h e g i v e n s t a t e s w h e t h e r s a t i s f i y t h e f u z z y b i s i m u l a t i o n,t h e s t a t e s p a c e i s d y n a m i c a l l y i n c r e a s e d,s o t h a t t h e a l g o r i t h m o n l y n e e d s t o t r a v e r s e p a r t o f t h e s t a t e s p a c e t o c o m p l e t e t h e v e r i f i c a t i o n.I n s o m e c a s e s,t h e l o c a l a l g o r i t h m o f f u z z y b i s i m u l a t i o n c a n v e r i f y w h e t h e r t h e g i v e n s t a t e s s a t i s f i y t h e f u z z y b i s i m u l a t i o n m o r e q u i c k l y,e s p e c i a l l y w h e n t h e t w o s t a t e s d o n o t s a t i s f y t h e f u z z y b i s i m u l a t i o n.T h e l o c a l a l g o-r i t h m a n d t h e e x i s t i n g g l o b a l a l g o r i t h m a r e i m p l e m e n t e d b y J a v a a n d c o m p a r e d b y e x p e r i m e n t s.T h e e x p e r i m e n t s,s h o w s t h a t t h i s a l g o r i t h m i s m o r e e f f i c i e n t t h a n t h e e x i s t i n g g l o b a l f u z z y b i s i m u l a t i o n a l g o r i t h m w h e n t h e g i v e n s t a t e s d o n o t s a t i s f i y t h e b i s i m u l a t i o n.K e y w o r d s:b i s i m u l a t i o n;f u z z y s e t;f u z z y t r a n s i t i o n s y s t e m s;f u z z y b i s i m u l a t i o n;l o c a l a l g o r i t h m 互模拟作为描述系统之间行为等价的重要概念,是解决状态空间爆炸问题的有效手段1。1 9 8 7年,P a i g e等2在划分精化的思想下,给出了时间复杂度为O(ml o g n)的互模拟等价类划分算法,该算法需要对整个迁移系统的状态空间进行预先存储,属于互模拟等价验证全局算法的一种。然而,在很多情况下,并不需要求得整个迁移系统状态空间的互模拟等价类,只需对迁移系统中的给定状态是否满足互模拟关系进行判断。1 9 8 9年,F e r n a n d e z等3提出了互模拟等价关系判断的局部算法,该算法又称为“o n t h e f l y”算法。“o n t h e f l y”算法通过构建2个迁移系统的同步积,并对要判定状态对的后续状态对进行深度优先或广度优先搜索遍历,同时判断每对状态对是否满足互模拟关系,该算法的时间复杂度为O(n2),其中n为L T S的状态数。D u等4在“o n t h e f l y”算法的基础上提出了介于局部算法与全局算法之间的互模拟等价验证的准局部算法,通过对状态添加状态0或1的方法,避免了对状态的重复访问,降低了算法的时间复杂度。L i n5将局部算法应用于值传递系统中,D e n g等6将局部算法应用于概率迁移系统,并提出了概率迁移系统的局部算法。DOI:10.16725/45-1351/tn.2023.01.001桂林电子科技大学学报2 0 2 3年2月模糊集合是经典集合的扩展,主要用于对事物的不确定性进行描述,可有效地对主观概念和不确定性概念进行分析7。将模糊论的定量分析应用到系统分析中,可很好地分析系统能够在多大程度上满足系统的性质规约,对模糊自动机8-1 0、模糊P e t r i网1 1-1 2及模糊迁移系统1 3-1 6的研究已经取得了很多学术成果。值得注意的是,当用模糊自动机构建系统模型时,所构造出来的模型并非唯一。为了更好地对这些模型是否等价进行判断,计算机科学工作者将互模拟的定义引入模糊迁移系统。P e t k o v i c等1 7通过代数的方法 提 出 了 有 限 模 糊 自 动 机 全 等 概 念。B u-c h o l z1 8和S u n等1 9对有限模糊自动机和有限模糊迁移系统的互模拟进行了研究。C a o等2 0针对无限迁移系统,提出了关于一般模糊迁移系统的模糊互模拟的定义。为了更好地对模糊迁移系统行为相似程度进行刻画,C a o等2 1提出了行为距离的概念,当2个模糊迁移系统完全满足模糊互模拟性质时,其行为距离为0。W u等2 2在算法和逻辑2个角度上对模糊互模拟进行了刻画。为了更好地对模糊迁移系统是否满足模糊互模拟关系进行判断,Ci r i c等2 3给出了有限模糊自动机的模糊互模拟等价验证算法;I g n j a t o v i c2 3提出了对2个模糊社交网络进行模糊互模拟等价验证的算法,该算法的时间复杂度为O(l c5),其中l为在计算过程中出现的不同模糊值的数量,c为社交网络中节点数;W u等2 2提出了一种模糊互模拟等价验证的全局算法,该算法的时间复杂度为O(m2n4),其中n为模糊迁移系统中状态的个数,m为模糊迁移系统中迁移的数量。尽管互模拟在模糊领域已经取得了一定成果,但到目前为止,对模糊互模拟局部算法的研究尚未得到广泛关注。为了更快地对指定状态是否满足模糊互模拟关系进行验证,基于文献5-6 的算法思想,提出了一种模糊互模拟等价关系验证的局部算法,以提高模糊互模拟等价验证的效率,并通过实验的方式与现有的模糊互模拟检验算法进行了比较。1 预备知识设S为非空集合,S上的模糊集合P为S到 0,1 的一个映射,:S0,1,用F(S)表示集合S上的全体模糊集,F(S),则模糊集的支撑集s u p p()定义为s u p p()=sS:(s)0。若s u p p()是有限的,则模糊集可用Z e d e h形式表示为=(s1)s1+(s2)s2+(sn)sn。对于任意的F(S)及US,(U)=s u psU(s)。特别地,()=0。设,为集合S上的2个模糊集合,且,对任意的sS,均有(s)(s)。定义19 模糊迁移系统(f u z z y t r a n s i t i o n s y s-t e m,简称F T S)是一个三元组(S,A,),其中:1)S为状态的集合;2)A为动作的集合;3)SAF(S)为迁移关系。定义22 2 给定集合S,RSS,若存在关于R的权重函数e:ss0,1 满足如下条件:1)对于任意的sS,(s)=s u psSe(s,t);2)对于任意的tS,(t)=s u ptSe(s,t);3)若e(s,t)0,则有(s,t)R。则称RF(S)F(S)为关系R的提升,使得R成立。定理12 2 令S为一个集合,RSS,F(S)。若R成立,则对任意的sS,均有1)(s)(Rs),2)(s)(Rs),其中,Rs=s:s R s ,Rs=s:s R s。定义32 2 若对于任意的RSS,s R t均满足以下条件:1)对于任意的s,均有tv,使得R成立;2)对于任意的tv,均有s,使得 R成立。则称R为互模拟关系。若存在一个模糊互模拟关系R,使得(s,t)R,则称状态s,t满足模糊互模拟等价关系,记为st。2 模糊互模拟验证的局部算法在递归定义的基础上,结合“O n T h e F l y”算法和对提升关系R的判断算法,给出模糊迁移系统的互模拟等价验证的局部算法。在模糊迁移系统中,互模拟可采用递归的方式进行定义。定义42 2 设F T S为一个三元组M=(S,A,),定义如下:1)R0=SS。63第1期胡晋玮等:一种模糊互模拟的局部算法2)对于任意的n0,s Rn+1t,若a)对于任意的s,存在tv,使得Rn成立;b)对于任意的tv,存在s,使得Rn成立。3)=n 0Rn。命题1 在有限F T S中,定义3与定义4所定义的模糊互模拟是相同的。证明 为了方便表示,用d e f 4表示定义4中所定义的模糊互模拟,用d e f 3表示定义3中表示的模糊互模拟,则1)根据d e f 3的定义可知,若sd e f 3t,则有sd e f 4t成立。2)设sd e f 4t,且s,要证d e f 4为模糊互模拟关系,即要证存在tv,使得d e f 4成立。设集合D=:tvd e f 4,即对于任意的T,均有n使得n。设nm a x=m a xn:T,则有nm a x。又因为F T S是有限的,故集合D是有限的。因为sd e f 4t成立,则有snm a x+1t,即存在,tv,使得nm a x且T。故对于任意的s,均存在使得d e f 4成立。同理,可证明若tv,则存在s,使得d e f 4成立。文献2 2 提出了对于给定的集合S,F(S),RSS,判断R的算法。该算法时间复杂度为O(n2)。在此基础上,结合“O n t h e F l y”算法的思想,提出了关于模糊互模拟验证的局部算法。在模糊互模拟局部算法中,用集合E r r o r s存储在算法执行过程中被判定为不具有互模拟性质的状态对;用数组V i s i t e d表示已经被遍历过的状态对。若一对状态已经被多次遍历,但其是否满足模糊互模拟关系尚不能确定时,则先假设其满足互模拟关系,同时用数组L e t B i s对其进行存储,若在后续的遍历过程中发现该状态对不满足互模拟关系,则将该状态对从数组L e t B i s中删除,同时将其添加到数组E r-r o r s中,并重新执行函数c h e c k B i s。为了保证状态遍历和判断的先后顺序,用栈S t a c k存储尚未完成模糊互模拟关系判断的状态对。算法1 模糊互模拟检测的局部算法输入:模糊迁移系统F T S以及状态对(s,t)输出:s,t是否满足模糊互模拟关系1.E r r o r s=2.i s B i s=u n k n o w3.w h i l e i s B i s=u n k n o w4.i s B i s=c h e c k B i s(s,t)5.r e t u r n i s B i sF u n c t i o n c h e c k B i s(s,t)6.V i s i t e d=7.L e t B i s=8.S t a c k=9.P u s h(s,t)i n t o S t a c k1 0.W h i l e S t a c k1 1.(s,t)t o p(S t a c k)1 2.V i s i t e d=V i s i t e d(s,t)1 3.i f a c t(s)=a c t(t)t h e n1 4.o u t e r1 5.f o r a l l a c t(s)1 6.f o r a l l s1 7.f o r a l l tt1 8.R=1 9.f o r a l l si s u p p(i)2 0.f o r a l l tj s u p p(j)2 1.i f(s,t)E r r o r s t h e n2 2.R=R2 3.e l s e i f(s,t)V i s i t e d t h e n2 4.R=R(s,t)2 5.L e t B i s L e t B i s(s,t)2 6.e l s e2 7.P u s h(si,tj)i n t o S t a c k2 8.B r e a k o u t e r2 9.bi,j c h e c k(i,j,R)3 0.a c t i o n B i s=(i(jbi j)(j(ibi j)3 1.i s B i s=AB3 2.e l s e3 3.i s B i s=f a l s e3 4.i f i s B i s=f a l s e t h e n 3 5.E r r o r s=E r r o r s(s,t)3 6.i f(s,t)L e t B i s t h e n3 7.r e t u r n u n k n o w3 8.i f i s B i s=t r u e t h e n3 9.r e t u r n t r u e4 0.e l s e 4 1.r e t u r n f a l s e在算法1的执行过程中,将集合E r r o r s设置为全局变量,并将其设置为空集,将集合V i s i t e d、L e t-B i s和S t a c k设置为函数c h e c k B i s(s,t)的局部变量,且每次执行函数c h e c k B i s(s,t)时,V i s i t e d、L e t-B i s和S t a c k都将被置为空集。设(s0,t0)为要验证是否满足模糊互模拟关系73桂林电子科技大学学报2 0 2 3年2月的状态对,(s,t)为(s0,t0)的某个后继状态对。在函数c h e c k B i s(s0,t0)中,当(s,t)第1次被访问时,将其加入集合V i s i t e d中。若(s,t)具有不同的动作,则其不满足模糊互模拟关系,将其加入集合E r-r o r s中;若(s,t)具有相同的动作,则对其后继状态继续进行遍历。当(s,t)已经存在于集合V i s i t e d中时,将其加入集合L e t B i s中,并在对(s0,t0)进行模糊互模拟关系判断时添加到关系集合R中。若在后续的遍历过程中,发现状态(s,t)L e t B i s不满足模糊互模拟关系,则将其从集合L e t B i s中删除,并加入集合E r r o r s中,同时返回结果u n k n o w,重新执行函数c h e c k B i s(s0,t0)。定理2 设F T S 1、F T S 2为2个有限模糊迁移系统,s、t分别为这2个迁移系统中的状态,则只有st时,算法1的返回结果为t r u e。证明 1)算法1的可终止性证明。令B i si为第i次执行函数c h e c k B i si,E r r o r si、L e t B i si分别为执行完c h e c k B i s之后的E r r o r s、L e t B i s集合。由算法1的第9 1 2行和第3 1 3 6行可知,当B i si执行结束时,会产生2种可能,即假设错误,执行算法1第3 4 3 7行或直接跳过执行第3 8行语句。对于前一种可能,由算法1的第3 2、3 3行可知,E r r o r siL e t-B i si;而后一种可能,算法则执行完毕。由算法1的第2 1 2 7行可知,E r r o r si-1L e t B i si=。根据算法1的第2 7行可知,E r r o r sj-1E r r o r si。假设在第j次执行完B i s后,s、t所有可达的非互模拟状态都已遍历完,则必有E r r o r sj=E r r o r sj+1,再由算法1的第3 2、3 3行可知,算法1一定会终止。2)算法1的正确性证明。设V i s i t e di为算法1第i次执行函数B i s所产生的V i s i t e d集合,Ri=V i s i t e di-E r r o r si。同时,假设算法在执行k次函数c h e c k B i s后终止。由定义4可知,对于任意的ik,随着i不断增大,Ri越来越接近模糊互模拟关系。在该情况下,对于任意的(si,tj)Ri,si与tj不确定是否满足互模拟状态,仅假设为互模拟状态,需要通过不断地遍历才可以确定是否满足模糊互模拟关系,但对于任意的(si,tj)Ri,必有si与tj不满足模糊互模拟关系。因此,当c h e c k B i sk的返回值为f a l s e时,s与t不满足模糊互模拟关系。当B i sk的返回值为t r u e时,必有c h e c k B i s为t r u e,即对于任意的A,s,tv,均有R。由定义3可知,状态对(s,t)满足模糊互模拟关系。3 数据结构和算法时间复杂度分析对于任意的模糊迁移系统,采用邻接链表的方式对其进行存储,其中模糊分布采用M a p类型的链表进行存储。存储模糊迁移系统的数据结构如图1所示。图1 存储模糊迁移系统的数据结构在图1所示的存储结构中,使用H a s h T a b l e对状态和迁移键值对以及动作和模糊分布键值对进行存储,使用M a p类型的L i s t对模糊分布进行存储,其中M a p的k e y值的数据类型与H a s h T a b l e中状态的数据类型保持一致,v a l u e类型则设置为d o u b l e类型。为了方便状态对的存储,设置S t a t e P a i r类对状态对进行存储,S t a t e P a i r类中主要包含属性状态s、t以及构造方法S t a t e P a i r(s,t),s、t的类型与最外层H a s h T a b l e中的k e y值类型相同。集合V i s i t e d、L e t B i s和E r r o r s均为S t a t e P a i r类型的链表。定理3 模糊互模拟局部算法的时间复杂为O(m1m2n31n32),空间复杂度为O(n1n2)。证明 由算法1的第15行可知,该算法的时间复杂度主要由函数c h e c k B i s决定。设s和t为c h e c k B i s中的2个状态,模糊迁移系统F T S 1的状态个数为n1,迁移数为m1,模糊迁移系统F T S 2的状态数为n2,迁移数为m1。1)当状态s、t为F T S 1、F T S 2的初始状态时,需要对F T S 1、F T S 2的全部状态进行遍历,此时共可构建n1n2个状态对。在函数中,栈S t a c k用于存储尚未判断是否满足模糊互模拟关系的状态对。根据函数的第5行可知,在最坏情况下,第1次执行函数c h e c k B i s时,所有遍历的状态对都进入栈中,该w h i l e循环至多执行n1n2次。根据函数的第3 13 6行可知,在最坏情况下,每执行1次c h e c k B i s函数,最多可以找到1对不满足模糊互模拟的状态。因此,在最坏情况下,第2次执行c h e c k B i s函数时,函数第5行的w h i l e循环需要执行n1n2-1次,第3次执行c h e c k B i s函数时,w h i l e循环需要执行n1n2-2次。故有n1n2i=1n1n2-i=(n1n2)2+(n1n2)(n1n2-1)283第1期胡晋玮等:一种模糊互模拟的局部算法3(n1n2)22。根据函数的第1 5 3 1行可知,对一个状态对进行检测时,最 多 对m1m2个 迁 移 进 行 遍 历。又 因 为c h e c k(i,j,R)的时间复杂度为O(n1n2),根据时间复杂度计算乘法原则,可得该算法的时间复杂度为O(m1m2n31n32)。2)根据c h e c k B i s的第2 2 2 5行及3 4 3 5行可知,当执行完一次c h e c k B i s函数时,集合V i s i t e d中的元素为集合L e t B i s与集合E r r o r s中元素的总和,即V i s i t e d=L e t B i sE r r o r s。在最坏情形下,执行1次c h e c k B i s时,所有的状态均被遍历,即V i s i t e d中包含n1n2个状态对时,算法的空间复杂度最高,故该算法的空间复杂度为O(n1n2)。4 算法的比较与实现在对相关的理论进行分析后,通过实验比较局部算法与全局算法2 2的实际效率。令F T S为一个模糊迁移系统,s、t为迁移系统中的任意2个状态。设F T S中的状态数为n,迁移数为m。当只对一个迁移系统进行验证时,有n=n1=n2,m=m1=m2,故在最坏情形下,局部算法验证状态对(s,t)是否满足模糊互模拟关系的时间复杂度为O(m2n6),全局算法验证状态s、t是否满足模糊互模拟关系的时间复杂度为O(m2n4)。然而,当2个状态不满足模糊互模拟关系时,局部算法只需对迁移系统的部分状态和迁移进行遍历,即可得到结果,具有更高的效率。由于目前尚无较好的模糊数据集,采用随机生成模糊迁移系统,并随机选取迁移系统中的状态的方法,对局部算法和全局算法进行对比。用T r u e表示检测的状态满足模糊互模拟关系,F a l s e表示检测的状态不满足模糊互模拟关系。采用J a v a语言对算法1进行了实现。实验环境为:W i n d o w s 1 0家 庭 中 文 版,I n t e l C o r eT Mi 7-7 7 0 0 HQ C P U 2.8 0 GH z,8 G i B R AM。首先在具有相同状态数不同迁移数的模糊迁移系统下,对算法的运行时间进行比较,结果如表1所示。从表1可看出,全局算法在状态数相同迁移数相差不大的情况下,运行时间相差无几;在状态满足互模拟关系与不满足互模拟关系的情况下,运行时间也相差不大,这与全局算法的特点相同;局部算法的运行时间与其所选择判断模糊互模拟关系的状态对有关;在对模糊迁移系统中任意的2个状态进行互模拟等价关系判断时,局部算法比全局算法的效率更高。表1 相同状态数,不同迁移数算法的运行时间snmR e s u l t局部算法全局算法2 03 7T r u e0.1 2 8 30.0 9 0 12 03 1F a l s e0.8 7 5 20.1 0 4 34 08 3T r u e0.1 9 9 30.1 6 8 74 01 1 9F a l s e0.0 6 4 20.1 8 8 18 03 0 4T r u e2.1 5 6 21.2 6 9 68 03 2 2F a l s e0.9 5 4 11.2 3 7 21 0 04 0 7T r u e2.2 1 9 82.4 9 8 61 0 03 8 6F a l s e0.6 5 9 52.0 9 6 41 5 05 6 8T r u e4.4 0 7 88.8 5 6 21 5 05 8 9F a l s e6.6 9 7 89.9 0 6 62 0 08 5 5T r u e1 4.9 5 6 52 5.5 1 8 22 0 07 2 1F a l s e7.7 4 1 22 2.3 5 8 5 当对2个不同的模糊迁移系统是否满足模糊互摸拟关系进行比较时,全局算法的时间复杂为O(m1+m2)2(n1+n2)4),时间复杂度高于局部算法。在对2个不同的迁移系统进行检测时,算法运行时间如表2所示。表2 2个不同迁移系统算法运行时间sn1m1n2m2R e s u l t局部算法全局算法1 02 21 03 2F a l s e0.0 6 8 30.1 2 4 13 08 43 08 4T r u e0.1 5 1 10.5 8 0 95 01 5 85 01 5 8T r u e0.2 7 5 21.7 5 3 37 02 1 87 02 1 8T r u e0.4 0 5 84.1 3 8 29 02 4 39 02 5 2F a l s e0.1 6 7 21 1.2 3 8 11 0 03 2 01 0 03 2 0T r u e0.7 4 8 01 9.8 1 2 5 从表2可看出,无论R e s u l t的结果为T r u e还是F a l s e,局部算法的运行效率都比全局算法的运行效率高,这与理论推导一致。由表1、2可知,虽然全局算法的时间复杂度比局部算法更低,但在对一个模糊迁移系统中的一对给定状态是否满足模糊互模拟关系进行判断,或者对2个不同模糊迁移系统中的给定状态对是否满足模糊互模拟关系时,局部算法往往比全局算法拥有更高的效率。5 结束语为了可以更加高效地对指定状态是否满足模糊互模拟关系进行判定,给出了模糊互模拟等价验证的局部算法。在局部算法中,对迁移系统进行深度优先搜索遍历,并在遍历的同时对其后继状态是否满足模糊互模拟关系进行判断。该模糊互模拟局部验证算法的时间复杂度为O(m1m2n31n32),空间复杂度为93桂林电子科技大学学报2 0 2 3年2月O(n1n2)。弱互模拟将一个给定的过程转变与另一个过程转变相匹配,同样是解决空间状态爆炸的有效途径。作为未来的工作,考虑将弱互模拟的概念引入到模糊迁移系统中,给出其定义,并对模糊弱互模拟等价验证的全局算法、局部算法和准局部算法进行研究。参考文献:1 B A I E R C,K A T O E N J P.P r i n c i p l e s o f M o d e l C h e c k i n gM.C a m b r i d g e:T h e M I T P r e s s,2 0 0 8:4 4 9-5 8 2.2 P A I G E R,T A R J A N R E.T h r e e p a r t i t i o n r e f i n e m e n t a l g o r i t h m sJ.S I AM J o u r n a l o n C o m p u t i n g,1 9 8 7,1 6(6):9 7 3-9 8 9.3 F E R N A N D E Z J C,MO U N I E R L.V e r i f y i n g b i s i m u l a-t i o n s o n t h e f l y C/P r o c e e d i n g s o f 3 r d I n t e r n a t i o n-a l C o n f e r e n c e o n F o r m a l D e s c r i p t i o n T e c h n i q u e s f o r D i s t r i b u t e d S y s t e m s a n d C o mm u n i c a t i o n P r o t o c o l s.N e w Y o r k,N Y:A C M:1 9 9 0:9 5-1 1 0.4 D U W,D E N G Y.A q u a s i-l o c a l a l g o r i t h m f o r c h e c k i n g b i s i m i l a r i t yC/I E E E I n t e r n a t i o n a l C o n f e r e n c e o n C o m p u t e r S c i e n c e a n d A u t o m a t i o n E n g i n e e r i n g.P i s c a t-a w a y,N J:I E E E P r e s s,2 0 1 1(2):1-5.5 L I N H M.O n-t h e-F l y I n s t a n t i a t i o n o f V a l u e-P a s s i n g P r o c e s s e sM/F o r m a l D e s c r i p t i o n T e c h n i q u e s a n d P r o t o c o l S p e c i f i c a t i o n,T e s t i n g a n d V e r i f i c a t i o n.B o s-t o n:S p r i n g e r,1 9 9 8:2 1 5-2 3 0.6 D E N G Y,D U W.A l o c a l a l g o r i t h m f o r c h e c k i n g p r o b a-b i l i s t i c b i s i m i l a r i t yC/F o u r t h I n t e r n a t i o n a l C o n f e r-e n c e o n F r o n t i e r o f C o m p u t e r S c i e n c e a n d T e c h n o l o g y.P i s c a t a w a y,N J:I E E E P r e s s,2 0 0 9:4 0 1-4 0 7.7 张小红,裴道武,代建华.模糊数学与R o u g h集理论M.北京:清华大学出版社,2 0 1 3:1-1 2.8 D O O S T F A T E M E H M,K R E M E R S C.N e w d i r e c t i o n s i n f u z z y a u t o m a t aJ.I n t e r n a t i o n a l J o u r n a l o f A p p r o x i-m a t e R e a s o n i n g,2 0 0 5,3 8(2):1 7 5-2 1 4.9 C A O Y,E Z AWA Y.N o n d e t e r m i n i s t i c f u z z y a u t o m a t aJ.I n f o r m a t i o n S c i e n c e s,2 0 1 2,1 9 1:8 6-9 7.1 0 L I Y.F u z z y t u r i n g m a c h i n e s:v a r i a n t s a n d u n i v e r s a l i t yJ.I E E E T r a n s a c t i o n s o n F u z z y S y s t e m s,2 0 0 8,1 6(6):1 4 9 1-1 5 0 2.1 1 B U G A R I N A J,B A R R O S.F u z z y r e a s o n i n g s u p p o r t e d b y P e t r i n e t sJ.I E E E T r a n s a c t i o n s o n F u z z y S y s-t e m s,1 9 9 4,2(2):1 3 5-1 5 0.1 2 P E D R Y C Z W,G OM I D E F.A g e n e r a l i z e d f u z z y p e t r i n e t m o d e lJ.I E E E T r a n s a c t i o n s o n F u z z y S y s t e m s,1 9 9 4,2(4):2 9 5-3 0 1.1 3 WU H,C H E N Y.C o a l g e b r a s f o r f u z z y t r a n s i t i o n s y s-t e m sJ.E l e c t r o n i c N o t e s i n T h e o r e t i c a l C o m p u t e r S c i-e n c e,2 0 1 4,3 0 1:9 1-1 0 1.1 4 WU H,D E N G Y.D i s t r i b u t i o n-b a s e d b e h a v i o r a l d i s-t a n c e f o r n o n d e t e r m i n i s t i c f u z z y t r a n s i t i o n s y s t e m sJ.I E E E T r a