A Constraint-Based Approach To Solving Games On Infinite Graphs
POPL(2014)
摘要
We present a constraint-based approach to computing winning strategies in two-player graph games over the state space of infinite-state programs. Such games have numerous applications in program verification and synthesis, including the synthesis of infinite-state reactive programs and branching-time verification of infinite-state 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 "Cinderella-Stepmother 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.
更多查看译文
关键词
program synthesis,games,reactive synthesis,proof rules,static analysis,Horn clauses
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络