Fully Automated and Correct-by-Construction Synthesis for Complex Control Problems

点击翻译按钮获取中文摘要

The technological developments in numerous areas of application are increasingly posing challenges, in the form of more and more complex control problems, that cannot be fully met using classical controller synthesis methods. Abstraction-based synthesis is a relatively recent approach possessing distinct advantages over classical methods, such as the capability of solving control problems for nonlinear continuous-state plants in a fully automated, correct-by-construction fashion, even for complex control objectives and in the presence of uncertainties and disturbances. However, some unresolved issues currently prevent the approach from being routinely applied. The applicant aims at advancing the theory and computational methods for abstraction-based controller synthesis to facilitate the practical applicability of the approach. In particular, methods should be provided that, firstly, are capable of solving more complex control problems than existing abstraction-based methods, that, secondly, are guaranteed to successfully synthesize a controller enforcing the specification whenever such a controller exists, and that, thirdly, yield controllers that are correct by construction. To meet these goals, established techniques to improve the efficiency ofabstraction-based controller synthesis, which currently apply only to rather simple control objectives, should be extended to cover a class of control objectives given as formulas in Linear TemporalLogic. Additionally, these techniques should be combined with entirely new approaches, to be explored in the project, which are based on exploiting the geometry of attainable sets computed in the synthesis process, on the adaptation of the computational accuracy on all algorithmic levels, and on the amortization of the cost of validated numerics, to drastically increase efficiency once again. The success of the project should be demonstrated through the solution of two challenging control problems whose treatment is beyond the capacity of existing abstraction-based methods.