Streett自动机确定化工具
作者:
作者单位:

作者简介:

王文胜(1993-),男,博士,主要研究领域为自动机理论,时序逻辑;田聪(1981-),女,博士,教授,博士生导师,CCF杰出会员,主要研究领域为软件安全,智能软件开发方法,可信软件基础理论与方法;段振华(1948-),男,博士,教授,博士生导师,CCF会士,主要研究领域为形式化方法,可信软件基础理论与方法

通讯作者:

田聪,E-mail:ctian@mail.xidian.edu.cn

中图分类号:

TP311

基金项目:

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


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.

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

王文胜,田聪,段振华. Streett自动机确定化工具.软件学报,2023,34(8):3659-3673

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2021-08-24
  • 最后修改日期:2021-10-14
  • 录用日期:
  • 在线发布日期: 2022-01-28
  • 出版日期:
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号