Kommunikation und Parallele Prozesse SS15

Fragen Antworten

• wie sehen die Formeln aus? Gramatik aufgestellt
• wie verhalten sich diese Formeln der Semantik nach? Semantik der Formeln erklärt
• Prozessdefinition für Puffer mit Kapazität 1 B1 B1 = ein.aus.Buf
• Prozessdefinition für Puffer mit Kapazität 2 B2 B2 = ein.B2' B2'=aus.B2 + ein.B2 B2=aus.B2'
• Wie kann man einen Puffer mit Kapazität 2 β2 unter zu Hilfenahme der Def. von B1 definieren β2 = B1|B1
• Sind diese Prozesse äquivalent? kommt unter Umständen auf die Äquivalenz an, Äquivalenzen aufgelistet
• Wie verhalten sich Traceäquivalenz und Bisimularität zueinander? Bisimilarität ⊆ Traceäquivalenz
• Erst Bisim. prüfen, vlt ergibt sich dann ja Traceäquivalenz Bisimulation aufgestellt
• Wie lautet der Satz von Knaster-Tarsky? Satz erklärt
• Was haben Fixpunkte mit der Vorlesung zu tun? Fixpunktcharakterisierung der Bisim. erklärt
• Wie war das mit der logischen Äquivalenz? Bzgl. welcher Lgoik? HML
• Unterschied zwischen HML und propositionaler Logik? Modaloperatoren
• Wie verhält sich [α]φ? q erfüllt [α]φ gdw. f.a q(→α)q' : q' erfüllt φ
• Wie verhalten sich Bisimilarität und logische Äquivalenz zueinander? Fallen zusammen bei endlicher Verzweigung
• Was bleibt von dieser Beziehung ohne endliche Verzweigung? Bisimilarität impliziert log. Äquivalenz, weil log. Äquvalenz mit Vereinigung der beschränkten Bisimilaritäten zusammenfällt(Anmerkung des Prüfers: Nur bei endlicher Zahl der Aktionen)