Strukturelle und spielbasierte Analyse von Auswertungs- und Erfüllbarkeitsproblemen

• Antragsteller: Professor Dr. Stephan Kreutzer
• Fachliche Zuordnung: Sicherheit und Verlässlichkeit, Betriebs-, Kommunikations- und verteilte Systeme
• Förderung: Förderung von 2005 bis 2009
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 5448415

Aufgrund ihrer Allgemeinheit haben algorithmische Probleme der Logik vielfältige Einsatzgebiete in der Informatik. Zu den wichtigsten dieser Probleme gehört das Erfüllbarkeitsproblem der Aussagenlogik (SAT), mit wichtigen Anwendungen unter anderem in der künstlichen Intelligenz. Daneben sind Auswertungsprobleme temporaler Logiken von großer praktischer Bedeutung, vor allem im Bereich der Verifikation. Zur Lösung solcher Auswertungsprobleme hat sich ein Ansatz als sehr erfolgreich erwiesen, der auf Verfahren aus der Spiel- und Automatentheorie basiert. Prominentestes Beispiel dieses Ansatzes ist die Charakterisierung des modalen µ-Kalküls durch Paritätsspiele. Trotz intensiver Forschung sind hier noch zentrale Aspekte weitgehend unverstanden, etwa die genaue Komplexität des Paritätsspielproblems. Im Rahmen des Projekts sollen das SAT-Problem sowie spieltheoretische Verfahren zur Lösung von Auswertungsproblemen in der Verifikation untersucht werden. Kern des Projekts ist die Untersuchung der Zusammenhänge zwischen strukturellen Eigenschaften der Eingabeinstanzen und der Komplexität der betrachteten Probleme und Algorithmen. Weiterhin soll eine Theorie für eine neue Art von Spielen entwickelt werden, mit denen komplexere Eigenschaften von Systemen modelliert werden können, wie sie etwa aus der Verifikation nebenläufiger Prozesse erwachsen.

• DFG-Verfahren: Emmy Noether-Nachwuchsgruppen (Aktionsplan Informatik)