| Büchi自动机确定化分析工具 |
| |
| 引用本文： | 马润哲,田聪,王文胜,段振华.Büchi自动机确定化分析工具[J].软件学报,2024,35(9). |
| |
| 作者姓名： | 马润哲 田聪 王文胜 段振华 |
| |
| 作者单位： | 西安电子科技大学 计算机科学与技术学院, 陕西 西安 710071 |
| |
| 基金项目： | 国家自然科学基金(62192734);国家重点研发计划(2018AAA0103202); |
| |
| 摘 要： | 无限字自动机的确定化是理论计算机研究重要的一部分,在形式化验证,时序逻辑,模型检测等方面有重要应用.自Büchi自动机提出半个世纪以来,其自动机的确定化算法始终是其中的基础.有别于当初只是在理论上对其大小上下界的探索,利用日新月异的高性能计算机技术不失为一种有效的辅助手段.为了深入研究非确定性Büchi自动机确定化算法的实现过程,我们希望重点研究确定化过程中的索引能否继续被优化的问题,实现了确定化研究工具NB2DR.可以对非确定性Büchi自动机进行高效的确定化,并通过工具提供的分析其确定化过程来达到对其确定化算法改进的目的.通过对生成的确定性无限字自动机的索引的深入分析来探索相关索引的理论.该工具还实现了可以根据需要的Büchi自动机的大小与字母表参数,生成确定化的Rabin自动机族,亦可以反向根据需要的指定索引的大小来生成全部Büchi自动机族,测试生成无限字自动机的等价性等功能.
|
| 关 键 词： | Büchi自动机 Rabin自动机 无限字自动机确定化 |
| 收稿时间： | 2023/9/18 0:00:00 |
| 修稿时间： | 2023/10/30 0:00:00 |
Tool for Determinization of Büchi Automata |
| |
| MA Run-Zhe,TIAN Cong,WANG Wen-Sheng,DUAN Zhen-Hua.Tool for Determinization of Büchi Automata[J].Journal of Software,2024,35(9). |
| |
| Authors: | MA Run-Zhe TIAN Cong WANG Wen-Sheng DUAN Zhen-Hua |
| |
| Affiliation: | School of Computer Science and Technology, Xidian University, Xi''an 710071, China |
| |
| Abstract: | |
| |
| Keywords: | |
|
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
|
