We present a method to solve certain infinite games over finite state spaces and apply this for the automatic synthesis of finite-state 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). © Springer-Verlag Berlin Heidelberg 2003.
CITATION STYLE
Wallmeier, N., Hütten, P., & Thomas, W. (2003). Symbolic synthesis of finite-state controllers for request-response specifications. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2759, 11–22. https://doi.org/10.1007/3-540-45089-0_3
Mendeley helps you to discover research relevant for your work.