diff --git a/Concurrent Systems/notes/11 - LTSs and Bisimulation.md b/Concurrent Systems/notes/11 - LTSs and Bisimulation.md index 64ed4d2..7eec1ba 100644 --- a/Concurrent Systems/notes/11 - LTSs and Bisimulation.md +++ b/Concurrent Systems/notes/11 - LTSs and Bisimulation.md @@ -90,7 +90,7 @@ where S1 and S2 are bisimulations, then we have to show that S is a bisimulation *Proof:* 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′)∈∼$$ +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.