Streett自动机确定化工具

TP311

Tool for Determinization of Streett Automata
Author:
Affiliation:

Fund Project:

• 摘要
• |
• 图/表
• |
• 访问统计
• |
• 参考文献
• |
• 相似文献
• |
• 引证文献
• |
• 资源附件
• |
• 文章评论
摘要:

自动机的确定化是将非确定性自动机转换为接收相同语言的确定性自动机, 是自动机理论的基本问题之一. ω自动机的确定化是诸多逻辑, 如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自动机, 构造相应的测试集, 进行对比实验, 结果表明各结构状态复杂度的实际效果与理论论证一致, 此外, 对运行效率也进行了比较分析.

Abstract:

Determinization of an automaton refers to the transformation of a nondeterministic automaton into a deterministic automaton recognizing the same language, which is one of the fundamental notions in automata theory. Determinization of ω automata serves as a basic step in the decision procedures of SnS, CTL*, and μ-calculus. Meanwhile, it is also the key to solving infinite games. Therefore, studies on the determinization of ω automata are of great significance. This study focuses on a kind of ω automata called Streett automata. Nondeterministic Streett automata can be transformed into equivalent deterministic Rabin or Parity automata. In the previous work, the study has obtained algorithms with optimal state complexity and optimal asymptotical performance, respectively. Furthermore, it is necessary to develop a tool supporting Streett determinization, so as to evaluate the actual effect of proposed algorithms and show the procedure of determinization visually. This study first introduces four different Streett determinization structures including μ-Safra trees, H-Safra trees, compact Streett Safra trees, and LIR-H-Safra trees. By H-Safra trees, which are optimal, and μ-Safra trees, deterministic Rabin transformation 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-automata and logics (GOAL), the study develops a tool for Streett determinization and names it NS2DR&PT to support the four structures. Besides, corresponding test sets are constructed by randomly generating 100 Streett automata, and comparative experiments are carried out. Results show that the actual effect of state complexity in each structure is consistent with theoretical analysis. Moreover, the efficiency of different algorithms is compared and analyzed.

参考文献
相似文献
引证文献

• 点击次数:
• 下载次数:
• HTML阅读次数:
##### 历史
• 收稿日期:2021-08-24
• 最后修改日期:2021-10-14
• 录用日期:
• 在线发布日期: 2022-01-28
• 出版日期: