Processing math: 22%
  • 中国期刊全文数据库
  • 中国学术期刊综合评价数据库
  • 中国科技论文与引文数据库
  • 中国核心期刊(遴选)数据库

一种模糊互模拟的局部算法

胡晋玮, 钱俊彦

胡晋玮, 钱俊彦. 一种模糊互模拟的局部算法[J]. 桂林电子科技大学学报, 2023, 43(1): 35-40.
引用本文: 胡晋玮, 钱俊彦. 一种模糊互模拟的局部算法[J]. 桂林电子科技大学学报, 2023, 43(1): 35-40.
HU Jinwei, QIAN Junyan. A local algorithm of fuzzy bisimulation[J]. Journal of Guilin University of Electronic Technology, 2023, 43(1): 35-40.
Citation: HU Jinwei, QIAN Junyan. A local algorithm of fuzzy bisimulation[J]. Journal of Guilin University of Electronic Technology, 2023, 43(1): 35-40.

一种模糊互模拟的局部算法

基金项目: 

国家自然科学基金 61562015

广西自然科学基金 2018GXNSFDA138003

详细信息
    通讯作者:

    钱俊彦(1973-),男,教授,博士,研究方向为软件工程、程序验证与测试、容错技术。E-mail: qjy2000@gmail.com

  • 中图分类号: TP301

A local algorithm of fuzzy bisimulation

  • 摘要: 为了快速地对模糊迁移系统中给定状态是否满足互模拟关系进行验证,提出了一种模糊互模拟的局部算法。该算法将验证与遍历相结合,在对状态是否满足模糊互模拟关系验证的同时,动态地增加状态空间,使得算法只需遍历部分状态空间即可完成验证。在部分情况下,尤其是当2个状态不满足模糊互模拟关系时,模糊互模拟的局部算法可以更快地对给定状态是否满足模糊互模拟关系进行验证。通过Java实现了模糊互模拟的局部算法和已有全局算法,并进行了比较实验。实验结果表明,在给定状态对不满足互模拟关系的情况下,本算法比现有模糊互模拟的全局算法的效率更高。
    Abstract: In order to verify whether the given states satisfiy the bisimulation, a local algorithm of fuzzy bisimulation is proposed. The algorithm takes verification and traversal at the same. While verify the given states whether satisfiy the fuzzy bisimulation, the state space is dynamically increased, so that the algorithm only needs to traverse part of the state space to complete the verification. In some cases, the local algorithm of fuzzy bisimulation can verify whether the given states satisfiy the fuzzy bisimulation more quickly, especially when the two states do not satisfy the fuzzy bisimulation. The local algorithm and the existing global algorithm are implemented by Java and compared by experiments.The experiments, shows that this algorithm is more efficient than the existing global fuzzy bisimulation algorithm when the given states do not satisfiy the bisimulation.
  • 互模拟作为描述系统之间行为等价的重要概念,是解决状态空间爆炸问题的有效手段[1]。1987年,Paige等[2]在划分精化的思想下,给出了时间复杂度为O(mlog n)的互模拟等价类划分算法,该算法需要对整个迁移系统的状态空间进行预先存储,属于互模拟等价验证全局算法的一种。然而,在很多情况下,并不需要求得整个迁移系统状态空间的互模拟等价类,只需对迁移系统中的给定状态是否满足互模拟关系进行判断。

    1989年,Fernandez等[3]提出了互模拟等价关系判断的局部算法,该算法又称为“on the fly”算法。“on the fly”算法通过构建2个迁移系统的同步积,并对要判定状态对的后续状态对进行深度优先或广度优先搜索遍历,同时判断每对状态对是否满足互模拟关系,该算法的时间复杂度为O(n2),其中n为LTS的状态数。Du等[4]在“on the fly”算法的基础上提出了介于局部算法与全局算法之间的互模拟等价验证的准局部算法,通过对状态添加状态0或1的方法,避免了对状态的重复访问,降低了算法的时间复杂度。Lin[5]将局部算法应用于值传递系统中,Deng等[6]将局部算法应用于概率迁移系统,并提出了概率迁移系统的局部算法。

    模糊集合是经典集合的扩展,主要用于对事物的不确定性进行描述,可有效地对主观概念和不确定性概念进行分析[7]。将模糊论的定量分析应用到系统分析中,可很好地分析系统能够在多大程度上满足系统的性质规约,对模糊自动机[8-10]、模糊Petri网[11-12]及模糊迁移系统[13-16]的研究已经取得了很多学术成果。

    值得注意的是,当用模糊自动机构建系统模型时,所构造出来的模型并非唯一。为了更好地对这些模型是否等价进行判断,计算机科学工作者将互模拟的定义引入模糊迁移系统。Petković等[17]通过代数的方法提出了有限模糊自动机全等概念。Bucholz[18]和Sun等[19]对有限模糊自动机和有限模糊迁移系统的互模拟进行了研究。Cao等[20]针对无限迁移系统,提出了关于一般模糊迁移系统的模糊互模拟的定义。为了更好地对模糊迁移系统行为相似程度进行刻画,Cao等[21]提出了行为距离的概念,当2个模糊迁移系统完全满足模糊互模拟性质时,其行为距离为0。Wu等[22]在算法和逻辑2个角度上对模糊互模拟进行了刻画。

    为了更好地对模糊迁移系统是否满足模糊互模拟关系进行判断,Ćirić等[23]给出了有限模糊自动机的模糊互模拟等价验证算法;Ignjatović[23]提出了对2个模糊社交网络进行模糊互模拟等价验证的算法,该算法的时间复杂度为O(lc5),其中l为在计算过程中出现的不同模糊值的数量,c为社交网络中节点数;Wu等[22]提出了一种模糊互模拟等价验证的全局算法,该算法的时间复杂度为O(m2n4),其中n为模糊迁移系统中状态的个数,m为模糊迁移系统中迁移的数量。

    尽管互模拟在模糊领域已经取得了一定成果,但到目前为止,对模糊互模拟局部算法的研究尚未得到广泛关注。为了更快地对指定状态是否满足模糊互模拟关系进行验证,基于文献[5-6]的算法思想,提出了一种模糊互模拟等价关系验证的局部算法,以提高模糊互模拟等价验证的效率,并通过实验的方式与现有的模糊互模拟检验算法进行了比较。

    S为非空集合,S上的模糊集合PS到[0, 1]的一个映射,μ: S→[0, 1],用F(S)表示集合S上的全体模糊集,μF(S),则模糊集μ的支撑集supp(μ)定义为

    supp(μ)={sS:μ(s)>0}

    若supp(μ)是有限的,则模糊集μ可用Zedeh形式表示为

    μ=μ(s1)s1+μ(s2)s2++μ(sn)sn

    对于任意的μF(S)及USμ(U)=supsUμ(s)。特别地,μ(Ø)=0。

    μ, ν为集合S上的2个模糊集合,且μν,对任意的sS,均有μ(s)≤ν(s)。

    定义1[9] 模糊迁移系统(fuzzy transition system,简称FTS)是一个三元组(S, A, →),其中:

    1)S为状态的集合;

    2)A为动作的集合;

    3)→⊆S×A×MF(S)为迁移关系。

    定义2[22] 给定集合SRS×S,若存在关于R的权重函数e: s×s→[0, 1]满足如下条件:

    1)对于任意的sSμ(s)=supsSe(s,t)

    2)对于任意的tSν(t)=suptSe(s,t)

    3)若e(s, t) > 0,则有(s, t)∈R

    则称RF(S)×F(S)为关系R的提升,使得\mu R^{†}ν成立。

    定理1[22] 令S为一个集合,RS×Sμ, νF(S)。若\mu R^{†} ν成立,则对任意的sS,均有

    1)\mu(s) \leqslant ν\left(\overrightarrow{R_s}\right),
    2)ν(s) \leqslant \mu\left(\overleftarrow{R_s}\right),

    其中,\overrightarrow{R_s}=\left\{s^{\prime}: s R s^{\prime}\right\}\overleftarrow{R_s}=\left\{s^{\prime}: s^{\prime} R s\right\}

    定义3[22] 若对于任意的RS×SsRt均满足以下条件:

    1)对于任意的s×αμ,均有t×αv,使得\mu R^{†} ν成立;

    2)对于任意的t×αv,均有s×αμ,使得ν R^{†} \mu成立。

    则称R为互模拟关系。

    若存在一个模糊互模拟关系R,使得(s, t)∈R,则称状态s, t满足模糊互模拟等价关系,记为s~t

    在递归定义的基础上,结合“On The Fly”算法和对提升关系R^{†}的判断算法,给出模糊迁移系统的互模拟等价验证的局部算法。

    在模糊迁移系统中,互模拟可采用递归的方式进行定义。

    定义4[22] 设FTS为一个三元组M=(S, A, →),定义如下:

    1)R0=S×S

    2)对于任意的n > 0,sRn+1t,若

    a)对于任意的s×αμ,存在t×αv,使得\mu R_n^{† ν}成立;

    b)对于任意的t×αv,存在s×αμ,使得\mu R_n^{† ν}成立。

    3)~=∩n≥0Rn

    命题1 在有限FTS中,定义3与定义4所定义的模糊互模拟是相同的。

    证明 为了方便表示,用~def4表示定义4中所定义的模糊互模拟,用~def3表示定义3中表示的模糊互模拟,则

    1)根据~def3的定义可知,若s~def3t,则有s~def4t成立。

    2)设s~def4t,且s×αμ,要证~def4为模糊互模拟关系,即要证存在t×αv,使得\mu \sim_{\operatorname{def} 4}^{†}ν成立。设集合D{\rm{ }} = \{ν :t \times \alpha \to v \wedge \mu \not \sim _{{\rm{def}}4}^†ν \},即对于任意的νT,均有nν使得\mu \not \sim _{{n_ν }}^†ν。设nmax=max{nν: νT},则有\mu \not \sim _{{n_{{\rm{max}}}}}^†ν。又因为FTS是有限的,故集合D是有限的。因为s~def4t成立,则有s~nmax+1t,即存在νt×αv,使得\mu \sim_{{n_{{\rm{max}}}}}^†ννT。故对于任意的s×αμ,均存在ν使得\mu \sim_{{\rm{def}}4}^†ν成立。同理,可证明若t×αv,则存在s×αμ,使得\mu \sim_{{\rm{def}}4}^†ν成立。

    文献[22]提出了对于给定的集合Sμ, νF(S),RS×S,判断\mu {R^† }ν 的算法。该算法时间复杂度为O(n2)。在此基础上,结合“On the Fly”算法的思想,提出了关于模糊互模拟验证的局部算法。

    在模糊互模拟局部算法中,用集合Errors存储在算法执行过程中被判定为不具有互模拟性质的状态对;用数组Visited表示已经被遍历过的状态对。若一对状态已经被多次遍历,但其是否满足模糊互模拟关系尚不能确定时,则先假设其满足互模拟关系,同时用数组LetBis对其进行存储,若在后续的遍历过程中发现该状态对不满足互模拟关系,则将该状态对从数组LetBis中删除,同时将其添加到数组Errors中,并重新执行函数checkBis。为了保证状态遍历和判断的先后顺序,用栈Stack存储尚未完成模糊互模拟关系判断的状态对。

    算法1 模糊互模拟检测的局部算法

    输入:模糊迁移系统FTS以及状态对(s, t)

    输出:s, t是否满足模糊互模拟关系

    1.Errors=Ø

    2.isBis=unknow

    3.while isBis=unknow

    4.   isBis=checkBis(s, t)

    5.return isBis

    Function checkBis(s, t)

    6.Visited=Ø

    7.LetBis=Ø

    8.Stack=Ø

    9.Push (s, t) into Stack

    10.While Stack≠Ø

    11.  (s, t)top(Stack)

    12.  Visited=Visited∪(s, t)

    13.  if act(s)==act(t) then

    14.   outer

    15.   for all α∈act(s)

    16.    for alls×αμ

    17.      for all t×ανt

    18.        R

    19.        for all si∈ supp(μi)

    20.         for all tj ∈ supp(νj)

    21.          if (s, t) Errors then

    22.             R=R

    23.         else if (s, t)∈ Visited then

    24.           R=R∪(s, t)

    25.           LetBis LetBis∪(s, t)

    26.           else

    27.           Push (si, tj) into Stack

    28.           Break outer

    29.   bi, j check (μi, νj, R)

    30. actionBis=(∧i(∨jbij))∧(∧j(∨ibij))

    31. isBis=∧αAB

    32.   else

    33.    isBis=false

    34.   if isBis=false then

    35.    Errors=Errors∪(s, t)

    36.     if (s, t) LetBis then

    37.     return unknow

    38.   if isBis=true then

    39.   return true

    40.else

    41.return false

    在算法1的执行过程中,将集合Errors设置为全局变量,并将其设置为空集,将集合Visited、LetBis和Stack设置为函数checkBis(s, t)的局部变量,且每次执行函数checkBis(s, t)时,Visited、LetBis和Stack都将被置为空集。

    设(s0, t0)为要验证是否满足模糊互模拟关系的状态对,(s, t)为(s0, t0)的某个后继状态对。在函数checkBis(s0, t0)中,当(s, t第1次被访问时,将其加入集合Visited中。若(s, t)具有不同的动作,则其不满足模糊互模拟关系,将其加入集合Errors中;若(s, t)具有相同的动作,则对其后继状态继续进行遍历。当(s, t)已经存在于集合Visited中时,将其加入集合LetBis中,并在对(s0, t0)进行模糊互模拟关系判断时添加到关系集合R中。若在后续的遍历过程中,发现状态(s, t)∈LetBis不满足模糊互模拟关系,则将其从集合LetBis中删除,并加入集合Errors中,同时返回结果unknow,重新执行函数checkBis(s0, t0)。

    定理2 设FTS1、FTS2为2个有限模糊迁移系统,st分别为这2个迁移系统中的状态,则只有s~t时,算法1的返回结果为true。

    证明 1)算法1的可终止性证明。令Bisi为第i次执行函数checkBisi,Errorsi、LetBisi分别为执行完checkBis之后的Errors、LetBis集合。由算法1的第9~12行和第31~36行可知,当Bisi执行结束时,会产生2种可能,即假设错误,执行算法1第34~37行或直接跳过执行第38行语句。对于前一种可能,由算法1的第32、33行可知,Errorsi∩LetBisi≠Ø;而后一种可能,算法则执行完毕。由算法1的第21~27行可知,Errorsi-1∩LetBisi=Ø。根据算法1的第27行可知,Errorsj-1⊆Errorsi。假设在第j次执行完Bis后,st所有可达的非互模拟状态都已遍历完,则必有Errorsj=Errorsj+1,再由算法1的第32、33行可知,算法1一定会终止。

    2) 算法1的正确性证明。设Visitedi为算法1第i次执行函数Bis所产生的Visited集合,Ri=Visitedi-Errorsi。同时,假设算法在执行k次函数checkBis后终止。由定义4可知,对于任意的i < k,随着i不断增大,Ri越来越接近模糊互模拟关系~。在该情况下,对于任意的(si, tj)∈Risitj不确定是否满足互模拟状态,仅假设为互模拟状态,需要通过不断地遍历才可以确定是否满足模糊互模拟关系,但对于任意的(si, tj)∉Ri,必有sitj不满足模糊互模拟关系。因此,当checkBisk的返回值为false时,st不满足模糊互模拟关系。当Bisk的返回值为true时,必有checkBis为true,即对于任意的αA, s×αμt×αv,均有\mu R^{†}ν。由定义3可知,状态对(s, t)满足模糊互模拟关系。

    对于任意的模糊迁移系统,采用邻接链表的方式对其进行存储,其中模糊分布采用Map类型的链表进行存储。存储模糊迁移系统的数据结构如图 1所示。

    图  1  存储模糊迁移系统的数据结构

    图 1所示的存储结构中,使用HashTable对状态和迁移键值对以及动作和模糊分布键值对进行存储,使用Map类型的List对模糊分布进行存储,其中Map的key值的数据类型与HashTable中状态的数据类型保持一致,value类型则设置为double类型。为了方便状态对的存储,设置StatePair类对状态对进行存储,StatePair类中主要包含属性状态st以及构造方法StatePair(s, t),st的类型与最外层HashTable中的key值类型相同。集合Visited、LetBis和Errors均为StatePair类型的链表。

    定理3 模糊互模拟局部算法的时间复杂为O(m1m2n13n23),空间复杂度为O(n1n2)。

    证明 由算法1的第1~5行可知,该算法的时间复杂度主要由函数checkBis决定。设st为checkBis中的2个状态,模糊迁移系统FTS1的状态个数为n1,迁移数为m1,模糊迁移系统FTS2的状态数为n2,迁移数为m1

    1) 当状态st为FTS1、FTS2的初始状态时,需要对FTS1、FTS2的全部状态进行遍历,此时共可构建n1n2个状态对。在函数中,栈Stack用于存储尚未判断是否满足模糊互模拟关系的状态对。根据函数的第5行可知,在最坏情况下,第1次执行函数checkBis时,所有遍历的状态对都进入栈中,该while循环至多执行n1n2次。根据函数的第31~36行可知,在最坏情况下,每执行1次checkBis函数,最多可以找到1对不满足模糊互模拟的状态。因此,在最坏情况下,第2次执行checkBis函数时,函数第5行的while循环需要执行n1n2-1次,第3次执行checkBis函数时,while循环需要执行n1n2-2次。故有

    \begin{array}{c} \sum\limits_{i = 1}^{{n_1}{n_2}} {{n_1}} {n_2} - i = {\left( {{n_1}{n_2}} \right)^2} + \frac{{\left( {{n_1}{n_2}} \right)\left( {{n_1}{n_2} - 1} \right)}}{2} \le \\ \frac{{3{{\left( {{n_1}{n_2}} \right)}^2}}}{2}。 \end{array}

    根据函数的第15~31行可知,对一个状态对进行检测时,最多对m1m2个迁移进行遍历。又因为check(μi, νj, R)的时间复杂度为O(n1n2),根据时间复杂度计算乘法原则,可得该算法的时间复杂度为O(m1m2n13n23)。

    2) 根据checkBis的第22~25行及34~35行可知,当执行完一次checkBis函数时,集合Visited中的元素为集合LetBis与集合Errors中元素的总和,即Visited=LetBis∪Errors。在最坏情形下,执行1次checkBis时,所有的状态均被遍历,即Visited中包含n1n2个状态对时,算法的空间复杂度最高,故该算法的空间复杂度为O(n1n2)。

    在对相关的理论进行分析后,通过实验比较局部算法与全局算法[22]的实际效率。

    令FTS为一个模糊迁移系统,st为迁移系统中的任意2个状态。设FTS中的状态数为n,迁移数为m。当只对一个迁移系统进行验证时,有n=n1=n2m=m1=m2,故在最坏情形下,局部算法验证状态对(s, t)是否满足模糊互模拟关系的时间复杂度为O(m2n6),全局算法验证状态st是否满足模糊互模拟关系的时间复杂度为O(m2n4)。然而,当2个状态不满足模糊互模拟关系时,局部算法只需对迁移系统的部分状态和迁移进行遍历,即可得到结果,具有更高的效率。由于目前尚无较好的模糊数据集,采用随机生成模糊迁移系统,并随机选取迁移系统中的状态的方法,对局部算法和全局算法进行对比。用True表示检测的状态满足模糊互模拟关系,False表示检测的状态不满足模糊互模拟关系。

    采用Java语言对算法1进行了实现。实验环境为:Windows 10家庭中文版,Intel® CoreTM i7-7700HQ CPU 2.80 GHz,8 GiB RAM。

    首先在具有相同状态数不同迁移数的模糊迁移系统下,对算法的运行时间进行比较,结果如表 1所示。从表 1可看出,全局算法在状态数相同迁移数相差不大的情况下,运行时间相差无几;在状态满足互模拟关系与不满足互模拟关系的情况下,运行时间也相差不大,这与全局算法的特点相同;局部算法的运行时间与其所选择判断模糊互模拟关系的状态对有关;在对模糊迁移系统中任意的2个状态进行互模拟等价关系判断时,局部算法比全局算法的效率更高。

    表  1  相同状态数,不同迁移数算法的运行时间 s
    n m Result 局部算法 全局算法
    20 37 True 0.128 3 0.090 1
    20 31 False 0.875 2 0.104 3
    40 83 True 0.199 3 0.168 7
    40 119 False 0.064 2 0.188 1
    80 304 True 2.156 2 1.269 6
    80 322 False 0.954 1 1.237 2
    100 407 True 2.219 8 2.498 6
    100 386 False 0.659 5 2.096 4
    150 568 True 4.407 8 8.856 2
    150 589 False 6.697 8 9.906 6
    200 855 True 14.956 5 25.518 2
    200 721 False 7.741 2 22.358 5
    下载: 导出CSV 
    | 显示表格

    当对2个不同的模糊迁移系统是否满足模糊互摸拟关系进行比较时,全局算法的时间复杂为O((m1+m2)2(n1+n2)4),时间复杂度高于局部算法。在对2个不同的迁移系统进行检测时,算法运行时间如表 2所示。

    表  2  2个不同迁移系统算法运行时间 s
    n1 m1 n2 m2 Result 局部算法 全局算法
    10 22 10 32 False 0.068 3 0.124 1
    30 84 30 84 True 0.151 1 0.580 9
    50 158 50 158 True 0.275 2 1.753 3
    70 218 70 218 True 0.405 8 4.138 2
    90 243 90 252 False 0.167 2 11.238 1
    100 320 100 320 True 0.748 0 19.812 5
    下载: 导出CSV 
    | 显示表格

    表 2可看出,无论Result的结果为True还是False,局部算法的运行效率都比全局算法的运行效率高,这与理论推导一致。

    表 12可知,虽然全局算法的时间复杂度比局部算法更低,但在对一个模糊迁移系统中的一对给定状态是否满足模糊互模拟关系进行判断,或者对2个不同模糊迁移系统中的给定状态对是否满足模糊互模拟关系时,局部算法往往比全局算法拥有更高的效率。

    为了可以更加高效地对指定状态是否满足模糊互模拟关系进行判定,给出了模糊互模拟等价验证的局部算法。在局部算法中,对迁移系统进行深度优先搜索遍历,并在遍历的同时对其后继状态是否满足模糊互模拟关系进行判断。该模糊互模拟局部验证算法的时间复杂度为O(m1m2n13n23),空间复杂度为O(n1n2)。

    弱互模拟将一个给定的过程转变与另一个过程转变相匹配,同样是解决空间状态爆炸的有效途径。作为未来的工作,考虑将弱互模拟的概念引入到模糊迁移系统中,给出其定义,并对模糊弱互模拟等价验证的全局算法、局部算法和准局部算法进行研究。

  • 图  1   存储模糊迁移系统的数据结构

    表  1   相同状态数,不同迁移数算法的运行时间 s

    n m Result 局部算法 全局算法
    20 37 True 0.128 3 0.090 1
    20 31 False 0.875 2 0.104 3
    40 83 True 0.199 3 0.168 7
    40 119 False 0.064 2 0.188 1
    80 304 True 2.156 2 1.269 6
    80 322 False 0.954 1 1.237 2
    100 407 True 2.219 8 2.498 6
    100 386 False 0.659 5 2.096 4
    150 568 True 4.407 8 8.856 2
    150 589 False 6.697 8 9.906 6
    200 855 True 14.956 5 25.518 2
    200 721 False 7.741 2 22.358 5
    下载: 导出CSV

    表  2   2个不同迁移系统算法运行时间 s

    n1 m1 n2 m2 Result 局部算法 全局算法
    10 22 10 32 False 0.068 3 0.124 1
    30 84 30 84 True 0.151 1 0.580 9
    50 158 50 158 True 0.275 2 1.753 3
    70 218 70 218 True 0.405 8 4.138 2
    90 243 90 252 False 0.167 2 11.238 1
    100 320 100 320 True 0.748 0 19.812 5
    下载: 导出CSV
  • [1]

    BAIER C, KATOEN J P. Principles of Model Checking[M]. Cambridge: The MIT Press, 2008: 449-582.

    [2]

    PAIGE R, TARJAN R E. Three partition refinement algorithms[J]. SIAM Journal on Computing, 1987, 16(6): 973-989. doi: 10.1137/0216062

    [3]

    FERNANDEZ J C, MOUNIER L. Verifying bisimulations "on the fly"[C]//Proceedings of 3rd International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols. New York, NY: ACM: 1990: 95-110.

    [4]

    DU W, DENG Y. A quasi-local algorithm for checking bisimilarity[C]//IEEE International Conference on Computer Science and Automation Engineering. Piscataway, NJ: IEEE Press, 2011(2): 1-5.

    [5]

    LIN H M. "On-the-Fly Instantiation" of Value-Passing Processes[M]//Formal Description Techniques and Protocol Specification, Testing and Verification. Boston: Springer, 1998: 215-230.

    [6]

    DENG Y, DU W. A local algorithm for checking probabilistic bisimilarity[C]//Fourth International Conference on Frontier of Computer Science and Technology. Piscataway, NJ: IEEE Press, 2009: 401-407.

    [7] 张小红, 裴道武, 代建华. 模糊数学与Rough集理论[M]. 北京: 清华大学出版社, 2013: 1-12.
    [8]

    DOOSTFATEMEH M, KREMER S C. New directions in fuzzy automata[J]. International Journal of Approximate Reasoning, 2005, 38(2): 175-214. doi: 10.1016/j.ijar.2004.08.001

    [9]

    CAO Y, EZAWA Y. Nondeterministic fuzzy automata[J]. Information Sciences, 2012, 191: 86-97. doi: 10.1016/j.ins.2011.12.024

    [10]

    LI Y. Fuzzy turing machines: variants and universality[J]. IEEE Transactions on Fuzzy Systems, 2008, 16(6): 1491-1502. doi: 10.1109/TFUZZ.2008.2004990

    [11]

    BUGARIN A J, BARRO S. Fuzzy reasoning supported by Petri nets[J]. IEEE Transactions on Fuzzy Systems, 1994, 2(2): 135-150. doi: 10.1109/91.277962

    [12]

    PEDRYCZ W, GOMIDE F. A generalized fuzzy petri net model[J]. IEEE Transactions on Fuzzy Systems, 1994, 2(4): 295-301. doi: 10.1109/91.324809

    [13]

    WU H, CHEN Y. Coalgebras for fuzzy transition systems[J]. Electronic Notes in Theoretical Computer Science, 2014, 301: 91-101. doi: 10.1016/j.entcs.2014.01.008

    [14]

    WU H, DENG Y. Distribution-based behavioral distance for nondeterministic fuzzy transition systems[J]. IEEE Transactions on Fuzzy Systems, 2017, 26(2): 416-429.

    [15]

    PAN H, ZHANG M, CHEN Y. Bisimilarity for fuzzy doubly labeled transition systems[J]. Quantitative Logic and Soft Computing, 2012: 207-214.

    [16]

    WU H, CHEN T, HAN T, et al. Bisimulations for fuzzy transition systems revisited[J]. International Journal of Approximate Reasoning, 2018, 99: 1-11. doi: 10.1016/j.ijar.2018.04.010

    [17]

    PETKOVIĆ T. Congruences and homomorphisms of fuzzy automata[J]. Fuzzy Sets and Systems, 2006, 157(3): 444-458. doi: 10.1016/j.fss.2005.06.017

    [18]

    BUCHHOLZ P. Bisimulation relations for weighted automata[J]. Theoretical Computer Science, 2008, 393(1/2/3): 109-123.

    [19]

    SUN D D, LI Y M, YANG W W. Bisimulation relations for fuzzy finite automata[J]. Fuzzy Systems and Mathematics, 2009, 23: 92-100.

    [20]

    CAO Y, CHEN G, KERRE E E. Bisimulations for fuzzy-transition systems[J]. IEEE Transactions on Fuzzy Systems, 2011, 19(3): 540-552. doi: 10.1109/TFUZZ.2011.2117431

    [21]

    CAO Y, SUN S X, WANG H, et al. A behavioral distance for fuzzy-transition systems[J]. IEEE Transactions on Fuzzy Systems, 2012, 21(4): 735-747.

    [22]

    WU H Y, CHEN Y X, BU T M, et al. Algorithmic and logical characterizations of bisimulations for non-deterministic fuzzy transition systems[J]. Fuzzy Sets and Systems, 2018, 333: 106-123. doi: 10.1016/j.fss.2017.02.008

    [23]

    ĆIRIĆ M, IGNJATOVIĆ J, JANČIĆ I, et al. Computation of the greatest simulations and bisimulations between fuzzy automata[J]. Fuzzy Sets and Systems, 2012, 208: 22-42. doi: 10.1016/j.fss.2012.05.006

    [24]

    IGNJATOVIC J, CIRIC M, STANKOVIC I. Bisimulations in fuzzy social network analysis[C]//Conference of the International Fuzzy Systems Association and the European Society for Fuzzy Logic and Technology. Gijón: Atlantis Press, 2015: 404-411.

    [25] 曾宇清, 钱俊彦. 基于自动机的并发程序符号可达分析[J]. 桂林电子科技大学学报, 2013, 33(4): 300-304. doi: 10.3969/j.issn.1673-808X.2013.04.011
    [26] 叶玲玲, 钱俊彦, 查显伟. 基于Büchi自动机化简的JavaMOP监控器构造方法[J]. 桂林电子科技大学学报, 2019, 39(5): 374-378. doi: 10.3969/j.issn.1673-808X.2019.05.006
  • 期刊类型引用(0)

    其他类型引用(1)

图(1)  /  表(2)
计量
  • 文章访问数:  102
  • HTML全文浏览量:  87
  • PDF下载量:  1364
  • 被引次数: 1
出版历程
  • 收稿日期:  2021-03-06
  • 网络出版日期:  2023-04-05
  • 刊出日期:  2023-02-24

目录

/

返回文章
返回