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

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

Streett自动机确定化工具

自动机的确定化是将非确定性自动机转换为接收相同语言的确定性自动机,是自动机理论的基本问题之一.ω自动机的确定化是诸多逻辑,如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自动机,构造相应的测试集,进行对比实验,结果表明各结构状态复杂度的实际效果与理论论证一致,此外,对运行效率也进行了比较分析.

模糊Rabin自动机和模糊Game自动机的等价性

自动机是理论计算机的一个重要的研究内容.模糊Rabin自动机和模糊Game自动机是经典自动机的延续,给出了模糊Rabin自动机和模糊Game自动机的相关定义,讨论各自的内在性质,并得到了二者的等价关系.这进一步丰富了模糊自动机理论.