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.