vault backup: 2025-04-08 09:46:02

Concurrent Systems/notes/11 - LTSs and Bisimulation.md

@@ -41,3 +41,11 @@ Intuitively, two states are equivalent if they can perform the same actions that
 ![](../../Pasted%20image%2020250408093840.png)
 P0 and Q0 are different because, after an a, the former can decide to do b or c, whereas the latter must decide this before performing a.
 
+Let (Q,T) be an LTS.
+A binary relation S ⊆ Q×Q is a simulation if and only if
+		∀(p,q) ∈ S∀p –a–> p′∃q –a–> q′ s.t. (p′,q′) ∈ S
+
+We say that p is simulated by q if there exists a simulation S such that $$(p,q) ∈ S$$
+We say that S is a bisimulation if both S and S−1 are simulations (where $$S^{-1} = \{(p,q) : (q,p) ∈ S\}$$)
+
+Two states q and p are bisimulation equivalent (or, simply, bisimilar) if there exists a bisimulation S such that (p, q) ∈ S; we shall then write p ∼ q.