Optimal Transformations of Muller Conditions

TL;DR

This paper introduces an optimal transformation method from Muller to parity automata, extending Zielonka's construction, with applications in automata determinisation and relabelling, achieving minimal automaton size and priorities.

Contribution

It presents the alternating cycle decomposition transformation, proving its strong optimality in producing minimal parity automata from Muller automata.

Findings

The transformation yields minimal size and priorities in parity automata.

Improves determinisation process of Büchi automata into parity automata.

Provides characterisations for automata relabelling with different acceptance conditions.

Abstract

In this paper, we are interested in automata over infinite words and infinite duration games, that we view as general transition systems. We study transformations of systems using a Muller condition into ones using a parity condition, extending Zielonka's construction. We introduce the alternating cycle decomposition transformation, and we prove a strong optimality result: for any given deterministic Muller automaton, the obtained parity automaton is minimal both in size and number of priorities among those automata admitting a morphism into the original Muller automaton. We give two applications. The first is an improvement in the process of determinisation of B\"uchi automata into parity automata by Piterman and Schewe. The second is to present characterisations on the possibility of relabelling automata with different acceptance conditions.