In this survey I would like to present some connections between the μ-calculus and games, more specifically games of possibly infinite duration played on labeled graphs. A fundamental connection was established by Emerson and Jutla and subsequently developed by several authors. Essentially, the result is that any formula of the μ-calculus expresses the existence of a strategy in a certain game. The idea of such a correspondence can be traced back to Buechi and McNaughton who observed a similar property of monadic second order arithmetic (see [10]). The contribution is mainly conceptual: infinite games (specifically, parity games) can help us to understand the μ-calculus formulas, and eventually design more efficient algorithms for related algorithmic problems as, e.g., model-checking. For a reader not well familiar with the μ-calculus, infinite games provide a good introductory example since they exhibit fixed points that are not necessarily least fixed points, and the μ-calculus arose from an observation that some properties can be expressed by fixed points, but not the least fixed points. Indeed, the expressive power of the μ-calculus results from the alternation of mutually dependent least and greatest fixed point operators. However the same feature makes the μ-calculus difficult to understand by a human. In fact, in contrast to first-order or temporal logic, the μ-calculus did not emerge by a formalization of the natural language.
展开▼
