Gerichtete ramseysche Quantoren mit Anwendungen in der formalen Verifikation

• Antragsteller: Professor Dr. Anthony Lin
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung seit 2023
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 522843867

In den letzten 15 Jahren ließ sich ein enormer Fortschritt im Bereich der automatisierten Verifikation erzielen. Im Rahmen der automatisierten Verifikation wird ein Berechnungsproblem als eine prädikatenlogische Formel modelliert, deren Belegungen den Lösungen des ursprünglichen Problems entsprechen. Der Fortschritt in der Entwicklung von effizienten SMT-Solvern (d.h. Algorithmen für Erfüllbarkeit Modulo Theorien) hat zahlreichen Anwendungen in der Industrie ermöglicht. Trotz des oben genannten Fortschritts bleibt ein Problem bestehen: wie lässt sich ein Berechnungsproblem auf ein SMT-Problem reduzieren, damit es mithilfe eines SAT/SMT-Solvers gelöst werden kann? Diese Frage stellte eine große Herausforderung dar. Daraus folgt unser Vorhaben: die Erweiterung von SMT-Theorien mit den sogenannten "gerichteten ramseyschen Quantoren" zu forschen. Mithilfe eines gerichteten ramseyschen Quantors lässt sich die Existenz einer gerichteten Clique beschreiben, wodurch zwei Anwendungen entstehen. Bei der ersten Anwendung handelt es sich um Liveness-Verifikation von unendlichen Systemen, die maßgeblich herausfordernder als Safety-Verifikation ist. Die zweite Anwendung betrifft monadische Dekomposition, d.h. eine mächtige Methode zur Behandlung von ausdrucksvolleren Theorien und zur Beschleunigung von rechenintensiven Methoden wie Quantorenelimination. Es sind bisher nur wenige Resultate zu Theorien erster Stufe (oder deren Fragmente) mit gerichteten ramseyschen Quantoren vorhanden. Das Ziel dieses Projekts ist es, einen großen Fortschritt in solchen erweiterten Theorien zu leisten, und zwar die Grundlagen (Entscheidbarkeit und Komplexität), die Entwicklung von Software-Tools (Integration mit SMT-Solvern) und die Umsetzung von solchen Algorithmen auf Anwendungen in der formalen Verifikation, einschließlich Liveness-Verifikation und monadische Dekomposition.

• DFG-Verfahren: Sachbeihilfen