Nichtsequentielle Systeme und Nebenläufige Prozesse
TUM-Informatik Log
o Technische Universität München
Fakultät für Informatik
Forschungs- und Lehreinheit VII
TUM Logo

V O R L E S U N G

Nichtsequentielle Systeme und nebenläufige Prozesse

Wahlpflichtvorlesung aus dem Bereich III (Theoretische Informatik) im SS02




Ein Lösungsvorschlag für die Klausur befindet sich auf der Übungsseite. Die Ergebnisse werden Am Freitag, den 19. Juli, in der Vorlesung bekanntgegeben. Eine Klausureinsicht findet am gleichen Freitag um 14:00 Uhr im Raum 2207 statt.

Die Klausur zur Vorlesung findet am Mittwoch, den 17. Juli, von 8:00-10:00 Uhr im Hörsaal 1260 statt. Es sind keine Hilfsmittel zugelassen. Bitte kommen Sie rechtzeitig vor 8:00 Uhr und bringen Sie zur Feststellung der Identität Ihren Studentenausweis und einen Personalausweis oder Reisepaß mit.

Die Übungsscheine können bei Frau Sterl (Raum 00.10.013) abgeholt werden.


Dozentin: Dr. Astrid Kiehn

Zeit und Ort: (Beginn: 17.4.)

Hörerkreis:
Studierende im Hauptstudium der Informatik, Studierende im Hauptstudium Mathematik mit Nebenfach Informatik.

Übung: Begleitend zur Vorlesung findet eine zweistündige Übung statt. Mit Bestehen der Klausur kann die Vorlesung zusammen mit der Übung als Theoriepraktikum eingebracht werden.

Zeit und Ort: Mo 13.00 - 14.30 Uhr, Raum 2710 (Beginn: 22.4.)

Inhalt und Literatur: hier

Skript (9.08.02) Das Skript ist in einigen Teilen noch skizzenhaft und wird weiter fortgeschrieben.


Folien aus der Vorlesung

Einführung
Äquivalenzbegriffe
Beispiele zur Bisimularität: Beispiele 1 Beispiele 2 Beispiele 3
Automatenbeispiele: Automaten 1,2 und 3 Automaten 4 und 5
Grundsätzliches zu Bisimulationen, n-Schritt-Äquivalenzen
Beispiel zum Bisimularitäts-Bestimmungs-Algorithmus
Bisimularitäts-Bestimmungs-Algorithmus, Progression und Up-to Bisimulationen
Divergenz
Philosophen-Beispiel: als Petrinetz, als Transitionssystem, nochmal als Transitionssystem
Fairness, Sicherheits- und Lebendigkeitseigenschaften
Büchi-Automaten
Komplementierung von Büchi-Automaten
I/O-Automaten
Stenning-Protokoll
Lamports Algorithmus
CCS
Beobachtungskongruenz
Beweissystem DED(A)
Gesetze (10.7.02)
Rekursionsesetze
Alternating-Bit-Protocol
ACP, TCSP (10.7.02)
CTL
LTL
Gegenüberstellung

Astrid Kiehn, Barbara König, Last modified: Mon Oct 7 13:43:30 MET DST 2002