Structural properties of automata over infinite words and memory for games

Overview & Synopsis

Automata and infinite duration games form the theoretical basis for the verification and synthesis of reactive systems. Contrary to the case of regular languages over finite words, several models of omega-automata exist, each one offering its own advantages. However, their structural and language-theoretical properties are still far from being fully understood. In this thesis, we study transformations between different types of omega-automata, as well as the minimisation problem. Moreover, we exhibit links between these automata and the complexity of winning strategies for games with omega-regular winning conditions, giving a complete characterisation of half-positionality for omega-regular languages.