TUM - Chair VII - Foundations of Software Reliability and Theoretical Computer Science


	Algorithmic Game Solving

News | Dates | Content | Material

Algorithmic Game Solving (Master Praktikum/Lab Course)

Instructors: Chih-Hong Cheng (I-6), Michael Luttenberger (I-7)
Maximal number of students: 6
Requirements: Students are assumed to have basic knowledge on automata theory and formal languages and to be familiar with JAVA

Description

This new lab course focuses on the study and implementation of algorithms for games used in verification and synthesis. As reasoning on the properties of computer systems interacting with the environment can often be reduced to deciding the winner of a game played on a graph, games are both of theoretical and practical interest (see Motivation).

The main motivation of the lab course is the extension of GAVS, a graphical tool for solving games which will be presented in its current version at ATVA'10. Currently GAVS supports the most fundamental types of games relevant for the verification of finite programs. With the help of the participating students, GAVS should be extended to support a broader class of games with the target to submit a tool paper on this new version to some larger conference on software verification. In particular, the contributors will be mentioned as coauthors.

The preliminary outline of the lab course is as follows:

In the first week of the winter semester, every student is assigned a research paper describing the planned extension.
Every student then has four weeks in order to prepare a short presentation which both summarizes the contents of the paper and also outlines the planned work schedule for the implementation. The supervisor will support the students in this step.
The implementation of the extensions into GAVS has to be finalized until the end of January.
In the first three weeks of the lab course, the lab course is supplemented by two to three lectures given by the instructors. These lectures will give an introduction on both the theoretical foundations and implementation details of the games currently supported by GAVS.

Preliminary list of extensions:

Implementations of the following papers are requested for an upcoming version of GAVS:

Further papers:

Motivation

In computer science, games are used to describe the interaction of a system with its environment. As a first very simple example, consider the following program fragment:

1: char c = cin.get();
2: if( c == 'e' ) {
3: nuclearPlant.explode();
} else {
4: nuclearPlant.haveAniceDay();
}

Here, only a very restricted interaction takes place, namley the input of a single character by the user. The relevant question which is obvious to answer in this case is whether the user can control the program in such a way that the nuclear plant does not explode. From a mathematical point of view, all the relevant information can described as a directed graph:

The graph is basically the control flow graph of the program, i.e, the nodes correspond to the control points while the edges describe the control flow; but the shape of the nodes is additionally used to encode whether the user (circular) or the program (rectangular) decides which node is to be visited in the next execution step of the program. In particular, our original question "Can the user prevent the nuclear plant from exploding?" becomes "Can the user always choose his actions in such a way that no path starting in node 1 visits node 3?". This brings us to the definition of safety games:

Safety Games

A safety game consists of a directed graph G=(V,E) whose nodes V are partitioned into two sets, say P (for program) and U (for user), and finally a set H of hazard states.
For instance, consider the following graph:

Again, the nodes of P, resp. U are of rectangular resp. circular shape.

Assume now that H consists only of the node 3 and that the program starts in node 0. The problem is to decide whether the user can control the program in such a way that no matter how the program behaves it will never visit the control state (node) 3.

In this example, we see that the user has can again ensure the safety property by simply moving from node 1 always back to node 0.
On the other hand, if we assume that H={3,4}, then the user cannot prevent the program from reaching node 4.

Reachability and Büchi Games

In the previous two sections, we have tried to motivate the use of games as a formalism for describing the interaction of a system (e.g., program) with its environment (e.g., user) where goal of the environment was to prevent the system to ever reach a particular set of states. Of course, we might also consider the dual goal, i.e., the environment should ensure that the system always visits some state of a given target set T. This leads to the notions of reachability games and Büchi games: in the reachability game, the environment has only to ensure that the system enters T at least once, while in the Büchi game the system should visit T again and again. Returning to our example from above with T = {1,2} one easily checks that the user/environment can win the reachability game starting from node 0 but never the Büchi game as the program/system might always move from node 4 back to node 5.

General definition of 2-Player Games

In general, a 2-player game consists of

a directed graph G=(V,E)
a partition of the nodes V into two sets V₀ and V₁ := V-V₀where the nodes V₀ belong to Player 0 and the nodes V₁ to Player 1
and a winning condition Win

Given a node v of V, a play v₀v₁v₂...v_iv_i+1.... is then a path in G which starts in v=v₀ and is maximal, i.e.,
the owner of node v_i determines the subsequent node v_i+1 visited by the play and the play only terminates if a node has no successors at all.
A play might therefore be an infinite path.

The winning condition then decides if a given play is won by Player 0; if not, the play is defined to be won by Player 1.
The relevant problem is then to decide for a given node if one of two players can always choose his moves such that he wins every possible play.

For instance, in the case of the safety game, the winning condition for Player 0 (the user) simply states that no node of the hazard set H should ever be visited. In the case of the reachability game, the winning condition for Player 0 says that a play should visit a state of T at least once, while in the Büchi game the winning condition for Player 0 becomes that a play should visit T infiinitely often.