vault backup: 2025-04-14 09:09:56

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) ∈ ∼.