Streett自动机确定化工具.pdf

Streett 自动机确定化工具*王文胜1,2,田聪1,2,段振华1,21(西安电子科技大学计算理论与技术研究所,陕西西安710071)2(综合业务网理论及关键技术国家重点实验室(西安电子科技大学),陕西西安710071)通信作者:田聪,E-mail:摘要:自动机的确定化是将非确定性自动机转换为接收相同语言的确定性自动机,是自动机理论的基本问题之一.自动机的确定化是诸多逻辑,如 SnS,CTL*,演算等,判定过程的基础,同时也是解决无限博弈求解问题的关键,因此对 自动机确定化的研究具有重要意义.主要关注一类 自动机Streett 自动机的确定化.非确定性 Streett 自动机可以转换为等价的确定性 Rabin 或 Parity 自动机,在前期工作中已经分别得到了状态复杂度最优以及渐进最优算法,为了验证提出的算法的实际效果,也为了形象地展示确定化过程,开发一款支持 Streett 自动机确定化的工具是必要的.首先介绍 4 种不同的 Streett 确定化结构:-Safratree 和 H-Safratree(最优)将 Streett 确定化为 Rabin 自动机,compactStreettSafratree 和 LIR-H-Safratree(渐进最优)将 Streett 确定化为 Parity 自动机;然后,根据 Streett 确定化算法,基于开源工具 GOAL(graphicaltoolforomega-automataandlogics),实现了 Streett 确定化工具 NS2DR&PT,以支持上述 4 种结构;最后,通过随机生成 100 个 Streett 自动机,构造相应的测试集,进行对比实验,结果表明各结构状态复杂度的实际效果与理论论证一致,此外,对运行效率也进行了比较分析.关键词:Streett 自动机;确定化;Rabin 自动机;Parity 自动机;工具中图法分类号:TP311中文引用格式:王文胜,田聪,段振华.Streett自动机确定化工具.软件学报,2023,34(8):36593673.http:/ for Determinization of Streett AutomataWANGWen-Sheng1,2,TIANCong1,2,DUANZhen-Hua1,21(InstituteofComputingTheoryandTechnology,XidianUniversity,Xian710071,China)2(StateKeyLaboratoryofIntegratedServiceNetworks(XidianUniversity),Xian710071,China)Abstract:Determinization of an automaton refers to the transformation of a nondeterministic automaton into a deterministic automatonrecognizing the same language,which is one of the fundamental notions in automata theory.Determinization of automata serves as abasic step in the decision procedures of SnS,CTL*,and-calculus.Meanwhile,it is also the key to solving infinite games.Therefore,studiesonthedeterminizationofautomataareofgreatsignificance.ThisstudyfocusesonakindofautomatacalledStreettautomata.Nondeterministic Streett automata can be transformed into equivalent deterministic Rabin or Parity automata.In the previous work,thestudy has obtained algorithms with optimal state complexity and optimal asymptotical performance,respectively.Furthermore,it isnecessary to develop a tool supporting Streett determinization,so as to evaluate the actual effect of proposed algorithms and show theprocedureofdeterminizationvisually.ThisstudyfirstintroducesfourdifferentStreettdeterminizationstructuresincluding-Safratrees,H-*基金项目:科技创新 2030“新一代人工智能”重大项目(2018AAA0103202);国家自然科学基金(61732013);陕西省重点科技创新团队(2019TD-001)本文由“形式化方法与应用”专题特约编辑陈立前副教授、孙猛教授推荐.收稿时间:2021-08-24;修改时间:2021-10-14;采用时间:2022-01-10;jos 在线出版时间:2022-01-28CNKI 网络首发时间:2023-01-19软件学报ISSN1000-9825,CODENRUXUEWE-mail:Journal of Software,2023,34(8):36593673doi:10.13328/ki.jos.006614http:/中国科学院软件研究所版权所有.Tel:[phone]Safratrees,compactStreettSafratrees,andLIR-H-Safratrees.ByH-Safratrees,whichareoptimal,and-Safratrees,deterministicRabintransformation automata are obtained.In addition,deterministic parity transformation automata are constructed via another two structures,where LIR-H-Safra trees are asymptotically optimal.Furthermore,based on the open source software named graphical tool for omega-automataandlogics(GOAL),thestudydevelopsatoolforStreettdeterminizationandnamesitNS2DR&PTtosupportthefourstructures.Besides,correspondingtestsetsareconstructedbyrandomlygenerating100Streettautomata,andcomparativeexperimentsarecarriedout.Resultsshowthattheactualeffectofstatecomplexityineachstructureisconsistentwiththeoreticalanalysis.Moreover,theefficiencyofdifferentalgorithmsiscomparedandanalyzed.Key words:Streettautomata;determinization;Rabinautomata;Parityautomata;toolAABAB自动机的确定化是自动机理论的基本问题之一,对于非确定性自动机,的确定化是指构造一个确定性自动机,使得和接收相同的语言.自动机于 20 世纪 60 年代首次提出,独特的接收条件使其可以接收无限字,用于解决数学和逻辑中的一些基本判定问题13,以及规约验证和非终止系统的合成4.在模型检测中,线性时序逻辑(lineartemporallogic,LTL)5是一种重要的规范语言,自动机理论要求首先要将 LTL 公式转换为 自动机,然后再对该自动机与待检测系统的计算结果进行分析6.而 自动机确定化的应用更为广泛,最直观的是可以用于求补,例如,对于 Bchi 自动机,尽管在理论复杂度方面,不需要确定化的求补方法优于基于确定化的求补方法,但文献 7 中的实验结果表明基于确定化的求补方法在实际中具有更好的效果.此外,自动机的确定化是诸如SnS、CTL*、演算等逻辑判定过程的基础8;也有助于解决无限博弈求解问题,特别地,针对 LTL 公式博弈求解的工具,目前实际效果最好的 Strix9便是基于确定性 Parity 自动机实现的.因此,对 自动机确定化的研究至关重要,同时,这也是计算复杂度理论中的重要问题.根据接收条件的不同,自动机可具体分为 Bchi1、Streett10、Rabin2以及 Parity11自动机等.其中,最常见的是 Bchi 自动机,它的接收条件是状态集合的子集,称为终态.本文对 Streett 自动机进行研究,其接收条件是由k 个 Streettpairs 组成的集合,每个 Streettpair 形如 Gi,Bi,Gi和 Bi均为状态集合的子集.相比于 Bchi 自动机,Streett自动机在描述系统的无限行为时更加简练12,因此,在对并发和反应系统的行为进行建模方面具有一定优势10.关于 Streett 自动机确定化的研究已经长达数十年之久.1992 年,Safra13首次创造性地提出了关于非确定性Streett 自动机(nondeterministicStreettautomata,NSA)的树状确定化结构,称为 StreettSafratree,基于该结构,NSA 可以确定化为 Rabin 或 Parity 自动机.此前,确定化为 Rabin 自动机的最优结构是通过减少 StreettSafratree中节点索引标签的冗余,以及使用批处理模式的节点命名规则得到的,称为-Safratree14;而确定化为 Parity 自动机的最优结构 compactStreettSafratree2是通过对 StreettSafratree 中的节点使用动态命名规则得到的.在我们的前期工作15中,分别对上述两种结构进行了改进.在-Safratree 的基础上,引入了索引节点命名规则,即节点的名字仅根据索引标签决定,由此得到一种新的确定化结构 H-Safratree;接下来,通过在 H-Safratree 上增加记录节点生成顺序的集合 LIR(latertntroductionrecords),得到 LIR-H-Safratree.经过这两种结构,NSA 分别被确定化为具有更优状态复杂度的 Rabin(Rabinpair 数量有所增加)和 Parity 自动机,并且,文献 13 证明了状态复杂度已分别达到最优(紧界)以及渐进最优(渐近紧界).而关于 自动机确定化的工具,目前仅有 OmegaDet16、Spot17和 GOAL(graphicaltoolforomega-autamataandlogics)18.其中,工具 OmegaDet 是为了比较 Bchi 自动机的两种确定化算法 Safra8和 Muller-Schupp19的差异而开发的,遗憾的是,该工具后期并没有继续扩展和维护,至今仍只支持初始的两种算法,并且该工具缺少图形交互界面,可读性与可操作性较差.Spot 是自动机理论领域著名的开源工具,目前已支持各种类型自动机的确定化,但也不支持图形交互界面,为使用增加了难度.GOAL 是用于定义和操作 自动机、时序逻辑公式以及博弈的图形交互工具,有助于对计算机逻辑领域的理解.该工具提供 自动机的图形交互界面,用户可方便、直观地修改状态、迁移和接收条件,或进行其他相关操作.经过版本的不断更新,该工具已较全面的支持 Bchi 自动机的确定化算法,但对其他 自动机的确定化操作涉及很少,特别是一些最新的算法.总之,现有的工具要么局限于 Bchi 自动机的确定化,要么不支持图形交互界面,无法满足我们的需求.因此,为了验证我们在文献 15 中提出的两种确定化结构的实际效果,也为了形象地展示确定化过程,使其更易理解,3660软件学报2023 年第 34 卷第 8 期我们需要开发一款可以自动化地完成 Streett 自动机确定化的工具,以代替人工繁琐的操作.而 Streett 自动机比Bchi 自动机更具普遍性、更复杂.同时,Streett 自动机的确定化树状结构与算法比 Bchi 自动机的复杂得多,过程更抽象、繁杂,导致实现相应的支撑工具也更困难,并且工具的实现并不是对现有 Bchi 自动机确定化模块的简单修改,而是对整体设计的重新考量,这不仅要求对 Streett 自动机确定化结构与算法有深刻的理解,而且需要对数据结构的设计有着准确的把握.我们在前期的理论工作中已经对 Streett 自动机确定化过程有了深入探索,这为我们工具的实现打下了坚实基础;此外,幸运的是,具有强大图形交互界面的工具 GOAL 是开源的.基于此,本文设计实现了针对 Streett 自动机的确定化工具 NS2DR&PT,支持 4 种确定化结构:-Safratree 和 H-Safratree,以及 compactStreettSafratree 和LIR-H-Safratree,用户可以根据自己的需求进行选择.通过调用 GOAL 的图形交互功能,可以轻松、直观地实现Streett 自动机的输入、定义和修改等,生成的确定性自动机也可以形象地展示出来,同时还可以查看每个状态对应的树状结构.随后,本文进行了实验性能比较,由于缺少现有的测试集,也为了实验的一般性,我们利用 GOAL中自动机随机生成的功能,随机生成了 100 个 NSA 作为测试集.使用工具 NS2DR&PT 对该测试集中所有的 NSA分别经 4 种确定化结构进行确定化,对比各算法在实例中的性能差异,并以此证明工具 NS2DR&PT 的可用性.本文第 1 节介绍 自动机的定义与相关的接收条件.第 2 节对 4 种确定化结构进行介绍.第 3 节详细描述工具 NS2DR&PT 的整体框架和实现过程.第 4 节展示工具的工作效果以及测试集的实验结果.第 5 节总结全文并展望未来的工作.1 自动机一般自动机的接收条件是定义在状态上的,即接收条件的集合元素是状态;而迁移自动机的接收条件是定义在迁移上的.在确定化过程中,得到的确定性自动机为迁移自动机时,其状态数更少.而确定化为一般自动机时,需要为树状结构增加额外的集合来记录相关信息,导致状态复杂度增大,也就意味着工具实现以及实验对比将付出更多的成本.同时,迁移自动机的比较足以说明各算法之间的性能差异.本文采用迁移自动机作为确定化得到的自动机.因此,本节将直接介绍接收条件定义在迁移上的 自动机.A定义 1.自动机.自动机是一个五元组=Q,Q0,其中,Q 是非空有限状态集合.Q0Q 是初始状态集合.是有限字母集合,称为字母表.A:Q2Q是迁移函数,具体地,(q,)表示读入 后,从 qQ 能到达的所有状态集合.是接收条件.NNInf()=|n N:(n)=NN 自动机可以接收无限字.一个无限字 是一个无限字母序列,每个字母都属于,形式化描述为:,其中,为非负整数集.因此,我们用(i)表示 中第 i(i0)个字母.Inf()表示 中出现无限次的字母集合,即,这里n的意思是在中存在无限个不同的 n.ANNAAInf()=Inf|n N:(n)=Inf 自动机关于无限字 的一条运行(run)是一个无限迁移序列:,使得(0)=(q0,(0),q1),其中,q0Q0,q1(q0,(0),并且对于所有的 i,(i)=(qi,(i),qi+1),其中,qi+1(qi,(i).如果|Q0|=1,并且对于任意qQ,满足|(q,)|1,那么被称为确定性的;否则被称为非确定性的.和无限字类似,用 Inf()表示 中出现无限次的迁移集合,即.不同的接收条件定义不同的自动机,这里我们仅展示其中的 3 种.Streett:=G1,B1,G2,B2,Gk,Bk,其中 Gi,Bi,称 Gi,Bi 为 Streettpair.是可接收的当且仅当对于所有的 1ik,都有 Inf()Gi或者 Inf()Bi=.Rabin:=A1,R1,A2,R2,Ak,Rk,其中 Ai,Ri,称 Ai,Ri 为 Rabinpair.是可接收的当且仅当存在 i(1ik),使得 Inf()Ai并且 Inf()Ri=.Parity:=1,2,2k且 122k=,称 i为 priority.是可接收的当且仅当满足 Inf()i的最王文胜等:Streett 自动机确定化工具3661小索引 i 是偶数.AAAAA对于自动机以及无限字,若中存在一条关于 的可接收 run,则接收.接收的所有字组成的集合称为语言,记为 L().2 确定化结构ABAAB对于有限自动机的确定化,子集构造法20是正确且完备的,得到的自动机的状态是原自动机的状态集合.但该方法并不适用于 自动机,以 Bchi 自动机(最简单的 自动机)为例,利用子集构造法对其进行确定化会扩大接收的语言,即得到的自动机可能接收不被原 Bchi 自动机接收的字.例如图 1 所示的非确定性 Bchi 自动机,终态集合为b.图 2 是子集构造法得到的自动机,每个状态是由中状态组成的集合,终态集合为a,b,a,b,c.而无限字 p被拒绝却可以被接收.因此,自动机的确定化需要对子集构造法进行扩展,确定化得到的自动机不再是原自动机的状态集合,而是由状态的子集组成的树状结构.对于 NSA 的确定化过程,概括来讲,首先构造初始状态,即初始树状结构;然后自初始树开始,依次读入字母表中的字母,每读入一个字母,树状结构都会发生转换,得到的新树即为一个新状态,期间需要记录树中某些节点信息,以此循环进行,直至没有新树生成,所有的树构成状态集合,树之间的转换关系便是迁移;最后根据迁移中的节点信息定义自动机的接收条件.由此便可得到所需的确定性自动机.本节将对 Streett 自动机的 4 种树状确定化结构(-Safratree,H-Safratree,compactStreettSafratree 以及 LIR-H-Safratree)逐一进行介绍.首先介绍将 NSA 确定化为确定性 Rabin 迁移自动机(deterministicRabintransitionautomata,DRTA)的两种结构.2.1 -Safra tree 和 H-Safra tree-Safratree 与 H-Safratree 的不同之处仅在于树中节点的命名方式,除此之外,它们具有相同的结构,称为包含状态和索引标签的结构有序树.给定一个具有 n 个状态和 k 个 Streettpairs 的 NSAS=(,Q,Q0,),S 的一棵包含状态和索引标签的结构有序树是一个五元组 Tsi=To,V,l,h,stor,其中,To是一棵有序树.V 是 To中所有节点的集合.l:V2Q是节点的状态标签(statelabel),并且满足:每个节点的状态标签等于它所有孩子节点状态标签的并集;任何两个兄弟节点的状态标签都不相交.h:V2k是节点的索引标签(indexlabel).根节点的索引标签为 k=1,2,k.每个非根节点 的索引标签都包含在其父节点 p的索引标签中,最多比父节点的索引标签少一个元素.非叶子节点至少有一个索引标签是它的真子集的子节点.stor 定义兄弟节点之间的结构顺序.对于非根节点,令 j()=max(h(p)0)h(),stor 的意思是对于任意两个兄弟节点 和,的位置在 的右侧当且仅当 j()j();或 j()=j()且 比 先生成.图 3 是一棵具有 9 个节点的包含状态和索引标签的结构有序树,节点内的状态集合是状态标签,集合 h 表示索引标签.在此基础上,不同的节点命名规则将对应不同的确定化结构.-Safratree 是 2012 年由 Cai 等人14提出的,应用批处理模式的节点命名规则,将节点划分到具有不同名字的分支,接着为分支中的每个节点命名,具体如下.规则 1.批处理模式命名规则 Mb14.如果 是名字为 b 的分支中的第 i 个节点,那么 的名字为 b.i,即Mb()=b.i.pppbcapA图1非确定性 Bchi 自动机pppaa,ba,b,cB图2经子集构造法得到的自动机3662软件学报2023 年第 34 卷第 8 期由此可得-Safratree 的定义.定义 1.-Safratree14.给定一个 NSAS,它的一棵-Safratree 是一个二元组 Tsi,Mb,其中,Tsi是关于 S 的一棵包含状态和索引标签的结构有序树,Mb是批处理节点命名规则.图 4 是将图 3 中的节点按照规则 1 命名得到的一棵-Safratree,包含 3 个分支,即1.1,1.2,1.3,1.4,2.1,2.2,2.3,3.1,3.2.图 4 中节点名字用加粗字体表示.而我们在前期工作15中提出的 H-Safratree 对应索引节点命名规则.节点的名字仅依赖于其索引标签与位置,即给定一棵包含状态和索引标签的结构有序树,其中每个节点的名字便唯一确定.规则 2.索引节点命名规则 Mh15.对于根节点 r,Mh(r)=.对于第 2 层的节点,Mh()=j()i+1,其中 i=|是 的左兄弟,且 j()=j()|.对于其他的节点,Mh()=Mh(p).j()i+1.应用该规则,我们可以得到 H-Safratree.定义 2.H-Safratree15.给定一个 NSAS,它的一棵 H-Safratree 是一个二元组 Tsi,Mh,其中,Tsi是关于 S 的一棵包含状态和索引标签的结构有序树,Mh是索引节点命名规则.将图 3 中的每个节点按照规则 2 命名,得到一棵 H-Safratree,如图 5 所示.图 5 中加粗字体表示节点的名字.h=1,2,3h=1,2h=1h=2h=h=h=2h=2,3h=b,da,b,c,dbdbda,ca,ca,c3131.2131.21.111131.1131.11.2111.3111.31.21图5一棵 H-Safratree 2.2 Compact Streett Safra tree 和 LIR-H-Safra tree下面对将 NSA 确定化为确定性 Parity 迁移自动机(deterministicParitytransitionautomata,DPTA)的两种结构进行介绍.2007 年,Piterman12通过动态节点命名,得到了 compactStreettSafratree.定义 3.CompactStreettSafratree12.给定一个 NSAS,它的一棵 compactStreettSafratree 是一个五元组 To,V,l,h,Md,其中,To,V,l,h 与 Tsi中的定义相同,Md:Vn(k+1)是动态命名规则,节点按生成顺序依次、连续命名.图 6 是一棵 compactStreettSafratree,节点的名字用加粗字体表示.除了节点命名方式不同,compactStreettSafratree 并不要求兄弟节点之间满足结构顺序.h=1,2,3h=1,2h=1h=2h=h=h=2h=2,3h=b,da,b,c,dbdbda,ca,ca,c图3一棵包含状态和索引标签的结构有序树h=1,2,3h=1,2h=1h=2h=h=h=2h=2,3h=b,da,b,c,dbdbda,ca,ca,c1.11.21.31.43.13.22.22.12.3图4一棵-Safratree王文胜等:Streett 自动机确定化工具3663值得注意的是,在确定化过程中,-Safratree 和 H-Safratree 要求叶子节点不断生成孩子节点,直至叶子节点的索引标签满足相应的条件,而 compactStreettSafratree 仅要求叶子节点生成一次孩子节点,因此,一般情况下其深度偏小.接下来,我们前期工作15中提出的 LIR-H-Safratree 是在 H-Safratree 的基础上增加记录节点生成顺序的集合得到的.定义 4.LIR-H-Safratree15.给定一个 NSAS,它的一棵 LIR-H-Safratree 是一个二元组 H,LIR,其中,H 是关于 S 的一棵 H-Safratree,LIR 是记录 H 中所有节点生成顺序的集合.图 7 是一棵 LIR-H-Safratree,LIR 中各节点用其名字表示,按生成的先后顺序依次排列.3 工具实现本文在 GOAL 的基础上设计实现了关于 NSA 的确定化工具 NS2DR&PT,该工具是基于 Windows 平台采用Java 语言开发的,整体框架如图 8 所示,支持 4 种 NSA 确定化结构(即图 8 中的树状结构,确定化算法详见相应的参考文献).输入构造初始树构造状态迁移系统构造接收条件DRTADPTADTDT1DT2DT3初始树状态迁移系统树状结构TNSA接收条件输出更新状态标签生成兄弟节点水平合并垂直合并更新节点命名生成孩子节点TTiiTiQDTtotoDT1T1T2TmTiQDT2m构造状态迁移系统图8NS2DR&PT 的框架h=1,2,3h=1,2h=1h=2h=2h=2,3b,da,b,c,da,ca,cdb123645图6一棵 compactStreettSafratreeh=1,2,3h=1,2h=1h=2h=h=h=2h=2,3h=b,da,b,c,dbdbda,ca,ca,c1131LIR=,31,31.21,11,31.21.11,11.31,11.3111.31.2131.11.2131.21.1131.2131.1111.31.21,31.11,31.11.21图7一棵 LIR-H-Safratree3664软件学报2023 年第 34 卷第 8 期-Safratree(NSA 确定化为 DRTA)14.H-Safratree(NSA 确定化为 DRTA)pactStreettSafratree(NSA 确定化为 DPTA)12.LIR-H-Safratree(NSA 确定化为 DPTA)15.在该工具中,输入、输出操作均调用 GOAL 的相关模块,充分利用其强大的图形交互界面.下面我们主要对构造初始树、构造状态迁移系统和构造接收条件这 3 个模块进行介绍.3.1 构造初始树为了将 NSAS=Q,Q0,确定化为 DRTA 或 DPTADT=QDT,QDT0,DT,DT,首先要构造相应的初始树.除了初始 compactStreettSafratree 是单节点标记树,其他 3 种初始结构均为单分支标记树.图 9 是一个 NSA 关于字母 的相关迁移片段,若初始状态为 a 和 d,其初始树如图 10 所示,T0、H0、LH0、Tc0分别是对应的初始-Safratree、H-Safratree、LIR-H-Safratree 以及 compactStreettSafratree.初始树将作为确定化后自动机 DT 的初始状态.在程序中,基本的数据结构是树,树中的节点包含标签、名字、父亲和孩子等元素,同时,为了便于展示与比较,我们定义树的特征字符串.对于一棵具有 m 个节点的树 T,从根节点开始,层层递进,每一层从左至右,所有节点依次排列的顺序为 1,2,m.那么 T 的特征字符串为 F(T)=F(1)F(2)F(m),其中,对于任意 1im,F(i)=f(i)f(i1)f(ik),i1,ik为 i的所有孩子节点,并且,f(i)=name-l-h表示节点 i的名字、状态标签、索引标签的连接,对于 H-Safratree,节点的名字由索引标签唯一决定,因此只需记录索引标签,即 f(i)=l-h.而对于 LIR-H-Safratree,其特征字符串 F(T)=F(i)F(m)-LIR.那么,图 10 中的初始树在程序中对应的特征字符串分别为:F(T0)=1.1-a,d-1,21.2-a,d-11.2-a,d-11.3-a,d-1.3-a,d-;F(H0)=a,d-1,2a,d-1a,d-1a,d-a,d-;F(LH0)=a,d-1,2a,d-1a,d-1a,d-a,d-,21,21.11;F(Tc0)=1-a,d-1,2.3.2 构造状态迁移系统自初始树开始,依次读入 中的字母,每个字母的读入都是树状结构的转换,由此循环进行,直至没有新树生成,此间,需比较特征字符串来判断生成的新树是否已存在.经过循环转换过程,每棵树都对应唯一的特征字符串,均作为 DT 的一个状态存在,生成的所有不同的树构成DT 的状态集合 QDT,而迁移集合 DT的元素对应树与树之间的转换.因此,在工具 NS2DR&PT 中,最关键的是树的转换环节,即当一棵树读入一个字母时,如何得到另一棵树.该转换过程需要 6 步完成,是整个工具的核心.第 1 步.更新状态标签.当一棵树读入一个字母时,树中节点的状态标签需要根据 NSA 中的相关迁移进行更新.第 2 步.生成兄弟节点.当节点的状态标签更新之后,需要检查是否有状态经过了某个 Streettpair,若有,则将这些状态提取出来,作为一个新生成的兄弟节点的状态标签,同时需定义该节点的索引标签.兄弟节点之间按结构badcG1=b,d,B1=cG2=a,c,B2=图9一个 NSA 关于 的相关迁移h=1,2h=1h=h=1,2h=1,2h=1h=1h=h=1.11.221211h=1,221.1121.111.3a,da,da,da,da,da,da,da,da,da,dT0H0LH0Tc0LIR=,21,21.11图104 种结构的初始树王文胜等:Streett 自动机确定化工具3665顺序排列.需要注意的是,Piterman 的确定化算法并不要求兄弟节点之间满足结构顺序.第 3 步.水平合并.此时兄弟节点的状态标签之间可能存在交集,违反节点状态标签的定义.因此,需要将重复的状态从某些节点的状态标签中删除.之后,树中可能存在状态标签为空的节点,需要将其删除,在此,删除的空节点称为拒绝节点(rejectingnodes),用于构造接收条件.第 4 步.垂直合并.当前树中兄弟节点之间的状态标签已不相交,且不存在空节点,但可能存在某个节点的索引标签与其各个孩子节点的索引标签相等,这违反了节点索引标签的定义.因此,需要删除该节点的所有后代节点,并称此类节点为接收节点(acceptingnodes),同样用于构造接收条件.删除的后代节点为拒绝节点.第 5 步.更新节点命名.因之前步骤中有节点被删除,导致可能存在名字不符合命名规则的节点.因此,需要对节点的命名进行更新.名字经过修改的节点同样称为拒绝节点.第 6 步.生成孩子节点.经过前 5 步,树中删除了某些节点.因此,需要生成新的孩子节点来补充,以便在读入其他字母时更快的得到接收节点.值得注意的是,在-Safratree,H-Safratree 和 LIR-H-Safratree 中,每个叶子节点生成的孩子将作为新的叶子节点,继续生成孩子节点,重复该操作,直至无新节点生成.而对于 compactStreettSafratree,每个叶子节点生成的孩子将不再生成新节点.T T经过以上 6 步,一棵树 T 读入字母 可以转换得到另一棵树 T.然后,通过匹配特征字符串来判断 T是否已存在,若不存在,T将作为 DT 的一个新状态,作为 DT 的一条新迁移;若存在,DT 仅新增一条迁移,该迁移指向与 T具有相同特征字符串的状态.同时,在此过程中,需要对接收、拒绝节点进行记录.对-Safratree 和 H-Safratree,每一次转换均需定义集合 Sigacc和 Sigrej,其中 Sigacc记录在此过程中所有的接收节点,Sigrej记录拒绝节点,集合中的节点用其名字表示,空集合即该过程中无接收或拒绝节点.而对于 compactStreettSafratree 和 LIR-HSafratree,树中包含所有节点的生成顺序,每一次转换只需定义二元组 Sig=(i,st)来记录接收和拒绝节点中生成顺序最小的节点,i 表示该节点的名字或在 LIR 中的位置,st 代表该节点是接收(acc)或拒绝(rej)的,Sig=表明该过程无接收或拒绝节点.对于图 10 中的 4 种初始树,读入,分别得到一棵新树,如图 11 所示,对应的特征字符串分别为:F(T1)=1.1-a,b,c-1,21.2-b-12.1-a,c-21.2-b-11.3-b-2.1-a,c-22.2-a,c-1.3-b-2.2-a,c-;F(H1)=a,b,c-1,2b-1a,c-2b-1b-a,c-2a,c-b-a,c-;F(LH1)=a,b,c-1,2b-1a,c-2b-1b-a,c-2a,c-b-a,c-,21,11,21.11,11.21;F(Tc1)=1-a,b,c-1,22-a,b,c-12-a,b,c-1.T0 H0 LH0 Tc0 每棵树均作为对应自动机的新状态,转换过程作为迁移,并且,在T1中,Sigacc=1.2,Sigrej=1.3;在H1中,Sigacc=21,Sigrej=21.11;在LH1中,Sig=(2,acc);在Tc1中,Sig=.经过构造状态迁移系统模块,DT 的迁移系统便构造完成,最后,将确定接收条件 DT.a,b,ca,b,ca,b,ca,b,ca,b,cba,ca,cbba,ca,cb1.11.22111ba,cba,c2111122.12.21.3h=1,2h=1,2h=1,2h=1h=1h=2h=2h=h=h=1h=1h=1,2h=h=h=h=2h=T1H1LH1Tc1LIR=,21,11,21.11,11.2111.2121.1121.1111.21图11初始树读入 的结果3666软件学报2023 年第 34 卷第 8 期 3.3 构造接收条件该模块根据每一条迁移记录的 Sig*(Sigacc、Sigrej或 Sig)来分配该迁移.若 DT 为 DRTA,接收条件 DT为 Rabinpair(AM,RM)组成的集合,其中,AM是迁移集合,且迁移中存在名字为 M 的接收节点;RM是迁移集合,且迁移中存在名字为 M 的拒绝节点.若 DT 为 DPTA,接收条件 DT为 prioritym组成的集合,其中,m亦为迁移集合,当 m 为偶数时,m包含Sig=(m/2,acc)的迁移,当 m 为奇数时,m包含 Sig=(m+1)/2,rej)的迁移,特别地,m中最后一个 priority 包含 Sig=或 Sig=(1,rej)(根节点为拒绝节点)的迁移.T0 Tc0 对于图 10 至图 11 的迁移,(1)在T1中,Sigacc=1.2且 Sigrej=1.3,则该迁移属于 A1.2以及 R1.3;(2)在H0H1中,Sigacc=21且 Sigrej=21.11,则该迁移属于 A2以及 R2.1;(3)在 LH0LH1中,Sig=(2,acc),则该迁移属于 4;(4)在Tc1中,Sig=,则该迁移属于 DT中最后一个 priority2N+1,其中,N 为 compactStreettSafratree中允许的最多节点数.在程序实现中,该过程是运行时动态分配的(on-the-fly),当一条迁移构造完成,便立即对其进行分配,而非待整个迁移系统构造完成之后再逐一分配,这样可以避免记录所有迁移的 Sig*,减少内存消耗.至此,迁移系统及其接收条件即构成与 NS