A Constraint-Based Approach to Solving Games on Infinite Graphs

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.