论文部分内容阅读
自动机的确定化是将非确定性自动机转换为接收相同语言的确定性自动机,是自动机理论的基本问题之一。对于ω自动机（可以接收无限字的有限状态自动机）,其确定化有助于解决求补问题;是诸多逻辑,如SnS、CTL*、Δ-PDL、μ演算等,判定过程的基础;可以为模型检测提供理论前景;也是解决无限博弈求解问题的关键。因此,对ω自动机确定化的研究具有重要意义,同时,寻求最优的确定化算法也是计算复杂度理论中的重要问题。本文主要关注一类ω自动机――Streett自动机的确定化。通过树状确定化结构,而非简单的子集构造法,非确定性Streett（迁移）自动机（Nondeterministic Streett（Transition）Automaton,NS（T）A）可以确定化为Rabin或parity自动机。然而,Streett确定化为Rabin自动机的状态复杂度的上、下界仅渐进匹配;确定化为parity自动机的状态复杂度的上、下界之间仍有很大鸿沟。为了缩小上、下界之间的差距,本文围绕Streett自动机确定化的相关理论展开研究,具体工作概括为以下方面:第一,提出了Streett确定化为Rabin自动机的最优状态复杂度算法。在现有确定化结构μ-Safra树的基础上,引入索引节点命名规则,即节点的名字仅由其索引标签和在树中的位置决定,巧妙规避了节点名字对状态复杂度的影响,由此得到一种新的确定化结构H-Safra树,在保证等价性的前提下,降低了状态复杂度。具体地,对于具有n个状态和k个Streett pair的NSA,H-Safra树将其转换为具有n5n（n!）n（当k=ω（n）时）;n5nknk（当k=O（n）时）个状态的确定性Rabin迁移自动机（Deterministic Rabin Transition Automaton,DRTA）,而对于具有n个状态和k个Streett pair的NSTA,H-Safra树将其转换为具有n3nkn（k+2）个状态的DRTA,分别取代了由μ-Safra树得到的目前最好结果。进一步,定义完全Streett迁移自动机（包含大量的字母且允许所有可能的迁移）以及与之匹配且接收相同语言的语言博弈L-game,其中,完全Streett迁移自动机对应的每棵H-Safra树均唯一对应该L-game的一个位置,而该L-game的动作则通过不同H-Safra树之间的结构差异来定义。继而根据L-game与确定性Rabin自动机之间的关系,给出了NSTA确定化为DRTA时状态复杂度的下界,即n3nkn（k+2）,与本文得到的状态复杂度（上界）精确匹配,该结果表明H-Safra树对应的确定化算法具有最优状态复杂度,从而彻底终结了Streett确定化为Rabin自动机的状态复杂度问题。第二,提出了Streett确定化为parity自动机的渐进最优状态复杂度算法。该过程中,树状结构中的节点命名规则需要具备描述节点生成顺序的能力。为了充分利用H-Safra树的优势,在其基础上增加了记录节点生成顺序的集合LIR（Later Introduction Record）,所有节点按生成的先后顺序依次排列,由此得到了另一种可以降低状态复杂度的确定化结构LIR-H-Safra树。具体地,经LIR-H-Safra树将NSA确定化得到的确定性parity迁移自动机（Deterministic parity Transition Automaton,DPTA）具有3（n（n+1）-1）!（n!）n+1（当k=ω（n）时）;3（n（k+1）-1）!n!knk（当k=O（n）时）个状态,而将NSTA确定化得到的DPTA具有3（n（n+1）-1）!（n!）n+1个状态,分别取代了由紧凑型Streett Safra树（compact Streett Safra tree）得到的目前最好结果。同样地,基于完全Streett迁移自动机,定义了相应的L-game,该L-game接收的语言是完全Streett迁移自动机语言的补集。取完全Streett迁移自动机对应的所有LIR-H-Safra树的子集来对应L-game的各个位置,而L-game的动作则通过该子集中不同LIR-H-Safra树之间的结构差异来定义。由此给出了NSTA确定化为DPTA时状态复杂度的下界,即2Ω（nklognk）,与本文得到的状态复杂度（上界）渐进匹配,该结果表明LIR-H-Safra树对应的确定化算法具有渐进最优状态复杂度,从而大大缩小了Streett确定化为parity自动机的状态复杂度上、下界之间的鸿沟。第三,实现了Streett自动机确定化工具NS2DR＆PA。为了验证所提出算法的实际效果,也为了形象地展示确定化的过程,本文根据Streett自动机确定化算法,基于开源工具GOAL（Graphical Tool for Omega-Automata and Logics）,实现了Streett确定化工具NS2DR＆PA,支持四种确定化结构:μ-Safra树和H-Safra树,以及紧凑型Streett Safra树和LIR-H-Safra树。该工具支持图形交互功能,便于直观地完成Streett自动机的相关操作,可以形象地展示生成的确定性自动机,还可查看每个状态对应的树状结构。最后,通过随机生成100个Streett自动机来构造相应的测试集,进行对比实验,结果表明各结构状态复杂度的实际效果与理论论证一致,此外,对运行效率也进行了比较分析。