Sciweavers

ATVA
2005
Springer

Multi-valued Model Checking Games

13 years 9 months ago
Multi-valued Model Checking Games
This work extends the game-based framework of µ-calculus model checking to the multi-valued setting. In multi-valued model checking a formula is interpreted over a Kripke structure defined over a lattice. The value of the formula is also an element of the lattice. We define a new game for this problem and derive from it a direct model checking algorithm that handles the multi-valued structure without any reduction. We investigate the properties of the new game, both independently, and in comparison to the automata-based approach. We show that the usual resemblance between the two approaches does not hold in the multivalued setting and show how it can be regained by changing the nature of the game.
Sharon Shoham, Orna Grumberg
Added 26 Jun 2010
Updated 26 Jun 2010
Type Conference
Year 2005
Where ATVA
Authors Sharon Shoham, Orna Grumberg
Comments (0)