软件学报

作者：王文胜，田聪，段振华

单位：王文胜，西安电子科技大学 计算理论与技术研究所, 陕西 西安 710071;综合业务网理论及关键技术国家重点实验室 (西安电子科技大学), 陕西 西安 71007111,田聪，西安电子科技大学 计算理论与技术研究所, 陕西 西安 710071;综合业务网理论及关键技术国家重点实验室 (西安电子科技大学), 陕西 西安 71007102,段振华，西安电子科技大学 计算理论与技术研究所, 陕西 西安 710071;综合业务网理论及关键技术国家重点实验室 (西安电子科技大学), 陕西 西安 71007103

关键词：Streett自动机;确定化;Rabin自动机;Parity自动机;工具

基金：科技创新2030—“新一代人工智能”重大项目(2018AAA0103202);国家自然科学基金(61732013);陕西省重点科技创新团队(2019TD-001)

自动机的确定化是将非确定性自动机转换为接收相同语言的确定性自动机, 是自动机理论的基本问题之一. ω自动机的确定化是诸多逻辑, 如SnS, CTL*, μ演算等, 判定过程的基础, 同时也是解决无限博弈求解问题的关键, 因此对ω自动机确定化的研究具有重要意义. 主要关注一类ω自动机——Streett自动机的确定化. 非确定性Streett自动机可以转换为等价的确定性Rabin或Parity自动机, 在前期工作中已经分别得到了状态复杂度最优以及渐进最优算法, 为了验证提出的算法的实际效果, 也为了形象地展示确定化过程, 开发一款支持Streett自动机确定化的工具是必要的. 首先介绍4种不同的Streett确定化结构: μ-Safra tree和H-Safra tree (最优)将Streett确定化为Rabin自动机, compact Streett Safra tree和LIR-H-Safra tree (渐进最优)将Streett确定化为Parity自动机; 然后, 根据Streett确定化算法, 基于开源工具GOAL (graphical tool for omega-automata and logics), 实现了Streett确定化工具NS2DR&PT, 以支持上述4种结构; 最后, 通过随机生成100个Streett自动机, 构造相应的测试集, 进行对比实验, 结果表明各结构状态复杂度的实际效果与理论论证一致, 此外, 对运行效率也进行了比较分析.

来源：2023年第8期

《软件学报》期刊编辑部

查看软件学报杂志2023年第8期