Ah, ich habe ein Interview, das ist mal gewesen und wir machen das ein bisschen weiter und
schauen, die auch die weitere Eigenschaften von Stark bis Himmels herrschen.
Und zwar, es gibt ein paar Eigenschaften und ich möchte die beweisen, aber dann habe ich geschaut
auf die kommenden Rundblätter und habe gesehen, dass es Nutzer hat, die das allein gemacht haben.
Aber zur Information kann ich sagen, dass die folgende Sache, wo die Äquivalenzen gelten,
zum Beispiel hier eigentlich gar nicht, es ist ein bisschen komisch, wenn nicht,
die Runde wird nicht behauptet, wahrscheinlich weil es filial ist.
Also das wird, glaube ich, eventuell eine Hausaufgabe und man kann auch die ähnlichen Sachen
für den dittimästischen Bein beweisen, also sowas wie q plus q, Äquivalent zu q plus pi,
q plus q, q plus q, q plus q, q plus q.
Dürfte sich das nicht eigentlich dadurch ergeben, dass wir eigentlich keine Reihenfolge für Summen haben?
Ja, wahrscheinlich ja.
Also das ist trotzdem zu devisen, ja.
Aber diese zwei Sachen, die freut er einfach, weil wir haben die Summe so definiert, dass p plus q gleich...
... ok, ich schreibe zu, p1 bis p2 gleich eben...
Also bei der Definition, diese Summe unterscheidet nicht zwischen den Prozessen, die in verschiedenen Reihenfolgen in diese Summe kommen.
Also das und das muss eigentlich nach der Definition werden.
Es gibt auch so ein Gesetz, p plus q, die Dämpferkanz, aber das folgt auch von hier, obwohl ich das nicht so natürlich finde.
Also wir haben hier eine Summe über die Menge, aber ich würde eigentlich das andere machen.
Ich würde eine Summe über die Multimente machen, sodass das nicht offensichtlich gilt, weil naja, das ist so eine Sache.
Also wie entscheidet die Summe, ob die Komponenten gleich sind oder nicht?
Zum Beispiel könnte ich einen Prozess, die eine Kopie von diesem Prozess ist, also irgendwas umnehmen,
und also inhaltlich dasselbe kriegen, aber unter anderem Name, deswegen ein bisschen komisch wahrscheinlich diese Definition für mich.
Aber es ist die Tradition, so ist das gemacht.
Ja, aber auf jeden Fall gilt es für die starke Bissimilation, für die starke Bissimilität.
Okay, und dann liegt es noch ein Teil zusammen.
Ja, wohl, ich kann wahrscheinlich das bereiten.
Und dann gibt es hier noch andere Teile.
Hier könnt ihr definitely was SBS machen, die вы farewell Washington, entrance.
Also, wir überweisen, dass R, also, die Flüßnumme, R, P, gilt mit R, vielleicht,
also, S, S, S, also, ich kann so eine Relation bilden und dann, also,
dann gilt das für die Definition und um zu zeigen, dass es eine B-Simulation ist,
okay, betrachte ich jetzt wieder S plus Null, also, ich sage mir, dass es eher mit S ist,
und, also, es gibt diese zwei Bedingungen, die zweite Bedingung ist einfacher,
ich fange mit der zweiten Bedingung an, also, wenn ich eine Transition auf dieser Seite habe,
dann habe ich auch eine, ja, eigentlich sind sie beide einfach,
also, das reicht eigentlich nicht aus, also, hier muss ich eigentlich S plus Null,
S und auch, also, die Parallel mit vielleicht dem ersten, zweiten Komponente betrachten,
und wir sehen jetzt, warum, also, es gibt eigentlich dann mehrere Fälle,
weil ich muss alle solche Zahlen betrachten, alle solche Zahlen betrachten, und zwei Bedingungen,
also, es gibt insgesamt vier Fälle, okay, aber das kriegt man, warum, weil, also,
man hier diese SOS-Tageln verwendet, weil hier sagen wir, okay, es gibt eine Tradition von S nach S Strich,
und das ist ein Prozess, wie, wie wissen wir, welche Bezüge für so ein Prozess möglich sind,
die verwenden halt die SOS-Regeln, also, wenn S nach S Strich wechselt,
dann wissen wir das, S plus Null macht S Strich, okay, also, ja, keine Null für S Strich,
und das gilt dann, weil ich diese extra Klausel hier hinzugeschügt habe, sonst würde ich nicht gehen,
also, ist es, kann man sagen, 2,1, dann gibt es 2,2, das ist, wenn die ursprünglich sowas haben,
das ist natürlich trivial, dann gibt es 1,2, und das ist S.
Also, und hier überlegen wir in eine andere Richtung,
wann ist diese Transition S plus Null möglich, es ist genau dann möglich, wenn man diese Regeln anwenden kann,
Presenters
Zugänglich über
Offener Zugang
Dauer
01:27:02 Min
Aufnahmedatum
2015-05-08
Hochgeladen am
2019-04-23 15:29:03
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.