Intro
Ich erinnere an die Konstrukte, die wir in der CCS gelernt haben.
Da war einerseits der Dam-Block, dass er nichts machen kann.
Man suche jeweils etwas aus, was P oder Q machen kann.
Wenn P oder Q nichts machen kann, kann ich mir aus P oder Q nichts aussuchen.
Man muss also automatisch mir etwas aus dem anderen aussuchen, das berührt.
Dann gab es Parallelkompositionen. Ich lasse zwei Prozesse nebeneinander herlaufen.
Die Prozesse können sich synchronisiert verhalten, also über einen gemeinsamen Kanalnamen gleichzeitig einen Schritt machen.
Oder sie können sich asynchron verhalten, in dem Fall findet der Leaving statt.
Die Restriktion heißt, dass die Aktionsnamen, die ich hier wegnehme, im Verhalten von P nicht mehr sichtbar auftauchen können.
Das heißt, sie dürfen nur noch im P zur internen Synchronisation verwendet werden, aber nicht mehr nach außen in der Schalung treten.
Wir haben das jetzt nicht formalisiert und es dauert noch ein bisschen, bis wir das hinbekommen.
Wir haben hier diese Farbe von Prozessnamen A und A quer, die der Synchronisation dienen.
Die Idee ist, dass so ein synchronisierter Schritt, wo ein Prozess A macht, der andere A quer, gleichzeitig synchronisiert einen Schritt machen,
als eine interne Aktion gilt, die also nach außen nicht sichtbar wird.
Während also einsam, ohne eine Partneraktion, asynchron vorgenommene Schritte immer nach außen sichtbar werden müssen.
Ich hatte eine Frage zu dieser Parallelausführung. Wenn ich jetzt danach weitermachen will, dann laufen beide bis zum Ende und danach behält man sich wie der nächste?
Kann man das überhaupt abbilden?
Der Normalfall ist ja ohnehin, dass die nicht irgendwo ein Ende haben.
Es kann natürlich mal sein, dass einer zu Ende ist, dann läuft halt der andere weiter.
Wenn der eine zu Ende ist, heißt also, der läuft irgendwann in Deadlock.
Wenn das passiert, dann ruft er auch nie mehr hier, wenn es an Scheduling geht, und dann kommt eben immer der andere dran.
So.
Das waren die Konstrukte, die wir bisher hatten. Eins fehlt noch, das würde ich gerne dann...
Da ist das Ding, zieh noch mal was vor, was sich auch ein bisschen auf den aktuellen Zettel zieht.
Nennt man folgende Prozesse, sehr einfach.
P macht also A1, dann A2, und dann wieder P.
Q macht erst B1, dann B2, dann wieder B3.
Wir haben jetzt von Zuständen noch gar nicht so richtig gesprochen, aber das machen wir nachher noch nicht.
Aber man sieht schon ungefähr, dass da so ein Begriff von Zustand im Hintergrund steht.
Soweit P einmal A1 gemacht hat, ist das also in einem neuen Zustand.
Mit A2 kommt es wieder in den Ausgangszustand, genauso für Q.
Man sollte mit Funk und Mess davon reden, dass P und Q jeweils zwei Zustände haben.
Die Frage ist jetzt, wie viele Zustände hat P parallel Q?
Drei.
Drei? Einmal hinmalen, wie das intuitiv aussieht.
Also formale Symmantik haben wir ja noch nicht.
Wenn ich manche so ein bisschen mache, dann ist hier so ein Stern.
Wir können so Kombinationen haben, Stern und Dreieck, was weiß ich.
Wir können haben Stern und Plus.
Und wir können haben, ich habe einen vergessen, wir können Dach haben, was weiß ich.
Wir können haben Dreieck und Dach und wir können haben Plus.
Genau, also vier Zustände hat das Ding entscheidend.
Es geht um formale Symmantik, um das tatsächlich zu machen.
Das mag nicht von der Pfütterlänge aus, weil die jeweils zwei Zustände haben.
Und die dann weglaufen.
Ja, ich hatte irgendwie den Anfangszustand vergessen.
Wir wollen doch auch diese, mit dem A und dem A-Q, dass da irgendwie da Synchronisation stattfindet.
Wie ist das, wenn da jetzt kein A-Q zumindest nicht explizit vorhanden ist?
Wie verhalten die sich dann?
Presenters
Zugänglich über
Offener Zugang
Dauer
01:16:06 Min
Aufnahmedatum
2015-04-23
Hochgeladen am
2019-04-23 13:32:37
Sprache
de-DE
- Beschriftete Transitionssysteme
-
Prozessalgebren
-
Starke und schwache Bisimulation
-
Hennessy-Milner-Logik
-
Modaler mu-Kalkül
Lernziele und Kompetenzen:
Fachkompetenz Wissen Die Studierenden geben elementare Definitionen und Fakten zu reaktiven Systemen wieder. Verstehen Die Studierenden
-
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.