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自动机的范形式进行了系统性研究。