Games in Verification

Moshe Y. Vardi
Section: Logic and Computation
Level: Advanced


Games have shown to provide a useful paradigm for reasoning about reactive systems. Not only can model-checking algorithms be formulated as games, but the interaction of reactive systems with their environments can also be modeled as a game. The aim of this course is to demonstrate the power of the game-theoretic approach, by showing how it gives rise to a unifying algorithmic framework through the use of tree automata as an underlying technical tool.


Familiarity with the basic concepts of first-order logic and automata theory.


PDFlecture notes


Moshe Y. Vardi
Department of Computer Science
Rice University
Houston, TX 77005-1892, USA
phone: +1-713-348-5977
fax: +1-713-348-5930