Les automates d'arbres infinis constituent un reconnaisseur adapté à la représentation des modèles d'une formule du mu-calcul. En effet, il est possible d'associer à toute formule du mu-calcul un automate d'arbre muni d'une condition d'acceptation de parité tel que les modèles de la formule soient précisément les graphes reconnus par l'automate.
Cette association entre automate et formule permet de résoudre le problèmes de satisfiabilité d'une formule : on construit, à partir de l'automate d'arbre associé à la formule, un jeu de parité pour lequel une stratégie gagnante permet de générer un modèle de la formule initiale. Une construction similaire permet la résolution du problème du model-checking.
Nous présenterons dans un premier temps les automates de mots infinis, puis les automates d'arbres infinis. Dans un deuxième temps, nous introduirons les jeux infinis. Enfin, nous exposerons les méthodes permettant de résoudre les problèmes de satisfiabilité et de model-checking du mu-calcul.