-
题名Streett自动机确定化工具
- 1
-
-
作者
王文胜
田聪
段振华
-
机构
西安电子科技大学计算理论与技术研究所
综合业务网理论及关键技术国家重点实验室(西安电子科技大学)
-
出处
《软件学报》
EI
CSCD
北大核心
2023年第8期3659-3673,共15页
-
基金
科技创新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自动机,构造相应的测试集,进行对比实验,结果表明各结构状态复杂度的实际效果与理论论证一致,此外,对运行效率也进行了比较分析.
-
关键词
Streett自动机
确定化
Rabin自动机
parity自动机
工具
-
Keywords
Streett automata
determinization
Rabin automata
parity automata
tool
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-