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

vault backup: 2025-04-09 17:50:41

Browse source
This commit is contained in:
Marco Realacci 2025-04-09 17:50:41 +02:00
parent f0332f2b7b
commit 5050c82097
7 changed files with 16 additions and 37 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -12,13 +12,13 @@ Automata Behaviour: language equivalence
>[!note] Language equivalence
>M1 and M2 are *language equivalent* if and only if L(M1)=L(M2)
![](../../Pasted%20image%2020250408091924.png)
![](images/Pasted%20image%2020250408091924.png)
By considering the starting states as also final, they both generate the same language, i.e.:
$$(20.(tea + 20.coffee))∗ = (20.tea + 20.20.coffee)∗$$
But, do they behave the same from the point of view of an external observer??
![](../../Pasted%20image%2020250408092853.png)
![](images/Pasted%20image%2020250408092853.png)
The essence of the difference is WHEN the decision to branch is taken
- language equivalence gets rid of branching points
- it is too coarse for our purposes!
@ -38,7 +38,7 @@ We shall usually write s –a–> s′ instead of ⟨s,a,s′⟩ ∈ T.
### Bisimulation
Intuitively, two states are equivalent if they can perform the same actions that lead them in states where this property still holds
![](../../Pasted%20image%2020250408093840.png)
![](images/Pasted%20image%2020250408093840.png)
P0 and Q0 are different because, after an a, the former can decide to do b or c, whereas the latter must decide this before performing a.
Let (Q,T) be an LTS.
@ -50,7 +50,7 @@ We say that S is a bisimulation if both S and S−1 are simulations (where $$S^{
Two states q and p are bisimulation equivalent (or, simply, bisimilar) if there exists a bisimulation S such that (p, q) ∈ S; we shall then write p ∼ q.
![](../../Pasted%20image%2020250408094749.png)
![](images/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)\}$$
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).