一句话：提出 GFG co-Büchi 迁移接受式字自动机的多项式最小化算法，并证明最小自动机可规范化。
形式方法中的许多自动机应用可以使用非确定性自动机，但合成等任务需要确定性或 good-for-games（GFG）自动机。确定性 Büchi 与 co-Büchi 字自动机的最小化是 NP 完全的，且不存在规范最小自动机，同一语言可有多个不同的最小确定性自动机。本文研究迁移接受式 GFG co-Büchi 字自动机：若一条运行只有限次经过指定迁移集合 α，则接受。作者给出一个多项式时间最小化算法，它通过对自动机施加一系列变换，并在此基础上定义最小商自动机。由此进一步证明规范化性质：所有最小自动机的不含 α 迁移的安全组件同构；当用 α 迁移饱和后，自动机完全同构。
While many applications of automata in formal methods can use nondeterministic automata, some applications, most notably synthesis, need deterministic or good-for-games (GFG) automata. The latter are nondeterministic automata that can resolve their nondeterministic choices in a way that only depends on the past. The minimization problem for deterministic B\"uchi and co-B\"uchi word automata is NP-complete. In particular, no canonical minimal deterministic automaton exists, and a language may have different minimal deterministic automata. We describe a polynomial minimization algorithm for GFG co-B\"uchi word automata with transition-based acceptance. Thus, a run is accepting if it traverses a set $\alpha$ of designated transitions only finitely often. Our algorithm is based on a sequence of transformations we apply to the automaton, on top of which a minimal quotient automaton is defined. We use our minimization algorithm to show canonicity for transition-based GFG co-B\"uchi word automata: all minimal automata have isomorphic safe components (namely components obtained by restricting the transitions to these not in $\alpha$) and once we saturate the automata with $\alpha$-transitions, we get full isomorphism.
@article{paperbot1675,
title = {Minimization and Canonization of GFG Transition-Based Automata},
author = {Bader Abu Radi and Orna Kupferman},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 3},
year = {2022},
doi = {10.46298/lmcs-18(3:16)2022}
}