Streett自动机确定化工具.pdf
《Streett自动机确定化工具.pdf》由会员分享,可在线阅读,更多相关《Streett自动机确定化工具.pdf(15页珍藏版)》请在咨信网上搜索。
1、Streett 自动机确定化工具*王文胜1,2,田聪1,2,段振华1,21(西安电子科技大学计算理论与技术研究所,陕西西安710071)2(综合业务网理论及关键技术国家重点实验室(西安电子科技大学),陕西西安710071)通信作者:田聪,E-mail:摘要:自动机的确定化是将非确定性自动机转换为接收相同语言的确定性自动机,是自动机理论的基本问题之一.自动机的确定化是诸多逻辑,如 SnS,CTL*,演算等,判定过程的基础,同时也是解决无限博弈求解问题的关键,因此对 自动机确定化的研究具有重要意义.主要关注一类 自动机Streett 自动机的确定化.非确定性 Streett 自动机可以转换为等价的
2、确定性 Rabin 或 Parity 自动机,在前期工作中已经分别得到了状态复杂度最优以及渐进最优算法,为了验证提出的算法的实际效果,也为了形象地展示确定化过程,开发一款支持 Streett 自动机确定化的工具是必要的.首先介绍 4 种不同的 Streett 确定化结构:-Safratree 和 H-Safratree(最优)将 Streett 确定化为 Rabin 自动机,compactStreettSafratree 和 LIR-H-Safratree(渐进最优)将 Streett 确定化为 Parity 自动机;然后,根据 Streett 确定化算法,基于开源工具 GOAL(graphi
3、caltoolforomega-automataandlogics),实现了 Streett 确定化工具 NS2DR&PT,以支持上述 4 种结构;最后,通过随机生成 100 个 Streett 自动机,构造相应的测试集,进行对比实验,结果表明各结构状态复杂度的实际效果与理论论证一致,此外,对运行效率也进行了比较分析.关键词:Streett 自动机;确定化;Rabin 自动机;Parity 自动机;工具中图法分类号:TP311中文引用格式:王文胜,田聪,段振华.Streett自动机确定化工具.软件学报,2023,34(8):36593673.http:/ for Determinization
4、 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 no
5、ndeterministic 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
6、.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
7、 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.ThisstudyfirstintroducesfourdifferentStreettde
8、terminizationstructuresincluding-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
9、 of Software,2023,34(8):36593673doi:10.13328/ki.jos.006614http:/中国科学院软件研究所版权所有.Tel:+86-10-62562563Safratrees,compactStreettSafratrees,andLIR-H-Safratrees.ByH-Safratrees,whichareoptimal,and-Safratrees,deterministicRabintransformation automata are obtained.In addition,deterministic parity transformati
10、on 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.Be
11、sides,correspondingtestsetsareconstructedbyrandomlygenerating100Streettautomata,andcomparativeexperimentsarecarriedout.Resultsshowthattheactualeffectofstatecomplexityineachstructureisconsistentwiththeoreticalanalysis.Moreover,theefficiencyofdifferentalgorithmsiscomparedandanalyzed.Key words:Streetta
12、utomata;determinization;Rabinautomata;Parityautomata;toolAABAB自动机的确定化是自动机理论的基本问题之一,对于非确定性自动机,的确定化是指构造一个确定性自动机,使得和接收相同的语言.自动机于 20 世纪 60 年代首次提出,独特的接收条件使其可以接收无限字,用于解决数学和逻辑中的一些基本判定问题13,以及规约验证和非终止系统的合成4.在模型检测中,线性时序逻辑(lineartemporallogic,LTL)5是一种重要的规范语言,自动机理论要求首先要将 LTL 公式转换为 自动机,然后再对该自动机与待检测系统的计算结果进行分析6.而
13、 自动机确定化的应用更为广泛,最直观的是可以用于求补,例如,对于 Bchi 自动机,尽管在理论复杂度方面,不需要确定化的求补方法优于基于确定化的求补方法,但文献 7 中的实验结果表明基于确定化的求补方法在实际中具有更好的效果.此外,自动机的确定化是诸如SnS、CTL*、演算等逻辑判定过程的基础8;也有助于解决无限博弈求解问题,特别地,针对 LTL 公式博弈求解的工具,目前实际效果最好的 Strix9便是基于确定性 Parity 自动机实现的.因此,对 自动机确定化的研究至关重要,同时,这也是计算复杂度理论中的重要问题.根据接收条件的不同,自动机可具体分为 Bchi1、Streett10、Rab
14、in2以及 Parity11自动机等.其中,最常见的是 Bchi 自动机,它的接收条件是状态集合的子集,称为终态.本文对 Streett 自动机进行研究,其接收条件是由k 个 Streettpairs 组成的集合,每个 Streettpair 形如 Gi,Bi,Gi和 Bi均为状态集合的子集.相比于 Bchi 自动机,Streett自动机在描述系统的无限行为时更加简练12,因此,在对并发和反应系统的行为进行建模方面具有一定优势10.关于 Streett 自动机确定化的研究已经长达数十年之久.1992 年,Safra13首次创造性地提出了关于非确定性Streett 自动机(nondetermin
15、isticStreettautomata,NSA)的树状确定化结构,称为 StreettSafratree,基于该结构,NSA 可以确定化为 Rabin 或 Parity 自动机.此前,确定化为 Rabin 自动机的最优结构是通过减少 StreettSafratree中节点索引标签的冗余,以及使用批处理模式的节点命名规则得到的,称为-Safratree14;而确定化为 Parity 自动机的最优结构 compactStreettSafratree2是通过对 StreettSafratree 中的节点使用动态命名规则得到的.在我们的前期工作15中,分别对上述两种结构进行了改进.在-Safratr
16、ee 的基础上,引入了索引节点命名规则,即节点的名字仅根据索引标签决定,由此得到一种新的确定化结构 H-Safratree;接下来,通过在 H-Safratree 上增加记录节点生成顺序的集合 LIR(latertntroductionrecords),得到 LIR-H-Safratree.经过这两种结构,NSA 分别被确定化为具有更优状态复杂度的 Rabin(Rabinpair 数量有所增加)和 Parity 自动机,并且,文献 13 证明了状态复杂度已分别达到最优(紧界)以及渐进最优(渐近紧界).而关于 自动机确定化的工具,目前仅有 OmegaDet16、Spot17和 GOAL(grap
17、hicaltoolforomega-autamataandlogics)18.其中,工具 OmegaDet 是为了比较 Bchi 自动机的两种确定化算法 Safra8和 Muller-Schupp19的差异而开发的,遗憾的是,该工具后期并没有继续扩展和维护,至今仍只支持初始的两种算法,并且该工具缺少图形交互界面,可读性与可操作性较差.Spot 是自动机理论领域著名的开源工具,目前已支持各种类型自动机的确定化,但也不支持图形交互界面,为使用增加了难度.GOAL 是用于定义和操作 自动机、时序逻辑公式以及博弈的图形交互工具,有助于对计算机逻辑领域的理解.该工具提供 自动机的图形交互界面,用户可方便
18、、直观地修改状态、迁移和接收条件,或进行其他相关操作.经过版本的不断更新,该工具已较全面的支持 Bchi 自动机的确定化算法,但对其他 自动机的确定化操作涉及很少,特别是一些最新的算法.总之,现有的工具要么局限于 Bchi 自动机的确定化,要么不支持图形交互界面,无法满足我们的需求.因此,为了验证我们在文献 15 中提出的两种确定化结构的实际效果,也为了形象地展示确定化过程,使其更易理解,3660软件学报2023 年第 34 卷第 8 期我们需要开发一款可以自动化地完成 Streett 自动机确定化的工具,以代替人工繁琐的操作.而 Streett 自动机比Bchi 自动机更具普遍性、更复杂.同
19、时,Streett 自动机的确定化树状结构与算法比 Bchi 自动机的复杂得多,过程更抽象、繁杂,导致实现相应的支撑工具也更困难,并且工具的实现并不是对现有 Bchi 自动机确定化模块的简单修改,而是对整体设计的重新考量,这不仅要求对 Streett 自动机确定化结构与算法有深刻的理解,而且需要对数据结构的设计有着准确的把握.我们在前期的理论工作中已经对 Streett 自动机确定化过程有了深入探索,这为我们工具的实现打下了坚实基础;此外,幸运的是,具有强大图形交互界面的工具 GOAL 是开源的.基于此,本文设计实现了针对 Streett 自动机的确定化工具 NS2DR&PT,支持 4 种确定
20、化结构:-Safratree 和 H-Safratree,以及 compactStreettSafratree 和LIR-H-Safratree,用户可以根据自己的需求进行选择.通过调用 GOAL 的图形交互功能,可以轻松、直观地实现Streett 自动机的输入、定义和修改等,生成的确定性自动机也可以形象地展示出来,同时还可以查看每个状态对应的树状结构.随后,本文进行了实验性能比较,由于缺少现有的测试集,也为了实验的一般性,我们利用 GOAL中自动机随机生成的功能,随机生成了 100 个 NSA 作为测试集.使用工具 NS2DR&PT 对该测试集中所有的 NSA分别经 4 种确定化结构进行确定
21、化,对比各算法在实例中的性能差异,并以此证明工具 NS2DR&PT 的可用性.本文第 1 节介绍 自动机的定义与相关的接收条件.第 2 节对 4 种确定化结构进行介绍.第 3 节详细描述工具 NS2DR&PT 的整体框架和实现过程.第 4 节展示工具的工作效果以及测试集的实验结果.第 5 节总结全文并展望未来的工作.1 自动机一般自动机的接收条件是定义在状态上的,即接收条件的集合元素是状态;而迁移自动机的接收条件是定义在迁移上的.在确定化过程中,得到的确定性自动机为迁移自动机时,其状态数更少.而确定化为一般自动机时,需要为树状结构增加额外的集合来记录相关信息,导致状态复杂度增大,也就意味着工具
22、实现以及实验对比将付出更多的成本.同时,迁移自动机的比较足以说明各算法之间的性能差异.本文采用迁移自动机作为确定化得到的自动机.因此,本节将直接介绍接收条件定义在迁移上的 自动机.A定义 1.自动机.自动机是一个五元组=Q,Q0,其中,Q 是非空有限状态集合.Q0Q 是初始状态集合.是有限字母集合,称为字母表.A:Q2Q是迁移函数,具体地,(q,)表示读入 后,从 qQ 能到达的所有状态集合.是接收条件.NNInf()=|n N:(n)=NN 自动机可以接收无限字.一个无限字 是一个无限字母序列,每个字母都属于,形式化描述为:,其中,为非负整数集.因此,我们用(i)表示 中第 i(i0)个字母
23、.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:=G
24、1,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对于自动机以及无限字,若中存在一条关于
25、的可接收 run,则接收.接收的所有字组成的集合称为语言,记为 L().2 确定化结构ABAAB对于有限自动机的确定化,子集构造法20是正确且完备的,得到的自动机的状态是原自动机的状态集合.但该方法并不适用于 自动机,以 Bchi 自动机(最简单的 自动机)为例,利用子集构造法对其进行确定化会扩大接收的语言,即得到的自动机可能接收不被原 Bchi 自动机接收的字.例如图 1 所示的非确定性 Bchi 自动机,终态集合为b.图 2 是子集构造法得到的自动机,每个状态是由中状态组成的集合,终态集合为a,b,a,b,c.而无限字 p被拒绝却可以被接收.因此,自动机的确定化需要对子集构造法进行扩展,确
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- Streett 自动机 确定 化工
1、咨信平台为文档C2C交易模式,即用户上传的文档直接被用户下载,收益归上传人(含作者)所有;本站仅是提供信息存储空间和展示预览,仅对用户上传内容的表现方式做保护处理,对上载内容不做任何修改或编辑。所展示的作品文档包括内容和图片全部来源于网络用户和作者上传投稿,我们不确定上传用户享有完全著作权,根据《信息网络传播权保护条例》,如果侵犯了您的版权、权益或隐私,请联系我们,核实后会尽快下架及时删除,并可随时和客服了解处理情况,尊重保护知识产权我们共同努力。
2、文档的总页数、文档格式和文档大小以系统显示为准(内容中显示的页数不一定正确),网站客服只以系统显示的页数、文件格式、文档大小作为仲裁依据,平台无法对文档的真实性、完整性、权威性、准确性、专业性及其观点立场做任何保证或承诺,下载前须认真查看,确认无误后再购买,务必慎重购买;若有违法违纪将进行移交司法处理,若涉侵权平台将进行基本处罚并下架。
3、本站所有内容均由用户上传,付费前请自行鉴别,如您付费,意味着您已接受本站规则且自行承担风险,本站不进行额外附加服务,虚拟产品一经售出概不退款(未进行购买下载可退充值款),文档一经付费(服务费)、不意味着购买了该文档的版权,仅供个人/单位学习、研究之用,不得用于商业用途,未经授权,严禁复制、发行、汇编、翻译或者网络传播等,侵权必究。
4、如你看到网页展示的文档有www.zixin.com.cn水印,是因预览和防盗链等技术需要对页面进行转换压缩成图而已,我们并不对上传的文档进行任何编辑或修改,文档下载后都不会有水印标识(原文档上传前个别存留的除外),下载后原文更清晰;试题试卷类文档,如果标题没有明确说明有答案则都视为没有答案,请知晓;PPT和DOC文档可被视为“模板”,允许上传人保留章节、目录结构的情况下删减部份的内容;PDF文档不管是原文档转换或图片扫描而得,本站不作要求视为允许,下载前自行私信或留言给上传者【自信****多点】。
5、本文档所展示的图片、画像、字体、音乐的版权可能需版权方额外授权,请谨慎使用;网站提供的党政主题相关内容(国旗、国徽、党徽--等)目的在于配合国家政策宣传,仅限个人学习分享使用,禁止用于任何广告和商用目的。
6、文档遇到问题,请及时私信或留言给本站上传会员【自信****多点】,需本站解决可联系【 微信客服】、【 QQ客服】,若有其他问题请点击或扫码反馈【 服务填表】;文档侵犯商业秘密、侵犯著作权、侵犯人身权等,请点击“【 版权申诉】”(推荐),意见反馈和侵权处理邮箱:1219186828@qq.com;也可以拔打客服电话:4008-655-100;投诉/维权电话:4009-655-100。