Trustworthy Systems

Interpolants in two-player games

Authors

Niklas Een, Alexander Legg, Nina Narodytska and Leonid Ryzhyk

University of California
Berkeley

NICTA

Abstract

We present a new application of interpolants in the context of two-player games. Two-player games is a useful formalism for the synthesis of reactive systems, with applications in device driver development, hardware design, industrial automation, etc.In particular, we consider reachability games over a finite state space, where the first player (the controller) must force the game into a given goal region given any valid behaviour of the second player (the environment). In this work, we focus on the strategy extraction problem in the context of a new counter example guided SAT-based algorithm for solving reachability games, recently proposed by Narodytska et al. We demonstrate how interpolants can be used to find a winning strategy.

BibTeX Entry

  @misc{Een_LNR_14,
    author           = {Een, Niklas and Legg, Alexander and Narodytska, Nina and Ryzhyk, Leonid},
    booktitle        = {iPRA workshop},
    keywords         = {termite, reactive synthesis, sat, qbf, interpolants},
    month            = jul,
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/8136.pdf},
    title            = {Interpolants in Two-Player Games},
    year             = {2014}
  }

Download