Games and Natural Number-valued Semantics of the Modal -calculus

The modal µ-calculus has strong expressive power to describe properties of Kripke structures. The seman-tics of the logic can be expressed using games: for a given Kripke structure, a parity game between Player and Opponent can be dened so that a state satises a formula if and only if the corresponding vertex of the game belongs to the winning region of Player. The games play an important role in the standard decision procedure for satisability. In previous research, we introduced a non-standard semantics of the logic: a truth value of a formula is an element of a natural number or the innity. Thus, formulae express quantitative properties of Kripke structures. In this work, toward the research of the satisability problem of our semantics, we develop a technique which is a counterpart of the game expression of the ordinary semantics.