Tradeoffs in der Controllersynthese (TriCS)

• Antragsteller: Dr. Martin Zimmermann
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2014 bis 2019
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 255340027

Das Ziel dieses Projekts ist die ist die Anwendbarkeit der Controllersynthese zu erweitern und die Qualität der synthetisierten Controller zu verbessern. Dazu werden Techniken entwickelt, mit denen Tradeoffs zwischen verschiedenen Optimierungskriterien wie Größe und Qualität des Controllers untersucht werden können, und Algorithmen, die optimale Controller bezüglich mehrerer dieser Kriterien berechnen. Damit können Controller mit geringem Speicherverbrauch synthetisiert werden, die ihre Spezifikation optimal erfüllen (z.B. die Wartezeiten zwischen Anfragen und deren Antworten minimieren).Wir werden drei Arten von Optimierungskriterien studieren, Größe, Qualität und Lookahead. Für alle üblichen Spezifikationssprachen gibt es übereinstimmende obere und untere Schranken für den Speicherbedarf. Andererseits rückt die Suche nach Präferenzordnungen für Controller und die Entwicklung von Algorithmen, die optimale Controller berechnen, immer weiter in den Vordergrund. Die dritte Dimension die wir hier betrachten ist der Lookahead auf die Eingaben, der nötig ist, um die Spezifikation zu erfüllen. Nach dem aktuellen Stand der Technik gibt es zwei Ansätze zur Synthese: Controller innerhalb der Schranken für den Speicherbedarf zu berechnen, oder optimale Controller zu berechnen, die jedoch viel größer als die oberen Schranken sind. Es stellt sich also die Frage, ob es einen Tradeoff zwischen Größe und Qualität gibt: Sind optimale Controller notwendigerweise größer als generische? Diese Frage ergibt sich auch bei Lookahead und Größe beziehungsweise Qualität.In diesem Projekt werden wir diese wichtigen Fragen beantworten und damit die beiden divergierenden Ansätze zur Synthese vereinigen, indem wir mehrere Optimierungskriterien gleichzeitig betrachten. Mit diesem Projekt werden wir das Syntheseproblem neu beleuchten, indem wir die Existenz und das Ausmaß der Tradeoffs für Spezifikationssprachen und Präferenzordnungen aus der Literatur untersuchen. Damit betrachten wir einen neuen Aspekt des Problems der über die klassischen Dimensionen Ausdrucksstärke, algorithmische Komplexität und Größe der synthetisierten Controller hinausgeht. Des Weiteren werden wir zum ersten Mal Synthesealgorithmen entwickeln, die mehr als ein Optimierungskriterium in Betracht ziehen.

• DFG-Verfahren: Sachbeihilfen
• Beteiligte Person: Professor Dr. Bernd Finkbeiner