The Complexity of the Graded $\mu$-Calculus
=========================================

In classical logic, existential and universal quantifiers express that
there exists at least one individual satisfying a formula, or that all
individuals satisfy a formula.  In many logics, these quantifiers have
been generalized to express that, for a non-negative integer $n$, at
least $n$ individuals or all but $n$ individuals satisfy a formula.
In modal logics, \emph{graded modalities} generalize standard
existential and universal modalities in that they express, e.g., that
there exist at least $n$ accessible worlds satisfying a certain
formula.  Graded modalities are useful expressive means in knowledge
representation; they are present in a variety of other knowledge
representation formalisms closely related to modal logic.

A natural question that arises is how the generalization of the
existential and universal modalities affects the decidability 
problem for the logic and its computational complexity, especially
when the numbers in the graded modalities are coded in binary.
In this paper we study the {\em graded $\mu$-calculus}, which extens
graded modal logic with fixed-point operators, or, equivalently, extends
classical $\mu$-calculus with graded modalities. We prove that 
the decidability problem for graded $\mu$-calculus is
EXPTIME-complete -- not harder than the decidability problem for
$\mu$-calculus, even when the numbers in the graded modalities are
coded in binary.