COCO: Kontrolläquivalenz für Cyber-Physische Modelle

Nichtlineare Differentialgleichungen sind von überragender Bedeutung in der Modellierung von biochemischen, epidemiologischen, cyber-physischen und verteilten Systemen. Leider ist deren exakte Parametrisierung wegen Messungenauigkeiten und fehlender Information oft nicht möglich. Deswegen erfordert die Verifikation dynamischer Systeme mit ungewissen Parametern eine formale Approximation der zugrundeliegenden Dynamik. Ein Beispiel wäre etwa zu verifizieren, dass der Autopilot ein Flugzeug in einer stabilen Fluglage hält, wenn realistische Turbulenzen auftreten. Ein anderes Beispiel wäre ein Wettermodell dessen Vorhersage sich nicht dramatisch verändert, wenn Ausgangsparameter wie Wind und Temperatur im Rahmen ihrer Messgenauigkeit verändert werden. Leider ist die Berechnung guter Approximationen im Falle von nichtlinearen Systemen sehr zeitaufwendig. Ein universeller Ansatz zur Lösung schwieriger Probleme ist der der Modellreduktion. Die Idee ist zu einem ursprünglichen Problem ein kleineres, reduziertes Problem zu konstruieren. Das reduzierte Problem ist dabei so zu wählen, dass dessen Lösung die ursprüngliche Lösung ganz oder teilweise beschreibt. Trotz der Tatsache, dass die Modellreduktion im Kontext der Approximation dynamischer Systeme in der Vergangenheit studiert worden ist, gibt es zurzeit keine effizienten Algorithmen, die ein gegebenes nichtlineares Approximationsproblem automatisch reduzieren. Das Forschungsprojekt wird diese Lücke schließen, indem es Approximationsprobleme als Optimierungsprobleme der Kontrolltheorie auffassen wird. Die innovative Grundidee ist dabei Symmetrien in dynamischen Systemen durch einen effizienten Algorithmus zu erkennen und zu beweisen, dass das dazugehörige Optimierungsproblem ebenfalls symmetrisch ist und effizient reduziert werden kann. Das Projekt wird realistische nichtlineare Modelle biochemischer, cyber- physischer und verteilter Systeme approximieren, die zurzeit aufgrund ihrer Größe nicht approximiert werden können. Ferner werden die neu entwickelten Algorithmen in einem Softwaretool zur Verfügung gestellt werden.

Nichtlineare Modelle sind von überragender Bedeutung in der Modellierung von biochemischen, epidemiologischen, cyber-physischen und verteilten Systemen. Leider ist deren exakte Parametrisierung wegen Messungenauigkeiten und fehlender Information oft nicht möglich. Deswegen erfordert die Verifikation dynamischer Systeme mit ungewissen Parametern eine formale Approximation der zugrundeliegenden Dynamik. Leider ist die Berechnung guter Approximationen im Falle von nichtlinearen Systemen sehr zeitaufwendig. Ein universeller Ansatz zur Lösung schwieriger Probleme ist der der Modellreduktion. Die Idee ist zu einem ursprünglichen Problem ein kleineres, reduziertes Problem zu konstruieren. Das reduzierte Problem ist dabei so zu wählen, dass dessen Lösung die ursprüngliche Lösung ganz oder teilweise beschreibt. Trotz der Tatsache, dass die Modellreduktion im Kontext der Approximation dynamischer Systeme in der Vergangenheit studiert worden ist, gibt es zurzeit keine effizienten Algorithmen, die ein gegebenes nichtlineares Approximationsproblem automatisch reduzieren. Das Projekt initiierte die Suche nach effizienten verifikations-erhaltenden Reduktionsalgorithmen, wurde aber vorzeitig beendet, weil der Forschungsleiter --- nicht zuletzt dank des Meitner-Projekts --- eine außerordentliche Professur an der Universität Aalborg in Dänemark angetreten ist. Erste vorläufige Resultate, die den Weg zum Projektziel ebnen, wurden aber veröffentlicht.