Lehrveranstaltungen Ingmar Meinecke

Die Übungsblätter sind hier als Postscript- und pdf-dateien erhältlich. Postscript-Dateien können z.B. mit GHOSTVIEW gelesen werden.

Lehrveranstaltungen SS 2011

Vorlesung "Verifikation durch Model Checking"

Modul: anrechenbar für das BSc-Modul "Formale Modelle" (10-201-2105) und für das MSc-Modul "Angewandte Automatentheorie" (10-202-2107) (jeweils 5 LP)

Inhalt: Eine wesentliche Frage sowohl für Software wie für Hardware ist: Tun diese Systeme das, was sie tun sollen? Dazu wurden in den letzten Jahrzehnten eine Reihe von Methoden zur Verifikation solcher Systeme entwickelt. In dieser Veranstaltung beschäftigen wir uns mit den Grundlagen des Model Checking. Das Model Checking ist eine vollautomatische Methode, die Modelle der Systeme auf Eigenschaften prüft. Folgende Punkte werden in der Veranstaltung bearbeitet:

Nützliche Vorkenntnisse: endliche Automaten, Logik, elementare Komplexitätstheorie

Erste Veranstaltung: Montag, 4.4., 13:15 Uhr, SG 1-14

Termine: Mo, 13:15 Uhr, SG 1-14 und Di, 9:15 Uhr, SG 1-14 (einer davon 14-tägig); Termine können wir gerne beim 1. Treffen noch mal besprechen und gegebenenfalls ändern.
Vorlesung und Übungen werden wir flexibel gestalten, Teil der Übungen wird auch das Kennenlernen des Model Checking Tools SPIN sein.

Einschreibung & Organisatorisches:
Wir benutzen zur Kommunikation und Organisation der Veranstaltung das Online Learning And Training (OLAT):

Sie finden im OLAT laufende Informationen zur Veranstaltung.

Seminar: Automatentheorie

Das Seminar findet am Mittwoch, 9:15 Uhr, in Jo 4-42 statt. Hier eine Liste der Vorträge. Wer noch Interesse an einer Teilnahme hat, melde sich bitte bei mir.

Die gesamten Vortragstermine werden auf das nächste Semester verschoben.
Datum Vortragende(r) Thema Betreuer(in)
WS 11/12 Marco Wittig Ableitungen rationaler Ausdrücke mit Vielfachheiten Thomas Weidner
WS 11/12 Benjamin Kiessling Algorithmen zur Bestimmung kürzester Wege Vitaly Perevoshchikov
WS 11/12 Anke Bremer Gedächtnislose Determiniertheit von Paritäts- und Mean-Payoff-Spielen Ingmar Meinecke

Lehrveranstaltungen WS 2010/11

Seminare: Automatentheorie

Modulnummern: Automatentheorie und Spiele (10-201-2010, Bachelor), Quantitative Automatentheorie (10-202-2011, Master)

Termin: Dienstag, 11:15 Uhr, Jo 4-42

Erstes Treffen: Dienstag, 12.10.2010, 11:15 Uhr, Jo 4-42 (dort werden Themen vorgestellt und vergeben, wenn Sie zu diesem Termin nicht können, bitte bei uns zwecks Thema melden)

Datum Vortragende(r) Thema Betreuer(in)
16.11. Matthias-Christian Ott Boolesche Grammatiken Ingmar Meinecke
30.11. Christian Franke Determinisierung von Büchi-Automaten Thomas Weidner
7.12. Marcel Pfütze Unendliche Spiele Karin Quaas
4.1. Christian Ludborzs Bildkompression Thomas Weidner

Übungen zur Vorlesung "Logik"

Modulnummer: 10-201-2108-1

Vorlesung: Freitag, 9:15 Uhr, HS 10

Übungsgruppen:

Beginn der Übungen erst in der 2. Vorlesungswoche 18.-22.10. Das ist eine B-Woche.

Tutorium: Montag, 15:15 Uhr, SG 3-10 (gehalten von Marcus Daum)
Das Tutorium dient dazu, dass Sie Fragen zum Stoff der Vorlesung stellen, zurückliegende Hausaufgaben besprechen, allgemeine mathematische Fragen klären. Es kommt dabei auf Sie an! Die Teilnahme ist freiwillig.

Einschreibung in die Übungsgruppen & Organisatorisches:
Wir benutzen zur Kommunikation und Organisation der Übungen das Online Learning And Training (OLAT):

Wir werden im Laufe des Semesters sehen, für was wir das OLAT alles nutzen werden. Sie finden dort laufende Informationen zur Veranstaltung. Die wichtigsten Infos werden auch hier veröffentlicht.

Prüfungsvorleistung:
Übungsschein (6 Übungsblätter mit Hausaufgaben von denen 50 % korrekt gelöst sein müssen)
Hier ist eine Liste mit den Resultaten der Prüfungsvorleistungen. Bei Unstimmigkeiten wenden Sie sich bitte schnell an mich.

Prüfung: schriftliche Klausur am 16.02.2011, 13 Uhr, Hörsaal 9
Bitte auf den Seiten des Prüfungsamtes anmelden. Die Anmeldung ist verbindlich, aber steht unter dem Vorbehalt des Bestehens der Prüfungsvorleistung. Wurde diese nicht erbracht, ist die Anmeldung nichtig.

Prüfungsergebnisse: finden Sie im OLAT unter dem entsprechenden Kurs, Punkt Prüfung, dort ist ein Ordner mit den Ergebnissen

Einsichtnahme in die Klausur: Freitag, 4.3.2011, 13-14 Uhr im Raum 4-42 (Joh 26)

Wiederholungsprüfung: Freitag, 1.4.2011, um 9:00 Uhr im Seminargebäude, Raum S 420
Für Studenten und Studentinnen, die zur Prüfung am 16.2.2011 angemeldet waren, ist keine wiederholte Anmeldung erforderlich.
Ergebnisse der Wiederholungsklausur vom 1.4.2011 sind im OLAT zu finden. Wer Einsicht in die Klausur nehmen will, mache bitte individuell einen Termin mit mir aus.

Konsultation: Do, 10.2., 13 Uhr, S 212
Sie fragen, wir antworten.
Weiterer Termin: Mo, 14.2., 13-15 Uhr in meinem Büro Jo 26, 4-43, bzw. 15-16 Uhr in Jo 26, Raum 4-42

Übungsblätter:

  1. Übungsblatt (Besprechung der Seminaraufgaben in den Übungen am 18., 19., 25. und 26.10., Abgabe der Hausaufgaben am Beginn der Vorlesung am 29.10.)
  2. Übungsblatt (Besprechung der Seminaraufgaben in den Übungen am 1., 2., 8. und 9.11., Abgabe der Hausaufgaben am Beginn der Vorlesung am 12.11.)
  3. Übungsblatt (Besprechung der Seminaraufgaben in den Übungen am 15., 16., 22. und 23.11., Abgabe der Hausaufgaben am Beginn der Vorlesung am 26.11.)
  4. Übungsblatt (Besprechung der Seminaraufgaben in den Übungen am 29., 30.11. und 6., 7.12., Abgabe der Hausaufgaben am Beginn der Vorlesung am 10.12.)
  5. Übungsblatt (Besprechung der Seminaraufgaben in den Übungen am 13., 14.12. und 3., 4.1., Abgabe der Hausaufgaben am Beginn der Vorlesung am 7.1.)
  6. Übungsblatt (Besprechung der Seminaraufgaben in den Übungen am 10., 11., 17. und 18.1., Abgabe der Hausaufgaben am Beginn der Vorlesung am 21.1.)
  7. Übungsblatt (Besprechung der Seminaraufgaben in den Übungen am 24., 25., 31.1. und 1.2., Abgabe der Zusatzaufgaben am Beginn der Vorlesung am 4.2.)

Lehrveranstaltungen SS 2010

Übungen zur Vorlesung "Automatentheorie"

Konsultation vor der Prüfung: Montag, 26.7.2010, 10:30 Uhr im Raum 4-42 (Johannisgasse 26)
Wir gehen auf Ihre Fragen ein. Die Fragen müssen Sie mitbringen.

Prüfung: mündlich, am 29.7.2010, im Raum 4-42 (Johannisgasse 26), in den Übungen einschreiben oder bei Herrn Weidner oder Herrn Meinecke persönlich melden, um sich einzuschreiben

Prüfungsliste:

Uhrzeit Name Vorname
10:15 Neudert Sebastian
11:00 Bin Simon
11:45 Laube Sören
14:00 Nudel Olga
14:45 Xu Jia
15:30 Bremer Anke

Termine: Vorlesung am Dienstag, 11:15 Uhr, HS 14, und am Donnerstag, 9:15 Uhr, HS 19
Übungsgruppen am Dienstag (T. Weidner), 15.15 Uhr, SG 1-10 und am Freitag (I.Meinecke) 11.15 Uhr, SG 1-10 (Beginn in der Woche 12.-16.4.)

Prüfungsvorleistung:
Sie müssen 25 Prozent der Punkte der Hausaufgaben erreichen, um zur Prüfung zugelassen zu werden.

Übungsblätter:
Die Hausaufgaben sind am Dienstag zu Beginn der Vorlesung abzugeben. Die Seminaraufgaben bis zur jeweiligen Übung vorzubereiten und dort vorzustellen.

  1. Übungsblatt (Besprechung in der Woche 12.-16.4., Abgabe HA am 13.4.)
  2. Übungsblatt (Besprechung in der Woche 19.-23.4., Abgabe HA am 20.4.)
  3. Übungsblatt (Besprechung in der Woche 26.-30.4., Abgabe HA am 27.4.)
  4. Übungsblatt (Besprechung in der Woche 10.-14.5., Abgabe HA am 11.5.)
  5. Übungsblatt (Besprechung in der Woche 17.-21.5., Abgabe HA am 18.5.)
  6. Übungsblatt (Besprechung in der Woche 25.-28.5., Abgabe HA am 25.5.)
  7. Übungsblatt (Besprechung in der Woche 31.5.-4.6., Abgabe HA am 1.6.)
  8. Übungsblatt (Besprechung in der Woche 7.6.-11.6., Abgabe HA am 8.6.)
  9. Übungsblatt (Besprechung in der Woche 14.6.-18.6., Abgabe HA am 15.6.)
  10. Übungsblatt (Besprechung in der Woche 21.6.-25.6., Abgabe HA am 22.6.)
  11. Übungsblatt (Besprechung in der Woche 28.6.-2.7., Abgabe HA am 29.6.)
  12. Übungsblatt (Besprechung in der Woche 5.7.-9.7., Abgabe HA am 6.7.)

Seminar: Automatentheorie für Bachelor

Termin: Mittwoch, 9:00 Uhr, Joh, 4-42 (erstes Treffen und Ausgabe der Themen am 7.4.)
Wer noch Interesse hat, melde sich bitte bei mir per email oder persölich.

Modul: BSc-Seminarmodul "Theoretische Informatik" (10-201-2116) (5 LP), Einschreibung beim ersten Treffen

Modulprüfung: Vortrag von 60 Minuten über ein selbständig zu erarbeitenden wissenschaftlichen Text, bei schlechtem Vortrag schriftliche Ausarbeitung

Seminarthema: Probabilistische Systeme

Datum Vortragende(r) Thema Betreuer(in)
19.5. Ngoc Diep Phan Markov-Ketten Karin Quaas
26.5. Maik Bärwald Erreichbarkeit in Markov-Ketten Thomas Weidner
9.6. Renata Wong Qualitative Eigenschaften Ingmar Meinecke
16.6. Matthias Schreiter Probabilistisches CTL Model Checking Ingmar Meinecke

Lehrveranstaltungen WS 2009/10

Vorlesung: Verifikation reaktiver Systeme durch Model Checking

Termine: Vorlesung am Dienstag, 17:15 Uhr, S 312,
Übung alle zwei Wochen am Donnerstag, 15:15 Uhr, S 414 (Beginn am 29.10.)

Modul: anrechenbar für das BSc-Modul "Formale Modelle" (10-201-2105) und für das MSc-Modul "Angewandte Automatentheorie" (10-202-2107) (jeweils 5 LP), Einschreibung in der ersten Vorlesung

Inhalt: Diese Vorlesung gibt einen Überblick über Methoden und Algorithmen des Model Checking für die Analyse reaktiver Systeme. Das Model Checking stellt eine vollautomatische Methode dar, um zu überprüfen, ob Systeme gewisse Eigenschaften besitzen. Dabei werden die Systeme als Transitionssysteme und die Eigenschaften durch temporale Logiken (linearer und verzweigender Zeit) modelliert. Effiziente Model Checker wie SPIN sind seit den 90ern im Einsatz.
Wir betrachten verschiedene Model Checking Algorithmen und ihre Komplexität. Tableau-, automatentheoretische und Fixpunktmethoden werden vorgestellt. Das Problem der Zustandsexplosion wird mittels symbolischem Model Checking angegangen. Beschließen wird die Veranstaltung ein Abriss weiterer wichtiger Gebiete des Model Checking.

Nützliche Vorkenntnisse: endliche Automaten, Logik, elementare Komplexitätstheorie

Literatur:

  • E.M. Clarke, O. Grumberg und D.A. Peled. Model Checking, The MIT Press, 1999.
  • C. Baier und J.-P. Katoen. Principles of Model Checking, The MIT Press, 2008.

Skript: 1 auf 1 und 4 auf 1 (Version 1.2.)

Übungsblätter:
Die Aufgaben sind bis zur jeweiligen Übung vorzubereiten. Dort diskutieren wir dann die Lösungen.

  1. Übungsblatt (Besprechung am 29.10.2009)
  2. Übungsblatt (Besprechung am 12.11.2009)
  3. Übungsblatt (Besprechung am 26.11.2009)
  4. Übungsblatt (Besprechung am 10.12.2009)
  5. Übungsblatt (Besprechung am 14.1.2010)
  6. Übungsblatt (Besprechung am 28.1.2010)

Seminar: Automatentheorie für Bachelor

Termin: Montag, 13:15 Uhr, S 114 (erstes Treffen und Ausgabe der Themen am 12.10.)
Wer noch Interesse hat, melde sich bitte bei mir per email oder persölich.

Modul: BSc-Seminarmodul "Theoretische Informatik" (10-201-2116) (5 LP), Einschreibung beim ersten Treffen

Modulprüfung: Vortrag von 60 Minuten über ein selbständig zu erarbeitenden wissenschaftlichen Text, bei schlechtem Vortrag schriftliche Ausarbeitung

Thema des Seminars: Transducer und rationale Relationen
Endliche Automaten akzeptieren Sprachen von Wörtern. Mittels Automaten können aber auch Relationen, hier oft auch Transduktionen genannt, und Funktionen erkannt werden. Automaten, die dies tun, werden Transducer genannt. Gegenstand des Seminars ist die Theorie der durch Transducer erkannten Relationen. In diesem Zusammenhang werden auch die Begriffe "Erkennbarkeit" und "Rationalität" in einem allgemeineren Zusammenhang behandelt.

Voraussetzungen: Vorlesung "Automaten und formale Sprachen"

Seminar: Automatentheorie für Master

Termin: Donnerstag, 13:15 Uhr, S 212 (erstes Treffen und Ausgabe der Themen am 15.10.)
Wer noch Interesse hat, melde sich bitte bei mir per email oder persönlich.
Vorträge finden im Raum 4-42, Johannisgasse 26 statt!!!

Modul: MSc-Seminarmodul "Automatentheorie" (10-202-2115) (5 LP), Einschreibung beim ersten Treffen

Modulprüfung: Vortrag von 60 Minuten über eine selbständig zu erarbeitendeForschungsarbeit, bei schlechtem Vortrag schriftliche Ausarbeitung

Thema des Seminars: Alternierende Automaten
Alternierende Automaten haben in den letzten Jahren große Bedeutung in der Automatentheorie gewonnen. Insbesondere lassen sie sich zur Lösung des Model Checking Problems für temporale Logik verzweigender Zeit nutzen. Wir behandeln hier alternierende Automaten auf Wörtern und Bäumen sowie ihre Anwendungen.

Voraussetzungen: Grundlagenvorlesungen aus dem BSc-Studium, Vorlesungen zu Omega-Automaten und/oder Baum-Automaten sind hilfreich, aber keine Bedingung

Datum Vortragende(r) Thema Betreuer(in)
3.12. Dung Phan Alternierende Automaten auf endlichen Wörtern Karin Quaas
14.1. Doreen Götze Simulation zwischen alternierenden Büchi-Automaten Daniel Kirsten
28.1. Manh Ha Nguyen Büchi-Automaten und alternierende Büchi-Automaten Karin Quaas

Lehrveranstaltungen SS 2009

Seminar Automatentheorie

Vorbesprechung Seminar "Automatentheorie" für das SS 2009:
Mittwoch, 8.4.2009, 9:15 Uhr, Johannisgasse 26, Raum 4-42
Es werden Artikel vorgestellt, die dieses Semester bearbeitet und vorgestellt werden können. Alle interessierten Bachelor- und Masterstudenten sind herzlich eingeladen.

Termin: Mittwoch, 9:15 Uhr, Johannisgasse 26, Raum 4-42 (Beginn am 13.5.)

Datum Vortragende(r) Thema Betreuer
13.5. Daniel Müller A. N. Trahtman:
The Černý Conjecture for Aperiodic Automata 		Kuske
20.5. Andreas Weise K. Chatterjee, L. Doyen, Th. A. Henzinger:
Quantitative Languages 		Droste/Meinecke
27.5. Konrad Höffner G. Jiraskova:
Magic Numbers and Ternary Alphabet 		Kuske
3.6. Nico Korn T. Yokomori:
Learning Non-deterministic Finite Automata from Queries and Counterexamples 		Quaas
10.6. Doreen Götze J. Sakarovitch:
Das Äquivalenzproblem für gewichtete Automaten über Körpern 		Kirsten
17.6. Matthias Berndt Vortrag fällt aus!!! Meinecke
24.6. Taras Zakharko M. Ahmed and A. Lubiw:
Shortest Paths Avoiding Forbidden Subpaths 		Meinecke

Lehrveranstaltungen & Prüfungen WS 2007/08

Verschiedenes

Vorbesprechung Seminar "Automatentheorie" für das SS 2008:
Donnerstag, 31.1.2008, 9:15 Uhr, Johannisgasse 26, Raum 4-42
Es werden Artikel vorgestellt, die nächtes Semester bearbeitet und vorgestellt werden können. Alle Interessierten sind herzlich eingeladen.

Abholung von Scheinen: prinzipiell im Sekretariat der Abteilung, Frau A. Hesse, Zimmer 4-44, Johannisgasse 26

Vorlesung Automatentheorie

Lesender: Prof. Dr. M. Droste

Übungsleiter: Dr. I. Meinecke und K. Quaas (bis 31.12.2007), Dr. D. Kirsten (ab 1.1.2008)

Achtung! Ab 1.1.2008 übernimmt Dr. D. Kirsten beide Übungsgruppen.

Termine:

Prüfungs- und Übungsmodalitäten:

  • Prüfung des Moduls am Ende des Semesters
  • wöchentliche Übungsblätter erscheinen auf dieser Seite jeden Freitag
  • schriftliche Hausaufgaben (kurz HA) in der darauf folgenden Woche direkt vor der Vorlesung am Freitag abzugeben
  • jede/r gibt einzeln und handschriftlich ab
  • auf sechs Übungsblättern gibt es Prüfungsaufgaben (kurz PA), die in die Prüfungsvorleistung eingehen und daher bearbeitet werden müssen (zum Bestehen der Prüfungsvorleistung sind 50% der Punkte dieser Aufgaben erforderlich)

Literatur: ist gut zur Vertiefung des Stoffes, einige Hinweise gibt es hier

Übungsaufgaben:
Rote Serien gehen in die Prüfungsvorleistung ein.

  1. Übung (Besprechung 15. & 17.10., HA bis 19.10.) pdf-file
  2. Übung (Besprechung 22. & 24.10., HA bis 26.10.) pdf-file
  3. Übung (Besprechung 29.10. & 2.11., PA bis 2.11.) pdf-file
  4. Übung (Besprechung 5.11. & 7.11., HA bis 9.11.) pdf-file
  5. Übung (Besprechung 12.11. & 14.11., PA bis 16.11.) pdf-file
  6. Übung (Besprechung 19.11. & 22.11., HA bis 23.11.) pdf-file
  7. Übung (Besprechung 26.11. & 28.11., PA bis 30.11.) pdf-file
  8. Übung (Besprechung 4.12. & 5.12., HA bis 7.12.) pdf-file
  9. Übung (Besprechung 10.12. & 12.12., PA bis 14.12.) pdf-file
  10. Übung (Besprechung 17.12. & 19.12., HA bis 21.12.) pdf-file
  11. Übung (Besprechung 7.1. & 9.1., PA bis 11.1.) pdf-file

Achtung! Die weiteren Übungsblätter finden Sie auf der Seite von Dr. Kirsten.

Seminar Automatentheorie

Vorbesprechung Seminar "Automatentheorie" für das SS 2008:
Donnerstag, 31.1.2008, 9:15 Uhr, Johannisgasse 26, Raum 4-42
Es werden Artikel vorgestellt, die nächtes Semester bearbeitet und vorgestellt werden können. Alle Interessierten sind herzlich eingeladen.

Leitung: Prof. Dr. M. Droste und Dr. D. Kuske

Termin: Do, 9:15 Uhr, Johannisgasse 26, Raum 04-42

Start der Vorträge: am 8.11.

Vortragsplan: siehe hier

Informationen zu Veranstaltungen vergangener Semester finden Sie hier.

(12.3.2007/im)