Satisfiability and Finite Model Property for the Alternating-Time µ-Calculus
Sven Schewe and Bernd Finkbeiner
This paper presents a decision procedure for the alternating-time µ-calculus. The algorithm is based on a representation of alternating-time formulas as automata over concurrent game structures. We show that language emptiness of these automata can be checked in exponential time. The complexity of our construction meets the known lower bounds for deciding the satisfiability of the classic µ-calculus. It follows that the satisfiability problem is EXPTIME-complete for the alternating-time µ-calculus.
15th Annual Conference on Computer Science Logic (CSL 2006).