Selbst wenn es in jeder Richtung eine Simulation gibt, beziehen sich die Vorwärts- und Rückwärtssimulationen möglicherweise nicht auf die gleichen Sätze von Zuständen. Manchmal haben Sie eine Simulation in einer Richtung und eine Simulation R 2 in der anderen Richtung und zwei Zustände p 1 und q, die durch R 1, aber nicht durch R 2 oder eine andere Simulation in derselben Richtung zusammenhängen.R1R2p1qR1R2
Das kanonische Beispiel sind zwei Systeme, die die gleichen Spuren haben, aber unterschiedliche Entscheidungen treffen . Stellen Sie sich zwei Getränkeautomaten vor: Die erste (die böse) nimmt eine Münze ( c
) und entscheidet nicht deterministisch, ob sie eine Tasse Tee liefert ( t
). Die zweite Maschine (die Gute) nimmt eine Münze ( c
) und liefert eine Tasse Tee ( t
).
Die gute Maschine simuliert die böse Maschine: nimm . Alle ausgehenden Zustandsübergänge werden abgedeckt, einschließlich r (das keinen ausgehenden Übergang hat, also ist es trivial). Beachten Sie, wie die gute Maschine den Unterschied zwischen r und p vergisst .R1={(s,s′),(p,p′),(q,q′),(r,p′)}rrp
Die böse Maschine simuliert die gute Maschine: nimm . Der Zustand r wird von dieser Simulation nicht verwendet. Tatsächlich ist es für eine Simulation nicht möglich, r zu verwenden , da s ' auf einen Zustand abgebildet werden muss, ab dem eine Spur der Länge 2 möglich ist, also muss es s sein ; p ' muss auf einen Nachfolger von s abbildenR2={(s′,s),(p′,p),(q′,q)}rrs′2sp′ Mit dem Label c , also ist es p oder r , aber dieser Zustand muss auch eine mögliche Spur der Länge 1 haben , also muss es p sein ; und aus der gleichen Überlegungmuss q ' auf q abbilden, wobei keine Möglichkeit übrig bleibt, irgendeinen Zustand auf r abzubilden.s′cpr1pq′qr
Ein simuation in eine Richtung muss senden irgendwo. Eine Simulation in die andere Richtung muss r vermeiden . Daher gibt es keine Beziehung, die eine Simulation in beide Richtungen darstellt: Die Systeme sind nicht bisimilar.rr
Der Unterschied zwischen den beiden Maschinen besteht darin, dass die gute Maschine deterministisch ist und (unter der Annahme, dass sie lebhaft ist) immer Tee liefert, wenn Sie eine Münze einwerfen, während die böse Maschine aus einer Laune heraus die Münze nehmen kann, aber stecken bleibt und keinen Tee liefern kann.
Diese Art von Unterschied tritt häufig bei der Untersuchung von gleichzeitigen Systemen auf. Die Antwort von jmad zeigt einen CCS-Prozess mit diesem LTS.
Für weitere Informationen über Bisimulationen empfehle ich Davide Sangiorgis Notizen zu den Ursprüngen der Bisimulation und der Koinduktion . (Dies ist Übung 1, S. 29, und die Notizen verwenden dasselbe Beispiel.)
Gilles' Antwort ist sehr gut und formal, und in der Tat, wenn durch simuliert L T S 2 mit einer Relation R und L T S 2 wird simuliert durch L T S 1 mit dem inversen von R , dann R ist eine Bisimulation.LTS1 LTS2 R LTS2 LTS1 R R
quelle