Seminar: Logik und Concurrency
|
|
|
|
Veranstaltungsnummer: 18.406
Titel: Seminar: Logik und Concurrency
Veranstalter: Berndt Farwer
Zeit und Ort: Do. 14-16, Beginn: Do., 23. Oktober
Inhalt: Kennenlernen verschiedener Modellierungsarten für nebenläufige Systeme sowie der Möglichkeiten zur Spezifikation und Verifikation von Eigenschaften solcher Systeme.
Lernziel: Die Studierenden erhalten einen umfassenden Überblick über den rasch wachsenden Einsatz von Logiken und Kalkülen bei der Erstellung von Modellen für Nebenläufigkeit.
Eine mögliche Auswahl an Themen ist:
- Nebenläufigkeitsmodelle: Prozeßalgebren, wie Milner's CCS und Hoare's CSP, Milner's Action Structures, Transitionssysteme, Petrinetze (sollen weniger intensiv behandelt werden, da bereits aus den Grundvorlesungen bekannt), Vgl. unterschiedlicher Semantiken (interleaving vs. real concurrency semantics).
- Logiken und Kalküle: Modale und temporale Logiken (UNITY, CTL, LTL, HML, ...), Lineare Logik, mu-Kalkül, pi-Kalkül,
- Beweisverfahren.
- Bisimulation
- Ausdruckstärke vs. Komplexität
Stellung im Studienplan: Hauptstudium, Vertiefungsgebiete:Th1, Th2, Th4; als theoretische Vertiefung für fast alle Gebiete geeignet.
Voraussetzungen: Grundkenntnisse von Petrinetzen aus den Kernvorlesungen, Grundkenntnisse über klassische Logik erster Stufe
Vorgehen: Vorträge der Teilnehmer, Diskussion in der Gruppe
Literatur:
Faron Moller, Graham Birtwistle (Eds.): Logics for Concurrency,
Springer-Verlag, LNCS 1043, 1996.
Weitere Literatur wird in der Veranstaltung bekanntgegeben.
Periodizität: einmalig
Eignung: Für Lehrer und Nebenfächler bedingt geeignet
Stichworte: Logik, Nebenläufigkeit, Concurrency
