Abstract
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).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
E. Clarke, O. Grumberg, and D. Peled. Model Checking. The MIT Press, Cambridge, Massachusetts, 1999.
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.
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.
W. Thomas. On the synthesis of strategies in infinite games. Lecture Notes in Computer Science, 900:1–13, 1995.
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.
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.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wallmeier, N., Hütten, P., Thomas, W. (2003). Symbolic Synthesis of Finite-State Controllers for Request-Response Specifications. In: Ibarra, O.H., Dang, Z. (eds) Implementation and Application of Automata. CIAA 2003. Lecture Notes in Computer Science, vol 2759. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45089-0_3
Download citation
DOI: https://doi.org/10.1007/3-540-45089-0_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40561-0
Online ISBN: 978-3-540-45089-4
eBook Packages: Springer Book Archive