diff --git a/Concurrent Systems/notes/11 - LTSs and Bisimulation.md b/Concurrent Systems/notes/11 - LTSs and Bisimulation.md index c6a75bc..41fed35 100644 --- a/Concurrent Systems/notes/11 - LTSs and Bisimulation.md +++ b/Concurrent Systems/notes/11 - LTSs and Bisimulation.md @@ -91,4 +91,12 @@ where S1 and S2 are bisimulations, then we have to show that S is a bisimulation The proof is done by showing that ∼ is a simulation. By definition of similarity, we have to show that $$∀(p,q)∈∼ ∀p –a–> p′ ∃q –a–> q′ s.t.(p′,q′)∈∼$$ +Let us fix a pair (p,q) ∈∼ +Bisimilarity of p and q implies the existence of a bisimulation S such that (p,q) ∈ S. +Hence, for every transition p –a–> p′, there exists a transition q –a–> q′ such that (p′, q′) ∈ S. +So, (p', q') ∈ ∼ + +**Theorem:** For every bisimulation S, it holds that S ⊆ ∼. +*Proof:* +Let (p,q) ∈ S. Then, there exists a bisimulation that contains the pair (p, q); thus, (p, q) ∈ ∼.