Die beiden ACP_tau Ausdrücke

a ( tau * b + c) und a * (b + c)

sind verzweigungsbisimilar und initial verzweigungsbisimilar.

Berechnet man jedoch die Prozessgraphen sind diese nicht kongruent. Die initiale Verzweigungsbisimulation soll nun aber laut Satz 4.43 im Gegensatz zur Verzweigungsbisimulation eine Kongruenzrelation für ACP_tau sein.

Wo liegt hier der Denkfehler?

Vielen Dank im vorraus.

Berechnet man jedoch die Prozessgraphen sind diese nicht kongruent. Die initiale Verzweigungsbisimulation soll nun aber laut Satz 4.43 im Gegensatz zur Verzweigungsbisimulation eine Kongruenzrelation für ACP_tau sein.

Wo liegt hier der Denkfehler?

Eine Kongruenzrelation ist eine Äquivalenzrelation auf einer Struktur (hier: die Menge der Prozessterme mit ihren Operatoren), die mit den Operatoren verträglich ist - d.h. wenn Du äquivalente (hier: initial verzweigungsbisimilare) Terme s und s' sowie t und t' hast, dann ist auch beispielsweise s+t äquivalent zu s'+t' (siehe S. 137).

Satz 4.43 sagt also nicht direkt etwas darüber aus, wie die Prozessgraphen aussehen müssen. Mit der Kongruenz ist keine geometrische Kongruenz gemeint, die man direkt am Prozessgraphen sehen würde.


Oh, mal abgesehen davon sind a * ( tau * b + c) und a * (b + c) gar nicht verzweigungsbisimilar. Dies kannst Du entweder an Hand der Axiome auf S. 156 überprüfen (nur nachgestellte tau-Aktionen können ignoriert werden), oder Du siehst es am Prozessgraphen: Zunächst können beide Terme nur a ausführen, das ist in Ordnung. Wenn jetzt Term 1 die tau-Aktion ausführt, hat er schon die Entscheidung für b getroffen, während Term 2 sich immer noch entscheiden kann. (Auf S. 153 sind weitere solche nicht-äquivalente Prozessterme angegeben).