Symbolic Synthesis of Finite-State Controllers for Request-Response Specifications
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).
KeywordsWinning Strategy Boolean Formula Binary Decision Diagram Input Language Transition Formula
Unable to display preview. Download preview PDF.
- E. Clarke, O. Grumberg, and D. Peled. Model Checking. The MIT Press, Cambridge, Massachusetts, 1999.Google Scholar
- J. Lind-Nielsen. Buddy-http://www.it-c.dk/research/buddy/
- H. Melcher. Hierarchische kompositionale Synthese von Steuerungen für reaktive Systeme. PhD thesis, Uni Karlsruhe, 2001.Google Scholar
- D. Perrin and J.-E. Pin. Infinite Words (to appear). Elsevier, http://www.liafa.jussieu.fr/~jep/Resumes/InfiniteWords.html, 2003.
- 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
- 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
- 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