从 Muller 到奇偶与 Rabin 自动机：保持（历史）确定性的最优变换

我们研究将使用 Muller 条件的自动机与博弈转换为使用奇偶或 Rabin 条件的等价形式。我们给出两种变换：一种将确定性 Muller 自动机转换为等价确定性奇偶自动机，另一种给出等价的历史确定性 Rabin 自动机。我们展示了强最优性结果：所得自动机在可通过复制原自动机状态而导出的自动机中规模最小。我们引入局部双射态射与历史确定性映射的概念，以形式化这些变换的正确性与最优性。所提变换基于一种称为交替环分解的新结构，其受 Zielonka 树启发并对其进行扩展。除提供自动机的最优变换外，交替环分解还给出关于其结构的基础信息。我们利用该信息清晰刻画了以不同接受条件重新标记自动机的可能性，并对奇偶自动机的一种规范形式进行系统研究。