marcorealacci/master-degree-notes
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

vault backup: 2025-04-14 11:59:53

Browse source
This commit is contained in:
Marco Realacci 2025-04-14 11:59:53 +02:00
parent efea5d2d41
commit ad90da6608
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
Concurrent Systems/notes/11 - LTSs and Bisimulation.md
View file

@ -90,7 +90,7 @@ where S1 and S2 are bisimulations, then we have to show that S is a bisimulation
*Proof:* *Proof:*
The proof is done by showing that ∼ is a simulation. 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) ∈∼ Let us fix a pair (p,q) ∈∼
Bisimilarity of p and q implies the existence of a bisimulation S such that (p,q) ∈ S. 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. Hence, for every transition p –a–> p′, there exists a transition q –a–> q′ such that (p′, q′) ∈ S.