Trustworthy Systems

SAT-based strategy extraction in reachability games

Authors

Niklas Een, Alexander Legg, Nina Narodytska and Leonid Ryzhyk

University of California
Berkeley

NICTA

Abstract

Reachability games are a useful formalism for the synthesis of reactive systems. Solving a reachability game involves (1) determining the winning player and (2) computing a winning strategy that determines the winning player’s action in each state of the game. State-of-the-art game solving methods employ computationally expensive procedures to compute the strategy. In this work, we present a simple and efficient strategy extraction technique for a class of reachability game solvers. Our algorithm is based on a SAT encoding of an abstraction of the game and uses interpolants to compute the strategy. Game abstractions are generated as intermediate outputs of the main game solver, which determines the winner of the game, and are reused in our algorithm to efficiently construct the strategy. Our experimental results show that our approach performs well on a number of software synthesis benchmarks.

BibTeX Entry

  @inproceedings{Een_LNR_15,
    address          = {Austin, TX, USA},
    author           = {Een, Niklas and Legg, Alexander and Narodytska, Nina and Ryzhyk, Leonid},
    booktitle        = {AAAI},
    keywords         = {termite, reactive synthesis, sat, qbf, interpolants},
    month            = jan,
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/8328.pdf},
    title            = {{SAT}-based Strategy Extraction in Reachability Games},
    year             = {2015}
  }

Download