Uni-Logo

This page is only available in German.

Seminar: Automatenkonstruktionen im Model Checking - Organisation

Veranstalter: Prof. Dr. Jan-Georg Smaus und Dr. Stefan Wölfl

Bei organisatorischen Fragen wenden Sie sich bitte an PD Dr. Jan-Georg Smaus.

Beschreibung

Model Checking ist die in der Praxis wichtigste Methode zur Verifikation und Falsifikation von Hardware- und Softwaresystemen. In diesem Seminar geht es vorrangig um den automatentheoretischen Ansatz zum Model Checking. Bei diesem Ansatz haben wir zum einen ein System, und zum anderen eine Eigenschaft, die dieses System haben soll. Das System ist gegeben als irgendeine Art von Automat (endlicher Automat, Büchi-Automat, verallgemeinerter Büchi-Automat etc.). Die Eigenschaft ist gegeben als Formel in einer Temporallogik (LTL, CTL, ATL, etc.). Die Eigenschaft wird nun in einen Automaten (den Formelautomaten) übersetzt und mit dem ersteren Automaten verglichen, d.h., je nach dem genauen Verfahren, muss etwa der Schnitt beider Automaten berechnet werden oder das Enthaltensein getestet werden, um festzustellen, ob der Systemautomat die Eigenschaft erfüllt.

Die Thematik des Seminars ist grob folgendermaßen untergliedert:

  • Logiken: LTL, ATL, CTL, Presburger Arithmetik, etc.
  • Automaten: endliche Automaten, Büchi-Automaten, verallgemeinerte Büchi-Automaten, etc.
  • Bezug zu Isabelle/HOL: Isabelle/HOL ist ein Beweiswerkzeug, das in der Vorlesung Computer-Supported Modeling and Reasoning gelehrt wird. Es gibt einige wenige Arbeiten dazu, wie man Isabelle/HOL auf Automatenkonstruktionen im Model Checking anwenden kann.
  • Spiele: Modellierung reaktiver Systeme als Spiele zwischen Controller und Umgebung, Algorithmen zum Lösen solcher Spiele.
  • Bezug zur Künstlichen Intelligenz: Anwendung von automatenbasierten Techniken auf Probleme aus der Künstlichen Intelligenz, Heuristiken im Model Checking.

Zeit und Ort

Hinweis: wenn Sie gerne am Seminar teilnehmen würden und lediglich aus terminlichen Gründen daran gehindert sind, melden Sie sich bitte bei PD Dr. Jan-Georg Smaus.

Vorbesprechung: Mittwoch, 11. Mai 2011, 14:15 Uhr, im Besprechungsraum 52-00-016.

Themenvergabe: Die Themen werden in der Vorbesprechung von den jeweiligen Betreuern vorgestellt und schon kurz davor auf der Themen-Seite aufgeführt. Kurze Zeit nach der Vorbesprechung kann jeder Teilnehmer Themenwünsche angeben. Jeder Seminarteilnehmer schickt seine Themenwünsche bitte als geordnete Liste mit fünf Themen aus mindestens drei der fünf Blöcke bis spätestens 16. Mai per E-Mail an PD Dr. Jan-Georg Smaus.

Abgabe der Ausarbeitung: 15. Juli 2010, 23.59 Uhr MESZ

Abgabe der Vortragsfolien: 22. Juli 2010, 23.59 Uhr MESZ

Bitte achten Sie darauf die Abgabetermine einzuhalten. Werden die Folien oder die Ausarbeitung später abgegeben, müssen wir aus Gründen der Gleichbehandlung für jeden Verspätungstag eine Notenstufe abziehen (bspw. von 2.3 auf 2.7).

Vorträge: Als Blockseminar am 28. und 29. Juli 2011.

Ort: Videokonferenzraum im Geb. 106, 04-007

Anforderungen

Um ECTS Punkte zu erhalten, müssen die Seminarteilnehmer

  • einen Vortrag von jeweils 25 Minuten Dauer halten,
  • eine Seminarausarbeitung abgeben,
  • über ein weiteres gewähltes Thema einen 5-minütigen Kurzkommentar nach dem jeweiligen Vortrag abgeben, sowie
  • während des gesamten Seminars anwesend sein.

Die Leistungen sind entweder auf deutsch oder auf englisch zu erbringen und werden benotet. Für die Beurteilung werden die Ausarbeitung, die Erstellung der Vortragsmaterialien, die Vorträge selbst sowie die Beteiligung am Seminar mit einbezogen. Es können 4 ECTS-Punkte erworben werden. Bitte beachten Sie, dass Sie sich auch für die Prüfung anmelden müssen, damit die Leistung auch als Prüfungsleistung gewertet werden kann.

Die Ausarbeitung sollte mit LaTeX erstellt werden und 10-12 Seiten umfassen. Kommentierte Beispiele, die zur Orientierung und für die Grundstruktur verwendet werden können, finden Sie in unserem Seminarratgeber. Dort gibt es auch weitere Hinweise zum Erstellen der Ausarbeitung und zum Halten eines Seminarvortrags.

Plagiate: Alle Zitate, wörtliche und sinngemäße, müssen als solche gekennzeichnet werden. Dies gilt auch für aus Quellen entnommene Abbildungen.