Trees, automata, and games

ABSTRACT

In 1969 Rabin introduced tree automata and proved one of the deepest decidability results. If you worked on decision problems you did most probably use Rabin's result. But did you make your way through Rabin's cumbersome proof with its induction on countable ordinals? Building on ideas of our predecessors-&-mdash;and especially those of B-&-uuml;chi-&-mdash;we give here an alternative and transparent proof of Rabin's result. Generalizations and further results will be published elsewhere.

REFERENCES

• 1: J. R. B-&-uuml;chi 1962, On a decision method in the restricted second-order arithmetic. Logic, Methodology, and Philosophy of Science: Proc. 1960 Intern. Congr., 1-11 (Stanford University Press, 1962).
• 2: J. R. B-&-uuml;chi and L. H. Landweber 1969, Solving sequential conditions by finite-state strategies. Trans. A.M.S., 138, 295-311.
• 3: J. R. B-&-uuml;chi 1973, The monadic second-order theory of -&-ohgr;1, Springer Lecture Notes in Math., 328, 1-127.
• 4: J. R. B-&-uuml;chi 1977, Using determinancy of games to eliminate quantifiers, Springer Lecture Notes in Comp. Sci., 56, 367-378.
• 5: J. R. B-&-uuml;chi 1981, Winning state-strategies for Boolean-F games, 45 pages, a manuscript.
• 6: M. Davis 1964, Infinite games of perfect information, Advances in Game Theory, Princeton University Press, Princeton, N.J., 85-101.
• 7: Y. Gurevich and S. Shelah 198?, Choice on the binary tree is not definable, in preparation.
• 8: Y. Gurevich, M. Magidor and S. Shelah 198?, The monadic theory of -&-ohgr;2, J. Symb. Logic, to appear.
• 9: L. Landweber 1967, Finite state games-&-mdash;A solvability algorithm for restricted second-order arithmetic, Notices Amer. Math. Soc., 14, 129-130.
• 10: R. McNaughton 1966, Testing and generating infinite sequences by a finite automaton, Information and Control, 9, 521-530.
• 11: D. E. Muller 1963, Infinite sequences and finite machines, Switching Circuit Theory and Logical Design: Proc. Fourth Annual Symp., 3-16 (I.E.E.E., New York).
• 12: M. O. Rabin 1969, Decidability of second-order theories and automata on infinite trees, Trans. A.M.S., 141, 1-35.
• 13: C. W. Rackoff 1972, The emptiness and complementation problems for automata on infinite trees, Master's thesis, M.I.T.
• 14: S. Shelah 1975, The monadic theory of order, Annals of Amer. Math. Soc., 102, 379-419.
• 15: J. Stupp 1975, The lattice-model is recursive in the original model, 25 pages, manuscript.
• 16: J. W. Thatcher and J. B. Wright 1968, Generalized automata theory with an application to a decision problem of second-order logic, Math. Systems Theory, 2, 57-81.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
          Subjects: Automata (e.g., finite, push-down, resource-bounded)

Additional Classification:
  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS
      G.2.0 General
      G.2.2 Graph Theory
          Subjects: Trees

General Terms:
Theory