Thomas Schneider: Komplexität hybrider Logiken über transitiven Rahmen

Modale Logik ist eine ausdrucksstarke Erweiterung der klassischen Aussagenlogik. Eine Ausprägung davon ist temporale Logik, mit deren Hilfe man das zeitliche Verhalten von Dingen beschreiben kann. Dort kann man zusätzlich zur Sprache der klassischen Aussagenlogik über Operatoren verfügen, die besagen, "es gibt einen Zeitpunkt in der Vergangenheit/Zukunft, zu dem phi wahr ist" (Future/Past) oder "in der Zukunft wird phi wahr sein, und bis dahin gilt immer psi"' (Until bzw. Since).

Temporale Logik wird über Rahmen interpretiert. Das sind Strukturen, die aus einer Menge von Zeitpunkten und einer binären Relation ("später als") bestehen. Ohne Zweifel ist die Klasse aller transitiven Rahmen eine der wichtigsten Klassen für temporale Anwendungen.

Will man Zeitpunkte direkt benennen, so reicht das Ausdrucksvermögen der "einfachen" temporalen Logik nicht aus. Hybride Logik besitzt zusätzlich sprachliche Mittel, die das leisten. So kann man Zeitpunkten Namen zuweisen (mittels Nominals), zu benannten Zeitpunkten springen (mittels des at-Operators) und Variablen an Zeitpunkte binden (mittels des downarrow-Operators).

Über die Komplexität des Erfüllbarkeitsproblems für hybride Sprachen ist bereits einiges bekannt: Je nach Umfang der Sprache und zugrunde liegender Klasse von Rahmen (der Strukturen, über denen die jeweilige Logik interpretiert wird) sind NP-, PSPACE-, EXPTIME- und Unentscheidbarkeitsresultate bekannt. Allerdings gibt es Lücken für bestimmte Sprachen über eingeschränkten Klassen von Rahmen, von denen wir zwei schließen konnten. Wir zeigen, dass das Erfüllbarkeitsproblem über transitiven Rahmen für die hybride Sprache mit Since und Until EXPTIME-vollständig ist. Dies ist dieselbe Komplexität wie für diese Sprache über allgemeinen Rahmen. Wir beweisen außerdem, dass das Erfüllbarkeitsproblem über transitiven Rahmen für Fragmente zweier hybrider downarrow-Sprachen unentscheidbar ist.

Literatur:
Martin Mundhenk, Thomas Schneider: "New Pages for the Road-Map: Complexity of Hybrid Logics over Transitive Frames", http://www.minet.uni-jena.de/~thschnei/publ/index.html.