Solving Games without Controllable Predecessor

Select |




Print


Narodytska, Nina; Legg, Alexander; Bacchus, Fahiem; Ryzhyk, Leonid; Walker, Adam Christopher

Narodytska, Nina; Legg, Alexander; Bacchus, Fahiem; Ryzhyk, Leonid; Walker, Adam Christopher


2014-07-19


Conference Material


International Conference on Computer Aided Verification (CAV)


Vienna, Austria


Two-player games are a useful formalism for the synthesis of reactive systems. The traditional approach to solving such games iteratively computes the set of winning states for one of the players. This requires keeping track of all discovered winning states and can lead to space explosion even when using efficient symbolic representations. We propose a new method for solving reach- ability games. Our method works by exploring a subset of the possible concrete runs of the game and proving that these runs can be generalised into a winning strategy on behalf of one of the players. We use counterexample-guided back- tracking search to identify a subset of runs that are sufficient to consider to solve the game. We evaluate our algorithm on several families of benchmarks derived from real-world device driver synthesis problems.


Termite, reactive synthesis, SAT, QBF


http://cavconference.org/


nicta:7885


Narodytska, Nina; Legg, Alexander; Bacchus, Fahiem; Ryzhyk, Leonid; Walker, Adam Christopher. Solving Games without Controllable Predecessor. In: International Conference on Computer Aided Verification (CAV); Vienna, Austria. 2014-07-19.



Loading citation data...

Citation counts
(Requires subscription to view)