On polynomial-size programs winning finite-state games

  • Helmut Lescow
Session 8: Invited Titorial
Part of the Lecture Notes in Computer Science book series (LNCS, volume 939)


Finite-state reactive programs are identified with finite automata which realize winning strategies in Büchi-Landweber games. The games are specified by finite “game graphs” equipped with different winning conditions (“Rabin condition”, “Streett condition” and “Muller condition”, defined in analogy to the theory of ω-automata). We show that for two classes of games with Muller winning condition polynomials are both an upper and a lower bound for the size of winning reactive programs. Also we give a new proof for the existence of no-memory strategies in games with Rabin winning condition, as well as an exponential lower bound for games with Streett winning condition.


Finite Automaton Outgoing Edge Winning Strategy Tree Automaton Strategy Graph 
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. [ALW89]
    M. Abadi, L. Lamport, and P. Wolper. Realizable and unrealizable specifications of reactive systems. In G. Ausiello et al., editor, Automata, Languages, and Programming, volume 372 of LNCS, pages 1–17, Berlin, Heidelberg, New York, 1989. Springer-Verlag.Google Scholar
  2. [BL69]
    J. R. Büchi and L. H. Landweber. Solving sequential conditions by finitestate strategies. Trans. Amer. Math. Soc., 138:295–311, 1969.Google Scholar
  3. [Bü83]
    J. R. Büchi. State strategies for games in F σδG δσ. J. Symb. Logic, 48:1171–1198, 1983.Google Scholar
  4. [EJ91]
    E.A. Emerson and C.S. Jutla. Tree automata, mu-calculus and determinacy. In Proc. 32nd IEEE Symp. on the Foundations of Computing, pages 368–377, 1991.Google Scholar
  5. [Em85]
    E. A. Emerson. Automat, tableaux, and temporal logics. In G. Goos and J. Hartmanis, editors, Logics of Programs, volume 803 of LNCS, pages 79–88, Berlin, Heidelberg, New York, 1985. Springer-Verlag.Google Scholar
  6. [GH82]
    Y. Gurevich and L. Harrinton. Trees, automata, and games. In Proc 14th ACM Symp. on the Theory of computing, pages 60–65, San Fancisco, 1982.Google Scholar
  7. [Kla94]
    N. Klarlund. Progress measures, immediate determinacy, and a subset construction for tree automata. Ann. Pure and Appl. Math., 69:243–268, 1994.Google Scholar
  8. [Lan69]
    L. H. Landweber. Decision problems for ω-automata. Mathematical Systems Theory, 3:376–384, 1969.Google Scholar
  9. [McN93]
    R. McNaughton. Infinite games played on infinite graphs. Ann. Pure Appl Logic, 65:149–184, 1993.Google Scholar
  10. [MPS95]
    O. Maler, A. Pnueli, and J. Sifakis. On the synthesis of discrete controllers for timed-systems. In Ernst W. Mayr and Claude Puech, editors, STACS 95, pages 229–242, Berlin, Heidelberg, New-York, 1995. Springer-Verlag.Google Scholar
  11. [PR89]
    A. Pnueli and R. Rosner. On the systhesis of a reactive module. In Proc. 16th ACM Sympos. on Principles of Prog. Lang., pages 179–190, Austin, 1989.Google Scholar
  12. [Sei95]
    S. Seibert. PhD thesis, University of Kiel, 1995. (in preparation).Google Scholar
  13. [Tho90]
    W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, chapter 4, pages 131–191. North-Holland, Amsterdam, 1990.Google Scholar
  14. [Tho95]
    W. Thomas. On effective strategies in infinite games. In Ernst W. Mayr and Claude Puech, editors, STACS 95, pages 1–13, Berlin, Heidelberg, New-York, 1995. Springer-Verlag.Google Scholar
  15. [Zie94]
    W. Zielonka. Infinite games on finitely coloured graphs with some applications. Manuscript, 1994.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Helmut Lescow
    • 1
  1. 1.Institut für Informatik und Praktische MathematikChristian-Albrechts-Universität KielKiel

Personalised recommendations