Language guided controller synthesis for discrete time linear systems

Aydın Göl, Ebru
Lazar, Mircea
Belta, Calin
This paper considers the problem of controlling discrete-time linear systems from specifications given as formulas of syntactically co-safe linear temporal logic over linear predicates in the state variables of the system. A systematic procedure is developed for the automatic computation of sets of initial states and feedback controllers such that all the resulting trajectories of the corresponding closed-loop system satisfy the given specifications. The procedure is based on the iterative construction and refinement of an automaton that enforces the satisfaction of the formula. Interpolation and polyhedral Lyapunov function based approaches are proposed to compute the polytope-to-polytope controllers that label the transitions of the automaton. The algorithms developed in this paper were implemented as a software package that is available for download. Their application and effectiveness are demonstrated for two challenging case studies.
Citation Formats
E. Aydın Göl, M. Lazar, and C. Belta, “Language guided controller synthesis for discrete time linear systems,” 2012, vol. 7, Accessed: 00, 2020. [Online]. Available: