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)