GRK 1298: Algorithmic Synthesis of Reactive and Discrete-continuous Systems (AlgoSyn)
Systems Engineering
Final Report Abstract
Während die formale Verifikation von Informatik-Systemen eine gut etablierte (und inzwischen auch industriell relevante) Disziplin darstellt, sind Methoden zur automatischen Synthese bisher nur rudimentär entwickelt. Ziel dieses Graduiertenkollegs war es, den Ansatz der algorithmischen Synthese auf mehreren Ebenen voranzubringen, und zwar in einer Kooperation von Grundlagenforschung, praktischer Informatik und Anwendungsprojekten. Hierzu kooperierten Forschungsgruppen der theoretischen Informatik (Logik, Algorithmik), der praktischen Informatik (Software-Engineering, Eingebettete Systeme) und der Ingenieurwissenschaften (Regelungstechnik, Prozessleittechnik, Bauingenieurswesen (Schienenverkehrsplanung)). Ausgangspunkt der Forschungen waren klassische Resultate der Automatentheorie zur algorithmischen Synthese von Finite-state-Programmen für Spezifikationen etwa in temporaler Logik. Dieses Fundament für die Zwecke der Controllersynthese zu nutzen und auszubauen, war der erste Schwerpunkt der Forschungen des Graduiertenkollegs. Ein wesentlicher Schritt war dabei die Erweiterung der betrachteten Systemmodelle durch Einbeziehung probabilistischer Aspekte und durch die Verknüpfung diskreten Verhaltens mit kontinuierlichen Parametern (hybride Systeme). Da sich die Aufgabe der Synthese unmittelbar auch in spieltheoretischer Form beschreiben lässt, nämlich als Konstruktion von Gewinnstrategien in Spielen, die in unterschiedlicher Weise formal spezifiziert sind, war der Forschungsbereich der algorithmischen Spieltheorie (insbesondere für Systeme mit mehreren Komponenten, also der Rahmen der Mehrpersonenspiele) ein weiterer Schwerpunkt der Grundlagenforschung. Um die Brücke zur Praxis der Systementwicklung zu schlagen wurden darauf aufsetzend Forschungsfragen zur Compilersynthese und zur automatisierten Synthese von Micro-Controllern untersucht (und gelöst). Schließlich wurden Aufgaben der Netzplantechnik (im Schienenverkehr) und der Prozessleittechnik im Verbund mit der Grundlagenforschung – vor allem durch die Konzeption geeigneter Formalisierungen – gelöst. Die Arbeiten der Promovierenden des Kollegs haben in allen genannten Feldern den Kenntnisstand auf internationaler Ebene wesentlich erweitert, was sich u.a. in Preisen für Dissertationen und in Best Paper Awards dokumentiert. Das Kolleg hat sichtbar dazu beigetragen, das Forschungsfeld der algorithmischen Synthese voranzutreiben; in der Tat ist die RWTH Aachen daher eine der führenden Adressen in diesem Bereich geworden. Innerhalb der RWTH Aachen hat die erfolgreiche Kooperation von Theoretikern, Praktikern und Ingenieuren zu einer stärkeren Integration der Forschung in unterschiedlichen Fakultäten geführt. Das Qualifizierungsprogramm enthielt neben zahlreichen gemeinsamen Veranstaltungen mehrere besondere Komponenten, darunter die Einbindung der Promovierenden in die Organisation (jährlich wechselndes „Steering Committee“ aus vier Promovierenden), die Erarbeitung eines Leitfadens „Mechanisms of Scientific Life“ (u.a. zur fairen Begutachtung wissenschaftlicher Arbeiten, zur Evaluierung von Wissenschaftler/inne/n und Institutionen, zum wissenschaftlichen Publikationswesen, zur Organisation von Tagungen). Hinzu kam ein vielfältiges und sehr erfolgreiches Programm zu Genderfragen, insbesondere das von der RWTH Aachen mit dem Brigitte-Gilles-Preis ausgezeichnete „Promotions-CAFÉ“. Die Kontakte mit anderen Graduiertenkollegs wurden nicht nur über die Vernetzungstreffen (jeweils im Juni in Dagstuhl) gepflegt sondern insbesondere auch durch die internationale Konferenz „Frontiers of Formal Methods“ im Februar 2015 in Aachen, bei der neben AlgoSyn drei weitere Graduiertenkollegs und ein österreichisches Forschungsnetzwerk als Mit-Organisatoren wirkten.
