Alternating tree automata, parity games, and modal {$\mu$}-calculus
Thomas Wilke · Bulletin of the Belgian Mathematical Society - Simon Stevin · 2001
A coherent exposition of the connection of alternating tree automata and modal μ-calculus is given, advocating an automaton model specifically tailored for working with modal μ-calculus. The advantage of the automaton model proposed is that it can deal with arbitrary branching in a very natural way. It is really equivalent to the modal μ-calculus with respect to expressive power, just as the one proposed by Janin and Walukiewicz, but simpler. The main focus is on the model checking and the satisfiability problem for μ-calculus. Both problems are solved by reductions to corresponding problems on alternating tree automata, namely to the acceptance and the (non-)emptiness problem, respectively. These problems, in turn, are solved using parity games. Resume On donne une presentation coherente du lien entre les automates d’arbres alternants et le mu-calcul modal, grâce a un modele d’automate specialement adapte au mu-calcul. L’avantage du modele d’automate propose est qu’il peut prendre en compte des branchements d’ordre arbitraire de maniere tres naturelle. Il a un pouvoir d’expression equivalent a celui du mu-calcul, tout comme celui propose par Janin et Walukiewicz. mais il est plus simple. L’accent est principalement mis sur la verification et le probleme de la satisfiabilite du mu-calcul. Ces deux problemes sont resolus par reduction aux problemes correspondants sur les automates d’arbres alternants, a savoir l’acceptance et le probleme du vide respectivement. Ces problemes sont a leur tour resolus en utilisant des jeux a parie. Bull. Belg. Math. Soc. -1993 (0), 359–391