Also ich weiß nicht, was Herr Prof. Schiller gesagt hat. Er ist weg in dieser Woche und ich weiß, wie er ist.

Das ist eine, die man heute noch nicht verstanden hat. Er ist jetzt aufgezählt.

Warum ist das? Ich glaube, dass diese Großrunde schon einmal...

Ja, weil es relativ interaktiv ist und sich manchmal ändert.

Ich finde das eigentlich viel praktischer. Ich mache auch einen anderen Kurs mit so einem kleinen Mikrofon.

Ich mache das auch bei ein bisschen kreativen Studenten. Die Studenten arbeiten am Tafel und wir müssen das immer wechseln. Das ist unfraktisch.

Das ist wahrscheinlich besser.

Okay, wir machen heute eine starke Zimtisation.

Es wurde euch diese Beispiele mit Kaffeemaschinen und Kaffeetrinker gezeigt.

Es wurde eine Art von Equivalenz für Prozesse eingeführt.

Die heißt Tracik Weivalence.

Das ist eine Form der Equivalenz, die normalerweise in der Theorie verwendet wurde.

Das ist die Hauptbegriff.

Es wird genauso, dass die nicht unbedingt starke Bissimulationen, aber verschiedene Art von Bissimulationen sind die Hauptequivalenzen für die Prozessalgibere.

Wenn man die Definition von LTS betrachtet, dann kann man merken, dass es fast genauso ist, als die Definition von einem Automaton.

Aber das Unterschied ist, dass die Automaten nicht miteinander kommunizieren.

Deswegen ist die Equivalenz, die man dafür verwendet, normalerweise diese Tracik über uns. Mehr braucht man nicht.

Durch dieses Feature von Prozessalgebern, dass die Prozesse miteinander kommunizieren, braucht man eine andere Art von Equivalenz.

Das sind verschiedene Art von Bissimulationen. Wir machen heute eine starke Bissimulation.

Es gab zwei Beispiele vom Kaffeemachine.

Das ist die CTM, das ist der Coin Coffee.

Das ist die CTM, das ist der Coin Coffee.

Das ist die CTM, das ist der Coin Coffee.

Der Unterschied ist, dass hier die Entscheidung, ob es Koffe oder Tier ausgegeben wurde, später getroffen ist.

Hier zieht sie die Klammer.

Hier wartet sie, bis sie ein Element zum Bekommen, und dann wird die Entscheidung getroffen.

Ich habe wahrscheinlich gesagt, dass diese zwei Beispiele, die in der Spurequivalenz sind, die Menge von Traces für beide sind gleich.

Aber dann kann man so ein Prozess betrachten.

Koffeedikt, also koffeesüchtiger, er will nur Koffe trinken und kein Tier.

Dann kann man so ein Experiment ausdenken, wie man so einen Prozess mit diesen zwei Koffeemachinen kommuniziert.

Da rechts im unteren sollte dadurch T quer stehen, in der Mitte. Coin.T quer, eigentlich T-Milch-Coffe.

Also man kann durch zwei solche Prozesse betrachten.

Der obere wird immer Kaffee ausgeben, weil T ausgeliefert wird.

Der untere entscheidet sich vorher und kann dann in den T-Fall kommen.

Für den Ersten ist das die einzige Möglichkeit.

Für den Zweiten gibt es die Möglichkeit, dass man nach dem Coin-Alt-Bein-Bluft den Druck bekommt.

Das ist keine gute Option, weil man die Prozesse so spezifizieren muss, dass man nie feststeckt.

Die Kaffee funktioniert als Service, also man muss nie feststecken, dass es schlecht ist.

Für dieses Beispiel ist es nicht so wichtig. Was wichtig ist, dass man durch dieses Experiment diese zwei Fälle unterscheiden kann.

Deswegen ist die Spur-Mekanik nicht so gut betrachtet, weil wenn diese zwei Maschinen gleich betrachten,

müssen sie sich auch gleich beenden. Wir müssen hier genau dieselben Ergebnisse bekommen.

Es sollte nicht sein, dass wir diese unterscheiden können.

Wir möchten eine andere Äquivalenz einführen, die stärker als die Technik-Äquivalenz ist.

Die Äquivalenz wird so bezeichnet, das heißt, starke Bissimulabilität.

Hier ist Bissimulabilität und hier Bissimulation. Das sind zwei Begriffe, die miteinander verknüpft sind.

Bissimulation verwendet man als Hilfsbegriff, um Bissimulabilität zu definieren.

Das wird dann eine Äquivalenz-Solution. Bevor ich das definiere, kann ich mit Hilfe dieses Beispieles eine Eigenschaft behaupten,

die diese Äquivalenz hat. Es folgt genau von diesem Beispiel.

Wir wollen nicht, dass diese zwei Prozesse äquivalent sind. Das heißt, wir wollen keine Distributivität.

Wir dürfen das nicht, dass wir diese Klemme auflösen können, sondern dass es diese Art von Distributivität hat.