On the size of good-for-games Rabin automata and its link with the memory in Muller games

TL;DR

This paper explores the relationship between good-for-games Rabin automata recognizing Muller languages and the memory needed for winning Muller games, showing minimal automata size matches minimal memory and can be exponentially smaller than deterministic automata.

Contribution

It establishes a precise link between automaton size and memory in Muller games, and provides methods to construct minimal automata efficiently.

Findings

Minimal good-for-games Rabin automata are as small as the minimal memory for Muller games.

Such automata can be exponentially more succinct than deterministic automata.

Chromatic memory for Muller games can be exponentially larger than unconstrained memory.

Abstract

In this paper, we look at good-for-games Rabin automata that recognise a Muller language (a language that is entirely characterised by the set of letters that appear infinitely often in each word). We establish that minimal such automata are exactly of the same size as the minimal memory required for winning Muller games that have this language as their winning condition. We show how to effectively construct such minimal automata. Finally, we establish that these automata can be exponentially more succinct than equivalent deterministic ones, thus proving as a consequence that chromatic memory for winning a Muller game can be exponentially larger than unconstrained memory.