Completeness for the modal μ-calculus: Separating the combinatorics from the dynamics

More in detail, prominent roles in our proof are played by two classes of modal automata: next to the disjunctive automata that are known from the work of Janin & Walukiewicz, we introduce here the class of semi-disjunctive automata that roughly correspond to the fragment of the mu-calculus for which Kozen proved completeness. We will establish a connection between the proof theory of Kozen's system, and two kinds of games involving modal automata: a satisfiability game involving a single modal automaton, and a consequence game relating two such automata. In the key observations on these games we bring the dynamics and combinatorics of parity automata together again, by proving some results that witness the nice behaviour of disjunctive and semi-disjunctive automata in these games. As our main result we prove that every formula of the modal mu-calculus provably implies the translation of a disjunctive automaton; from this the completeness of Kozen's axiomatization is immediate.