Interpolants in two-player games
Niklas Eén, Alexander Legg, Nina Narodytska, Leonid Ryzhyk · 2014
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). A winning strategy for the controller is a mapping that associates with every state a controllable action to play in this state. To solve a game, the algorithm must (1) prove that there exists a winning strategy for the controller and (2) generate a concrete winning strategy. In this work we focus on the latter problem, which we refer to as strategy extraction. We address the strategy extraction problem in the context of a new counterexampleguided SAT-based algorithm for solving reachability games, recently proposed by Narodytska et al. [1]. If a strategy for the controller exists, the algorithm produces a certificate of strategy existence in the form of a game tree that specifies a set of moves of the controller at each round of the game. Figure 1 shows an example game tree