Multi-valued model checking games (Q414899)

The game-based approach offers a very elegant way for establishing properties of systems modeled by Kripke structures. The paper extends the game-based framework of \(\mu\)-calculus model checking to the multi-valued setting. Structures in the multi-valued semantics are Kripke structures defined over a lattice. The meaning of a \(\mu\)-calculus formula in a state \(s\) of the Kripke structure is an element of the lattice, called the value of the formula in \(s\). The task of the multi-valued model checking problem is then to compute the value of a given formula in a given state. This problem has many applications in verification, such as handling abstract or partial models, analyzing systems in the presence of inconsistent views, and performing temporal logic query checking. The paper defines a new game for the multi-valued model checking problem of the full \(\mu\)-calculus, and demonstrates how to derive from it a direct model checking algorithm for its alternation-free fragment. The algorithm handles the multi-valued structure without any reduction. The paper discusses properties of the new game. It also shows that the usual resemblance between the automata-based and the game-based approach does not hold in the multi-valued setting and how it can be regained by changing the nature of the game.