Can I read A Constraint-based Approach to Solving Games on Infinite Graphs on EtoBox?

A Constraint-based Approach to Solving Games on Infinite Graphs by Tewodros Beyene; Swarat Chaudhuri; Corneliu Popeea; Andrey Rybalchenko is a Computer Science article available to read on EtoBox.

What is A Constraint-based Approach to Solving Games on Infinite Graphs about?

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.

Who reads A Constraint-based Approach to Solving Games on Infinite Graphs?

Author

Tewodros Beyene; Swarat Chaudhuri; Corneliu Popeea; Andrey Rybalchenko

Publisher

ACM

Published

2014

Language

EN

Field

Computer Science (Physical Sciences)