SAT-Based Strategy Extraction in Reachability Games

Authors

  • Niklas Een University of California, Berkeley
  • Alexander Legg NICTA and UNSW Australia
  • Nina Narodytska University of Toronto and NICTA
  • Leonid Ryzhyk Carnegie Mellon University

DOI:

https://doi.org/10.1609/aaai.v29i1.9752

Keywords:

SAT, interpolants, reachability games

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. Recently, a new family of game solvers has been proposed, which rely on counterexample-guided search to compute winning sequences of actions represented as an abstract game tree. While these solvers have demonstrated promising performance in solving the winning determination problem, they currently do not support strategy extraction. We present the first strategy extraction algorithm for abstract game tree-based game solvers. Our algorithm performs SAT encoding of the game abstraction produced by the winner determination algorithm and uses interpolation to compute the strategy. Our experimental results show that our approach performs well on a number of software synthesis benchmarks.

Downloads

Published

2015-03-04

How to Cite

Een, N., Legg, A., Narodytska, N., & Ryzhyk, L. (2015). SAT-Based Strategy Extraction in Reachability Games. Proceedings of the AAAI Conference on Artificial Intelligence, 29(1). https://doi.org/10.1609/aaai.v29i1.9752

Issue

Section

Main Track: Search and Constraint Satisfaction