Verifikation und Synthese dynamischer Netzwerkalgorithmen

• Antragsteller: Professor Dr. Javier Esparza
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung seit 2025
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 551606821

Klassische Modelle des Verteilten Rechnens bestehen aus wenigen Agenten mit vielen Rechenressourcen, angeordnet in einer rigiden Kommunikationsstruktur (Reihe, Ring, Baum). Im Gegensatz dazu bestehen moderne Modelle aus einer sehr großen Anzahl von Komponenten (Billionen in einigen Bereichen des Natural Computings) mit sehr wenigen Ressourcen und einer ad-hoc Kommunikationsstruktur, die sich dynamisch ändern kann. Diese Rechenmodelle, oft kollektiv als dynamische Netzwerke bezeichnet, finden in Bereichen wie drahtlose Netzwerke, soziale Netzwerke, Nanotechnologien, Natural Computing und sogar in der Physik Anwendung. Populationsprotokolle sind das erfolgreichste Model der Theorie dynamischer Netzwerke. Ein Populationsprotokoll beschreibt das Verhalten einer „Suppe‘‘ ununterscheidbarer mobiler Agenten mit endlich vielen Zuständen. Die Agenten interagieren paarweise mit dem Ziel zu entscheiden, ob die Anfangskonfiguration der „Suppe‘‘ eine gegebene Eigenschaft erfüllt. In den letzten Jahren haben wir die ersten Softwarewerkzeuge für die automatische Verifikation der Korrektheit und Laufzeit eines Protokolls erstellt, sowie automatische Syntheseprozeduren entworfen, die, gegeben eine Eigenschaft, ein Populationsprotokoll produzieren, das sie entscheidet. Populationsprotokolle werden zurzeit aufgrund ihres großen Erfolgs und ihren Anwendungen im Bereich der molekularen Programmierung in verschiedenen Richtungen verallgemeinert. Diese erweiterten, mächtigeren Modelle haben zu revolutionären Fortschritten geführt, wie z.B. extrem effizienten verteilten Algorithmen für Leader Election und Mehrheitsbestimmung mit ununterscheidbaren Wählern, oder Implementierungen von Algorithmen auf chemischer oder biologischer Hardware. Das Ziel des Projekts ist die Entwicklung von Verifikations- und Synthesealgorithmen für diese verallgemeinerten Modelle und insbesondere für Chemical Reaction Networks, ein Berechnungsmodell mit Molekülen als Rechenagenten. Das Projekt wird die folgenden drei Fragen untersuchen: (1) Ausdrucksmächtigkeit. Welche Entscheidungsprobleme können von den neuen Modellen gelöst werden? (2) Formale Verifikation. Welche Verifikationsprobleme sind entscheidbar und mit welcher Komplexität? Wie können Unentscheidbarkeits- oder Komplexitätsbarrieren überwunden werden? (3) Synthese. Gibt es automatische Syntheseverfahren, die ein korrektes Protokoll für ein gegebenes Entscheidungsproblem ausgeben, innerhalb vorgegebener Ressourcenlimits? Die Resultate des Projekts werden auf Fallstudien der molekularen Programmierung und der Biologie sowie im Bereich der sozialen Netzwerke angewendet werden.

• DFG-Verfahren: Reinhart Koselleck-Projekte