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

vault backup: 2025-04-08 10:51:20

Browse source
This commit is contained in:
Marco Realacci 2025-04-08 10:51:20 +02:00
parent 8b8414f6ef
commit f0332f2b7b
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -53,4 +53,5 @@ Two states q and p are bisimulation equivalent (or, simply, bisimilar) if there
![](../../Pasted%20image%2020250408094749.png) ![](../../Pasted%20image%2020250408094749.png)
q0 is simulated by p0; this is shown by the following simulation relation: $$S = \{(q0,p0), (q1,p1), (q2,p1), (q3,p2), (q4,p3)\}$$ q0 is simulated by p0; this is shown by the following simulation relation: $$S = \{(q0,p0), (q1,p1), (q2,p1), (q3,p2), (q4,p3)\}$$
To let p0 be simulated by q0, we should have that p1 is simulated by q1 or q2. To let p0 be simulated by q0, we should have that p1 is simulated by q1 or q2.
If S contained one among (p1,q1) or (p1,q2), then it would not be a simulation: indeed, p1 can perform both a c (whereas q1 cannot) and a b (whereas q2 cannot) If S contained one among (p1,q1) or (p1,q2), then it would not be a simulation: indeed, p1 can perform both a c (whereas q1 cannot) and a b (whereas q2 cannot).