| 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. |
