Solving Games without Controllable Predecessor

  • Nina Narodytska
  • Alexander Legg
  • Fahiem Bacchus
  • Leonid Ryzhyk
  • Adam Walker
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8559)


Two-player games are a useful formalism for the synthesis of reactive systems. The traditional approach to solving such games iteratively computes the set of winning states for one of the players. This requires keeping track of all discovered winning states and can lead to space explosion even when using efficient symbolic representations. We propose a new method for solving reachability games. Our method works by exploring a subset of the possible concrete runs of the game and proving that these runs can be generalised into a winning strategy on behalf of one of the players. We use counterexample-guided backtracking search to identify a subset of runs that are sufficient to consider to solve the game. We evaluate our algorithm on several families of benchmarks derived from real-world device driver synthesis problems.


Winning Strategy Winning State Partial Strategy Losing State Safety Game 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    de Alfaro, L., Roy, P.: Solving games via three-valued abstraction refinement. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 74–89. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  2. 2.
    Alur, R., Madhusudan, P., Nam, W.: Symbolic computational techniques for solving games. STTT 7(2), 118–128 (2005)CrossRefGoogle Scholar
  3. 3.
    Biere, A., Lonsing, F., Seidl, M.: Blocked clause elimination for QBF. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 101–115. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  4. 4.
    Bloem, R., Galler, S., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Specify, compile, run: Hardware from PSL. ENTCS 190(4), 3–16 (2007)Google Scholar
  5. 5.
    Bloem, R., Könighofer, R., Seidl, M.: SAT-based synthesis methods for safety specs. CoRR abs/1311.3530 (2013)Google Scholar
  6. 6.
    Cassez, F.: Efficient on-the-fly algorithms for partially observable timed games. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 5–24. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  7. 7.
    Cassez, F., Jessen, J.J., Larsen, K.G., Raskin, J.F., Reynier, P.A.: Automatic synthesis of robust and optimal controllers - an industrial case study. In: HSCC, San Francisco, CA, USA, pp. 90–104 (April 2009)Google Scholar
  8. 8.
    Cavada, R., Cimatti, A., Jochim, C.A., Keighren, G., Olivetti, E., Pistore, M., Roveri, M., River, A.T.: NuSMV 2.5 user manualGoogle Scholar
  9. 9.
    Henzinger, T.A., Jhala, R., Majumdar, R.: Counterexample-guided control. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 886–902. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  10. 10.
    Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.: Solving QBF with counterexample guided refinement. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 114–128. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  11. 11.
    Kupferman, O., Lustig, Y., Vardi, M.Y., Yannakakis, M.: Temporal synthesis for bounded systems and environments. In: STACS, pp. 615–626 (March 2011)Google Scholar
  12. 12.
    Lonsing, F., Biere, A.: Integrating dependency schemes in search-based QBF solvers. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 158–171. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  13. 13.
    Morgenstern, A., Gesell, M., Schneider, K.: Solving games using incremental induction. In: IFM, Turku, Finland, pp. 177–191 (June 2013)Google Scholar
  14. 14.
    Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of Reactive(1) designs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 364–380. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  15. 15.
    Ryzhyk, L., Chubb, P., Kuz, I., Le Sueur, E., Heiser, G.: Automatic device driver synthesis with Termite. In: Proceedings of the 22nd ACM Symposium on Operating Systems Principles, Big Sky, MT, USA (October 2009)Google Scholar
  16. 16.
    Sabharwal, A., Ansótegui, C., Gomes, C.P., Hart, J.W., Selman, B.: QBF modeling: Exploiting player symmetry for simplicity and efficiency. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 382–395. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  17. 17.
    Walker, A., Ryzhyk, L.: Predicate abstraction for reactive synthesis. Technical ReportGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Nina Narodytska
    • 1
    • 2
  • Alexander Legg
    • 1
  • Fahiem Bacchus
    • 2
  • Leonid Ryzhyk
    • 1
    • 2
  • Adam Walker
    • 1
  1. 1.NICTA and UNSWSydneyAustralia
  2. 2.University of TorontoCanada

Personalised recommendations