Also ich würde fast vorschlagen, wir machen ein Wiederholung vom letzten Mal.

Sollen wir denn das Material machen?

Wir machen das auch so wieder hier.

Wir können ja folgendes machen. Wir beschäftigen uns eingangs noch mal kurz mit den Regeln für die Semantik.

Dann habe ich noch zwei Beispiele über, die ich letztes Mal machen wollte und nicht wirklich geschafft habe.

Dann können wir uns noch kurz über Tresemantik unterhalten, die ist nicht schwer zu definieren.

Da wollte ich dann die elementaren Eigenschaften von angucken, ob wir so weit kommen.

Wir erklären einfach noch mal diese Regeln der CCS Semantik.

Es gibt im Wesentlichen immer pro Konstrukt der Sprache eine oder manchmal mehrere Regeln, die einem gestatten,

Übergänge herzuleiten, die ein solcher Prozess macht.

Was das Ganze letztlich tut, ist, es definiert ein Label Transition System.

Zunächst definieren wir ein riesengroßes Label Transition System, in dem alle CCS Terme leben.

Die Zustände des Label Transition Systems sind gerade die CCS Terme.

Man interessiert sich dann, wenn man eine bestimmte Prozessdefinition hat, nur für den Teil des großen Systems,

den man dann von da aus erreicht. Die Semantik ist ein bisschen erreichbarer als Teil des großen Systems.

Genauer gesagt hat man dann als die eigentliche Syntax einer Prozessdefinition,

die eine Teilmenge der Menge aller Prozessnamen abbildet, auf jeweils eine Definition dafür.

Die wiederum Prozessnamen aus dieser Teilmenge verwenden.

Ich darf nur solche Prozessnamen verwenden, die ich auch definiere.

Ein solches Ding, das erzeugt jetzt ein LTS. Was genau da erzeugt wird,

werden wir nachher sehen von dieser Definition auch tatsächlich.

Was ein Prozessname tut, das hängt eben von seiner Definition ab.

Das LTS, das von diesen Dingern hier erzeugt wird, in dem Sinne,

dass ich praktisch eine Ackermelde habe, Kappa0 nach Q, die eigentlich nur eine Einglättung ist.

Und Q ist die Teilmenge der Prozessterne über Kappa0.

Das schließt dann die Namen in Kappa0 selbst ein.

Jeder Name ist ja selber ein legaler Prozessterne.

Und dieses Kappa schlicht und einfach eine Einglättung, aber gleichzeitig sind sie eine Abbildung von einem Prozessname

auf seine Bedeutung als Zustand in diesem großen Transitionssystem.

Das Ganze funktioniert über Regeln, zum Beispiel diese hier.

Wenn ich ein Action-Prefixing habe, dann bewirkt das eben einen Übergang mit genau dem Label,

der als Aktion dransteht und man kommt in einem Zustand an, wo diese Aktion schon erledigt ist,

dann ist man also diesen Restprozessterne als neuer Zustand.

Warum ist das eine Regel?

Das ist ein Spezialfall einer Regel, sie hat hier oben keine Prämissen.

Die Regel heißt aber, wenn ich die Prämissen hergeleitet habe, darf ich die Konklusion herleiten.

Hier habe ich keine Prämissen, das heißt, ich darf die Konklusion einfach so herleiten.

Dann gibt es diese hier.

Da habe ich jetzt eine Regel, wie verhält sich eine Summe von Prozessen,

die ja unendlich viele Summen haben kann, wenn sie will.

Die Sache ist dabei, ich verhalte mich eben wie ein irgendwie ausgewählter Prozess aus dieser Summe.

Wenn der einen Übergang machen kann unter irgendeiner Aktion alpha nach gestrich,

dann kann die Summe das auch.

So, dann.

Jetzt schon parallel.

Dann kommt die Restriktion, also ich habe einen Prozess P, in dem ich eine Anzahl von Aktionen verstecke.

Damit der einen Übergang alpha machen kann, muss das ein Name alpha sein, der nicht versteckt ist.

Das heißt, alpha und alpha quer dürfen beide ein bisschen hell sein, also mit einer Wortnummer wird in jedem Namen auch der zugehörige Kohlarme versteckt.

So, und wenn das so ist, dann kann dieser Prozess das machen, was eben P machen kann.

Das hält sich ansonsten gleich, außer dass eben die Aktionen verboten sind, die versteckt waren.