Tewodros Beyene
ABSTRACT
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.
Supplemental Material
- R. Alur, P. Cerný, P. Madhusudan, and W. Nam. Synthesis of interface specifications for java classes. In POPL, pages 98--109, 2005. Google Scholar
Digital Library
- T. Ball and O. Kupferman. An abstraction-refinement framework for multi-agent systems. In LICS, pages 379--388. IEEE, 2006. Google ScholarDigital Library
- T. Beyene, C. Popeea, and A. Rybalchenko. Solving existentially quantified Horn clauses. In CAV, 2013. Google ScholarDigital Library
- M. Bodlaender, C. Hurkens, V. Kusters, F. Staals, G. Woeginger, and H. Zantema. Cinderella versus the Wicked Stepmother. In IFIP TCS, pages 57--71, 2012. Google ScholarDigital Library
- M. Bofill, R. Nieuwenhuis, A. Oliveras, E. Rodrıguez-Carbonell, and A. Rubio. The Barcelogic SMT solver. In CAV, pages 294--298, 2008. Google ScholarDigital Library
- C. Borralleras, S. Lucas, A. Oliveras, E. Rodrıguez-Carbonell, and A. Rubio. SAT modulo linear arithmetic for solving polynomial constraints. J. Autom. Reasoning, 48 (1): 107--131, 2012. Google ScholarDigital Library
- J. R. Büchi and L. Landweber. Solving sequential conditions by finite-state strategies. Trans. Amer. Math. Soc., 138: 295--311, 1969.Google ScholarCross Ref
- T. Cachat. Symbolic strategy synthesis for games on pushdown graphs. In ICALP, pages 704--715. 2002. Google ScholarDigital Library
- T. Cachat. Uniform solution of parity games on prefix-recognizable graphs. Electronic Notes in Theoretical Computer Science, 68 (6): 71--84, 2003.Google ScholarCross Ref
- K. Chatterjee and L. Doyen. Energy parity games. TCS, 2012. Google ScholarDigital Library
- B. Cook and E. Koskinen. Reasoning about nondeterminism in programs. In PLDI, 2013. Google ScholarDigital Library
- L. De Alfaro, T. Henzinger, and R. Majumdar. Symbolic algorithms for infinite-state games. In phCONCUR, pages 536--550. Springer, 2001. Google ScholarDigital Library
- L. M. de Moura and N. Bjørner. Z3: An efficient SMT solver. In TACAS, 2008. Google ScholarDigital Library
- E. A. Emerson and C. Jutla. Tree automata, mu-calculus and determinacy. In FOCS, pages 368--377. IEEE, 1991. Google ScholarDigital Library
- H. Fecher and M. Huth. Ranked predicate abstraction for branching time: Complete, incremental, and precise. In ATVA, pages 322--336. Springer, 2006. Google ScholarDigital Library
- H. Fecher and S. Shoham. Local abstraction--refinement for the μ-calculus. STTT, 13 (4): 289--306, 2011. Google ScholarDigital Library
- P. Gastin and D. Oddoux. Fast LTL to Büchi automata translation. In CAV, pages 53--65, 2001. Google ScholarDigital Library
- E. Grädel, W. Thomas, and T. Wilke, editors. Automata, Logics, and Infinite Games: A Guide to Current Research, 2002.Google Scholar
- S. Grebenshchikov, A. Gupta, N. P. Lopes, C. Popeea, and A. Rybalchenko. HSF(C): A software verifier based on Horn clauses - (competition contribution). In TACAS, 2012. Google ScholarDigital Library
- S. Grebenshchikov, N. P. Lopes, C. Popeea, and A. Rybalchenko. Synthesizing software verifiers from proof rules. In phPLDI, 2012. Google ScholarDigital Library
- A. Griesmayer, R. Bloem, and B. Cook. Repair of boolean programs with an application to C. In phCAV, pages 358--371. Springer, 2006. Google ScholarDigital Library
- O. Grumberg, M. Lange, M. Leucker, and S. Shoham. Don't know in the μ-calculus. In phVMCAI, pages 233--249, 2005. Google ScholarDigital Library
- O. Grumberg, M. Lange, M. Leucker, and S. Shoham. When not losing is better than winning: Abstraction and refinement for the full μ-calculus. Information and Computation, 205 (8): 1130--1148, 2007. Google ScholarDigital Library
- A. Gurfinkel and M. Chechik. Why waste a perfectly good abstraction? In TACAS, pages 212--226. 2006. Google ScholarDigital Library
- A. Harding, M. Ryan, and P.-Y. Schobbens. A new algorithm for strategy synthesis in ltl games. In TACASs, pages 477--492. Springer, 2005. Google ScholarDigital Library
- T. A. Henzinger, R. Jhala, and R. Majumdar. Counterexample-guided control. In ICALP, pages 886--902, 2003. Google ScholarDigital Library
- K. Hoder, N. Bjørner, and L. M. de Moura. Z- an efficient engine for fixed points with constraints. In CAV, pages 457--462, 2011. Google ScholarDigital Library
- A. J. C. Hurkens, C. A. J. Hurkens, and G. J. Woeginger. How Cinderella won the bucket game (and lived happily ever after). Mathematics Magazine, 84 (4): pp. 278--283, 2011.Google ScholarCross Ref
- B. Jobstmann, A. Griesmayer, and R. Bloem. Program repair as a game. In CAV, pages 226--238, 2005. Google ScholarDigital Library
- M. JurdziŃski. Small progress measures for solving parity games. In STACS, pages 290--301, 2000. Google ScholarDigital Library
- V. Kuncak, M. Mayer, R. Piskac, and P. Suter. Complete functional synthesis. In phPLDI, 2010. Google ScholarDigital Library
- O. Kupferman and M. Y. Vardi. Robust satisfaction. In CONCUR, pages 383--398, 1999. Google ScholarDigital Library
- Z. Manna and A. Pnueli. Completing the temporal picture. Theor. Comput. Sci., 83 (1): 91--130, 1991. Google ScholarDigital Library
- Z. Manna and R. Waldinger. A deductive approach to program synthesis. TOPLAS, 2 (1): 90--121, 1980. Google ScholarDigital Library
- D. Martin. Borel determinacy. The Annals of Mathematics, 102 (2): 363--371, 1975.Google ScholarCross Ref
- E.-R. Olderog and K. R. Apt. Fairness in parallel programs: The transformational approach. TOPLAS, 10 (3), 1988. Google ScholarDigital Library
- N. Piterman, A. Pnueli, and Y. Saar. Synthesis of reactive(1) designs. In VMCAI, pages 364--380, 2006. Google ScholarDigital Library
- A. Pnueli and R. Rosner. On the synthesis of a reactive module. In POPL, pages 179--190. ACM, 1989. Google ScholarDigital Library
- A. Podelski and A. Rybalchenko. Transition invariants. In LICS, 2004. Google ScholarDigital Library
- M. Slanina. Control rules for reactive system games. In AAAI Spring Symposium on Logic-Based Program Synthesis, 2002.Google Scholar
- A. Solar-Lezama, L. Tancau, R. Bodík, S. A. Seshia, and V. A. Saraswat. Combinatorial sketching for finite programs. In ASPLOS, pages 404--415, 2006. Google ScholarDigital Library
- S. Srivastava, S. Gulwani, and J. S. Foster. From program verification to program synthesis. In POPL, pages 313--326, 2010. Google ScholarDigital Library
- W. Thomas. On the synthesis of strategies in infinite games. In STACS, pages 1--13, 1995.Google ScholarCross Ref
- M. Y. Vardi. Verification of concurrent programs: The automata-theoretic framework. Ann. Pure Appl. Logic, 51 (1--2): 79--98, 1991.Google ScholarCross Ref
- M. T. Vechev, E. Yahav, and G. Yorsh. Abstraction-guided synthesis of synchronization. In POPL, 2010. Google ScholarDigital Library
- I. Walukiewicz. Pushdown processes: Games and model-checking. Information and computation, 164 (2): 234--263, 2001. Google ScholarDigital Library
- W. Zielonka. Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science, 200 (1): 135--183, 1998. Google ScholarDigital Library
Index Terms
- A constraint-based approach to solving games on infinite graphs
Recommendations
Strategy synthesis for linear arithmetic games
Many problems in formal methods can be formalized as two-player games. For several applications—program synthesis, for example—in addition to determining which player wins the game, we are interested in computing a winning strategy for that player. This ...
A constraint-based approach to solving games on infinite graphs
POPL '14We 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 ...
Symbolic computational techniques for solving games
Games are useful in modular specification and analysis of systems where the distinction among the choices controlled by different components (for instance, the system and its environment) is made explicit. In this paper, we formulate and compare various ...
Comments