GFG中的规范性与变迁自动机
Canonicity in GFG and Transition-Based Automata
摘要：
有限字上的确定性自动机的最小化导致{ \em规范自动机。对于无限词上的确定性自动机，不存在规范的最小自动机，并且一种语言可能有不同的最小确定性Büchi（DBW）或co-Büchi（DCW）自动机。近年来，研究人员研究了{ \em good-for-games\/}（GFG）自动机--一种非确定性自动机，它可以以一种只依赖于过去的方式解决其非确定性选择。自动机在形式化方法中的几个应用，最值得注意的是传统上基于确定性自动机的合成，可以基于GFG自动机。DBW和DCW的{ \em极小化\/}问题是NP-完全的，GFG Büchi和co-Büchi自动机的{ \em极小化\/}问题是NP-完全的.另一方面，基于{ \em transition-based\/}接受的GFG co-Büchi自动机（GFG-tNCW）的最小化问题可以在多项式时间内求解.在这些自动机中，接受是由一组$α$转换定义的，如果一个运行只频繁地遍历$α$中的转换，则它是接受的。这就提出了最小的确定性和GFG自动机与过渡为基础的接受规范性的问题。在本文中，我们研究这个问题。我们从GFG-tNCW开始，并表明所有最小的GFG-tNCW的安全组件（即通过限制转换到$α$中的安全组件）是同构的，并且通过用$α$中的转换饱和自动机，我们得到所有最小的GFG-tNCW之间的同构。因此，可以在多项式时间内获得最小GFG-tNCW的标准型。我们继续使用基于转换的接受（tDCW）及其双tDBW。我们表明，在这里，虽然没有规范形式的最小自动机的存在，限制注意的安全组件是有用的，并意味着只有最小的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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
