Symbolic Synthesis of Finite-State Controllers for Request-Response Specifications

  • Nico Wallmeier
  • Patrick Hütten
  • Wolfgang Thomas
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2759)


We present a method to solve certain infinite games over finite state spaces and apply this for the automatic synthesis of finitestate controllers. A lift-controller problem serves as an example for which the implementation of our algorithm has been tested. The specifications consist of safety conditions and so-called “request-response-conditions” (which have the form “after visiting a state of P later a state of R is visited”). Many real-life problems can be modeled in this framework. We sketch the theoretical solution which synthesizes a finite-state controller for satisfiable specifications. The core of the implementation is a convenient input language (based on enriched Boolean logic) and a realization of the abstract algorithms with OBDD’s (ordered binary decision diagrams).


Winning Strategy Boolean Formula Binary Decision Diagram Input Language Transition Formula 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    E. Clarke, O. Grumberg, and D. Peled. Model Checking. The MIT Press, Cambridge, Massachusetts, 1999.Google Scholar
  2. [2]
    J. Lind-Nielsen. Buddy-
  3. [3]
    H. Melcher. Hierarchische kompositionale Synthese von Steuerungen für reaktive Systeme. PhD thesis, Uni Karlsruhe, 2001.Google Scholar
  4. [4]
    D. Perrin and J.-E. Pin. Infinite Words (to appear). Elsevier,, 2003.
  5. [5]
    D. Schmitz and J. Vöge. Implementation of a strategy improvement algorithm for parity games. In Proceedings of the 5th International Conference on the Implementation and Application of Automata, CIAA 2000, pages 45–51, 2000.Google Scholar
  6. [6]
    W. Thomas. On the synthesis of strategies in infinite games. Lecture Notes in Computer Science, 900:1–13, 1995.CrossRefGoogle Scholar
  7. [7]
    W. Thomas. Languages, automata, and logic. In G. Rozenberg and A. Salomaa, editors, Handbook of Formal Languages, volume III, pages 389–455. Springer, New York, 1997.Google Scholar
  8. [8]
    W. Thomas. Infinite games and verification. In Proceedings of the International Conference on Computer Aided Verification CAV’02, volume 2404 of Lecture Notes in Computer Science, pages 58–64. Springer, 2002.CrossRefGoogle Scholar
  9. [9]
    J. Vöge and M. Jurdziński. A discrete strategy improvement algorithm for solving parity games. In Proceedings of the 12th International Conference on Computer Aided Verification, CAV 2000, volume 1855 of Lecture Notes in Computer Science, pages 202–215. Springer, 2000.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Nico Wallmeier
    • 1
  • Patrick Hütten
    • 1
  • Wolfgang Thomas
    • 1
  1. 1.Lehrstuhl für Informatik VIIRWTH AachenAachenGermany

Personalised recommendations