hospital
Die Schwache Bismilarität
Jo, Thema heute, Schwache Bismilarität.
Bei der Schwachen Bismilarität soll nun endlich das Tau seine Rolle ausspielen.
Das heißt, das Tau soll in irgendeinem geeigneten Sinne unbeobachtbar werden.
Das ist das, was wir meinen mit interner Aktion.
Das ist irgendwas, was im schwarzen Kastenstab findet und das wir nicht sehen.
Ja, gut, da muss man sich nun aber natürlich sorgfältig überlegen, was das heißt.
Wir fangen mal an mit einem Beispiel.
Wie immer, jetzt dreht sich das Beispiel von Informatiker und Kaffeemaschinen.
Wir haben ja unser Informatiker unverändert. Der publiziert und dann kräftig durchatmen und sich einen Kaffee holen, bevor er wieder publizieren kann.
Jetzt haben wir hier eine Kaffeemaschine und die Kaffeemaschine ist aber eine Bad-Koffeemaschine.
Das klingt ja schon schlecht wie Kaffee aus. Nein, das ginge ja noch.
Sie kann sich dann ständig verhalten und die Münze entgegennehmen, Kaffee ausgehen und vorne anfangen.
Aber manchmal nutzt sie auch unsere Münze und fliegt dann in der Rio.
Das ist nun ein Platz zu polieren, wo sie uns entgegen und weg von vorne an, ohne einen Kaffee auszugeben.
Das ist ein Blockschimmer.
Dann sehen wir uns natürlich das übliche System an. Wir schalten den Informatiker parallel mit der Kaffeemaschine.
Das verstecken wir gleich.
Fangen wir an damit, dass wir jetzt ausrechnen, wie das System aussieht.
So viel país posted, aber ich kann können cardido eine Linie光et auf,
Wie sieht es aus?
Anbauen oder was?
Anbauen.
Wir starten hier mit auf.
Von hier geht es an einmal ein KU-Übergang weg, wo wir quasi das schlechte Verhalten von der Kaffeemaschine haben.
Wir haben also einen Kaffee.cs-Paradiel-BCM ohne L.
Und einmal das normale Verhalten.
Und hier nach dem Koffeepunkt.
Und das da oben ist der weniger Deadlock.
Von da geht es nicht weiter, weil Kaffee ist eine versteckte Aktion und BCM-Kanäle.
Genau. Wir hatten ja immer dieses System verglichen mit diesem Serialmachen-Prozess.
Unserer Publisher-Courage-Prozess, der ständig nur Publikationen absondert.
Und wir hatten irgendwann mal gesagt, unser System mit der Heilen-Kaffeemaschine sah ja so aus.
Dann gab es einen Tau-Übergang für Nutzer-Einwerfen und noch einen Tau-Übergang für Kaffee-Ausgeben.
Und dann ging es von vorne los. Und wir haben gesagt, das wollen wir eigentlich selber sehen.
Wie sieht es da mit aus? Die Taus sollen eben unberuhigbar sein, dass sie nur zwei Tauschen sind.
Was ist das mit dem System?
Das ist unbedingt nicht equivalent sein, weil es hat irgendwie die Möglichkeit, zwischendrin zu deadlocken.
Was hat die Möglichkeit zu deadlocken andererseits? Ich kann das eigentlich nicht sehen.
Wenn ihr jetzt einfach anfangen, nach dem Bordel, alle Taus, lasse ich mal zusammenschnurren.
Ich könnte auch zum Beispiel auf die Idee kommen, wenn zwei Zustände durch einen Tau verbunden sind, dann sehe ich sie zum Beispiel.
Wenn ich das mit dem System hier mache, also die beiden zusammenschnurren lasse und die beiden zusammenschnurren lasse,
dann kommt genau das System raus durch das zusammenziehen der Taub-Übergänge.
Man muss halt gucken, dass die Zustände, die ich irgendwie zusammenführe, die gleichen Transitionen machen können.
Genau. Sehr wichtig. Das heißt, wir müssen nachher wieder sehen, dass wir eine passende Begriffung und Disimmulation kriegen.
Das wird ja auch durch den Namen schon angeleitet.
Das heißt, die native Lösung, einfach Taub-Übergänge zusammenziehen, die klappt auch mal nicht.
Wenn ich diesen Taub-Übergang hier zusammenziehe, dann kriege ich wieder das, was genauso aussieht, wieder nichts.
Das heißt, da sitzen noch die Stapeln.
Presenters
Zugänglich über
Offener Zugang
Dauer
01:26:37 Min
Aufnahmedatum
2015-05-22
Hochgeladen am
2019-04-23 13:50:45
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.