SCOPE

Kontext

Die Herausforderung bei der Entwicklung moderner Systeme liegt häufig in ihrer enormen Komplexität. Formale Methoden können eingesetzt werden, um die Eigenschaften solcher Systeme zu analysieren und die Auswirkungen von Veränderungen auf das Verhalten dieser Systeme zu verstehen. Dies ist besonders wichtig für kritische Systeme, die zuverlässig und widerstandsfähig gegenüber Fehlern und äußeren Einflüssen sein müssen. Mit Hilfe formaler Methoden kann auch nach Lösungen gesucht werden (z.B. Systemkonfigurationen), die bestimmte Eigenschaften optimal erfüllen.

Zielsetzung und Lösungsansatz

In diesem Projekt wird die Verwendung von Logik als vereinheitlichendes Werkzeug für die Modellierung, Argumentation, Suche und Erklärung optimaler Berechnungswege untersucht.

Ziel ist die Entwicklung eines formalen (und nachweislich korrekten) Ansatzes zur effizienten Suche nach optimalen Lösungswegen in Berechnungen unter Berücksichtigung verschiedener zu optimierender Parameter (Zeit, Vollständigkeit, Wirksamkeit, Kosten, Energieverbrauch usw.). Der Ansatz soll jedoch nicht nur optimale Lösungen berechnen, sondern auch den Lösungsweg sowie die resultierenden Lösungen nachvollziehbar und erklärbar machen. Erklärbarkeit ist eine wichtige Eigenschaft, die dem Benutzer erlaubt verschiedene Lösungen zu vergleichen, die Unterschiede zu verstehen und die optimale Lösung bzw. den optimalen Lösungsweg für den jeweiligen Einsatzzweck auszuwählen. Die Basis für diesen Ansatz bilden moderne SMT-Solver, die eine skalierbare und effiziente Lösungsfindung gewährleisten.

Ergebnis und Anwendungsbereiche

Der Fokus auf einen automatisierten, effizienten und flexiblen Ansatz ermöglicht, praktische Probleme in einer Vielzahl von Anwendungsbereichen wie Robotik, Automotive Systeme, Energie- und Ressourcenoptimierung oder auch Anwendungen im Gesundheitswesen zu entwickeln. Im Bereich der personalisierten Medizin bietet der Ansatz beispielsweise die Möglichkeit, komplexe Behandlungspläne optimal auf Patienten abzustimmen sowie die Patientensicherheit zu verbessern, indem Risiken von Wechsel- bzw. Nebenwirkungen von Medikationen vermieden werden.

Fördergeber

Das Projekt wird vom Wissenschaftsfonds FWF im Rahmen des Lise-Meitner-Programms gefördert.

Projektdauer

24 Monate (Juli 2022 - Juni 2024)