5 - Kommunikation und Parallele Prozesse [ID:10732]
50 von 530 angezeigt

und zwar nur so ganz blöd die Größe eines LTS

ist im Prinzip einfach die Anzahl der Zustände. Damit ist gemeint die Anzahl der Zustände.

Also streng genommen müsste man natürlich genauer messen als Anzahl Zustände,

Flussanzahl, Transitionen oder so, das je nachdem wie man es repräsentiert.

Also gemeint ist einfach Anzahl Schrift. Genau. Und bei der letzten Aufgabe,

Rekursive Definitionen, das ist aber also nicht nur blödes Umbenennen von Prozessen,

sondern wenn ich einen Prozess A habe, der irgendwie einen Prozess B auf der rechten

Seite hat und dieser Prozess B hat irgendwo wieder einen Prozess A, das ist auch dann,

also es gilt als Rekursiver Teil. Das heißt da muss wirklich am Ende dann eine Null stehen.

Genau, wenn es nicht Rekursiv ist, dann ja, da muss nicht unbedingt am Ende eine Null

stehen, weil ich ja aus dem Rekursiven Teil Prozessnamen habe. Also,

ja, also ich habe, was weiß ich, also nur so als Beispiel, ja unser übliches Beispiel, ja, das hier

wäre ja unsere Kaffeemaschine, das wäre also im BPA, ja, also verwendet ja noch nicht mal Summe und

der hier der Computer Scientist wäre da ja auch drin, ja. Und was jetzt gemeint ist mit dem

richt nicht Rekursiven Teil, das ist, das sind also Definitionen, die sich nicht mehr selbst

aufrufen, wohl aber natürlich eventuell die anderen, ja, also zum Beispiel die Universität zu nehmen.

Dieses Tier hier, ja, das wäre noch legal. Okay, also es ist doch recht ein beliebiger Term über

dem Rest stehen, nicht? Nur ich darf eben nicht wieder Rekursiv sein, also wenn ich Rekursiv sein

will, dann muss ich mich im BPA halten und sonst eben nicht. Rekursiv heißt wirklich, dass der Graf dieser Aufrufe irgendwann bei mir wieder ankommt. Genau das war, wo ich mir halt konfrontiert war, weil die Universität kommt ja irgendwie streng genommen quasi wieder bei CEM, bei WCS ohne CoinCopy. Ja, nee, ich will jetzt nicht von wegen streng genommen, sondern ich mal mir den Aufruf Graf dieser Prozessnamen, ja, und dann gibt es

Dinge, die also irgendwann mittelbar sich selber wieder aufrufen, wörtlich, ja, indem sie halt den Prozess erwähnen, der den Prozess erwähnt, der sie wieder erwähnt oder so, ja, und dann gibt es Dinge wie dieses Gu hier, wo wenn ich die Rekursiven aufrufe, verfolge ich nie wieder bei dem Ankommen. Okay.

Woher war es eigentlich unsere Symante, was jetzt von den Prozessdefinitionen quasi der Startzustand ist? Es gibt in dem Sinne keinen Startzustand, erst wenn ich mir einen Prozessnamen aussuche, dann ist der Prozessname in meinem Transitionssystem in irgendeinem Maßen der Startzustand.

Wo wird der quasi bestimmt? Der steckt da quasi im Namen, also du sagst ja nicht der Startzustand von diesem System, sondern du sagst, du hast ja U zum Beispiel und U ist der Schreibtier. Also habe ich dann natürlich quasi ein LTS nicht zu diesen Prozessdefinitionen, sondern zu konkret zum Beispiel.

Ja, ich kann, also im Level Transitionssystem steht ja eigentlich nichts davon da, dass es einen Startzustand hat. Und ich kann es mir natürlich aussuchen, ja, also ich sag entweder ich habe, ich mach noch U oder A.

Ich komme mal zum Beispiel auf Gewehr 1, leiten Sie blablabla, das LTS für den Prozess und das 1. Du könntest auch ein LTS für den Prozess User.

Ja, dann mache ich noch ein LTS für den Startzustand. In dieser letzten Aufgabe mit der Größe da kommt es mich drauf an.

Gemein ist mit der Größe immer das, was ich für, also die Gesamtgröße der LTS an allen benannten Prozessen hängt.

Das sieht mir jetzt ganz zu viel aus.

Ich war nur gedanklich gerade schon bei der Aufgabe 2.

Welche war das jetzt vielleicht? Das war genau die mit der Größe.

Ja, da gibt es natürlich zwei sehr kleine Teile, also die und A, die einfach nur B.

Q ist gleich A.B.Q.

Also Q selber ist natürlich ein benannter Zustand in dem System, was an Q dran hängt, ist sehr klein.

Der andere Teil des Systems ist natürlich der große Prozess, der parallel zu sich geschaltet ist.

Das ist der Teil, der interessiert wird in der Aufgabe.

Das ist ein bisschen ein Problem im Bereich des, wie kann ich sagen, dass das wirklich verschiedene Zustände sind?

Damit ich die Größe des Systems bestimmen kann, müsste ich ja irgendwie sagen, dass das wirklich verschiedene Zustände sind.

Wir haben noch keine Prozess-Äquivalenzen.

Das ist jetzt nicht verlangt zu zeigen, dass das Ding groß ist, nur irgendeine Prozess-Äquivalenz.

Auch das ist des Vierens.

Also wir würden einfach herausreichen, dass die Therma anders aussehen wird.

Ja, genau. Alles, was wir bisher kennen über so ein Transitionssystem ist, ist ein Knoten mit irgendeiner Identität.

Das ist in diesem Fall die Identität einfach zu einem Prozesstherm.

So viele Prozesstherme, die ich unterwegs treffe, das ist die große Neu-Systems-Äquivalenz.

Ich kann ja mehrere Eingänge zu einem Knoten machen.

Ja, genau. Das ist die Systeme, die zusammenlaufen können.

Das sind keine Beute.

So stellt man es zwar auch manchmal gerne vor, dass das in dem System, wo wir so nennlich aufgefüllt sind, der Bau ist.

Aber so machen wir es hier nicht. Ja, sondern es kann in einem Zustand abläufen mit verschiedenen Historie-Zusammenbauten.

Okay, wir wollen heute relativ gemütlich anfangen mit dem Thema Prozess-Äquivalenzen.

Ja, das ist ein Gehirn falsch verraten.

Zugänglich über

Offener Zugang

Dauer

01:33:54 Min

Aufnahmedatum

2015-04-30

Hochgeladen am

2019-04-23 13:35:46

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.

Anwenden Die Studierenden
  • ü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.

Analysieren Die Studierenden
  • leiten einfache Meta-Eigenschaften von Kalkülen her

  • wählen für die Läsung gegebener nebenläufiger Probleme geeignete Formalismen aus

Evaluieren (Beurteilen) Die Studierenden
  • vergleichen prozessalgebraische und logische Kalküle hinsichtlich Ausdrucksmächtigkeit und Berechenbarkeitseigenschaften

  • hinterfragen die Eignung eines Kalküls zur Lösung einer gegebenen Problemstellung

Lern- bzw. Methodenkompetenz Die Studierenden beherrschen das grundsätzliche Konzept des Beweises als hauptsächliche Methode des Erkenntnisgewinns in der theoretischen Informatik. Sie überblicken abstrakte Begriffsarchitekturen. Sozialkompetenz Die Studierenden lösen abstrakte Probleme in kollaborativer Gruppenarbeit.

 

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.

Einbetten
Wordpress FAU Plugin
iFrame
Teilen