So, man kann das Blatt so wie es im Gestell ist noch nicht lösen, weil wir eben die Semantik,
verwendet wird, wollte ich ja erst kennenlernen, aber ich bereite das schon mal.
Ich mache das mit Vorhersicht, man weiß, worauf man dann aufpassen muss,
wie es dann muss. Also nach der heutigen Sitzung sollte man in der Lage sein,
das Platz zu lösen, wenn man nicht mehr schreiben darf.
Also wir haben hier erstmal hier so etwas Praktisches,
ein Mutual-Explosion-Argorithmus, wo also eine Demokore verwendet wird,
um zwei Benutzer, ihr seht hier erstmal, sobald es hier gescrollt ist, nur ein,
um bei zwei Minuten und halb zu regeln, wie die einen kritischen Abschnitt gemeinsam betreten.
Dazu muss also jedes Mal, wer den kritischen Abschnitt betreten will,
er muss erstmal die Demokore setzen, dann kann er rein, wenn er die erfolgreich gesetzt hat.
Wer rausgeht, gibt den Sender wieder frei und fängt von vorne an.
Dann nimmt man die Demokore, die das einfache Prozess, der von Flag an Flag aus macht,
und synchronisiert natürlich über P und V hier mit dem User-Prozess.
Dann soll man nun verschiedenes tun.
Man soll gemäß der CCS-Demantik ein Label Transition System herleiten.
Das soll man hinmalen.
Zunächst mal für den Fall, wo keine Control-Excusesion gefragt ist,
wo nur ein einzelner Benutzer ständig dies vorgesetzt hat.
Dann packt man einen zweiten User dazu.
Das macht überraschend, dass der zweite User genauso aussieht wie der erste.
Aber zweimal den selben Prozess parallel laufen lassen mit sich selber ist nicht dasselbe wie nur eine Kopie.
Das kann man sich kurz ändern. Das ist wie wenn zwei Informatiker in die Kaffeemaschine wollen.
Das ist eigentlich so genau das, was wir hier machen.
Dann argumentieren Sie, warum das Nutex-Problem in Nutex 2 löst.
Argumentieren heißt, man sagt, was in dem Graphen nicht auftaucht, was den Geschwindigsten verletzen würde.
Dann wird der User geändert, sodass der Simapore zu spät freigibt.
Das ist eine falsche Plenetierung von diesem Simapore-Verfahren.
Wenn der Simapore-Verfahren schon freigibt und er dann wieder rausgeht,
dann wird es offensichtlich vorkommen können, dass die beiden User gleichzeitig bei einem klinischen Erschütz sind.
Sobald er nicht freigegeben hat, dann der nächste hier reinspringen kann.
Das ist keine Rocket-Silence, das darf schief gehen.
Aber man soll eben mal sehen, dass wenn man das Nutex 2 jetzt mit dem geänderten User laufen lässt,
dann er einen Graphen rauskriegt, der offensichtlich die User verletzt.
Dann Aufgabe 2.
Hier ist es auch nicht so richtig schwierig gegeben, was wir uns letztes Mal schon angeguckt haben.
Das ist jetzt ein Prozess, in dem ich im Prinzip so aussieht, wie wenn ich einen neuen Tag habe.
Ich weiß nicht, ob das ein Prinzip ist, sondern genau so.
Der Simapore wechselt auf einen Weg und läuft leider immer im Kreis.
Den schalte ich endmal zu sich selber parallel.
Da soll einfach mal ausgerechnet werden, wie groß ist eigentlich der Graph,
den das nachher infizit bestreitet, also wie viele Zustände hat das Technik.
Das sieht man im Grunde so, aber schon durch ein paar formale Weisen, in denen man halt Motionen macht.
Nichts, wenn man auf dem Ausdenken darüber denkt, welches groß ist,
wenn man also dieser Graph ist, dann ist es ein Transition System.
Und das beweist man, welche Motionen da hängen.
Der Witz daran ist, er ist ziemlich groß.
Das ist ein relativ übersichtlicher Ausdruck, dass er immer im Schrei,
wenn es relativ locker nicht zu groß ist, dagegen kann man ja schon relativ kleine Hände,
ziemlich große Graphen erzeugen.
Presenters
Zugänglich über
Offener Zugang
Dauer
01:28:40 Min
Aufnahmedatum
2015-04-24
Hochgeladen am
2019-04-23 13:33:08
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.