Obersemiarvortrag: Die Komplexität der bimodalen Logiken S4xS5 und SSL

Vortragende: Gisela Krommes

Termin: Dienstag, 4. Juni 2019, ab 12:45 Uhr

Ort: 41/0401

Titel: Die Komplexität der bimodalen Logiken S4xS5 und SSL

Zusammenfassung:

Eine fundamentale komplexitätstheoretische Aussage über Logik ist der Satz von Cook, der besagt, dass das Erfüllbarkeitsproblem der Aussagenlogik NP-vollständig ist. Seither ist die Komplexität vieler anderer Logiken untersucht worden. In diesem Vortrag beschäftigen wir uns mit den beiden bimodalen Logiken S4xS5 und SSL. Für beide Logiken war die Komplexität des Erfüllbarkeitsproblems bisher unbekannt. Maarten Marx hat vor zwanzig Jahren die Frage nach der Komplexität von S4xS5 aufgeworfen und die Vermutung formuliert, dass das Erfüllbarkeitsproblem der Logik S4xS5 EXPSPACE-vollständig ist. Wir zeigen, dass diese Vermutung richtig ist und dass auch das Erfüllbarkeitsproblem der Logik SSL EXPSPACE-vollständig ist.

Tatsächlich zeigen wir für beide Probleme einerseits, dass sie sogar in der Komplexitätsklasse ESPACE liegen. Die Algorithmen verwenden Ideen, die auch in Tableau-Verfahren verwendet werden. Der Kern des Beweises dafür, dass diese Probleme andererseits EXPSPACE-hart sind, ist eine in logarithmischem Platz durchführbare Reduktion des Wortproblems für sogenannte Alternierende Turingmaschinen, die in Exponentialzeit arbeiten, auf das Erfüllbarkeitsproblem der Logik SSL. Bekanntlich erkennen derartige Maschinen gerade die Sprachen, die von gewöhnlichen Turingmaschinen in exponentiellem Platz erkannt werden. Die EXPSPACE-Härte von S4xS5 zeigen wir schließlich durch eine ebenfalls in logarithmischem Platz durchführbare Übersetzung von SSL-Formeln in erfüllbarkeitsäquivalente S4xS5-Formeln.

Einführend werden wir auf das Wesen von modalen Logiken eingehen, die Konstruktion von bimodalen Logiken behandeln und die Logiken S4xS5 und SSL einführen. Außerdem werden wir die Arbeitsweise von Alternierenden Turingmaschinen kurz beschreiben.