论文标题
GFG和基于过渡的自动机中的规范性
Canonicity in GFG and Transition-Based Automata
论文作者
论文摘要
在有限词上最小化确定性自动机会导致{\ em canonical \/}自动机。对于无限单词上的确定性自动机，不存在规范的最小自动机，并且一种语言可能具有不同的最小确定性Büchi（DBW）或Co-Büchi（DCW）自动机。近年来，研究人员研究了{\ em Good-Games \/}（GFG）Automata-非确定性自动机，可以以仅取决于过去的方式来解决其非确定选择。自动机在形式方法中的几种应用，最著名的是基于确定性自动机的合成，可以基于GFG自动机。 DBW和DCW的{\ em最小化\/}问题是NP组的，并且它保留了GFGBüchi和Co-BüchiAutomata的NP完整问题。另一方面，可以在多项式时间内解决GFG Co-Büchi自动机的最小化自动机（GFG-TNCWS）。在这些自动机中，接受是由集合的$α$过渡定义的，如果它仅限于有限频繁地经常以$α$的方式穿越$α$，则可以接受。这提出了一个基于过渡的接受度的最小确定性和GFG自动机的规范性问题。在本文中，我们研究了这个问题。我们从GFG-TNCWS开始，并表明所有最小GFG-TNCW的安全组件（即，通过将其限制为$α$中的过渡而获得的安全组件（这些组件）都是同构的，并且通过$α$中的过渡饱和自动机，我们得到了所有极小的Minimalal gfg-tncws。因此，可以在多项式时间内获得最小GFG-TNCW的规范形式。我们继续以基于过渡的接受（TDCW）及其双重TDBW进行DCW。我们在这里表明，虽然没有最小自动机的规范形式，但限制对安全组件的关注是有用的，这意味着唯一没有规范形式的最小TDCW是GFG模型的过渡会导致严格较小的自动机的过渡，这确实具有规范的最小形式。
Minimization of deterministic automata on finite words results in a {\em canonical\/} automaton. For deterministic automata on infinite words, no canonical minimal automaton exists, and a language may have different minimal deterministic Büchi (DBW) or co-Büchi (DCW) automata. In recent years, researchers have studied {\em good-for-games\/} (GFG) automata -- nondeterministic automata that can resolve their nondeterministic choices in a way that only depends on the past. Several applications of automata in formal methods, most notably synthesis, that are traditionally based on deterministic automata, can instead be based on GFG automata. The {\em minimization\/} problem for DBW and DCW is NP-complete, and it stays NP-complete for GFG Büchi and co-Büchi automata. On the other hand, minimization of GFG co-Büchi automata with {\em transition-based\/} acceptance (GFG-tNCWs) can be solved in polynomial time. In these automata, acceptance is defined by a set $α$ of transitions, and a run is accepting if it traverses transitions in $α$ only finitely often. This raises the question of canonicity of minimal deterministic and GFG automata with transition-based acceptance. In this paper we study this problem. We start with GFG-tNCWs and show that the safe components (that is, these obtained by restricting the transitions to these not in $α$) of all minimal GFG-tNCWs are isomorphic, and that by saturating the automaton with transitions in $α$ we get isomorphism among all minimal GFG-tNCWs. Thus, a canonical form for minimal GFG-tNCWs can be obtained in polynomial time. We continue to DCWs with transition-based acceptance (tDCWs), and their dual tDBWs. We show that here, while no canonical form for minimal automata exists, restricting attention to the safe components is useful, and implies that the only minimal tDCWs that have no canonical form are these for which the transition to the GFG model results in strictly smaller automaton, which do have a canonical minimal form.
