monadische logik 2.ordnung (mso)
DESCRIPTION
Monadische Logik 2.Ordnung (MSO). Ilhan Aslan Betreuer: Tim Priesnitz Seminar SS/03 „Logische Aspekte in XML“ Gert Smolka PS-Lab Universität des Saarlandes. Motivation: Baue Logik. möglichst expressive aber entscheidbar. - PowerPoint PPT PresentationTRANSCRIPT
Monadische Logik 2.Ordnung (MSO)
Ilhan Aslan
Betreuer: Tim Priesnitz
Seminar SS/03 „Logische Aspekte in XML“
Gert Smolka
PS-Lab
Universität des Saarlandes
Motivation: Baue Logik
• möglichst expressive
• aber entscheidbar
Logik 1.Ordnung vs. Logik 2.Ordnung
1.Ordnung:– Variablen werden durch Individuen interpretiert.
z.B. Aussagenlogik
2.Ordnung:– Variablen werden durch Mengen von Individuen interpretiert.
z.B. Baumlogiken
Logik 2. Ordnung ist unentscheidbar
..
..
..
• Logik 1.Ordnung mit Mengenvariablen
x
…
Band von TM
…
…t Gitter realisiert durch binäres Prädikat P(x,t).
TM hält gdw. t: P(x+1,t) = halt
Kopf
Übersetzung von Bit-Mustern
• ew
P1 1 0
0 1 1
ti
ti+1
TM wird definiert durch endl. viele Muster-Übergänge.
Bsp.: t x: P(x,t) P(x+1,t) P(x+2,t) → P(x+3,t+1) P(x+4,t+1) P(x+5,t+1)
xi xi+1
Monadische Logik 2.Ordnung (SiS)
Syntax
• φ ::= Xφ φ φ v φ Si(X,Y) X Y
x φ x Y S(x,y)
x φ x Y x < y
Einelementig(X) : ↔ Y ((Y X ) (Y=X) Z (Z X →Z=X v Z=Y))
Syntax Varianten
Definiere Syntax mit x φ x Y S(x,y)
X Y :↔ x (x X → x Y)x = y :↔ Z ((x Z) ↔ (y Z)) S(X,Y) :↔ x,y ((x X) (y Y) z(((z=x) → (z X)) ((z=y) → (y Y))) S(x,y))
Definiere Syntax mit x φ x Y x < y
S(x,y) :↔ (x < y z(x < z z < y))
Interpretation von Variablen in (schwacher) SiS
1 Nachfolger (i=1)
Universum: 1*
1
1
2 Nachfolger (i=2)
Universum: (1∪2)*
1 2
1 2
Individuen-Variablen
Shape von String Pfad
Mengen-Variablen
(endl.) Menge von Shapes von Strings
(endl.) Menge von Pfade
Menge von Pfade = Baum ?
Menge von Pfade {ε,1,2,11,12,121}
11
1
12
2
Setze einzelne Pfade zusammen!
1
2
1 22 2
2
2
211
1
1
1
1
1
1
Menge von Pfade = Baum ?
Menge von Pfade {ε,1,2,11,12,121}
11
1
12
2
Setze einzelne Pfade zusammen.
1
2
22 2
2
2
21
1
1
1
1
1
1
Erfüllbarkeit von (schwacher)S2S
Sei β eine Belegunsfunktion mit : β :x π , π ist Pfad
β :X 2 π
β |= y X <=> β(y) β(X)
β |= S1(x,y) <=> β(x)1 = β(y)
β |= S2(x,y) <=> β(x)2 = β(y)
β |= Xφ <=> β[B/X] |= φ für ein B 2 π
…
Bsp.: Definiere Prefix-Abgeschlossenheit mit (schwacher)S2S
Pfad-bis-Vater-von(y) X :↔ z (S0(z, y) v S1(z, y) z X)
Prefixpfade-von-Pfad(x) Y :↔ x Y z((zY ¬ (z=ε)) Pfad-bis-Vater-von(z) Y (z0 Y ¬ (z1 Y)) (z1 Y ¬ (z0 Y)))
21
1
z.B. für X = { ε , 1, 11, 2 } Für y = 11 ist Pfad-bis-Vater-von(y) X erfüllbar weil 1 X!
21
1z.B. für X = { ε , 1, 11, 2 } Für y = 11 ist Prefixpfade-von-Pfad(x) X erfüllbar weil ε,1,11 X !
Bsp.: Definiere Prefix-Abgeschlossenheitmit (schwacher)S2S
2
2
1
1
1
Eine Menge von Pfaden ist Prefix-Abgeschlossen ( definiert einen Baum) wenn gilt :
Prefix-Abgeschlossen(Z) :↔ z ((zZ) Prefixpfade-von-Pfad(z) Z)
Ein Pfad (121) ist Prefix-Abgeschlossen bzgl. einer Menge von Pfaden, wenn alle Prefixpfade(ε ,1,2,12,121) in der Menge enthalten sind!
Prädikate → Mengen
Gegeben: Unäres Prädikat P: Σ* {0,1}charachteristische Menge:
MP = {x Σ* P(x) = 1}
Prädikate ← Mengen
Gegeben: Menge M Σ* charackteristisches Prädikat:
PM(x) = 1 , falls x M
0 , sonst
Unäre Prädikate in (schwacher)SiS
Y(x) <=> x Y
X(Y) unentscheidbar (Logik 3.Ordnung)
..
..
..
x
t
P({t,x}) = P({x,t})Gitter realisierbar durchP(X) x X t X Zweielementig(X)
Kodiere ω-Strings in S1S
Axiomatisierung in S1S:
La ,Lb : La ∩ Lb = La ∪ Lb = 1*
Jede Adresse hat höchstens ein Label
Jede Adresse hat mindestens ein Label
ε 1 11 111 …a b a b …1 0 1 0 …0 1 0 1 …
Beispiel: ω-String über A={ a, b }
La = { ε, 11,1111,… }Lb = { 1,111,11111,… }
La
Lb
Kodiere Strings in schwacher S1S
Axiomatisierung in schwacher S1S:
La ,Lb : La ∩ Lb = prefix-abgeschlossen(La ∪ Lb)
ε 1 11 111a b a b1 0 1 00 1 0 1
Jede Adresse hat höchstens ein Label
Jede Adresse hat mindestens ein Label
La
Lb
La = { ε, 11 }Lb = { 1,111}
Beispiel: String über A={ a, b }
Kodiere ω -Bäume in S2S
g
Beispiel: ω-Baum über A = {f/2, g/2}
f
ff2
2
1
1 Lf = { ε, 11,12, …} Länge der Adr. gerade
Lg = { ε, 1,2 } Länge der Adr. ungerade
Axiomatisierung in S2S:
Lg ,Lf : Lg ∩ Lf = Lg ∪ Lf = (1 ∪ 2)*
g
f21
f…
… Jede Adresse hat höchstens
ein Label
Jede Adresse hat mindestens
ein Label
Kodiere Bäume in schwacher S2S
f
Beispiel: Baum über A = {f/2, a/0}f
aa
a2
2
1
1
La = { ε, 1,21,22}
Lf = { ε, 2 }
Axiomatisierung in (schwacher)S2S
Lf ,La : La ∩ Lf = Prefix-Abgeschlossen(La ∪ Lf) (1) (2) (La ∪ Lf) =
(1) zf Lf :
x,y (La ∪ Lf):
S1(z,x) S2(z,y)
(2) za La, z (La ∪ Lf) :
¬ (za < z)
Aritäten-Konsistenz
Baum ist nicht Leer
Referenzen[1] Wolfgang Thomas,Languages, Automata, and Logic, May 1996,Bericht 9607
Institut für Informatik und Praktische Mathematik Der Christian-Albrechts-Universität zu Kiel D-24098 Kiel
[2] Khoussainov, Bakhodyr and Nerode,Anil: Automata Theory and Its Applications, Progress in Computer Science, Birkhäuser,Boston;Berlin(2001)
[3] David Basin, Felix Klaedke, Monadic Second-Order Logics in Theory and Practice, Albert-Universität, Freiburg
[5] Hupert Comon, Max Dauchet, Rémi Gilleron, Denis Lugiez, Sophie Tison, Marc Tommasi, Tree Automata Techniques and Applications
[6] Erich Grädel, Wolfgang Thomas, Thomas Wilke (Eds.), Automata, Logics, and Infinite Games, A Guide to Current Research (Part VI Monadic Second-Order Logic), Springer (2001)
[7] H.Hermes, Einführung in die Mathematische Logik, B.G. Teubner, Stuttgart (1972)