Tradeoffs in Controller Synthesis (TriCS)

• Applicant: Dr. Martin Zimmermann
• Subject Area: Theoretical Computer Science
• Term: from 2014 to 2019
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 255340027

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.

• DFG Programme: Research Grants
• Participating Person: Professor Dr. Bernd Finkbeiner