Alles klar, also, letztes Mal haben wir für die, die nicht da waren, so ein bisschen lockerere Einführungen gemacht,
was interessiert einen überhaupt, wenn man ein nebenbeutelendes System spezifizieren will, in welche Aspekte muss man denken,
rausgekommen ist, dass man also offenbar bei nebenbeuteligen Systemen an zumindest drei Arten an der Idee denkt.
Also erstens, man hat irgendwie so Prozesse, die haben interne Zustände zwischen denen, die Übergänge haben.
Zweitens, diese Übergänge, die senden eventuell mal Signale nach außen, also ein Lieblingsbeispiel, wie immer,
in solchen Kursen und auch in Büchern zum Thema ist die Kaffeemaschine. Und ein Signal der Kaffeemaschine wäre zum Beispiel,
zwei einer, erstens zum Beispiel Kaffee auszugeben und zweitens eine Münze entgegen zu geben. Das würde beides also als ein Signal
zählen, das bei so einem Übergang stattfindet. Und letztlich hat man dann eine Konfiguration von Prozessen,
zum Beispiel eines Betriebssystems klar gemacht, wo also diese Signale wieder ausgetauscht werden, mehr oder weniger als Ports fungieren,
mit denen einzelne Prozesse untereinander verbunden sind. Okay, jetzt gehen wir um diese Grundideen,
die wir nun alle relativ einfach sind, klar gemacht haben. Wollen wir also heute kennenlernen, erst mal eher
noch auf Informellerebene, also mit einer formalen Syntax, aber noch ohne die Semantik tatsächlich formal festzulegen,
und jetzt zu den Kalkülern dafür. Und zwar heißt der CCS, das ist der, nochmal, Calculus of Communicating Systems,
der ist vom kürzlich erst etwas zu jung verstorbenen Robin Möhner, da man soll man es genau ansetzen,
das Buch ist 1987 erschienen, in der Entwicklung an sich muss man wohl eher auf 1986 da klicken.
So, CCS ist jetzt einfach eine Sprache formaler Ausdrücke, die ich jetzt im Prinzip als Einzeiter über so eine Grammatik
anschreiben könnte, das würde ich eher erst am Schluss machen, sondern nicht als die Konstrukte dieser Grammatik jetzt
eins nach dem anderen einführen, und dann werden wir uns also mehr so informell Gedanken machen über die Semantik dieser Konstrukte,
wir lassen es natürlich nicht auf dieser informellen Ebene, sondern wir nehmen uns nächste Woche,
ja, was also die tatsächlich Formal- und Syntax-Semantik dieser Konstrukte ist.
Achso, apropos nächste Woche, wir haben ja noch nicht so das Rundehende Vorgehen besprochen,
das ist, ich glaube im Umnis als was, als Vorlesung mit Übung, das trifft auch zu, also ich werde Vorlesungen und Übungen
in lockerer Folge miteinander abwechseln lassen, dazu muss ich natürlich Zettel rausgeben, damit man in der Übung was zu machen hat,
das werde ich vermutlich nächste Woche das erste Mal tun, es gibt typischerweise nicht so rasend viele Zettel in einem normalen Semester,
während es tendenziell so was wie sechs ist, aber dieses Semester, Moment, wir haben Dienstag und Donnerstag,
also es fällt einfach relativ viel aus, ich habe es jetzt anders als für Theorie der Programmierung nicht an den Teil vorher ausgewächt,
wie viel ausfällt, in der Programmierung kamen da also praktisch drei Wochen aus, die ausfallen, das wird hier nicht ganz so viel, weil...
Letzter Donnerstag fällt aber einiges aus.
Ja, also Donnerstag fällt einiges aus und ich glaube, nein, Dienstag und Montag ist sogar egal, es fallen praktisch drei Wochen flach,
es fallen ja zwei Dienstag flach, nämlich Dienstag nach Ostern und Bergdienstag, das ist genauso viel wie Montag, und das am Montag?
Nee, Montag ist nichts, ich habe nur für die Kombination Montag und Donnerstag, habe ich es ausgerechnet, das genau drei Wochen ausfallen,
und die Kombination Dienstag und Donnerstag ist aber genauso, weil eben die nach den freien Monate am Montag und die Dienstage jeweils ja auch immer freisegen.
Und es ist fein ja also nicht weniger als vier Donnerstage flach, also wir haben im Endeffekt nur elf Wochen, von denen die erste ja auch gleich rum ist,
also das heißt, wir schaffen wahrscheinlich nicht ganz sechs Zettel, wahrscheinlich vier.
Die Zettel würde ich also rausgeben, wir besprechen die dann hier in den Übungen in offenbar familiärer Atmosphäre,
und ich korrigiere die auch, dann bekommen sie also letztlich auf die Zettel eine, ja dann natürlich bei so kleiner Statistik,
daumengefallene Note, die dann berechnet wird mit der eigentlichen Prüfung, der möglichen Prüfung am Ende.
Man hat uns gesagt, dass wir das nicht mehr als Klausur mit Zusatzleistungen in Unibis eintragen dürfen aus rechtlichen Gründen,
also ist das jetzt offiziell eine Portfolio-Prüfung, was mit sich bringt, dass also tatsächlich einfach die Endnote aus Prüfungsleistungen,
also aus Übungsleistungen und lündlicher Prüfung gemittelt wird.
Was für Sie einen positiven und einen negativen Effekt mit sich bringt, der negative ist,
also anders als bei der früheren Regelung, können Sie sich durch schlechte Übungsleistungen in der lündlichen Note nachher auch noch verschlechtern,
früher konnte man sie nur verbessern.
Positiv ist, Sie könnten ein eventuelles Durchfallen mit den Übungsleistungen da rausreißen, das würde ja nicht gehen.
Beides würde ich sagen, typischerweise in diesen Veranstaltungen, mir theoretisch.
Ich bin es gewohnt, diese Arrangements vor Akteurin zu diskutieren,
wenn jemand noch Vorschläge oder Ergänzungen hat, das hier nicht gut findet, kann er das gerne sagen.
Wie gesagt, es gibt eine Anzahl syntaktischer Konstrukte, mit denen ich also jetzt in jedem Leute die Prozesse beschwanken kann.
Das Einfachste ist diese Inge, Null.
Die Null, das schnell erklärt, Null ist der Deadlock.
Presenters
Zugänglich über
Offener Zugang
Dauer
01:26:50 Min
Aufnahmedatum
2014-04-10
Hochgeladen am
2019-04-21 00:29:22
Sprache
de-DE
-
erläutern semantische Grundbegriffe, insbesondere Systemtypen und Systemäquivalenzen, und identifizieren ihre wesentlichen Eigenschaften
-
erläutern die Syntax und Semantik von Logiken und Prozesskalkülen
-
fassen wesentliche Metaeigenschaften von Logiken und Prozesskalkülen zusammen.
-
übersetzen Prozessalgebraische Terme in ihre denotationelle und operationelle Semantik
-
prüfen Systeme auf verschiedene Formen von Bsimilarität
-
prüfen Erfüllheit modaler Fixpunktformeln in gegebenen Systemen
-
implementieren nebenläufige Probleme in Prozessalgebren
-
spezifizieren das Verhalten nebenläufiger Prozesse im modalen mu-Kalkül.
-
leiten einfache Meta-Eigenschaften von Kalkülen her
-
wählen für die Läsung gegebener nebenläufiger Probleme geeignete Formalismen aus
-
vergleichen prozessalgebraische und logische Kalküle hinsichtlich Ausdrucksmächtigkeit und Berechenbarkeitseigenschaften
-
hinterfragen die Eignung eines Kalküls zur Lösung einer gegebenen Problemstellung
Literatur:
- Robin Milner, Communication and Concurrency, Prentice-Hall, 1989
-
Julian Bradfield and Colin Stirling, Modal mu-calculi. In: Patrick Blackburn, Johan van Benthem and Frank Wolter (eds.), The Handbook of Modal Logic, pp. 721-756. Elsevier, 2006.
-
Jan Bergstra, Alban Ponse and Scott Smolka (eds.), Handbook of Process Algebra, Elsevier, 2006.