Skip to main content


Solving games without controllable predecessor


Nina Narodytska, Alexander Legg, Fahiem Bacchus, Leonid Ryzhyk and Adam Christopher Walker


University of Toronto


Two-player games are a useful formalism for the synthesis of reactive systems. The traditional approach to solving such games iteratively computes the set of winning states for one of the players. This requires keeping track of all discovered winning states and can lead to space explosion even when using efficient symbolic representations. We propose a new method for solving reach- ability games. Our method works by exploring a subset of the possible concrete runs of the game and proving that these runs can be generalised into a winning strategy on behalf of one of the players. We use counterexample-guided back- tracking search to identify a subset of runs that are sufficient to consider to solve the game. We evaluate our algorithm on several families of benchmarks derived from real-world device driver synthesis problems.

BibTeX Entry

    author           = {Narodytska, Nina and Legg, Alexander and Bacchus, Fahiem and Ryzhyk, Leonid and Walker, Adam
    month            = jul,
    year             = {2014},
    keywords         = {termite, reactive synthesis, sat, qbf},
    title            = {Solving Games without Controllable Predecessor},
    booktitle        = { International Conference on Computer Aided Verification},
    address          = {Vienna, Austria}