FB18 - Das Forum für Informatik

fb18.de / Bachelorstudieng / PM Formale Informatik

FGI 2, Zettel 8, Aufgabe 8.1: Verzweigungsbisimulation

FGI 2, Zettel 8, Aufgabe 8.1: Verzweigungsbisimulation 2007-12-17 17:26
Dive
Hi Leute,
ich hab ein Problem mit Aufgabe 8.1.2/3/4:
Müssen wir für s bzw. t die verschiedenen Fälle s=x+y, s=xy, s=x||y,… betrachten und wenn ja, wieso? Macht es einen Unterschied, da wir ja nur das (Tau) auf der rechten Seite ausführen müssen um zu zeigen, dass die Terme verzweigungsbisimilar sind. In allen Fällen könnten wir ja gleichermaßen nach Regel 1 und 2 aus der Definition 4.37, Skript S. 161 vorgehen, ohne s und t genauer zu spezifizieren (wird ja im Skript mit p und q auch nicht gemacht).

Grüße

RE: FGI 2, Zettel 8, Aufgabe 8.1: Verzweigungsbisimulation 2007-12-18 09:12
Lehrkraft
Nein, man muss die verschiedenen Möglichkeiten, wie s bzw. t zusammengesetzt sein kann, nicht alle einzeln ausdifferenzieren. Für die Betrachtung im Rahmen dieser Aufgabe reicht es zu wissen, dass in dem komplexen Term s mindestens eine Aktion v ausgeführt werden kann, die dann zu einem Prozessterm s' führt (für t analog). Die verschiedenen in s tatsächlich möglichen Aktionen, deren mögliche Zusammensetzungen durch die bekannten Operatoren und die entsprechend vielfältigen Folgeterme lassen sich so zusammenfassen, weil sie auf die Anwendung der Regeln, die die Verzweigungsbisimulation definieren, keine Auswirkung haben. Lediglich der Fall, dass s mit einer Aktion direkt terminieren könnte, beeinflusst womöglich die Anwendung der Regeln 3. und 4. und sollte daher extra betrachtet werden (es stellt sich dann aber heraus, dass auch dort kein abweichendes Verhalten zu beobachten ist).

Es reicht aber nicht, nur die Verzweigungsbisimilarität ausgehend von der Aktion [latex]\tau[/latex] im zweiten vorgegebenen Term aus zu überprüfen. Zu jeder der auf beiden Seiten möglichen Aktionen (unter Berücksichtigung der eben erwähnten Zusammenfassung) muss die Anwendbarkeit der Regeln überprüft werden. Das ist besonders bei den Aufgaben 8.2.3 und 8.2.4 relevant, wo mehr Termstruktur (um s und t herum) bekannt ist. Am besten skizziert man dafür den Anfang des Prozessgraphen, damit man keine Variante übersieht.