Logik Teil 4: Prädikatenlogik zweiter Stufe
Übersicht Teil 4
2
• Kapitel 4.1: Syntax und Semantik
• Kapitel 4.2: Entscheidbarkeit und Komplexität
• Kapitel 4.3: MSO über linearen Strukturen
• Kapitel 4.4: Temporallogik
• Kapitel 4.5: Logik und Komplexitätstheorie
Prädikatenlogik Zweiter Stufe
3
Kapitel 4.1: Syntax und Semantik
Logik zweiter Stufe
4
Die Logik zweiter Stufe (SO) erweitert die Logik erster Stufe,behebt die meisten Unzulänglichkeiten in der Ausdrucksstärke
Grundidee:
Man kann nicht nur über Elemente von Strukturen quantifizieren,sondern auch über Mengen von Elementen und Relationen
Zum Beispiel definiert folgende SO-Formel die transitive Hülle von E:
! X(y)�
'(x, y) = 8X�
(X(x) ^ 8z8z0 (X(z) ^ E(z, z0) ! X(z0)))
„Jede Knotenmenge, die x enthält und unter Nachfolgernabgeschlossen ist, enthält auch y.“
Logik zweiter Stufe
5
Wir fixieren fur jedes n � 1 eine abzahlbar unendliche MengeVARn = {X1, X2, X3, . . . } von n-aren Relationsvariablen.
Wir werden sehen, dass die Logik zweiter Stufe (SO)
• eine sehr befriedigende Ausdrucksstärke hat
• eng mit anderen Gebieten der Informatik zusammenhängt, insbesondere den formalen Sprachen und der Komplexitätstheorie
Diesen Vorteilen steht aber eine (noch) schlechtere Berechnungs-komplexität als in FO gegenüber
SO sollte als interessante Logik zur Definition interessanter Eigenschaftenbetrachtet werden, weniger als Logik zu Deduktion.
Logik zweiter Stufe
6
Definition SO-Formeln
Sei ⌧ eine Signatur. Die Menge SO(⌧) der ⌧ -Formeln der Pradikatenlogikzweiter Stufe ist induktiv wie folgt definiert:
• sind t1, t2 2 T (⌧), dann ist t1 = t2 eine Formel
• sind t1, . . . , tn 2 T (⌧) und P 2 Rn(⌧), dann ist P (t1, . . . , tn) eine Formel
• sind t1, . . . , tn 2 T (⌧) und X 2 VARn(⌧), dann ist X(t1, . . . , tn)
eine Formel
• wenn ' und Formeln sind, dann auch ¬', (' ^ ), (' _ )
• wenn ' eine Formel ist und x 2 VAR, dann sind 9x' und 8x' Formeln
• wenn ' eine Formel ist und X 2 VARn, dann sind 9X '
und 8X ' Formeln
Ist die konkrete Signatur unwichtig, so schreiben wir auch einfach SO.
Sprechweisen und Konventionen
7
• Atome haben nun drei mogliche Formen:
t = t0, P (t1, . . . , tn), X(t1, . . . , tn)
• Die Quantoren 9X und 8X binden genau wie 9x und 8x
(starker als ^ und _, die wiederum starker als !, $).
• Relationsvariablen konnen ebenso wie Objektvariablenfrei oder gebunden vorkommen.
• Ein Satz ist eine Formel ohne freie Variablen beider Arten.
Semantik
8
Definition SO-Zuweisung, SO-Semantik
Wir gehen wieder in zwei Schritten vor: zunächst Terme, dann Formeln
Erweiterung der Erfulltheitsrelation |= auf SO:
• A,� |= X(t1, . . . , tn) gdw. (�(t1), . . . ,�(tn)) 2 �(X)
• A,� |= 9X ' mit X 2 VARn gdw. ein R ✓ An existiert mit A,�[X/R] |= '
• A,� |= 8X ' mit X 2 VARn gdw. fur alle R ✓ An gilt, dass A,�[X/R] |= '
Sei A eine ⌧ -Struktur. Eine SO-Zuweisung in A ist eine Abbildung �, die
• jeder Objektvariablen x 2 VAR ein Element �(x) 2 A und
• jeder n-aren Relationsvariablen X 2 VARn eine
n-are Relation �(X) ✓ An
zuweist. Wie in FO erweitert man � induktiv auf ⌧ -Terme.
Logik zweiter Stufe – Beispiele
9
Erreichbarkeit:
EVEN = {A | |A| geradzahlig }
! X(y)⌘'(x, y) = 8X
⇣ �X(x) ^ 8z8z0 (X(z) ^ E(z, z0) ! X(z0))
�
Func(R) = 8x8y8y0 ( R(x, y) ^ R(x, y0) ! y = y0 )
Func�(R) = 8x8y8y0 ( R(y, x) ^ R(y0, x) ! y = y0 )
' = 9R�8x9y R(x, y) _ R(y, x)
^8x ( 9y R(x, y) ! ¬9y R(y, x) )
^Func(R) ^ Func�(R)�
„Jede Knotenmenge, die x enthältund unter Nachfolgern abgeschlossen ist,enthält auch y.“
„A kann ohne Überlappungenmit R 2 VAR2 überdeckt werden.“
Logik zweiter Stufe – Beispiele
10
Unendliche Strukturen:
Endliche Strukturen:
⌘
¬'1
Auch Abzählbarkeit und Überabzählbarkeit sind definierbar.
Löwenheim-Skolem gilt also nicht (weder aufwärts noch abwärts).
'1 = 9R⇣9x9y R(x, y)^8x8y
�R(x, y) ! 9z R(y, z)
�^
8x ¬R(x, x)^8x8y8z
�(R(x, y) ^ R(y, z)) ! R(x, z)
�
„Man kann eine Teilmenge des Universums in einer irreflexiven,transitiven Ordnung ohne größtes Element anordnen.“
Logik zweiter Stufe – Beispiele
11
Betrachte folgende Menge von SO-Sätzen:
� = {¬�1} ⇥ {�n | n � 1}
Offensichtlich:
SO hat also nicht die Kompaktheits-Eigenschaft
wobei 'n = 9x1 · · · 9xn
V1i<jn xi 6= xj
„Die Struktur hatGröße � n.“
• � ist unerfullbar
• Jede endliche Teilmenge � ✓ � ist erfullbar(in einer Struktur der Große max{n | 'n 2 �})
Logik zweiter Stufe – Beispiele
12
Die Peano-Axiome (in leicht angepasster Form):
Wegen des aufsteigenden Satzes von Löwenheim-Skolem für FOgibt es keine FO-Formel, die das leistet!
LemmaA |= � gdw. A isomorph zu ( , nf, 0).
Betrachte Signatur mit Konstantensymbol 0, unarem Funktionssymbol nf
also lasst sich Arithmetik bis auf Isomorphie definieren!
• 8x nf(x) 6= 0
• 8x8y (nf(x) = nf(y) ! x = y)
• 8X⇣�
X(0) ^ 8x (X(x) ! X(nf(x)))�! 8x X(x)
⌘
In SO lassen sich basierend auf 0 und nf auch + und · definieren;
Einfache Resultate
13
Folgende Resultate überträgt man leicht von FO nach SO:
• Koinzidenzlemma und Isomorphielemma
• Existenz äquivalenter Formeln in Negationsnormalform und Pränex-Normalform (alle herstellbar in Linearzeit)
Die Dualität der Quantoren gilt auch für SO-Quantoren:
fur Relationsvariablen R
beliebiger Stelligkeit
¬9R ¬' ⌘ 8R'
¬8R ¬' ⌘ 9R'
MSO
14
Zusammenhang von Graphen ist MSO-ausdrückbar
Definition: Monadische Logik zweiter Stufe (MSO)
Für viele Zwecke genügen bereits unäre Relationsvariablen.
Beispiel:
Das resultierende MSO hat oft bessere Eigenschaften als volles SO.
' = 8X⇣ ⇣
9x X(x) ^8x8y
�(X(x) ^ E(x, y)) ! X(y)
�^
8x8y�
(X(x) ^ E(y, x)) ! X(y)� ⌘
! 8x X(x)⌘
Eine SO-Formel ' heißt monadisch,wenn sie keine Relationsvariablen mit Aritat > 1 enthalt.
MSO(⌧) ist die Menge aller monadischen Formeln aus SO(⌧ ).
„Jede Zusammenhangs-komponente enthältalle Knoten.“
Prädikatenlogik zweiter Stufe
15
Kapitel 4.2: Entscheidbarkeit und Komplexität
Auswertungsproblem
16
Der Algorithmus für das Auswerten von FO-Formeln kann leicht auf SO-Formeln erweitert werden.
Der erweiterte Algorithmus benötigt
• polynomiell viel Platz für MSO
• exponentiell viel Platz für volles SO
Dieser Platzverbrauch ist optimal, denn
• das MSO-Auswertungsproblem ist PSpace-vollständig
• das SO-Auswertungsproblem ist „ungefähr ExpSpace-vollständig“
Eine Analyse der Zeit komplexität zeigt aber wichtige Unterschiedezwischen FO und MSO!
Zur Erinnerung: der Algorithmus für FO
17
ausw(A,�,')
case' = (t = t0): return 1 if �(t) = �(t0), else return 0
' = P (t1, . . . , tk): return 1 if (�(t1), . . . ,�(tk)) 2 PA, else return 0
' = ¬ : return 1�ausw(A,�, )
' = ^ #: return min{ausw(A,�, ), ausw(A,�,#)}' = _ #: return max{ausw(A,�, ), ausw(A,�,#)}' = 9x :
rufe ausw(A,�[x/a], ) fur alle a 2 A
return 1 if ein Ruf erfolgreich, else return 0
' = 8x :rufe ausw(A,�[x/a], ) fur alle a 2 A
return 1 if alle Rufe erfolgreich, else return 0endcase
Erweiterung des Algorithmus auf SO
18
Fälle für die SO-Teilformeln:
case' = X(t1, . . . , t`): return 1 if (�(t1), . . . ,�(t`)) 2 �(X),
else return 0
' = 9X wobei X eine `-stellige Relationsvariable:rufe ausw(A,�[X/B], ) fur alle B ✓ A`
return 1 if ein Ruf erfolgreich, else return 0
' = 8X wobei X eine `-stellige Relationsvariable:rufe ausw(A,�[X/B], ) fur alle B ✓ A`
return 1 if alle Rufe erfolgreich, else return 0endcase
Platzkomplexität von Auswertung
19
Lemma
Das Auswertungsproblem ist damit für MSO PSpace-vollständig,genauso wie für FO.
Warum beruht SQL dann auf FO und nicht auf dem deutlichausdrucksstärkeren MSO?
Zur Antwort betrachten wir die Zeit komplexität des Auswertungsproblems
Der Algorithmus benotigt
1. polynomiell viel Platz, wenn die Eingabe eine MSO-Formel ist
2. exponentiell viel Platz im Allgemeinen
Zeitkomplexität von Auswertung
20
Lemma
Beachte: in Anwendungen ist ...
Diese Komplexitäten kann man (wahrscheinlich) nicht wesentlich verbessern
Diese Beobachtungen führen zur Idee der Datenkomplexität
• n meist sehr groß (Datenbank, zu verifizierendes System, . . . )
• k meist eher klein (Datenbankanfrage, zu verifizierende Eigenschaft, . . . )
Bei Eingabe einer Struktur A der Große n und einer Formel ' derGroße k benotigt der Algorithmus
1. Zeit O(nk), wenn ' eine FO-Formel ist
2. Zeit 2O(nk), wenn ' eine MSO-Formel ist
3. Zeit 2O(n2k) im Allgemeinen.
Datenkomplexität von Auswertung
21
Aus dieser Perspektive:die Zeitkomplexität von (M)SO ist für praktischen Einsatz zu groß!
LemmaBei Eingabe einer Struktur A der Große n benotigt der Algorithmus
1. Zeit poly(n) wenn eine FO-Formel ausgewertet wird
2. Zeit 2O(n) wenn eine MSO-Formel ausgewertet wird
3. Zeit 2poly(n) wenn eine SO-Formel ausgewertet wird
Der Algorithmus hat dann folgende Komplexität:
Bei der Datenkomplexitat betrachtet man
• nur die Struktur A als Eingabe (die Datenbank bzw. das System)
• die Formel ' als fixiert, also ist ihre Große k eine Konstante.
Komplexität von Gültigkeit
22
Theorem
Auch die erfüllbaren Formeln und unerfüllbaren Formeln sind natürlich nicht rekursiv aufzählbar; das alles gilt bereits in MSO.
Das bedeutet natürlich:Theorembeweisen im Sinne von FO ist in SO nicht möglich.
Gültigkeit ist in SO (und MSO) ein noch schwierigeres Problem als in FO
Es gibt trotzdem SO-Beweiser (wie Isabelle/HOL),die aber vom Benutzer „geleitet“ werden müssen.
Wenn ⌧ mind. ein binares Relationssymbol enthalt,ist die Menge der Tautologien in SO(⌧) nicht rekursiv aufzahlbar.
Prädikatenlogik zweiter Stufe
23
Kapitel 4.3: MSO über linearen Strukturen
MSO über linearen Strukturen
24
Eine wichtige Eigenschaft von MSO ist die Entscheidbarkeit von Erfüllbarkeit, Gültigkeit, etc. über eingeschränkten Strukturklassen:
• endliche und unendliche lineare Strukturen
• endliche und unendliche Baumstrukturen
Diese Strukturen liefern auch einen interessanten Zusammenhang zuden formalen Sprachen, denn
endliche lineare Struktur ≈ Wort im Sinne der formalen Sprachen
Der Einfachheit halber betrachten wir hier nur endliche lineare Strukturen,also Wörter
MSO über linearen Strukturen
25
Definition MSO eines Nachfolgers (S1S)Die Menge S1S der MSO-Formeln eines Nachfolgers sind die MSO-Formeln in der folgenden Signatur:
• ein Konstantensymbol „0“
• ein einstelliges Funktionssymbol „s“ (für „successor“, „Nachfolger“)
• ein zweistelliges Relationssymbol „<“
• einstellige Relationssymbole P1, P2, P3, . . .
In S1S sind nur Strukturen A zugelassen mit A = {0, . . . , n} für ein n � 0.Die Interpretation aller Symbole außer der Pi ist wie folgt fixiert:
• 0A = 0;
• sA(n) = n + 1 wenn n + 1 2 A, sonst sA(n) = n
• <A = {(n, m) | n, m 2 A ^ n < m}
S1S Beispiel 1
26
Lineare Strukturen modellieren Läufe von Systemen in der Verifikation
0
Zum Beispiel:
1 2 3 4
S1S beschreibt zu verifizierende Eigenschaften, z.B.:
Wi: Prozess i wartet auf kritischen Abschnitt
Ai: Prozess i im kritischen Abschnitti � {1, 2}
W1 A1 A1
W2
A2 A2
W1
5A1
s s s s s s
Die Elemente des Universums entsprechen dann Zeitpunkten
¬9x�
A1(x) ^ A2(x)�
^
i2{1,2}8x
⇣Wi(x) ! 9y ( x < y ^ Ai(y) )
⌘
S1S Beispiel 2
27
S1S Struktur ≈ Wort
Fur das Alphabet �n := {0, 1}n gilt die Entsprechung
Wir beschranken uns auf endlich viele Relationssymbole P1, . . . , Pn
uber ⌃n im Sinne der formalen Sprachen
Beispiel fur n = 2:
0 1 2 3 4P1 P1
P2
P2 P1
P2
ss
s s s
�00
�= a
�10
�= b
�01
�= c
�11
�= d
entspricht Wort�10
��11
��00
��01
��11
�
Spezielle Form des Alphabetes keine Einschrankung,
obiges Wort wird z.B. bdacd bei Zuordnung
S1S Beispiel 2
28
Mit dieser Beobachtung werden die S1S-Sätze zum Werkzeug zurDefinition von formalen Sprachen
Definition MSO-definierte Sprache
L(�) = {w � �n | w |= �}
Ein S1S-Satz � mit Symbolen P1, . . . , Pn definiert folgende Spracheuber dem Alphabet �n = {0, 1}n:
Welche Klasse von Sprachen lässt sich mittels S1S/MSO definieren?
S1S-Strukturen uber P1, . . . , Pn und Worter uber ⌃n sind also
genau dasselbe, nur leicht unterschiedlich präsentiert.
Büchi-Elgot-Trakhtenbrot
29
Interessanterweise sind die MSO-definierbaren Sprachen nichts anderes als die regulären Sprachen.
Um zu beweisen, dass jede MSO-definierbare Sprache regulär ist,zeigen wir:
Dies zeigt auch:
Erfüllbarkeit und Gültigkeit in S1S ist entscheidbar
und das Leerheitsproblem für endliche Automaten ist entscheidbarDenn � ist erfullbar gdw. L(�) 6= ;,
Jeder S1S-Satz ' kann in einen endlichen Automaten A'
gewandelt werden, so dass L(') = L(A').
Eine technische Anmerkung
30
In logischen Strukturen darf das Universum per Def. nicht leer sein.
Daher hat das leere Wort keine Entsprechung als logische Struktur.
Wir betrachten daher im Folgenden ausschließlich Sprachen, die das leere Wort nicht enthalten:
z.B. ist also mit „reguläre Sprache“ gemeint:„reguläre Sprache, die nicht das leere Wort enthält“.
Aus Sicht der formalen Sprachen ist das Weglassen des leeren Wortes keine wesentliche Änderung.
Büchi-Elgot-Trakhtenbrot
31
Theorem von Büchi-Elgot-TrakhtenbrotFur jede formale Sprache L sind aquivalent:
1. L ist regular
2. L = L(�) fur einen S1S-Satz �
Wir beweisen zunächst 1 ) 2:
Übersetzung von endlichen Automaten in „äquivalenten“ S1S-Satz
Büchi-Elgot-Trakhtenbrot
32
LemmaJeder S1S-Satz kann effektiv in einen aquivalenten Satz in Normal-form gewandelt werden.
Beweis von 2 ) 1:
zunachst bringen wir den S1S-Satz in eine geeignete Normalform:
• FO-Variablen werden nicht verwendet
• atomare Formeln haben die Form
– X ✓ Y , mit Semantik 8x ( X(x) ! Y (x) )
– succ(X) = Y , mit Semantik„X und Y sind Einermengen {k} und {`} mit ` = k + 1“
wobei X und Y Relationsvariablen oder Relationssymbole sind
• (die Symbole 0, <, s werden also nicht verwendet)
Büchi-Elgot-Trakhtenbrot
33
Theorem von Büchi-Elgot-Trakhtenbrot
Die strukturelle Induktion macht es notwendig, auch Formelnmit freien Variablen zu betrachten
Diese werden wie die unaren Relationssymbole P1, P2, . . . behandelt,
z.B. liefert ⇥Y�
X � Y ⇤ P1 � Y�
Sprache uber �2 = {0, 1}2
Fur jede formale Sprache L sind aquivalent:
1. L ist regular
2. L = L(�) fur einen S1S-Satz �
Wir beweisen nun 2 ) 1:
Induktive Übersetzung von S1S-Formeln in Normalformin „äquivalenten“ endlichen Automaten (NEA)
FO und formale Sprachen
34
Welche Sprachklasse entspricht den F1S-definierbaren Sprachen?
Da MSO-Definierbarkeit genau den regulären Sprachen entspricht,ist eine natürliche Frage:
Definition: sternfreie Sprachen
Beachte: Im Unterschied zu den regulären Sprachen steht derKleene-Stern nicht zur Verfügung, dafür aber Komplement
Sei F1S die Einschränkung von S1S auf FO
Die Klasse der sternfreien Sprachen uber einem Alphabet ⌃ist die kleinste Klasse, so dass:
• ; und {a} sind sternfreie Sprachen fur alle a 2 ⌃.
• wenn L und L0 sternfreie Sprachen sind, dann auchL = ⌃⇤ \ L, L \ L0, L [ L0 und L � L0 = {ww0 | w 2 L, w0 2 L0}.
FO und formale Sprachen
35
Theorem
Dieses Resultat ist erheblich schwieriger zu beweisen als das Theoremvon Büchi-Elgot-Trakhtenbrot
Ohne Beweis:
Beispiel für eine nicht sternfreie/F1S-definierbare reguläre Sprache:
Leven = {w � {0, 1}⇤ | |w| ist geradzahlig }
Beweis mittels EF-Spielen möglich
Fur jede formale Sprache L sind aquivalent:
1. L ist sternfrei
2. L = L(�) fur einen F1S-Satz �
Entscheidbarkeit S1S
36
TheoremIn S1S sind Erfullbarkeit und Gultigkeit entscheidbar.
Die Komplexität ist jedoch beträchtlich:
Es gibt trotzdem Reasoner für (Varianten von) S1S wie Mona
• jede Negation: konstruierter NEA wird exponentiell größerer DEA jede existentielle Quantifizierung macht aus DEA wieder NEA
• das Entscheidungsverfahren ist daher nicht-elementar; man kann beweisen, dass es nicht besser geht
Da Leerheit von endlichen Automaten entscheidbar:
� erfullbar gdw. es gibt S1S-Struktur w mit w |= � gdw. L(A') �= ⇥Fur jeden S1S-Satz ':
Entscheidbarkeit S1S
37
Das Entscheidbarkeitsresultat lässt sich auf einige andere wichtigeStrukturklassen übertragen
TheoremMSO ist uber den folgenden Strukturklassen entscheidbar:
• unendliche lineare Strukturen (unendl. Worter)
• endliche und unendliche Baumstrukturen
Der Beweis ist im Prinzip ähnlich, außer dass
1. man andere Arten von Automaten benötigt, die unendliche Wörter bzw. endliche/unendliche Bäume verarbeiten
2. einige der Konstruktionen erheblich anspruchsvoller werden (insbesondere das Komplementieren von Automaten)
(siehe auch Master-Kurs „Automatentheorie und ihre Anwendungen“)
Prädikatenlogik Zweiter Stufe
38
Kapitel 4.4: Temporallogik
Temporallogik
39
In der Verifikation verwendet man S1S meist nicht direkt, sondernspezialisierte Temporallogiken wie LTL, CTL und das μ-Kalkül
0
Nochmal das Verifikations-Beispiel:
1 2 3 4
Wi: Prozess i wartet auf kritischen Abschnitt
Ai: Prozess i im kritischen Abschnitti � {1, 2}
W1 A1 A1
W2
A2 A2
W1
5A1
s s s s s s
Eigenschaften kann man nun statt in S1S auch z.B. in LTL beschreiben:
¬9x�
A1(x) ^ A2(x)�
^
i2{1,2}8x
⇣Wi(x) ! 9y ( x < y ^ Ai(y) )
⌘¬3(A1 ^ A2)
^
i2{1,2}2(Wi ! 3Ai)
↝↝
LTL: Syntax
40
Wir werfen einen kurzen Blick auf LTL (Linear Temporal Logic)
Sie verhalten sich ähnlich wie Aussagenvariablen der Aussagenlogik, können allerdings zu jedem Zeitpunkt einen unterschiedlichen Wahrheitswert annehmen.
Fixiere eine abzahlbar unendliche Menge TVAR = {p1, p2, p3, . . . } vontemporalen Aussagenvariablen.
Diese Variablen entsprechen den unaren Relationssymbolen Pi in S1S.
LTL: Syntax
41
Definition LTL-SyntaxDie Menge der LTL-Formeln ist induktiv definiert wie folgt:
• jede temporale Aussagenvariable ist eine LTL-Formel
• wenn ' und LTL-Formeln sind, dann auch
¬'' ^ ' _ #' „im nächsten Zeitpunkt '“3' „in Zukunft irgendwann '“2' „in Zukunft immer '“' U „' until “
LTL: Semantik
42
Die Semantik von LTL basiert üblicherweise auf unendlichen linearenStrukturen; wir verwenden hier endliche S1S-Strukturen
Definition LTL-Semantik
LTL Formeln haben einen Wahrheitswert, der abhängig ist vom Zeitpunkt
Wir definieren Erfulltheitsrelation (A, n) |= ' induktiv,fur S1S-Struktur A, Zeitpunkt n 2 A und LTL-Formel ':
• A, n |= pi gdw. n 2 PAi
• A, n |= ¬' gdw. A, n 6|= ', ahnlich fur ^ und _
• A, n |= #' gdw. n + 1 2 A und A, n + 1 |= '
• A, n |= 3' gdw. 9m 2 A mit m � n und A, m |= '
• A, n |= 2' gdw. 8m 2 A mit m � n gilt: A, m |= '
• A, n |= ' U gdw. 9m 2 A, so dass m � n,A, k |= ' fur n k < m und A, m |=
LTL versus F1S
43
• Syntaktisch kann man LTL als Erweiterung von Aussagenlogik auffassen
• Semantisch handelt es sich eher um eine Logik erster Stufe, bei der die FO-Variablen aber implizit sind
• Derartige Logiken nennt man auch Modallogik
Beachte:
Lemma
Eine LTL-Formel ' ist initial aquivalent zu einer S1S-Formel (x)
mit einer freien Variablen wenn A, 0 |= ' gdw. A |= [0] fur alle A.
Zu jeder LTL-Formel ' existiert eine initial aquivalente F1S-Formel (x).
LTL versus F1S
44
Theorem (Kamp)
Sehr viel überraschender (und schwieriger zu beweisen):
Also ist LTL bzgl. Ausdrucksstärke nichts anderes als Logik erster Stufe!
(es folgt auch: in LTL lassen sich genau die sternfreien Sprachen definieren)
Zu jeder F1S-Formel '(x) mit einer freien Variablen existiert eine initialaquivalente LTL-Formel .
LTL: Komplexität
45
Diese Differenz in der Knappheit (engl. Succinctness) schlägt sichin der Komplexität von Erfüllbarkeit/Gültigkeit wieder:
Theorem
Bei der Ubersetzung F1S ) LTL kann die Formel nicht-elementargroßer werden.
Das Auswertungsproblem ist für LTL ebenfalls PSpace-vollständig,wie für MSO/S1S und F1S.
Das Erfullbarkeitsproblem und das Gultigkeitsproblem sind
• PSpace-vollstandig in LTL
• nicht-elementar in F1S (und S1S)
Beide Probleme werden einfacher (NP-vollstandig), wenn mannicht alle temporalen Operatoren zulasst (z. B. nur 3, 2 oder nur #)
Weitere Verifikationslogiken
46
Insbesondere hat das temporale μ-Kalkül dieselbe Ausdrucksstärkewie S1S
Es gibt in der Verifikation noch andere wichtige Logiken, z.B.:
• CTL, CTL* und das μ-Kalkül für Baumstrukturen
(Branching time: es gibt mehr als eine mögliche Zukunft, z.B. wegen unbekannter Benutzer-/Sensoreingabe)
• das temporale μ-Kalkül für lineare Strukturen (wie LTL)
Prädikatenlogik Zweiter Stufe
47
Kapitel 4.5: Logik und Komplexitätstheorie
Deskriptive Komplexitätstheorie
48
Es besteht ein enger Zusammenhang zwischen (Fragmenten von) SOund verschiedenen in der Informatik wichtigen Komplexitätsklassen.
Die grundlegende Beobachtung ist:
Die in existentiellem SO definierbaren Entscheidungsprobleme sind exakt die Probleme in der Komplexitätsklasse NP.
Diese und ähnliche Beobachtungen erlauben ein Studium von komplexitätstheoretischen Fragen wie „P vs NP“ mit logischen Mitteln.
Man nennt diese Forschungsrichtung Deskriptive Komplexitätstheorie.
„Existentielles SO“ (ESO) meint dabei Formeln der Form
9X1 · · · 9Xn ', Xi beliebige Aritat und ' FO-Formel
Deskriptive Komplexitätstheorie – Beispiel 1
49
3-Färbbarkeit ist ein wohlbekanntes NP-vollständiges Problem
Definition (3-Färbbarkeit)
^
1i<j3
¬(Ci(x) � Cj(x)) �
E(x, y) �^
1i3
¬(Ci(x) ⇥ Ci(y)� ⌘
Betrachte
Diese ESO-Formel definiert 3F:
Ein ungerichteter Graph G = (V, E) ist 3-farbbar gdw. es eineAbbildung f : V ! {r, g, b} gibt, so dass gilt:
• fur alle {v1, v2} 2 E ist f(v1) 6= f(v2)
3F ist die Klasse aller 3-farbbaren Graphen.
G |= '3F gdw. G 2 3F fur alle ungerichteten Graphen G
'3F = 9C19C29C3
⇣8x8y
�(C1(x) _ C2(x) _ C3(x)) ^
Deskriptive Komplexitätstheorie – Beispiel 2
50
Das Hamiltonkreis-Problem ist ein weiteres NP-vollständiges Problem
Definition (Hamiltonkreis) Sei G = (V, E) ein ungerichteter Graph. Ein Hamiltonkreis in G ist eingeschlossener Pfad, der jeden Knoten genau einmal enthalt.
HK ist die Klasse aller Graphen, die einen Hamiltonkreis enthalten.
Die folgende ESO-Formel definiert HK:
S ist Nachfolgerrelation von L,
verbindet zusatzlich großtes L-Element mit kleinstem ^
alle Elemente des Universums kommen in L vor ^
8x8y�
S(x, y) ! E(x, y)� ⌘
binär
'HK = 9L 9S⇣
L ist strikte lineare Ordnung ^
Fagins Theorem
51
Wenn man mit Turingmaschinen arbeitet, repräsentiert man
• Probleminstanzen als Wörter
• Entscheidungsprobleme als Mengen von Wörtern
Wir stellen hier Logik in den Mittelpunkt, repräsentieren
• Probleminstanzen als endliche relationale Strukturen
• Entscheidungsprobleme als Klassen von solchen Strukturen
Dies stellt keinerlei Einschränkung der Allgemeinheit dar:
jedes Entscheidungsproblem kann sowohl als Menge von Wörternals auch als Klasse von endlichen Strukturen dargestellt werden
Fagins Theorem
52
Definition (ESO-definierbare Probleme)
Schon gesehen: 3F und HK sind ESO-definierbar
Um präzise machen zu können, was wir damit meinen, dass ein Problem(Klasse von endlichen relationalen Strukturen) in NP ist, müssen wir Probleminstanzen (Strukturen) als Wörter darstellen
Ein Problem (Klasse von endlichen relationalen Strukturen) K istESO-definierbar, wenn es einen ESO-Satz 'K gibt, so dass
A 2 K gdw. A |= 'K fur alle endlichen Strukturen A
Fagins Theorem
53
Wir fixieren eine beliebige lineare Ordnung auf A, z.B. a1 � · · · � an
Eine einzelne k-stellige Relation RA wird wie folgt kodiert:
• betrachte die lexikographische Ordnung aller k-Tupel uber A:
(a1, . . . , a1), (a1, . . . , a1, a2), · · · , (an, . . . , an, an�1), (an, . . . , an)
(entspricht Zahlen zur Basis n)
• reprasentiere RA als Wort wR � {0, 1}⇤ der Lange nk:
das i-te Symbol ist
(1 wenn das i-te k-Tupel in RA ist0 sonst
Sei A eine endliche ⌧ -Struktur mit A = {a1, . . . , an}.
wA = 0|A|1| {z }
Große A
0s11wR1| {z }RA
1
0s21wR2| {z }RA
2
· · · 0s`1wR`| {z }RA
`
Fur ⌧ = {R1, . . . , R`} und sj = Stelligkeit(Rj) reprasentieren wir A als Wort
Fagins Theorem
54
Beachte:
• das Prafix 0n1 kodiert die (endliche) Große von A
• ohne diese Information kann man aus wR1· · · wR`
die RelationenRA
1 , . . . , RA� nicht auf eindeutige Weise extrahieren
„Unsere“ Definition von NP ist nun wie folgt:
Ein Problem (Klasse von endlichen relationalen Strukturen) K ist in NP,wenn es eine nichtdeterministische Turingmaschine MK gibt, so dass:
1. A 2 K gdw. wA 2 L(MK)
2. bei Eingabe wA terminiert MK in Zeit poly(|wA|)
Beachte zu Punkt 2: |wA| ist polynomiell in der Große von A
Fagins Theorem
55
Theorem (Fagin)
Dieses Theorem stellt eine vollkommen maschinenunabhängigeCharakterisierung von NP zu Verfügung.
Es reduziert das schwierige Problem der Trennung von Komplexitäts-klassen (z. B. P von NP) auf ein rein logisches Problem
Man sagt auch: ESO erfasst (engl. captures) NP
Leider ist bis heute im Allgemeinen nicht klar,welche Logik der Komplexitätsklasse P entspricht.
Fur jedes Problem K gilt: K ist in NP gdw. K ist ESO-definierbar.
Fagins Theorem
56
Es folgt leicht aus Fagins Theorem:
Korollar
Das „NP vs coNP“-Problem ist also: haben ESO und USO auf endlichenrelationalen Strukturen dieselbe Ausdrucksstärke?
Theorem (Fagin) Fur jedes Problem K gilt: K ist in NP gdw. K ist ESO-definierbar.
Beachte: wenn man NP ≠ coNP zeigen könnte (wie allgemein vermutet), dann folgt daraus auch P ≠ NP!
Fur jedes Problem K gilt: K ist in coNP gdw. K ist USO-definierbar.(USO = universelles SO)
Fagins Theorem – Beweis
57
Theorem (Fagin) Fur jedes Problem K gilt: K ist in NP gdw. K ist ESO-definierbar.
Lemma
Die einfache Richtung des Beweises ist die folgende:
Strategie für Gegenrichtung:
Jedes ESO-definierbare Problem K ist in NP.
Mit anderen Worten: ESO-Auswertung ist in NP bzgl. Datenkomplexitat.
Zeige, dass es fur jede nichtdeterministische Polyzeit-Turingmaschine M
einen ESO-Satz 'M gibt, so dass A |= 'M gdw. wA 2 L(M) fur alle A.
Fagins Theorem – Beweis
58
Das Arbeitsband ist einseitig unendlich, der Kopf und die Eingabestehen anfangs ganz links; wir nehmen an, dass M
Sei M = (Q,⌃,�,�, q0, QA, QR), wobei
• Q = {q1, . . . , qm} Zustandsmenge, ⌃ = {0, 1} Eingabealphabet
• � = {a1, . . . , ap} ◆ ⌃ Arbeitsalphabet mit Blanksymbol ? 2 �
• � ✓ Q ⇥ ⌃⇥ Q ⇥ ⌃⇥ {L, R} Ubergangsrelation
• q0 2 Q Startzustand
• QA, QR ✓ Q Menge der akzeptierenden bzw. verwerfenden Zustande
1. auf jeder Eingabe der Lange n maximal nk Schritte macht
2. am linken Ende des Bandes niemals einen Schritt nach links versucht
3. bei Zustand in Q \ (QA [ QR) immer mindestens einen Ubergangzur Verfugung hat, bei Zustand in QA [ QR jedoch keinen Ubergang
Fagins Theorem – Beweis
59
Die Formel �M soll einen akzeptierenden Lauf von M auf der Eingabesimulieren, wenn so ein Lauf existiert
Schwierigkeit:
Lösung:
• uns steht eine Struktur A der Große |A| zur Verfugung
• wir mussen Bandinhalte, Zustande und Kopfpositionen einesLaufes der Lange |wA|k reprasentieren
• wähle ein k0 so dass |A|k0 � |wA|k
• repräsentiere Schrittzähler und Bandposition als k0-Tupel über A,verwende beliebige (strikte) lineare Ordnung über Ak0
zurRepräsentation der „Reihenfolge“
Fagins Theorem – Beweis
60
Der Satz 'M hat die Form
Die Formel � beschreibt nun das Verhalten von M .
• L die strikte lineare Ordnung reprasentiert
• Tai(p, t) ausdruckt, dass Bandzelle p zum Zeitpunkt t
das Symbol ai enthalt
• Hqi(p, t) ausdruckt, dass M zum Zeitpunkt t in Zustand qi ist
und der Kopf sich auf Bandzelle p befindet
9L9Ta0 · · · 9Ta`9Hq1 · · · 9Hqm
wobei alle Relationsvariablen (2 · k0)-stellig sind und
Fagins Theorem – Beweis
61
Die Formel besteht aus folgenden Konjunkten:
• �lin druckt aus, dass L lineare Ordnung ist
• �ok stellt sicher, dass Bandsymbole und Zustand eindeutig sind
• �move erzwingt, dass alle Ubergange � entsprechen
• �acc fordert, dass ein akzeptierender Zustand erreicht wird
• �const stellt sicher, dass sich der Inhalt von Bandzellen, die sichnicht unter dem Kopf befinden, bei einem Ubergang nicht andert
• �ini beschreibt die Startkonfiguration: Band beschriftet mit Ein-gabe gefolgt von Blanks, Kopf ganz links, M in Startzustand
Fagins Theorem – Beweis
62
Zusammenfassung:
• Die SO-Variablen erlauben es, die Berechnung einer Turing- maschine zu beschreiben
• Die existentielle SO-Quantifizierung von ESO entspricht dem Nichtdeterminismus der TM
• Die Definierbarkeit einer linearen Ordnung erlaubt es, die „Reihenfolge“ der Bandpositionen und Schritte zu repräsentieren
• Es ergeben sich technische Schwierigkeiten aus den unter- schiedlichen Kodierungen von Probleminstanzen als Graphen und Wörter; die lassen sich aber lösen
Deskriptive Komplexitätstheorie
63
Welche Logik könnte die Komplexitätsklasse P erfassen?
• FO ist viel zu schwach, kann einfache P-Probleme nicht ausdrücken wie EVEN oder Zusammenhang.
• das in diesem Zusammenhang frappierendste Defizit von FO ist: es gibt keinen Rekursionsmechanismus.
• (E)SO erlaubt Rekursion, ist aber offensichtlich zu ausdrucksstark.
Fixpunktoperatoren stellen einen schwächeren Rekursionsmechanismusdar als SO-Quantifikation.
Tatsächlich erfasst LFP (die Erweiterung von FO um Fixpunktoperatoren)genau P, wenn man annimmt, dass die Eingabestrukturen mit einer linearenOrdnung < ausgestattet sind.
Deskriptive Komplexitätstheorie
64
Dumm nur: in vielen natürlichen Problemen wie 3F oder HK gibt es keine„eingebaute Ordnung“
In LFP ist diese Ordnung auch nicht definierbar
Was wie ein kleines technisches Hindernis aussieht, stellt sich alssehr großes Problem heraus
Es wurde sogar vermutet, dass es keine Logik gibt, die P erfasst(basierend auf einer vernünftigen Definition von „Logik“; Gurevich)
Wenn das so ist, ist es schwer zu beweisen, denn es impliziertnatürlich P ≠ NP
Fast fertig für dieses Semester ...
65
Vielen Dankfür eure Aufmerksamkeit!