Büchi自动机确定化分析工具
CSTR:
作者:
作者单位:

作者简介:

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

通讯作者:

田聪, E-mail: ctian@mail.xidian.edu.cn;王文胜, E-mail: wswang@xidian.edu.cn

中图分类号:

基金项目:

国家自然科学基金(62192734); 国家重点研发计划(2018AAA0103202)


Tool for Determinization of Büchi Automata
Author:
Affiliation:

Fund Project:

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

    无限字自动机的确定化是理论计算机研究重要的一部分, 在形式化验证, 时序逻辑, 模型检测等方面有重要应用. 自Büchi自动机提出半个世纪以来, 其自动机的确定化算法始终是其中的基础. 有别于当初只是在理论上对其大小上下界的探索, 利用日新月异的高性能计算机技术不失为一种有效的辅助手段. 为了深入研究非确定性Büchi自动机确定化算法的实现过程, 希望重点研究确定化过程中的索引能否继续被优化的问题, 实现确定化研究工具NB2DR. 可以对非确定性Büchi自动机进行高效的确定化, 并通过工具提供的分析其确定化过程来达到对其确定化算法改进的目的. 通过对生成的确定性无限字自动机的索引的深入分析来探索相关索引的理论. 该工具还实现了可以根据需要的Büchi自动机的大小与字母表参数, 生成确定化的Rabin自动机族, 亦可以反向根据需要的指定索引的大小来生成全部Büchi自动机族, 测试生成无限字自动机的等价性等功能.

    Abstract:

    The ω automata determinization is an important part of theoretical computer research and has important applications in formal verification, sequential logic, and model checking. Since the Büchi automata was proposed for half a century, its deterministic algorithm has always been the basis. Different from the exploration of the upper and lower bounds of its size in theory at the beginning, the use of ever-changing high-performance computer technology is an effective auxiliary means. To deeply study the implementation process of the deterministic algorithm of non-deterministic Büchi automata, this study focuses on the question of whether the index can continue to be optimized and realizes the deterministic research tool NB2DR. The non-deterministic Büchi automata can be determined efficiently, and the determinization algorithm can be improved by analyzing the determinization process provided by the tool. A theoretical upper bound on correlation indexing is explored through an in-depth analysis of the indexing of generated deterministic ω automata. The tool also realizes that the deterministic Rabin automaton family can be generated according to the size of the required Büchi automaton and the alphabet parameters. It can also be reversed to generate all the Büchi automata families according to the size of the specified index required and test the equivalence of ω functions.

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

马润哲,田聪,王文胜,段振华. Büchi自动机确定化分析工具.软件学报,2024,35(9):4310-4323

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

京公网安备 11040202500063号