Trustworthy Systems

Solving games without controllable predecessor

Authors

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

NICTA

University of Toronto

Abstract

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

  @inproceedings{Narodytska_LBRW_14,
    address          = {Vienna, Austria},
    author           = {Narodytska, Nina and Legg, Alexander and Bacchus, Fahiem and Ryzhyk, Leonid and Walker, Adam
                        Christopher},
    booktitle        = { International Conference on Computer Aided Verification},
    keywords         = {termite, reactive synthesis, sat, qbf},
    month            = jul,
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/7885.pdf},
    title            = {Solving Games without Controllable Predecessor},
    year             = {2014}
  }

Download