Automata theory has various applications in the theory of the modal µ-calculus. One such application is for the tableaux games for the modal µ-calculus introduced by Niwinski and Walukiewicz, in which one player has a winning strategy iff the formula is satisfiable. The winning condition of that game can be naturally checked by a nondeterministic parity automaton. We show how the determinisation of that automaton may be used to obtain a proof system. We then introduce a determinisation method for nondeterministic parity automata, which will be used to define a new annotated cyclic proof system for the modal µ-calculus.

(joint work with Johannes Marti and Yde Venema)