We study transformations of automata and games using Muller conditions into equivalent ones using parity or Rabin conditions. We present two transformations, one that turns a deterministic Muller automaton into an equivalent deterministic parity automaton, and another that provides an equivalent history-deterministic Rabin automaton. We show a strong optimality result: the obtained automata are minimal amongst those that can be derived from the original automaton by duplication of states. We introduce the notions of locally bijective morphisms and history-deterministic mappings to formalise the correctness and optimality of these transformations. The proposed transformations are based on a novel structure, called the alternating cycle decomposition, inspired by and extending Zielonka trees. In addition to providing optimal transformations of automata, the alternating cycle decomposition offers fundamental information on their structure. We use this information to give crisp characterisations on the possibility of relabelling automata with different acceptance conditions and to perform a systematic study of a normal form for parity automata.
翻译:我们研究了利用Muller条件的自动机与博弈向等价parity或Rabin条件的变换。我们提出两种变换:一种将确定型Muller自动机转化为等价的确定型parity自动机,另一种则提供等价的历史确定型Rabin自动机。我们证明了一个强最优性结果:所得到的自动机是所有可通过状态复制从原始自动机衍生出的自动机中规模最小的。我们引入局部双射态射和历史确定性映射的概念,以形式化这些变换的正确性与最优性。所提出的变换基于一种名为交替环分解的新颖结构,该结构受Zielonka树启发并对其进行了扩展。除了为自动机提供最优变换外,交替环分解还揭示了自动机结构的基本信息。我们利用这些信息对具有不同接受条件的自动机重标号可能性给出了清晰刻画,并对parity自动机的一种范式进行了系统性研究。