Klassen von Graphen mit beschränkter Shrub-Weite

• Antragsteller: Dr. Roman Rabinovich
• Fachliche Zuordnung: Theoretische Informatik ; Mathematik
• Förderung: Förderung von 2018 bis 2019
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 420419861

Eine wichtige Aufgabe der Informatik ist automatische Verifikation der Eigenschaften von Systemen. Ein System kann eine komplexe und sicherheitskritische Maschine oder eine Konstruktion sein: ein Flugzeug oder ein AKW, ein Stadtplan, ein oder ein Programm. Eine Eigenschaft ist z.B., dass 3 Feuerwehrstationen in einer Stadt so platziert werden können, dass die Feuerwehr jede Adresse erreichen kann, ohne mehr als 5 Zwischenstationen zu besuchen. Für die automatische Verifikation solcher Eigenschaften müssen das System und die Eigenschaft formalisiert werden. Ein in der Informatik gängiger Formalismus für Systeme sind Graphen, deren Elemente Knoten heißen, wobei manche Knoten miteinander paarweise durch Kanten, verbunden sind. Unter vielen Methoden, mit denen man Eigenschaften formalisiert, sind Logiken ein klassisches Mittel. Eine logische Formel ist eine Zeichenfolge, die nach bestimmten Regeln gebaut ist, und eine Logik ist die Menge aller solcher Formeln. Eine Formel kann z.B. die Eigenschaft über die Feuerwehr von oben ausdrücken. Eine viel benutzte Logik ist die Prädikatenlogik (FO), die alle lokalen Eigenschaften wie die über die Feuerwehr ausdrücken kann.Obwohl es einen einfachen Brute-Force-Algorithmus gibt, der jede FO-Eigenschaft für jeden Graphen überprüft, ist seine Leistung fernab jeder praktischen Anwendung. Auf nicht zu großen Graphen für kleine Formeln wäre seine Laufzeit größer als die seit dem Urknall. Das Problem ist, dass sie von der Eingabegröße exponentiell abhängt, aber höchstens die Polynomialzeit gilt als noch als effizient. Es gibt jedoch theoretische Ergebnisse, aus denen folgt, dass die Existenz eines solchen Algorithmus unwahrscheinlich ist.Ein möglicher Weg, dieses Problems zu lösen, ist es den Begriff der Effizienz zu verfeinern. Die Idee ist, dass der Graph typischerweise groß und die Formel klein ist. Allerdings sogar unter konstanter Größe der Formel ist die Laufzeit inakzeptabel hoch: die Größe des Graphen hoch die Größe der Formel. Unser Ziel ist es, einen Algorithmus zu entwerfen, dessen Laufzeit eine Funktion der Größe der Formel mal die Größe des Graphen wäre, was in unserem Szenario deutlich kleiner wäre.Aber auch dieses Ziel scheint aus komplexitätstheoretischen Überlegungen unerreichbar zu sein. Ein bewährter Ansatz in theoretischer Informatik ist, sich auf Teilklassen der Graphen zu beschränken, die aber in der Praxis oft vorkommen. Eine lange Forschungsreihe bestimmte sehr reichhaltige dünnbesetzte Graphklassen, die ein effizientes Testen der FO-Eigenschaften erlauben. Ein Graph is dünnbesetzt, wenn er strukturell eine kleine Anzahl der Kanten im Vergleich zur der der Knoten aufweist.Wir wollen diese Ergebnisse auf dichte Graphen erweitern. Die Idee ist es, dünnbesetzte interne Strukturen in dichten Graphen zu finden und die Methoden aus dem dünnbesetzten Fall auf dichte Graphen zu verallgemeinern. Vorläufige Ergebnisse lassen uns glauben, dass die Shrub-Weite ein geeigneter Begriff dafür ist.

• DFG-Verfahren: Forschungsstipendien
• Internationaler Bezug: Frankreich
• Gastgeber: Professor Dr. Patrice Ossona de Mendez