Abstract. 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 § , at least § individuals or all but § individuals satisfy a formula. In modal logics, graded modalities generalize standard existential and universal modalities in that they express, e.g., that there exist at least § 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 graded¨-calculus, which extens graded modal logic with fixed-point operators, or, equivalently, extends classical¨-calculus with graded modalities. We prove that the decidability problem for graded¨-calculus is EXPTIME-complete -not harder than the decidability problem for¨-calculus, even when the numbers in the graded modalities are coded in binary.
Kupferman, Sattler and Vardi study a µ-calculus with graded modalities where one can express, e.g., that a graph node has at least n successors satisfying a certain property REF .
The Complexity of the Graded µ-Calculus
CADE
Mathematics Computer Science