@inproceedings{beyene2014a,
author = {Beyene, Tewodros A. and Chaudhuri, Swarat and Popeea, Corneliu and Rybalchenko, Andrey},
title = {A Constraint-Based Approach to Solving Games on Infinite Graphs},
booktitle = {Principles of Programming Languages (POPL)},
year = {2014},
month = {January},
abstract = {We present a constraint-based approach to computing winning strategies in two-player graph games over the state space of infinitestate programs. Such games have numerous applications in program verification and synthesis, including the synthesis of infinitestate reactive programs and branching-time verification of infinitestate programs. Our method handles games with winning conditions given by safety, reachability, and general Linear Temporal Logic (LTL) properties. For each property class, we give a deductive proof rule that — provided a symbolic representation of the game players — describes a winning strategy for a particular player. Our rules are sound and relatively complete. We show that these rules can be automated by using an off-the-shelf Horn constraint solver that supports existential quantification in clause heads. The practical promise of the rules is demonstrated through several case studies, including a challenging “CinderellaStepmother game” that allows infinite alternation of discrete and continuous choices by two players, as well as examples derived from prior work on program repair and synthesis.},
publisher = {ACM - Association for Computing Machinery},
url = {http://approjects.co.za/?big=en-us/research/publication/a-constraint-based-approach-to-solving-games-on-infinite-graphs/},
edition = {Principles of Programming Languages (POPL)},
}