Vorlesung: Automaten und Logik

Sommersemester 2006

Zeiten und Ort

Dienstag 10:15 - 11:45 Uhr SR 1 Cantorhaus
Donnerstag 14:15 - 15:45 Uhr HS 1.23 VSP

Inhalt

Zur Verifikation und Spezifikation von Sytemen und Programmen werden verschiedene Klassen von Automaten und Logiken verwendet. Automaten eignen sich besonders zur Modellierung dynamischen Verhaltens, statische Eigenschaften lassen sich einfacher logisch beschreiben. Übersetzungen zwischen beiden Formalismen sind sowohl praktisch nützlich als auch theoretisch interessant.

In der Vorlesung werden Zusammenhänge zwischen endlichen Automaten über endlichen und unendlichen Wörtern und Bäumen und verschiedenen dazu passenden Logiken vorgestellt.

Vorlesungen

4.4.2006 Einführung, Wiederholung formale Sprachen
6.4.2006 MSO[S,<], FO[S,<] - Syntax und Semantik
11.4.2006 MSO[S,<]- und FO[S,<]- definierbare Sprachen
13.4.2006 Wiederholung NFA
18.4.2006 Satz von Büchi/Elgot über Regularität und MSO[S,<]-Definierbarkeit
20.4.2006 Satz von Büchi/Elgot
25.4.2006 Folgerungen
27.4.2006 omega-Sprachen allgemein, reguläre omega-Sprachen
2.5.2006 omega-Automaten allgemein, Büchi-Automaten
4.5.2006 Übung
9.5.2006 Muller-Automaten (deterministisch)
11.5.2006 Übung
16.5.2006 Safra-Bäume
18.5.2006 Satz von McNaughton
23.5.2006 Satz von Büchi
25.5.2006 Entscheidbarkeitsresultate
6.6.2006 Übung
8.6.2006 Baumsprachen, Bottom-Up-Baumautomaten
13.6.2006 Top-Down-Baumautomaten
15.6.2006 Pumping-Lemma, Abschlußeigenschaften erkennbarer Baumsprachen
20.6.2006 Baum-Homomorphismen
22.6.2006 Abschluß unter linearen und inversen Homomorphismen
27.6.2006 MSO[S1,..,Sk] - Syntax und Semantik
28.6.2006 Satz von Doner, Thatcher/Wright
29.6.2006 Übung
4.7.2006 omega-Baumsprachen, omega-Baumautomaten, Satz von Rabin
5.7.2006 Entscheidbarkeit von S2S,SkS, Baummodelleigenschaft
6.7.2006 Modallogik, Bisimulation, Baummodelleigenschaft
11.7.2006 Bildsprachen, Tiling-Systeme
13.7.2006 Logik über Bildern

Zusammenfassung der bisherigen Vorlesungen (ps, pdf)

Übungen

Die praktischen Übungsaufgaben bekommen Sie vom autotool. Dazu melden Sie sich bitte dort bei "Uni Halle" zur Vorlesung "Logik" an und schreiben Sie sich in die Übungsgruppe ein (ab 7.4.2006 möglich). Hier gibt es Tips für die Leipziger autotool-Nutzer. Bei Problemen finden Sie vielleicht dort einen geeigneten Hinweis.

Theoretische Aufgaben:

Zu geeigneten Zeitpunkten werden statt der Vorlesung Übungen durchgeführt. Diese Übungstermine werden in der Vorlesung bekanntgegeben.

Literatur

H.Straubing: Finite Automata, Formal Logic, and Circuit Complexity 1994
W.Thomas: Applied Automata Theorie 2003
W.Thomas: Languages, Automata, and Logic (ps) 1996
I. Walukiewicz: Automata and Logic 2002
J.-E. Pin, D. Perrin: Automata and infinite words, 1.Kapitel aus Infinite Words 2004
H. Comon, M. Dauchet, R. Gilleron, D. Lugiez, S. Tison, M. Tommasi: Tree Automata Techniques and Applications

Das an der RWTH Aachen entwickelte Programm OmegaDet konstruiert (unter anderem durch Safra-Bäume) zu einem gegebenen Büchi-Automaten äquivalente deterministische Muller-Automaten.

Zusammenfassung (ps) der Vorlesung "Mathematische Logik" im SS 2005

http://nirvana.informatik.uni-halle.de/~schwarz/ mailto:schwarzs@informatik.uni-halle.de