基于转移的GFG自动机的最小化与规范化

尽管自动机在形式化方法中的许多应用可以使用非确定性自动机，但某些应用（最显著的是合成）需要确定性或good-for-games(GFG)自动机。后者是能够以仅依赖于过去的方式解决其非确定性选择的非确定性自动机。确定性Büchi和co-Büchi字自动机的最小化问题是NP完全的。特别地，不存在规范的最小确定性自动机，且一种语言可能具有不同的最小确定性自动机。我们描述了一种针对基于转移的接受条件的GFG co-Büchi字自动机的多项式时间最小化算法。因此，若一条运行仅有限次遍历一组指定的转移$\alpha$，则该运行是接受的。我们的算法基于对自动机施加的一系列变换，并在此之上定义一个最小商自动机。我们利用最小化算法证明了基于转移的GFG co-Büchi字自动机的规范性：所有最小自动机具有同构的安全分量（即通过将该自动机的转移限制为不在$\alpha$中的转移而获得的分量），并且一旦我们用$\alpha$-转移对自动机进行饱和，便得到完全同构。