7,5 Millionen Euro EU-Förderung für Forschungsprojekt an der Grenze zwischen Mathematik und Theoretischer Informatik

Florian Luca (l.) und Joël Ouaknine (r.) vom Saarbrücker Max-Planck-Institut für Softwaresysteme. Foto: Bertram Somieski/ MPI-SWS

Sogenannte „diskrete dynamische Systeme“ bilden die Grundlage für rechenbasierte Problemstellungen in vielen Bereichen, von der Programmanalyse und computergestützten Verifizierung bis hin zu künstlicher Intelligenz und theoretischer Biologie. Die Entwicklung von Algorithmen, um diese Systeme mit automatisierten Verifizierungswerkzeugen zugänglich zu machen, stellt nach wie vor eine große Herausforderung dar. Forscher des Max-Planck-Instituts für Softwaresysteme in Saarbrücken und des französischen „Centre National de la Recherche Scientifique“ arbeiten nun daran, diese automatisierte Verifizierung voranzutreiben, mit umfangreicher finanzieller Unterstützung des Europäischen Forschungsrats.

Das interdisziplinäre Projekt mit dem Titel „Dynamical and Arithmetical Model Checking (DynAMiCs)“ wird von den drei verantwortlichen Wissenschaftlern Professor Joël Ouaknine, wissenschaftlicher Direktor am Max-Planck-Institut für Softwaresysteme (MPI-SWS) in Saarbrücken, Professor Florian Luca, ebenfalls MPI-SWS und Stellenbosch University in Südafrika, und Professor Valérie Berthé vom französischen „Institut de recherche en informatique fondamentale“ am „Centre National de la Recherche Scientifique (CNRS)“ an der Universität Paris Cité, geleitet. 

„Das Paradigma des ‚Model Checking‘ ist eine leistungsstarke Methode, mit der wir automatisch und mit mathematischer Sicherheit überprüfen können, ob sich ein System wie vorgesehen verhält“, sagt Prof. Joël Ouaknine. Viele diskrete dynamische Systeme – also Systeme, die sich im Laufe der Zeit nach bestimmten Regeln verändern – können derzeit jedoch nicht mit den verfügbaren Modellprüfungsansätzen verifiziert werden.  

Eines der Hauptziele dieses neuen Forschungsprojekts besteht daher darin, die Klassen und Eigenschaften dynamischer Systeme, die algorithmisch durch Modellprüfung erfasst werden können, erheblich zu erweitern. Die Forschenden wollen dabei insbesondere seit langem ungelöste mathematische Fragen wie das Skolem-Problem angehen, die zu Durchbrüchen beim Verständnis und der Überprüfung des Verhaltens anderer komplexer Systeme führen könnten.  

Das Skolem-Problem fragt, ob in einem System, das festgelegten mathematischen Regeln folgt, irgendwann ein bestimmter Zustand erreicht wird. Übertragen könnte diese Frage bedeuten, ob ein Computerprogramm unter bestimmten Bedingungen beendet wird, wann die Batterie eines Elektrofahrzeugs nach einem bestimmten Fahrmuster vollständig entladen ist, oder ob ein Fertigungsroboter ein genaues Ziel erreicht, indem er programmierten Bewegungsabläufen folgt. Obwohl es einfach erscheint, ist dieses mathematische Problem seit fast einem Jahrhundert ungelöst. 

Neben dem Skolem-Problem befasst sich das Projekt auch mit weiteren seit langem bestehenden mathematischen Herausforderungen wie der Pisot-Vermutung, der „piecewise-affine map reachability” und der Periodizitätsvermutung. Die Lösung dieser komplexen Probleme erfordert innovative Ansätze, die Fachwissen aus verschiedenen Bereichen der Mathematik und der Informatik vereinen. „Diese Projektfinanzierung ermöglicht es uns, die interdisziplinären Synergien zwischen verschiedenen Fachgebieten zu nutzen und Expertise zusammenzubringen, die sonst vielleicht nicht zusammengekommen wäre“, sagt Florian Luca. Im DynAMiCs-Projekt vereinen sich Kompetenzen in algorithmischer Verifikation unter der Leitung von Prof. Joël Ouaknine, symbolischer Dynamik unter der Leitung von Prof. Valérie Berthé und analytischer Zahlentheorie unter der Leitung von Prof. Florian Luca.  

Das Projekt wird über einen Synergy Grant des Europäischen Forschungsrats (ERC) in Höhe von insgesamt 7,5 Millionen Euro über sechs Jahre finanziert, wovon 5 Millionen Euro an das MPI-SWS gehen. ERC Grants gehören zu den renommiertesten Forschungspreisen weltweit, wobei Synergy Grants besonders kompetitiv sind und die höchsten Fördersummen bieten. In der aktuellen Förderrunde wurden 548 Anträge eingereicht, von denen nur 57 bewilligt wurden. 

Weitere Informationen:

Pressemeldung des Europäischen Forschungsrates: https://erc.europa.eu/news-events/news/erc-2024-synergy-grants-results
Liste der geförderten Projekte: https://erc.europa.eu/sites/default/files/2024-11/erc-2024-syg-results-all-domains.pdf
Pressemeldung der Max-Planck-Gesellschaft: https://www.mpg.de/23705070/erc-synergy-grants-2024 

Wissenschaftlicher Ansprechpartner (auf Englisch):

Professor Joël Ouaknine, PhD
Wissenschaftlicher Direktor MPI SWS und Coordinating Principal Investigator von DynAMiCs
Max Planck Institute für Softwaresysteme, Saarbrücken
Tel: +49 681 9303 9701
E-Mail: joel@mpi-sws.org 

Redaktion: 

Philipp Zapf-Schramm
Max-Planck-Institut für Informatik
Tel: +49 681 9325 4509
E-Mail: pzs@mpi-inf.mpg.de