Tradeoffs in Controller Synthesis (TriCS)

拟议项目的目标是通过开发技术来分析优化标准（如控制器的大小和质量）之间的权衡，并通过开发算法来计算相对于其中一个以上标准的最优控制器，从而提高自动控制器综合的适用性，并提高综合控制器的质量。这将允许合成具有较小内存需求的控制器，以最佳方式满足其规范（例如，考虑最小化请求与其响应之间的等待时间）。我们将研究三种类型的优化标准：大小、质量和前瞻性。目前，所有常见的规范形式都知道匹配内存需求的上限和下限。另一方面，最近很多人关注的是寻找控制器的偏好顺序，并开发合成算法，以产生最优（相对于这些顺序）控制器。我们在这里考虑的第三个维度是控制器实现规范所必需的输入前瞻量。根据目前的技术状况，有两种不同的综合方法：在内存需求的上限内计算控制器，但不考虑语义质量，或者计算比上限大得多的最优控制器。这就提出了一个问题：大小和质量之间是否存在权衡：最优控制器是否一定比一般控制器大？同样的问题也出现在前瞻性和规模或质量之间。该项目将回答这些重要的问题，从而通过同时考虑多个优化标准，将两种不同的综合方法结合起来。我们通过系统地研究文献中讨论的规范形式主义和偏好顺序的权衡的存在和程度，推进了综合技术的发展。因此，我们在规范形式的表达性、该形式的综合问题的算法复杂性以及综合控制器的大小等经典问题之外，为综合问题增加了一个新的方面。此外，我们将首次开发考虑多个优化标准的综合算法。

The goal of the proposed project is to increase the applicability of automated controller synthesis and to improve the quality of synthesized controllers} by developing techniques to analyze tradeoffs between optimization criteria like size and quality of the controller, and by developing algorithms to compute controllers that are optimal with respect to more than one of these criteria. This will allow to synthesize controllers with small memory requirements which satisfy their specification optimally (e.g., think of minimizing the waiting times between requests and their responses).We will study three types of optimization criteria, size, quality, and lookahead. Currently, matching upper and lower bounds on memory requirements are known for all common specification formalisms. On the other hand, recently much attention is paid to finding preference orders for controllers and to develop synthesis algorithms that yield optimal (with respect to these orders) controllers. The third dimension we consider here is the amount of lookahead on the inputs that is necessary for the controller to implement the specification.According to the state of the art there are two diverging approaches to synthesis: compute controllers within the upper bounds on memory requirements, but disregarding semantic quality, or to compute optimal controllers, which are much larger than the upper bounds. This raises the question whether there is a tradeoff between size and quality: are optimal controllers necessarily larger than generic ones? The same question arises between lookahead and size or quality, respectively.This project will answer these important questions and thereby join the two diverging approaches to synthesis by considering more than one optimization criterion at the same time. We advance the state of the art in synthesis by systematically studying the existence and extent of tradeoffs for the specification formalisms and preference orders discussed in the literature. Thereby, we add a new aspect to the synthesis problem beyond the classical ones like expressiveness of the specification formalism, algorithmic complexity of the synthesis problem for this formalism, and size of the synthesized controllers. Furthermore, for the first time, we will develop synthesis algorithms that take more than one optimization criterion into account.