Back

Games in Verification

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

Description

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.

Prerequisites

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

Materials

PDFlecture notes

Lecturers

Moshe Y. Vardi
Department of Computer Science
Rice University
Houston, TX 77005-1892, USA
vardi@cs.rice.edu
phone: +1-713-348-5977
fax: +1-713-348-5930
http://www.cs.rice.edu/~vardi