Generating Dominant Strategies for Continuous Two-Player Zero-Sum Games

Marcell Vazquez-Chanlatte, Shromona Ghosh, Vasumathi Raman, Alberto Sangiovanni-Vincentelli, and Sanjit A. Seshia. Generating Dominant Strategies for Continuous Two-Player Zero-Sum Games. In IFAC Conference on Analysis and Design of Hybrid Systems (ADHS), 2018.

Download

[pdf] 

Abstract

Motivated by the synthesis of controllers from high level temporal specifications, we present two algorithms to compute dominant strategies for continuous two-player zero-sum games based on the Counter Example Guided Inductive Synthesis (CEGIS) paradigm. In CEGIS, we iteratively propose candidate dominant strategies and find counterexamples. For scalabilty, past work has constrained the number of counterexamples used to generate new candidates, which leads to oscillations and incompleteness, even in very simple examples. Our first variant leverages Satisfiability Module Theory (SMT) along side optimization to efficiently implement CEGIS. The second abstracts previously refuted strategies, while maintaining a finite counterexample set. We characterize sufficient conditions for soundness/termination and show both algorithms are sound and terminate. Additionally, the second approach can be made arbitrarily close to complete. We conclude by comparing across different variants of CEGIS.

BibTeX

@inproceedings{vazquez-adhs18,
  author = {Marcell Vazquez-Chanlatte and Shromona Ghosh and Vasumathi Raman and Alberto Sangiovanni-Vincentelli and Sanjit A. Seshia},
  title = {Generating Dominant Strategies for Continuous Two-Player Zero-Sum Games},
  booktitle = {IFAC Conference on Analysis and Design of Hybrid Systems (ADHS)},
  year = {2018},
  abstract = {Motivated by the synthesis of controllers from high level temporal specifications,  
we present two algorithms to compute dominant strategies for continuous two-player zero-sum 
games based on the Counter Example Guided Inductive Synthesis (CEGIS) paradigm.  
In CEGIS, we iteratively propose candidate dominant strategies and find counterexamples. For 
scalabilty, past work has constrained the number of counterexamples used to generate new 
candidates, which leads to oscillations and incompleteness, even in very simple examples. Our 
first variant leverages Satisfiability Module Theory (SMT) along side optimization to efficiently 
implement CEGIS. The second abstracts previously refuted strategies, while maintaining a 
finite counterexample set. We characterize sufficient conditions for soundness/termination and 
show both algorithms are sound and terminate. Additionally, the second approach can be made 
arbitrarily close to complete. We conclude by comparing across different variants of CEGIS.},
}