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

vault backup: 2025-04-14 08:29:56

Browse source
This commit is contained in:
Marco Realacci 2025-04-14 08:29:56 +02:00
parent a8ea324614
commit 16a89a0328
5 changed files with 70 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -55,3 +55,9 @@ q0 is simulated by p0; this is shown by the following simulation relation: $$S =
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).
**Remark:** for proving equivalence, it is NOT enough to find a simulation of p by q and a simulation of q by p
![](../../Pasted%20image%2020250414082824.png)
p0 is simulated by q0: $$S = {(p0, q0), (p1, q2), (p2, q3)}$$
q0 is simulated by p0: $$S′ ={(q0,p0),(q1,p1),(q2,p1),(q3,p2)}$$
However, p0 and q0 are not bisimilar: the transition q0 -> a -> q1 is not bisimulable by any transition from p0