Advertisement

Graph Games and Reactive Synthesis

  • Roderick Bloem
  • Krishnendu Chatterjee
  • Barbara Jobstmann
Chapter

Abstract

Graph-based games are an important tool in computer science. They have applications in synthesis, verification, refinement, and far beyond. We review graph-based games with objectives on infinite plays. We give definitions and algorithms to solve the games and to give a winning strategy. The objectives we consider are mostly Boolean, but we also look at quantitative graph-based games and their objectives. Synthesis aims to turn temporal logic specifications into correct reactive systems. We explain the reduction of synthesis to graph-based games (or equivalently tree automata) using synthesis of LTL specifications as an example. We treat the classical approach that uses determinization of parity automata and more modern approaches.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Abadi, M., Lamport, L., Wolper, P.: Realizable and unrealizable specifications of reactive systems. In: Ausiello, G., Dezani-Ciancaglini, M., Della Rocca, S.R. (eds.) Intl. Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol. 372, pp. 1–17. Springer, Heidelberg (1989) CrossRefGoogle Scholar
  2. 2.
    de Alfaro, L., Faella, M., Henzinger, T.A., Majumdar, R., Stoelinga, M.: The element of surprise in timed games. In: Amadio, R.M., Lugiez, D. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol. 2761, pp. 144–158. Springer, Heidelberg (2003) Google Scholar
  3. 3.
    de Alfaro, L., Henzinger, T.A.: Interface automata. In: Tjoa, A.M., Gruhn, V. (eds.) Intl. Symp. on Foundations of Software Engineering (FSE), pp. 109–120. ACM, New York (2001) Google Scholar
  4. 4.
    de Alfaro, L., Henzinger, T.A.: Interface theories for component-based design. In: Henzinger, T.A., Kirsch, C.M. (eds.) Intl. Conf. on Embedded Software (EMSOFT). LNCS, vol. 2211, pp. 148–165. Springer, Heidelberg (2001) Google Scholar
  5. 5.
    de Alfaro, L., Henzinger, T.A., Kupferman, O.: Concurrent reachability games. Theor. Comput. Sci. 386(3), 188–217 (2007) MathSciNetzbMATHCrossRefGoogle Scholar
  6. 6.
    de Alfaro, L., Henzinger, T.A., Mang, F.: Detecting errors before reaching them. In: Emerson, E.A., Sistla, A.P. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 1855, pp. 186–201. Springer, Heidelberg (2000) CrossRefGoogle Scholar
  7. 7.
    de Alfaro, L., Majumdar, R.: Quantitative solution of omega-regular games. In: Vitter, J.S., Spirakis, P.G., Yannakakis, M. (eds.) Annual ACM Symposium on Theory of Computing (STOC), pp. 675–683. ACM, New York (2001) Google Scholar
  8. 8.
    Alur, R., Bodík, R., Dallal, E., Fisman, D., Garg, P., Juniwal, G., Kress-Gazit, H., Madhusudan, P., Martin, M.M.K., Raghothaman, M., Saha, S., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. In: Irlbeck, M., Peled, D.A., Pretschner, A. (eds.) Dependable Software Systems Engineering, pp. 1–25. IOS Press, Amsterdam (2015) Google Scholar
  9. 9.
    Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49, 672–713 (2002) MathSciNetzbMATHCrossRefGoogle Scholar
  10. 10.
    Alur, R., Torre, S.L.: Deterministic generators and games for LTL fragments. In: Symp. on Logic in Computer Science (LICS), pp. 291–302. IEEE, Piscataway (2001) Google Scholar
  11. 11.
    Antoniotti, M.: Synthesis and verification of discrete controllers for robotics and manufacturing devices with temporal logic and the Control-D system. Ph.D. thesis, New York University (1995) Google Scholar
  12. 12.
    Baier, C., Größer, M., Leucker, M., Bollig, B., Ciesinski, F.: Controller synthesis for probabilistic systems. In: IFIP Intl. Conf. on Theoretical Computer Science, pp. 493–506 (2004) Google Scholar
  13. 13.
    Beeri, C.: On the membership problem for functional and multivalued dependencies in relational databases. ACM Trans. Database Syst. 5, 241–259 (1980) zbMATHCrossRefGoogle Scholar
  14. 14.
    Bertrand, N., Genest, B., Gimbert, H.: Qualitative determinacy and decidability of stochastic games with signals. In: Symp. on Logic in Computer Science (LICS), pp. 319–328. IEEE, Piscataway (2009) Google Scholar
  15. 15.
    Björklund, H., Sandberg, S., Vorobyov, S.: A discrete subexponential algorithms for parity games. In: Annual Symposium on Theoretical Aspects of Computer Science (STACS). LNCS, vol. 2607, pp. 663–674. Springer, Heidelberg (2003) Google Scholar
  16. 16.
    Bjorklund, H., Sandberg, S., Vorobyov, S.: A combinatorial strongly subexponential strategy improvement algorithm for mean payoff games. In: Intl. Symp. on Mathematical Foundations of Computer Science (MFCS). LNCS, vol. 3153, pp. 673–685. Springer, Heidelberg (2004) Google Scholar
  17. 17.
    Blass, A., Gurevich, Y., Nachmanson, L., Veanes, M.: Play to test. In: Intl. Conf. on Formal Approaches to Software Testing (FATES). LNCS, vol. 3997. Springer, Heidelberg (2005) Google Scholar
  18. 18.
    Bloem, R., Chatterjee, K., Greimel, K., Henzinger, T.A., Jobstmann, B.: Robustness in the presence of liveness. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 6174, pp. 410–424. Springer, Heidelberg (2010) CrossRefGoogle Scholar
  19. 19.
    Bloem, R., Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Better quality in synthesis through quantitative objectives. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 5643, pp. 140–156. Springer, Heidelberg (2009) CrossRefGoogle Scholar
  20. 20.
    Bloem, R., Greimel, K., Henzinger, T.A., Jobstmann, B.: Synthesizing robust systems. In: Formal Methods in Computer Aided Design (FMCAD), pp. 85–92. IEEE, Piscataway (2009) Google Scholar
  21. 21.
    Bodík, R., Jobstmann, B.: Algorithmic program synthesis: introduction. Int. J. Softw. Tools Technol. Transf. 15(5–6), 397–411 (2013) CrossRefGoogle Scholar
  22. 22.
    Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N., Srba, J.: Infinite runs in weighted timed automata with energy constraints. In: Intl. Conf. on Formal Modeling and Analysis of Timed Systems (FORMATS). LNCS, vol. 5215, pp. 33–47. Springer, Heidelberg (2008) zbMATHCrossRefGoogle Scholar
  23. 23.
    Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N.: Ouaknine, J., Worrell, J., Verification of real-time systems. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018) zbMATHGoogle Scholar
  24. 24.
    Bradfield, J., Walukiewicz, I.: The mu-calculus. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018) zbMATHGoogle Scholar
  25. 25.
    Brázdil, T., Brozek, V., Chatterjee, K., Forejt, V., Kucera, A.: Two views on multiple mean-payoff objectives in Markov decision processes. In: Symp. on Logic in Computer Science (LICS), pp. 33–42. IEEE, Piscataway (2011) Google Scholar
  26. 26.
    Brázdil, T., Chatterjee, K., Forejt, V., Kucera, A.: Trading performance for stability in Markov decision processes. In: Symp. on Logic in Computer Science (LICS), pp. 331–340. IEEE, Piscataway (2013) zbMATHGoogle Scholar
  27. 27.
    Brázdil, T., Chatterjee, K., Kucera, A., Novotný, P.: Efficient controller synthesis for consumption games with multiple resource types. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 7358, pp. 23–38. Springer, Heidelberg (2012) CrossRefGoogle Scholar
  28. 28.
    Brim, L., Chaloupka, J., Doyen, L., Gentilini, R., Raskin, J.F.: Faster algorithms for mean-payoff games. Form. Methods Syst. Des. 38(2), 97–118 (2011) zbMATHCrossRefGoogle Scholar
  29. 29.
    Bryant, R.E.: Binary decision diagrams: an algorithmic basis for symbolic model checking. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018) Google Scholar
  30. 30.
    Büchi, J.R., Landweber, L.H.: Solving sequential conditions by finite-state strategies. Trans. Am. Math. Soc. 138, 295–311 (1969) MathSciNetzbMATHCrossRefGoogle Scholar
  31. 31.
    Cassandras, C.G., Lafortune, S.: Introduction to Discrete Event Systems, 2nd edn. Springer, Heidelberg (2008) zbMATHCrossRefGoogle Scholar
  32. 32.
    Cerný, P., Chatterjee, K., Henzinger, T.A., Radhakrishna, A., Singh, R.: Quantitative synthesis for concurrent programs. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 6806, pp. 243–259. Springer, Heidelberg (2011) CrossRefGoogle Scholar
  33. 33.
    Chakrabarti, A., de Alfaro, L., Henzinger, T.A., Stoelinga, M.: Resource interfaces. In: Intl. Conf. on Embedded Software (EMSOFT). LNCS, vol. 2855, pp. 117–133. Springer, Heidelberg (2003) Google Scholar
  34. 34.
    Chatterjee, K.: Stochastic \(\omega\)-regular games. Ph.D. thesis, UC Berkeley (2007) Google Scholar
  35. 35.
    Chatterjee, K.: The complexity of stochastic Müller games. Inf. Comput. 211, 29–48 (2012) zbMATHCrossRefGoogle Scholar
  36. 36.
    Chatterjee, K., de Alfaro, L., Henzinger, T.A.: The complexity of stochastic Rabin and Streett games. In: Intl. Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol. 3580, pp. 878–890. Springer, Heidelberg (2005) CrossRefGoogle Scholar
  37. 37.
    Chatterjee, K., de Alfaro, L., Henzinger, T.A.: The complexity of quantitative concurrent parity games. In: ACM-SIAM Symposium on Discrete Algorithms (SODA), pp. 678–687. ACM/SIAM, New York/Philadelphia (2006) Google Scholar
  38. 38.
    Chatterjee, K., de Alfaro, L., Henzinger, T.A.: Strategy improvement in concurrent reachability games. In: Intl. Conf. on Quantitative Evaluation of Systems (QEST), pp. 291–300. IEEE, Piscataway (2006) Google Scholar
  39. 39.
    Chatterjee, K., de Alfaro, L., Henzinger, T.A.: Qualitative concurrent parity games. ACM Trans. Comput. Log. 12(4), 28 (2011) MathSciNetzbMATHCrossRefGoogle Scholar
  40. 40.
    Chatterjee, K., Chmelik, M., Tracol, M.: What is decidable about partially observable Markov decision processes with omega-regular objectives. In: Annual Conf. on Computer Science Logic (CSL). LIPIcs, vol. 23 (2013) Google Scholar
  41. 41.
    Chatterjee, K., Doyen, L.: The complexity of partial-observation parity games. In: Intl. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR). LNCS, vol. 6397, pp. 1–14. Springer, Heidelberg (2010) CrossRefGoogle Scholar
  42. 42.
    Chatterjee, K., Doyen, L.: Energy parity games. Theor. Comput. Sci. 458, 49–60 (2012) MathSciNetzbMATHCrossRefGoogle Scholar
  43. 43.
    Chatterjee, K., Doyen, L.: Partial-observation stochastic games: how to win when belief fails. In: Symp. on Logic in Computer Science (LICS), pp. 175–184. IEEE, Piscataway (2012) Google Scholar
  44. 44.
    Chatterjee, K., Doyen, L., Gimbert, H., Henzinger, T.A.: Randomness for free. In: Intl. Symp. on Mathematical Foundations of Computer Science (MFCS). LNCS, vol. 6281, pp. 246–257. Springer, Heidelberg (2010) Google Scholar
  45. 45.
    Chatterjee, K., Doyen, L., Henzinger, T., Raskin, J.F.: Generalized mean-payoff and energy games. In: Annual Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS). LIPIcs, vol. 8, pp. 505–516. Schloss Dagstuhl—LZI, Dagstuhl (2010) Google Scholar
  46. 46.
    Chatterjee, K., Doyen, L., Henzinger, T.A.: Qualitative analysis of partially-observable Markov decision processes. In: Intl. Symp. on Mathematical Foundations of Computer Science (MFCS). LNCS, vol. 6281, pp. 258–269. Springer, Heidelberg (2010) Google Scholar
  47. 47.
    Chatterjee, K., Doyen, L., Henzinger, T.A.: A survey of partial-observation stochastic parity games. Form. Methods Syst. Des. 43(2), 268–284 (2013) zbMATHCrossRefGoogle Scholar
  48. 48.
    Chatterjee, K., Doyen, L., Henzinger, T.A., Raskin, J.: Algorithms for omega-regular games with imperfect information. In: Annual Conf. on Computer Science Logic (CSL). LNCS, vol. 4207, pp. 287–302. Springer, Heidelberg (2006) CrossRefGoogle Scholar
  49. 49.
    Chatterjee, K., Doyen, L., Nain, S., Vardi, M.Y.: The complexity of partial-observation stochastic parity games with finite-memory strategies. In: Intl. Conf. on Foundations of Software Science and Computational Structures (FoSSaCS). LNCS, vol. 8412. Springer, Heidelberg (2014) Google Scholar
  50. 50.
    Chatterjee, K., Forejt, V., Wojtczak, D.: Multi-objective discounted reward verification in graphs and MDPs. In: Intl. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR). LNCS, vol. 8312. Springer, Heidelberg (2013) Google Scholar
  51. 51.
    Chatterjee, K., Goyal, P., Ibsen-Jensen, R., Pavlogiannis, A.: Faster algorithms for algebraic path properties in recursive state machines with constant treewidth. In: Symp. on Principles of Programming Languages (POPL). ACM, New York (2015) Google Scholar
  52. 52.
    Chatterjee, K., Henzinger, M.: An O(n\(^{\mbox{2}}\)) time algorithm for alternating Büchi games. In: ACM-SIAM Symposium on Discrete Algorithms (SODA), pp. 1386–1399 (2012) CrossRefGoogle Scholar
  53. 53.
    Chatterjee, K., Henzinger, M.: Efficient and dynamic algorithms for alternating Büchi games and maximal end-component decomposition. J. ACM 61(3), 15:1–15:40 (2014) zbMATHCrossRefGoogle Scholar
  54. 54.
    Chatterjee, K., Henzinger, T.A.: Semiperfect-information games. In: Annual Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS). LNCS, vol. 3821, pp. 1–18. Springer, Heidelberg (2005) Google Scholar
  55. 55.
    Chatterjee, K., Henzinger, T.A.: Assume-guarantee synthesis. In: Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 4424, pp. 261–275. Springer, Heidelberg (2007) Google Scholar
  56. 56.
    Chatterjee, K., Henzinger, T.A.: A survey of stochastic omega-regular games. J. Comput. Syst. Sci. 78(2), 394–413 (2012) zbMATHCrossRefGoogle Scholar
  57. 57.
    Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Environment assumptions for synthesis. In: Intl. Conf. on Concurrency Theory (CONCUR). CONCUR, vol. 2008, pp. 147–161. Springer, Heidelberg (2008) Google Scholar
  58. 58.
    Chatterjee, K., Henzinger, T.A., Jobstmann, B., Singh, R.: Measuring and synthesizing systems in probabilistic environments. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 6174, pp. 380–395. Springer, Heidelberg (2010) CrossRefGoogle Scholar
  59. 59.
    Chatterjee, K., Henzinger, T.A., Jurdziński, M.: Games with secure equilibria. In: Symp. on Logic in Computer Science (LICS), pp. 160–169. IEEE, Piscataway (2004) Google Scholar
  60. 60.
    Chatterjee, K., Henzinger, T.A., Jurdzinski, M.: Mean-payoff parity games. In: Symp. on Logic in Computer Science (LICS), pp. 178–187 (2005) Google Scholar
  61. 61.
    Chatterjee, K., Henzinger, T.A., Piterman, N.: Algorithms for Büchi games. In: Workshop on Games in Design and Verification (GDV) (2006) Google Scholar
  62. 62.
    Chatterjee, K., Henzinger, T.A., Piterman, N.: Generalized parity games. In: Intl. Conf. on Foundations of Software Science and Computational Structures (FoSSaCS). LNCS, vol. 4423, pp. 153–167. Springer, Heidelberg (2007) Google Scholar
  63. 63.
    Chatterjee, K., Henzinger, T.A., Piterman, N.: Strategy logic. Inf. Comput. 208(6), 677–693 (2010) MathSciNetzbMATHCrossRefGoogle Scholar
  64. 64.
    Chatterjee, K., Jurdziński, M., Henzinger, T.A.: Simple stochastic parity games. In: Annual Conf. on Computer Science Logic (CSL). LNCS, vol. 2803, pp. 100–113. Springer, Heidelberg (2003) CrossRefGoogle Scholar
  65. 65.
    Chatterjee, K., Jurdziński, M., Henzinger, T.A.: Quantitative stochastic parity games. In: ACM-SIAM Symposium on Discrete Algorithms (SODA), pp. 121–130. SIAM, Philadelphia (2004) Google Scholar
  66. 66.
    Chatterjee, K., Majumdar, R., Henzinger, T.A.: Markov decision processes with multiple objectives. In: Annual Symposium on Theoretical Aspects of Computer Science (STACS). LNCS, vol. 3884, pp. 325–336. Springer, Heidelberg (2006) Google Scholar
  67. 67.
    Chatterjee, K., Majumdar, R., Henzinger, T.A.: Stochastic limit-average games are in EXPTIME. Int. J. Game Theory 37(2), 219–234 (2008) MathSciNetzbMATHCrossRefGoogle Scholar
  68. 68.
    Chatterjee, K., Pavlogiannis, A., Velner, Y.: Quantitative interprocedural analysis. In: Symp. on Principles of Programming Languages (POPL). ACM, New York (2015) Google Scholar
  69. 69.
    Chatterjee, K., Raman, V.: Synthesizing protocols for digital contract signing. In: Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI). LNCS, vol. 7148, pp. 152–168. Springer, Heidelberg (2012) CrossRefGoogle Scholar
  70. 70.
    Chatterjee, K., Raman, V.: Assume-guarantee synthesis for digital contract signing. Form. Asp. Comput. 26(4), 825–859 (2014) MathSciNetzbMATHCrossRefGoogle Scholar
  71. 71.
    Chatterjee, K., Randour, M., Raskin, J.F.: Strategy synthesis for multi-dimensional quantitative objectives. In: Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol. 7454, pp. 115–131. Springer, Heidelberg (2012) Google Scholar
  72. 72.
    Chatterjee, K., Velner, Y.: Mean-payoff pushdown games. In: Symp. on Logic in Computer Science (LICS), pp. 195–204. IEEE, Piscataway (2012) Google Scholar
  73. 73.
    Chatterjee, K., Velner, Y.: Hyperplane separation technique for multidimensional mean-payoff games. In: Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol. 8052, pp. 500–515. Springer, Heidelberg (2013) Google Scholar
  74. 74.
    Chen, T., Forejt, V., Kwiatkowska, M.Z., Simaitis, A., Wiltsche, C.: On stochastic games with multiple objectives. In: Intl. Symp. on Mathematical Foundations of Computer Science (MFCS). LNCS, vol. 8087, pp. 266–277. Springer, Heidelberg (2013) zbMATHGoogle Scholar
  75. 75.
    Church, A.: Logic, arithmetic, and automata. In: Proceedings of the International Congress of Mathematicians, pp. 23–35. Institut Mittag-Leffler, Djursholm (1962) Google Scholar
  76. 76.
    Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Logic of Programs. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1981) CrossRefGoogle Scholar
  77. 77.
    Condon, A.: The complexity of stochastic games. Inf. Comput. 96(2), 203–224 (1992) MathSciNetzbMATHCrossRefGoogle Scholar
  78. 78.
    Condon, A.: On algorithms for simple stochastic games. In: Advances in Computational Complexity Theory. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 13, pp. 51–73. AMS, Providence (1993) CrossRefGoogle Scholar
  79. 79.
    Dill, D.L.: Trace theory for automatic hierarchical verification of speed-independent circuits. Ph.D. thesis, ACM Distinguished Dissertation Series. MIT Press (1989) Google Scholar
  80. 80.
    Dziembowski, S., Jurdziński, M., Walukiewicz, I.: How much memory is needed to win infinite games? In: Symp. on Logic in Computer Science (LICS), pp. 99–110. IEEE, Piscataway (1997) Google Scholar
  81. 81.
    Ehlers, R.: ACTL ∩ LTL synthesis. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 7358, pp. 39–54. Springer, Heidelberg (2012) CrossRefGoogle Scholar
  82. 82.
    Ehlers, R.: Symbolic bounded synthesis. Form. Methods Syst. Des. 40(2), 232–262 (2012) MathSciNetzbMATHCrossRefGoogle Scholar
  83. 83.
    Ehrenfeucht, A., Mycielski, J.: Positional strategies for mean payoff games. Int. J. Game Theory 8(2), 109–113 (1979) MathSciNetzbMATHCrossRefGoogle Scholar
  84. 84.
    Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Program. 2(3), 241–266 (1982) zbMATHCrossRefGoogle Scholar
  85. 85.
    Emerson, E.A., Jutla, C.S.: The complexity of tree automata and logics of programs. In: Annual Symp. on Foundations of Computer Science (FOCS), pp. 328–337. IEEE, Piscataway (1988) Google Scholar
  86. 86.
    Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus and determinacy. In: Annual Symp. on Foundations of Computer Science (FOCS), pp. 368–377. IEEE, Piscataway (1991) Google Scholar
  87. 87.
    Etessami, K., Kwiatkowska, M.Z., Vardi, M.Y., Yannakakis, M.: Multi-objective model checking of Markov decision processes. Log. Methods Comput. Sci. 4(4) (2008) Google Scholar
  88. 88.
    Etessami, K., Wilke, T., Schuller, R.A.: Fair simulation relations, parity games, and state space reduction for Büchi automata. SIAM J. Comput. 34(5), 1159–1175 (2005) MathSciNetzbMATHCrossRefGoogle Scholar
  89. 89.
    Etessami, K., Yannakakis, M.: Recursive Markov decision processes and recursive stochastic games. In: Intl. Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol. 3580, pp. 891–903. Springer, Heidelberg (2005) zbMATHCrossRefGoogle Scholar
  90. 90.
    Etessami, K., Yannakakis, M.: Recursive concurrent stochastic games. In: Intl. Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol. 4052, pp. 324–335. Springer, Heidelberg (2006) CrossRefGoogle Scholar
  91. 91.
    Etessami, K., Yannakakis, M.: On the complexity of Nash equilibria and other fixed points. SIAM J. Comput. 39(6), 2531–2597 (2010) MathSciNetzbMATHCrossRefGoogle Scholar
  92. 92.
    Filar, J., Vrieze, K.: Competitive Markov Decision Processes. Springer, Heidelberg (1997) zbMATHGoogle Scholar
  93. 93.
    Filiot, E., Jin, N., Raskin, J.F.: An antichain algorithm for LTL realizability. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 5643, pp. 263–277. Springer, Heidelberg (2009) CrossRefGoogle Scholar
  94. 94.
    Finkbeiner, B., Schewe, S.: Uniform distributed synthesis. In: Symp. on Logic in Computer Science (LICS), pp. 321–330. IEEE, Piscataway (2005) Google Scholar
  95. 95.
    Finkbeiner, B., Schewe, S.: Coordination logic. In: Annual Conf. on Computer Science Logic (CSL). LNCS, vol. 6247, pp. 305–319. Springer, Heidelberg (2010) zbMATHCrossRefGoogle Scholar
  96. 96.
    Forejt, V., Kwiatkowska, M.Z., Norman, G., Parker, D., Qu, H.: Quantitative multi-objective verification for probabilistic systems. In: Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 6065, pp. 112–127. Springer, Heidelberg (2011) zbMATHGoogle Scholar
  97. 97.
    Friedmann, O.: An exponential lower bound for the parity game strategy improvement algorithm as we know it. In: Symp. on Logic in Computer Science (LICS), pp. 145–156. IEEE, Piscataway (2009) Google Scholar
  98. 98.
    Friedmann, O.: Exponential lower bounds for solving infinitary payoff games and linear programs. Ph.D. thesis, University of Munich (2011) Google Scholar
  99. 99.
    Gastin, P., Oddoux, D.: Fast LTL to Büchi automata translation. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 2102, pp. 53–65. Springer, Heidelberg (2001) CrossRefGoogle Scholar
  100. 100.
    Girault, A., Rutten, É.: Automating the addition of fault tolerance with discrete controller synthesis. Form. Methods Syst. Des. 35(2), 190–225 (2009) zbMATHCrossRefGoogle Scholar
  101. 101.
    Gurevich, Y., Harrington, L.: Trees, automata, and games. In: Annual ACM Symposium on Theory of Computing (STOC), pp. 60–65. ACM, New York (1982) Google Scholar
  102. 102.
    Hansen, K.A., Koucký, M., Lauritzen, N., Miltersen, P.B., Tsigaridas, E.P.: Exact algorithms for solving stochastic games: extended abstract. In: Annual ACM Symposium on Theory of Computing (STOC), pp. 205–214 (2011) Google Scholar
  103. 103.
    Henzinger, T.A., Krishnan, S., Kupferman, O., Mang, F.: Synthesis of uninitialized systems. In: Intl. Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol. 2380, pp. 644–656. Springer, Heidelberg (2002) CrossRefGoogle Scholar
  104. 104.
    Henzinger, T.A., Kupferman, O., Rajamani, S.: Fair simulation. Inf. Comput. 173, 64–81 (2002) MathSciNetzbMATHCrossRefGoogle Scholar
  105. 105.
    Horn, F.: Streett games on finite graphs. In: Workshop on Games in Design and Verification (GDV) (2005) Google Scholar
  106. 106.
    Immerman, N.: Number of quantifiers is better than number of tape cells. J. Comput. Syst. Sci. 22, 384–406 (1981) MathSciNetzbMATHCrossRefGoogle Scholar
  107. 107.
    Jacobs, S., Bloem, R.: Parameterized synthesis. In: Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 7214, pp. 362–376. Springer, Heidelberg (2012) Google Scholar
  108. 108.
    Jobstmann, B., Bloem, R.: Optimizations for LTL synthesis. In: Formal Methods in Computer Aided Design (FMCAD), pp. 117–124. IEEE, Piscataway (2006) Google Scholar
  109. 109.
    Jobstmann, B., Staber, S., Griesmayer, A., Bloem, R.: Finding and fixing faults. J. Comput. Syst. Sci. 78(2), 441–460 (2012) MathSciNetzbMATHCrossRefGoogle Scholar
  110. 110.
    Jurdziński, M.: Deciding the winner in parity games is in UP ∩ co-UP. Inf. Process. Lett. 68(3), 119–124 (1998) MathSciNetzbMATHCrossRefGoogle Scholar
  111. 111.
    Jurdziński, M.: Small progress measures for solving parity games. In: Annual Symposium on Theoretical Aspects of Computer Science (STACS). LNCS, vol. 1770, pp. 290–301. Springer, Heidelberg (2000) Google Scholar
  112. 112.
    Jurdziński, M., Paterson, M., Zwick, U.: A deterministic subexponential algorithm for solving parity games. In: ACM-SIAM Symposium on Discrete Algorithms (SODA), pp. 117–123. ACM/SIAM, New York/Philadelphia (2006) Google Scholar
  113. 113.
    Katz, G., Peled, D.: Synthesizing solutions to the leader election problem using model checking and genetic programming. In: Intl. Haifa Verification Conference (HVC). LNCS, vol. 6405, pp. 117–132. Springer, Heidelberg (2009) Google Scholar
  114. 114.
    Kitzelmann, E.: Inductive programming: a survey of program synthesis techniques. In: Intl. Workshop on Approaches and Applications of Inductive Programming (AAIP), pp. 50–73 (2009) Google Scholar
  115. 115.
    Klein, U., Piterman, N., Pnueli, A.: Effective synthesis of asynchronous systems from GR(1) specifications. In: Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI). LNCS, vol. 7148, pp. 283–298. Springer, Heidelberg (2012) CrossRefGoogle Scholar
  116. 116.
    Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Complete functional synthesis. In: Conf. on Programming Language Design and Implementation (PLDI), pp. 316–329. ACM, New York (2010) Google Scholar
  117. 117.
    Kupferman, O., Piterman, N., Vardi, M.Y.: Safraless compositional synthesis. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 4144, pp. 31–44. Springer, Heidelberg (2006) CrossRefGoogle Scholar
  118. 118.
    Kupferman, O., Vardi, M.: Synthesis with incomplete information. In: 2nd International Conference on Temporal Logic, Manchester, pp. 91–106 (1997) Google Scholar
  119. 119.
    Kupferman, O., Vardi, M.: Weak alternating automata and tree automata emptiness. In: Annual ACM Symposium on Theory of Computing (STOC), pp. 224–233. ACM, New York (1998) Google Scholar
  120. 120.
    Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: Annual Symp. on Foundations of Computer Science (FOCS), pp. 531–542. IEEE, Piscataway (2005) Google Scholar
  121. 121.
    Madusudan, P.: Control and synthesis of open reactive systems. Ph.D. thesis, Theoretical Computer Science Group, Institute of Mathematical Sciences, University of Madras (2001) Google Scholar
  122. 122.
    Maidl, M.: The common fragment of CTL and LTL. In: Annual Symp. on Foundations of Computer Science (FOCS), pp. 643–652. IEEE, Piscataway (2000) Google Scholar
  123. 123.
    Maler, O., Pnueli, A., Sifakis, J.: On the synthesis of discrete controllers for timed systems. In: Annual Symposium on Theoretical Aspects of Computer Science (STACS). LNCS, vol. 900, pp. 229–242. Springer, Heidelberg (1995) zbMATHGoogle Scholar
  124. 124.
    Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Heidelberg (1992) zbMATHCrossRefGoogle Scholar
  125. 125.
    Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems. Springer, Heidelberg (1995) zbMATHCrossRefGoogle Scholar
  126. 126.
    Manna, Z., Wolper, P.: Synthesis of communicating processes from temporal logic specifications. Trans. Program. Lang. Syst. 6(1), 68–93 (1984) zbMATHCrossRefGoogle Scholar
  127. 127.
    Martin, D.: The determinacy of Blackwell games. J. Symb. Log. 63(4), 1565–1581 (1998) MathSciNetzbMATHCrossRefGoogle Scholar
  128. 128.
    McNaughton, R.: Infinite games played on finite graphs. Ann. Pure Appl. Log. 65, 149–184 (1993) MathSciNetzbMATHCrossRefGoogle Scholar
  129. 129.
    Miyano, S., Hayashi, T.: Alternating finite automata on omega-words. Theor. Comput. Sci. 32, 321–330 (1984) zbMATHCrossRefGoogle Scholar
  130. 130.
    Mogavero, F., Murano, A., Sauro, L.: On the boundary of behavioral strategies. In: Symp. on Logic in Computer Science (LICS), pp. 263–272 (2013) zbMATHCrossRefGoogle Scholar
  131. 131.
    Mogavero, F., Murano, A., Vardi, M.Y.: Reasoning about strategies. In: Annual Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS). LIPIcs, vol. 8, pp. 133–144 (2010) Google Scholar
  132. 132.
    Morgenstern, A.: Symbolic controller synthesis for LTL specifications. Ph.D. thesis, TU Kaiserslautern (2010) Google Scholar
  133. 133.
    Mostowski, A.: Regular expressions for infinite trees and a standard form of automata. In: Symposium on Computation Theory. LNCS, vol. 208, pp. 157–168. Springer, Heidelberg (1984) CrossRefGoogle Scholar
  134. 134.
    Muller, D.E., Schupp, P.E.: Alternating automata on infinite objects, determinacy and Rabin’s theorem. In: Automata on Infinite Words. LNCS, vol. 192, pp. 100–107. Springer, Heidelberg (1984) Google Scholar
  135. 135.
    Nain, S., Vardi, M.Y.: Solving partial-information stochastic parity games. In: Symp. on Logic in Computer Science (LICS), pp. 341–348. IEEE, Piscataway (2013) Google Scholar
  136. 136.
    Papadimitriou, C.H., Tsitsiklis, J.N.: The complexity of Markov decision processes. Math. Oper. Res. 12, 441–450 (1987) MathSciNetzbMATHCrossRefGoogle Scholar
  137. 137.
    Piterman, N.: From nondeterministic Büchi and Streett automata to deterministic parity automata. In: Symp. on Logic in Computer Science (LICS), pp. 255–264. IEEE, Seattle (2006) Google Scholar
  138. 138.
    Piterman, N., Pnueli, A.: Faster solution of Rabin and Streett games. In: Symp. on Logic in Computer Science (LICS), pp. 275–284. IEEE, Piscataway (2006) Google Scholar
  139. 139.
    Piterman, N., Pnueli, A.: Temporal logic and fair discrete systems. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018) Google Scholar
  140. 140.
    Piterman, N., Pnueli, A., Sa´ar, Y.: Synthesis of reactive(1) designs. In: Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI). LNCS, vol. 3855, pp. 364–380. Springer, Heidelberg (2006) CrossRefGoogle Scholar
  141. 141.
    Pnueli, A.: The temporal logic of programs. In: Annual Symp. on Foundations of Computer Science (FOCS), pp. 46–57. IEEE, Piscataway (1977) Google Scholar
  142. 142.
    Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Symp. on Principles of Programming Languages (POPL), pp. 179–190. ACM, New York (1989) Google Scholar
  143. 143.
    Pnueli, A., Rosner, R.: On the synthesis of an asynchronous reactive module. In: Intl. Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol. 372, pp. 652–671. Springer, Heidelberg (1989) CrossRefGoogle Scholar
  144. 144.
    Pnueli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: Annual Symp. on Foundations of Computer Science (FOCS), pp. 746–757. IEEE, Piscataway (1990) Google Scholar
  145. 145.
    Puchala, B.: Asynchronous omega-regular games with partial information. In: Intl. Symp. on Mathematical Foundations of Computer Science (MFCS). LNCS, vol. 6281, pp. 592–603. Springer, Heidelberg (2010) Google Scholar
  146. 146.
    Rabin, M.O.: Decidability of second-order theories and automata on infinite trees. Trans. Am. Math. Soc. 141, 1–35 (1969) MathSciNetzbMATHGoogle Scholar
  147. 147.
    Ramadge, P.J., Wonham, W.M.: Supervisory control of a class of discrete event processes. SIAM J. Control Optim. 25, 206–230 (1987) MathSciNetzbMATHCrossRefGoogle Scholar
  148. 148.
    Ramadge, P.J.G., Wonham, W.M.: The control of discrete event systems. Proc. IEEE 77, 81–98 (1989) zbMATHCrossRefGoogle Scholar
  149. 149.
    Reif, J.H.: Universal games of incomplete information. In: Annual ACM Symposium on Theory of Computing (STOC), pp. 288–308. ACM, New York (1979) Google Scholar
  150. 150.
    Rosner, R.: Modular synthesis of reactive systems. Ph.D. thesis, Weizmann Institute of Science (1992) Google Scholar
  151. 151.
    Safra, S.: On the complexity of \(\omega\)-automata. In: Annual Symp. on Foundations of Computer Science (FOCS), pp. 319–327. IEEE, Piscataway (1988) Google Scholar
  152. 152.
    Schewe, S.: Synthesis for probabilistic environments. In: Intl. Symp. Automated Technology for Verification and Analysis (ATVA). LNCS, vol. 4218, pp. 245–259. Springer, Heidelberg (2006) CrossRefGoogle Scholar
  153. 153.
    Schewe, S.: Solving parity games in big steps. In: Annual Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS). LNCS, vol. 4855, pp. 449–460. Springer, Heidelberg (2007) Google Scholar
  154. 154.
    Schewe, S.: An optimal strategy improvement algorithm for solving parity and payoff games. In: Annual Conf. on Computer Science Logic (CSL). LNCS, vol. 5213, pp. 369–384. Springer, Heidelberg (2008) CrossRefGoogle Scholar
  155. 155.
    Schewe, S., Finkbeiner, B.: Synthesis of asynchronous systems. In: Intl. Sym. on Logic-Based Program Synthesis and Transformation, 16th International (LOPSTR). LNCS, vol. 4407, pp. 127–142. Springer, Heidelberg (2006) CrossRefGoogle Scholar
  156. 156.
    Schewe, S., Finkbeiner, B.: Bounded synthesis. In: Intl. Symp. Automated Technology for Verification and Analysis (ATVA). LNCS, vol. 4762, pp. 474–488. Springer, Heidelberg (2007) CrossRefGoogle Scholar
  157. 157.
    Schneider, K.: Improving automata generation for linear temporal logic by considering the automaton hierarchy. In: Intl. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR). LNCS, vol. 2250, pp. 39–54. Springer, Heidelberg (2001) CrossRefGoogle Scholar
  158. 158.
    Sebastiani, R., Tonetta, S.: “More deterministic” vs. “smaller” Büchi automata for efficient LTL model checking. In: Correct Hardware Design and Verification Methods (CHARME). LNCS, vol. 2860, pp. 126–140. Springer, Heidelberg (2003) CrossRefGoogle Scholar
  159. 159.
    Shapley, L.: Stochastic games. Proc. Natl. Acad. Sci. USA 39, 1095–1100 (1953) MathSciNetzbMATHCrossRefGoogle Scholar
  160. 160.
    Sohail, S., Somenzi, F.: Safety first: a two-stage algorithm for LTL games. In: Formal Methods in Computer Aided Design (FMCAD), pp. 77–84. IEEE, Piscataway (2009) Google Scholar
  161. 161.
    Solar-Lezama, A., Jones, C.G., Bodík, R.: Sketching concurrent data structures. In: Conf. on Programming Language Design and Implementation (PLDI), pp. 136–148. ACM, New York (2008) Google Scholar
  162. 162.
    Solar-Lezama, A., Rabbah, R.M., Bodík, R., Ebcioglu, K.: Programming by sketching for bit-streaming programs. In: Conf. on Programming Language Design and Implementation (PLDI), pp. 281–294. ACM, New York (2005) Google Scholar
  163. 163.
    Solar-Lezama, A., Tancau, L., Bodík, R., Seshia, S.A., Saraswat, V.A.: Combinatorial sketching for finite programs. In: Architectural Support for Programming Languages and Operating Systems (ASPLOS), pp. 404–415. ACM, New York (2006) Google Scholar
  164. 164.
    Somenzi, F.: Colorado University Decision Diagram Package (1998). http://vlsi.colorado.edu/~fabio/CUDD/
  165. 165.
    Somenzi, F., Bloem, R.: Efficient Büchi automata from LTL formulae. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 1855, pp. 248–263. Springer, Heidelberg (2000) CrossRefGoogle Scholar
  166. 166.
    Stockmeyer, L.: The complexity of decision problems in automata theory and logic. Ph.D. thesis, Massachusetts Institute of Technology (1974) Google Scholar
  167. 167.
    Thomas, W.: Automata on infinite objects. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 133–191. Elsevier, Amsterdam (1990) Google Scholar
  168. 168.
    Thomas, W.: On the synthesis of strategies in infinite games. In: Annual Symposium on Theoretical Aspects of Computer Science (STACS). LNCS, vol. 900, pp. 1–13. Springer, Heidelberg (1995) Google Scholar
  169. 169.
    Thomas, W.: Languages, automata, and logic. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages, vol. 3, pp. 389–455. Springer, Heidelberg (1997). Beyond Words, Chap. 7 CrossRefGoogle Scholar
  170. 170.
    Vardi, M.Y.: An automata-theoretic approach to fair realizability and synthesis. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 939, pp. 267–278. Springer, Heidelberg (1995) CrossRefGoogle Scholar
  171. 171.
    Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1–37 (1994) MathSciNetzbMATHCrossRefGoogle Scholar
  172. 172.
    Vechev, M.T., Yahav, E., Yorsh, G.: Inferring synchronization under limited observability. In: Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 5505, pp. 139–154. Springer, Heidelberg (2009) Google Scholar
  173. 173.
    Vechev, M.T., Yahav, E., Yorsh, G.: Abstraction-guided synthesis of synchronization. In: Symp. on Principles of Programming Languages (POPL), pp. 327–338. ACM, New York (2010) zbMATHGoogle Scholar
  174. 174.
    Velner, Y., Rabinovich, A.: Church synthesis problem for noisy input. In: Intl. Conf. on Foundations of Software Science and Computational Structures (FoSSaCS). LNCS, vol. 6604, pp. 275–289. Springer, Heidelberg (2011) Google Scholar
  175. 175.
    Vöge, J., Jurdziński, M.: A discrete strategy improvement algorithm for solving parity games. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 1855, pp. 202–215. Springer, Heidelberg (2000) CrossRefGoogle Scholar
  176. 176.
    Walukiewicz, I.: Pushdown processes: games and model checking. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 1102, pp. 62–74. Springer, Heidelberg (1996) CrossRefGoogle Scholar
  177. 177.
    Walukiewicz, I.: Pushdown processes: games and model-checking. Inf. Comput. 164(2), 234–263 (2001) MathSciNetzbMATHCrossRefGoogle Scholar
  178. 178.
    Walukiewicz, I.: A landscape with games in the background. In: Symp. on Logic in Computer Science (LICS), pp. 356–366. IEEE, Piscataway (2004) Google Scholar
  179. 179.
    Wang, Y., Lafortune, S., Kelly, T., Kudlur, M., Mahlke, S.A.: The theory of deadlock avoidance via discrete control. In: Symp. on Principles of Programming Languages (POPL), pp. 252–263. ACM, New York (2009) zbMATHGoogle Scholar
  180. 180.
    Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor. Comput. Sci. 200(1–2), 135–183 (1998) MathSciNetzbMATHCrossRefGoogle Scholar
  181. 181.
    Zwick, U., Paterson, M.: The complexity of mean payoff games on graphs. Theor. Comput. Sci. 158, 343–359 (1996) MathSciNetzbMATHCrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  • Roderick Bloem
    • 1
  • Krishnendu Chatterjee
    • 2
  • Barbara Jobstmann
    • 3
  1. 1.Graz University of TechnologyGrazAustria
  2. 2.IST AustriaKlosterneuburgAustria
  3. 3.École Polytechnique Fédérale de LausanneLausanneSwitzerland

Personalised recommendations