In this essay we discuss the origin, central results, and some perspectives of algorithmic synthesis of nonterminating reactive programs. We recall the fundamental questions raised more than 50 years ago in “Church’s Synthesis Problem” that led to the foundation of the algorithmic theory of infinite games. We outline the methodology developed in more recent years for solving such games and address related automata theoretic problems that are still unresolved.


Winning Strategy Kripke Structure Tree Automaton Game Graph Winning Condition 
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.
    Büchi, J.R.: Weak second-order arihmetic and finite automata. Z. Math. Logik Grundlagen Math. 6, 66–92 (1960)CrossRefzbMATHGoogle Scholar
  2. 2.
    Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Nagel, E., et al. (eds.) Proc. 1960 International Congress on Logic, Methodology and Philosophy of Science, pp. 1–11. Stanford University Press (1962)Google Scholar
  3. 3.
    Büchi, J.R., Landweber, L.H.: Solving sequential conditions by finite-state strategies. Trans. Amer. Math. Soc. 138, 367–378 (1969)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Church, A.: Applications of recursive arithmetic to the problem of circuit synthesis. In: Summaries of the Summer Institute of Symbolic Logic, vol. I, pp. 3–50. Cornell Univ., Ithaca (1957)Google Scholar
  5. 5.
    Church, A.: Logic, arithmetic, and automata. In: Proc. Int. Congr. Math. 1962, Inst. Mittag-Leffler, Djursholm, Sweden, pp. 23–35 (1963)Google Scholar
  6. 6.
    Eilenberg, S.: Automata, Languages, and Machines, vol. A. Academic Press, New York (1974)zbMATHGoogle Scholar
  7. 7.
    Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus, and determinacy. In: Proc. 32nd FoCS 1991, pp. 368–377. IEEE Comp. Soc. Press, Los Alamitos (1991)Google Scholar
  8. 8.
    Emerson, E.A., Jutla, C.S., Sistla, A.P.: On model checking for fragments of the μ-calculus. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 385–396. Springer, Heidelberg (1993)CrossRefGoogle Scholar
  9. 9.
    Fischer, D., Grädel, E., Kaiser, L.: Model checking games for the quantitative μ-Calculus. In: Albers, S., Weil, P. (eds.) Proc. STACS 2008, pp. 301–312 (2008)Google Scholar
  10. 10.
    Gurevich, Y., Harrington, L.: Trees, automata, and games. In: Proc. 14th ACM Symp. on the Theory of Computing, pp. 60–65. ACM Press, New York (1982)Google Scholar
  11. 11.
    Grädel, E.: Banach-Mazur games on graphs. In: Proc. FSTTCS 2008 (2008),
  12. 12.
    Gale, D., Stewart, F.M.: Infinite games with perfect information. Ann. Math. Studies 28, 245–266 (1953)MathSciNetzbMATHGoogle Scholar
  13. 13.
    Grädel, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games. LNCS, vol. 2500. Springer, Heidelberg (2002)zbMATHGoogle Scholar
  14. 14.
    Hausdorff, F.: Grundzüge der Mengenlehre, Leipzig (1914)Google Scholar
  15. 15.
    Hosch, F.A., Landweber, L.H.: Finite delay solutions for sequential conditions. In: Nivat, M. (ed.) Proc. ICALP 1972, pp. 45–60. North-Holland, Amsterdam (1972)Google Scholar
  16. 16.
    Kechris, A.S.: Classical Descriptive Set Theory. Springer, New York (1995)CrossRefzbMATHGoogle Scholar
  17. 17.
    McNaughton, R.: Finite-state infinite games, Project MAC Rep., MIT, Cambridge, Mass (September 1965)Google Scholar
  18. 18.
    McNaughton, R.: Testing and generating infinite sequences by a finite automaton. Inf. Contr. 9, 521–530 (1966)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    Mostowski, A.W.: Regular expressions for infinite trees and a standard form of automata. In: Skowron, A. (ed.) SCT 1984. LNCS, vol. 208, pp. 157–168. Springer, Heidelberg (1984)CrossRefGoogle Scholar
  20. 20.
    Putnam, H.: Decidability and essential undecidability. JSL 22, 39–54 (1957)MathSciNetzbMATHGoogle Scholar
  21. 21.
    Rabin, M.O.: Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc. 141, 1–35 (1969)MathSciNetzbMATHGoogle Scholar
  22. 22.
    Rabin, M.O.: Automata on infinite objects and Church’s Problem. Amer. Math. Soc., Providence (1972)CrossRefzbMATHGoogle Scholar
  23. 23.
    Rabinovich, A., Thomas, W.: Logical Refinements of Church’s Problem. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 69–83. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  24. 24.
    Selivanov, V.: Fine hierarchies and Boolean terms. J. Smb. Logic 60, 289–317 (1995)MathSciNetCrossRefzbMATHGoogle Scholar
  25. 25.
    Thomas, W.: Solution of Church’s Problem: A tutorial. In: Apt, K., van Rooij, R. (eds.) New Perspectives on Games and Interaction. Texts on Logic and Games, vol. 5, pp. 211–236. Amsterdam Univ. PressGoogle Scholar
  26. 26.
    Trakhtenbrot, B.A., Barzdin, Y.M.: Finite Automata. Behavior and Synthesis. North-Holland, Amsterdam (1973)zbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Wolfgang Thomas
    • 1
  1. 1.RWTH Aachen UniversityAachenGermany

Personalised recommendations