9 - Kommunikation und Parallele Prozesse [ID:10681]
50 von 481 angezeigt

So weit hatte ich natürlich und das gar nicht zu Ende gedacht, dass man über diese Kopien da rein kann.

Moment, also wie war es genau gestellt? Ich habe jetzt das Q gleich A, B, Q, das sind praktisch 1, 2, das sind gerade drei Zustände.

Also immer 2 auf N plus 1, im Fall für N größer bleibt 1, im Fall N gleich 0 halt 1.

Also 1 plus 2 hat N, 2 mit 1 plus 2. Der eine für den Namen Q, also nach den Regeln, Q und A, B, Q sind ja zwei verschiedene Zustände.

Das ist schon ein bisschen Haarspreiterei. So weit hatte ich noch gar nicht gedacht, aber das ist streng vorgetrieben.

Und dann muss man sich ja nochmal überlegen, wie das eigentlich mit dem frei fliegenden Term dann ist, parallel zu sich selbst.

Also eigentlich sind wir dann bei 2 plus und so weiter, dass die ja auch nochmal einen Namen kriegen.

Ja, aber auch nicht weiß, zumal man ja auch jetzt irgendwie, es ist leicht problematisch, wenn man dann erstmal einfach nur die Striche so hinstreibt,

weil man ja nicht weiß, wie ist da die Assoziativität bei dieser Parallelkomposition. Also das ist natürlich...

Ja, darunter ist dann, das kann man ja klammern, wie man will, da ist dann die Anzahl Zuständen, die man kriegt, die bleibt darunter immer in Variante.

Und darunter auch.

Gut, dann fangen wir einfach mal an.

So, das ist nicht ein möglicher Nöner, der so nicht bloß so tief zu kaffeehaut ist.

Das klingt schon, das klingt nicht so wie eine Kaffeemaschine, sondern ein Kaffee.

Das ist dann ein Computer-Scientist, der da sitzt und die ganze Zeit publiziert, der mit Kaffeemaschine direkt daneben steht.

Der kriegt man dann nicht mit von.

Ja, das heißt also, wir fangen an mit Aufgabe 3.8. Wir können das einfach 3 umwandlern lassen, oder es kann sich hier auch vordrängeln.

Die 3 ist nicht so hübsch. Also nicht die 3, ach so, ich wollte nicht mit der 3 anfangen, aber mit der 1 anfangen natürlich.

1, Nummer 1.

Also um die Situation ein bisschen knapp zu halten, mache ich auch wieder das mit dem, dass ich einfach für einen Prozess,

der sich durch eine Ableitung mit Aktionen ergibt, dass ich einfach so einen Strich dransetze an den Namen.

Das heißt, dann habe ich halt immer User, User Strich, User 2 Strich und ich mache einfach U und S für User und Send.

Und genau, wenn wir jetzt dann, dann fangen wir einfach mit dem, mit diesem Utex 1 an und schauen, was können wir da, was können wir dafür herleiten.

Dann ist die einzige Regel, die erstmal matcht, halt die, wie heißt sie, die Con, also Constant. Das heißt, wir haben hier U, S ohne L,

wobei L halt diese ausgeschlossene Menge ist mit PV. Gut, was matcht darauf? Darauf matcht jetzt nur Restriktion.

Das heißt, wir haben hier U, S.

Ich wollte mal einen betrobischen Tipp geben, man soll ja auch fürs Leben lernen. Ich konzentriere mich auch mal sehr konzentrierendes zu machen und zwar, man trennt Schreiben und Sprechen.

Deswegen, weil man ja das Publikum ansprechen will und nicht in der Lage ist, wenn man nach vorne spricht, nach hinten zu schreiben.

Ich würde immer vorschlagen, erst schreiben, dann erläutern, was man gerade geschrieben hat und dann muss man sich natürlich überlegen, was für Etappen man schreiben kann.

Gut, wenn wir uns jetzt das anschauen, dann matchen da halt die drei Regeln Con 1 bis Con 3 drauf.

Aber wenn ich mir jetzt hier anschaue, ich will ja was hier verheirleiten und hier sind P und V ausgeschlossen und mit Con 1 und Con 2 kriege ich nur Übergänge mit P und V.

Deswegen schaue ich mir nur Con 3 an.

Dann bekommen wir hier eben diese Silent Transition und das setzt sich dann nach unten fort.

Okay.

Gut, das war jetzt der einzige, den wir hier gefunden haben. Das heißt, wir machen mit dem hier weiter.

Ja, wie ausführlich soll ich das jetzt machen? Es wiederholt sich dann allmählich.

Dann sind wir hier bei dem hier und suchen einen Übergang, den er machen kann. Dann matcht halt auch wieder nur Restriktion.

Und hier matcht jetzt eben Con 3 nicht, weil S Strich kann nur mit V einen Übergang machen und U Strich nur mit Enter.

Und Con 2 kann ich jetzt auch wieder vernachlässigen, weil der dann diese Restriktion nicht überlebt.

Insgesamt bekommen wir dann den hier und das ist der einzige, der möglich ist.

Gut.

Und wenn ich jetzt von dem hier weiter mache, dann bekomme ich auch wieder nur einen möglichen und zwar sieht der so aus. Ich gehe von diesem hier mit Exit.

Und das ist bis auf Unbenennung genau diese Herleitung.

Genau und wenn ich den hier herleiten will, dann sieht die Herleitung genauso wie das hier aus.

Insgesamt das LTS, was man bekommt, ist dann eben...

Wie folgt?

Also wir haben hier fünf Zustände in unserem LTS.

Dann kommt also als nächstes... das hier ist ja noch nicht die tatsächliche Nutex Situation, weil es nur einen Userprozess gibt.

Dann müssen wir hier jetzt rein.

Also die Angabe ist glaube ich einfach nur, dass du den Nutex 2 hast, der im Prinzip das da ist, nur dass innerhalb der inneren Klammer nochmal eine Klammer drumrum kommt mit einem User 2.

Zugänglich über

Offener Zugang

Dauer

01:15:10 Min

Aufnahmedatum

2014-05-15

Hochgeladen am

2019-04-21 09:19:03

Sprache

de-DE

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