Servicenavigation

Detailseite

Zurück

Projekt Druckansicht

Nichtklassische Logiken: Parametrisierte Komplexität und Enumeration

Antragsteller Professor Dr. Arne Meier
Fachliche Zuordnung Theoretische Informatik
Förderung Förderung von 2014 bis 2022
Projektkennung Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 247444366
 
Erstellungsjahr 2023

Zusammenfassung der Projektergebnisse

Abhängigkeiten auf funktionaler Ebene spielen eine wichtige Rolle im Bereich von Datenbanken. Es gibt jedoch auch Konzepte in anderen Gebiete (bspw. Spieltheorie, Social Choice Theorie oder Statistik) wie zum Beispiel physikalische Eigenschaften, die sich mit diesen Abhängigkeiten modellieren lassen. Modere Abhängigkeitslogiken formalisieren dies in der sogenannten Team Semantik mit Hilfe von speziellen Operatoren. Die zentralen Probleme für diese Logiken sind Modellverifikation sowie Formelkonsistenzprüfung; naheliegend sind Anwendungsszenarien in oben genannten Bereichen. Die Komplexität dieser Probleme ist jedoch häufig sehr hoch und erlaubt es nicht, diese von Computern in annehmbarer, d. h. praktikabler Zeit zu lösen. Bisher gab es noch keine Untersuchungen der parametrisierten Komplexität von Problemen in dieser Logik; hierbei sucht man nach sogenannten Parametern, welche in der Praxis konstant sind oder nur langsam wachsen und dadurch spezielle Algorithmen erlauben, die auf diese Parameter angepasst sind und ein schnelles Lösen erlauben. In diesem Kontext haben wir eine Reihe solcher effizienter Spezialfälle identifiziert. Ein weiteres Thema dieses Projekts war die Aufzählungskomplexität von Problemen. Bei Aufzählungsproblemen geht es darum, wie der Name schon besagt, alle Lösungen einer gegebenen Instanz aufzuzählen. Ein naheliegendes Praxisbeispiel ist die Tupelauflistung von Datenbankanfragen; wir sehen, dass auch hier wieder der Datenbankkontext von Relevanz ist. In der Enumeration dürfen keinesfalls Lösungen doppelt ausgeben werden und es soll möglichst ein uniformer Ausgabestrom erreicht werden. Man sagt, dass dies effizient geschieht, wenn man einen Algorithmus entwickeln kann, für den garantiert wird, dass maximal Polynomialzeit in der Eingabelänge zwischen zwei ausgegebenen Lösungen verstreicht und dies für alle ausgegebenen Lösungen gilt. Wir haben solche Algorithmen für die Aufzählung von erfüllenden Teams zu Formeln mit sogenannten lnklusionsabhängigkeiten entwickelt, die kurze Wartezeiten zwischen zwei ausgegebenen Teams haben. Des Weiteren haben wir gezeigt, dass es für andere Operatoren (funktionale (Un-)Abhängigkeiten) aller Voraussicht nach leider keine effizienten Aufzählungsalgorithmen geben wird. Den Ansatz der parametrisierten Komplexität haben wir auch für eine Fülle an weiteren Logiken und Konzepten im Bereich der KI erfolgreich eingesetzt. Im Folgenden gehen wir auf diese etwas genauer ein. Nicht-monotone Logiken sind entstanden, um menschliches Schließen zu formalisieren, welches von genau dieser Form ist: die Hinzunahme zusätzlicher Information kann möglicherweise dazu führen, dass weniger Schlussfolgerungen gezogen werden können, als es ohne diese der Fall gewesen ist. Abduktion ist ein solcher nicht-monotoner Formalismus, der im Bereich der medizinischen Diagnose eingesetzt wird. Die in diesem Projekt hierzu betrachteten Problemlösungsalgorithmen sind alle hochgradig ineffizient und erlauben kein effizientes Lösen der Probleme. Wir haben eine beinahe vollständige Analyse für spezielle Einschränkungen der Probleme durchgeführt, die eine Reihe an Fällen identifiziert, in denen die Probleme in der Praxis gelöst werden können. Logik-basierte beziehungsweise abstrakte Argumentation wird vielfältig in der künstlichen Intelligenz zum Modellieren und Evaluieren von Argumenten eingesetzt. Wir beantworten die bisher offene Frage nach der Zählkomplexität (Wie schwierig ist die Anzahl der Lösungen zu berechnen?) von Problemen in diesem Bereich und liefern optimale Algorithmen, die voraussichtlich keine weitere Verbesserung zulassen. In diesem Bereich haben wir auch eine Fülle an natürlichen Fragestellungen gefunden, die Repräsentanten für höhere Level in der Polynomialzeithierarchie sind. Dies verbesserte das Verständnis von höheren Graden an Ineffizienz von Problemen, welches bisher noch sehr beschränkt gewesen ist. Darüber hinaus haben wir eine allgemeine Technik (sogenannte Time Evaluation Functions) für Logiken entwickelt, welche es ermöglicht, zeitliche Aussagen über bestimmte Eigenschaften (soge­ nannte Hyperproperties) auszudrücken; diese spielen eine Rolle im Bereich von sicherheitskritischen Anwendungen. Des Weiteren haben wir zugehörige Verifikationsprobleme auf ihre Komplexität hin untersucht und haben gezeigt, dass diese äußerst stark eingeschränkt werden müssen, bevor eine Anwendbarkeit in der Praxis überhaupt möglich ist. Ohne diese Einschränkungen können diese Fragen niemals von Computern beantwortet werden.

Projektbezogene Publikationen (Auswahl)

 
 

Zusatzinformationen

© 2026 DFG Kontakt / Impressum / Datenschutz

Textvergrößerung und Kontrastanpassung