On the Model Checking of the Graded μ-calculus on Trees

The mu-calculus is an expressive propositional modal logic augmented with least and greatest fixed-points, and encompasses many temporal, program, dynamic and description logics. The model checking problem for the mu-calculus is known to be in NP n Co-NP. In this paper, we study the model checking problem for the mu-calculus extended with graded modalities. These constructors allow to express numerical constraints on the occurrence of accessible nodes (worlds) satisfying a certain formula. It is known that the model checking problem for the graded mu-calculus with finite models is in EXPTIME. In the current work, we introduce a linear-time model checking algorithm for the graded mu-calculus when models are finite unranked trees.