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.
Presenters
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.
-
ü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.