Büchi自动机确定化分析工具  

Tool for Determinization of Büchi Automata

作　　者：马润哲 田聪[1] 王文胜 段振华[1] MA Run-Zhe;TIAN Cong;WANG Wen-Sheng;DUAN Zhen-Hua(School of Computer Science and Technology,Xidian University,Xi’an 710071,China)

机构地区：[1]西安电子科技大学计算机科学与技术学院,陕西西安710071

出　　处：《软件学报》2024年第9期4310-4323,共14页Journal of Software

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

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

分 类 号：TP301[自动化与计算机技术—计算机系统结构]