Streett自动机确定化工具

TP311

Tool for the Determinization of Streett Automata
Author:
Affiliation:

Fund Project:

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

自动机的确定化是将非确定性自动机转换为接收相同语言的确定性自动机, 是自动机理论的基本问题之一.ω自动机的确定化是诸多逻辑, 如SnS, CTL*, μ演算等, 判定过程的基础, 同时也是解决无限博弈求解问题的关键, 因此对ω自动机确定化的研究具有重要意义.我们主要关注一类ω自动机——Streett自动机的确定化.非确定性Streett自动机可以转换为等价的确定性Rabin或parity自动机, 我们在前期工作中已经分别得到了状态复杂度最优以及渐进最优算法, 为了验证提出的算法的实际效果, 也为了形象地展示确定化过程, 开发一款支持Streett自动机确定化的工具是必要的.本文首先介绍四种不同的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, 以支持上述四种结构; 最后, 通过随机生成100个Streett自动机, 构造相应的测试集, 进行对比实验, 结果表明各结构状态复杂度的实际效果与理论论证一致, 此外, 对运行效率也进行了比较分析.

Abstract:

Determinization of a nondeterministic automaton is to construct another deterministic automaton that recognizes the same language as the nondeterministic one, which is one of the fundamental notions in automata theory. Determinization of ω automata serves as a natural basic step in the decision procedures of SnS, CTL*, μ-calculus etc. Meanwhile, it is also the key of solving infinite games. Therefore, it is of great significance to study the determinization of ω automata. We focus on a kind of ω automata called Streett automata. Nondeterministic Streett automata can be transformed into equivalent deterministic Rabin or parity automata. In our previous work, we have obtained the optimal and asymptotically optimal determinziation algorithms respectively. For evaluating the theoretical results of proposed algorithms and showing the procedure of determinization visually, it is necessary to develop a tool to support Streett determinization. In this paper, we first introduce four different Streett determinization constructions, 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 transition automata are obtained. In addition, deterministic parity transition automata are constructed via another two structures, where LIR-H-Safra trees are asymptotically optimal. Further, based on the open source software, named Graphical Tool for Omega-Automata and Logics (GOAL), we implement a tool for Streett determinization, named NS2DR & PT. Besides, a benchmark is constructed by randomly generating 100 Streett automata. We have implemented these determinization constructions on the benchmark in NS2DR & PT, which shows that experimental results are consistent with theoretical analyses on state complexity. Moreover, the efficiency of different algorithms is also compared and analyzed.

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

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