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

vault backup: 2025-04-14 15:25:00

Browse source
This commit is contained in:
Marco Realacci 2025-04-14 15:25:00 +02:00
parent fb2fac8387
commit 28e90444ab
16 changed files with 30 additions and 30 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -56,14 +56,14 @@ 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)
![](images/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 (ndeed, p0 –a–> p1 does not suffice, because p1 can perform a b and so cannot be bisimilar to q1).
#### Bisimulation is NOT isomorfism
![](../../Pasted%20image%2020250414084615.png)
![](images/Pasted%20image%2020250414084615.png)
$S = \{(p0,q0), (p1,q1), (p2,q1), (p0,q2)\}$
$S^{−1} = \{(q0,p0), (q1,p1), (q1,p2), (q2,p0)\}$
@ -101,10 +101,10 @@ So, (p', q') ∈ ∼
Let (p,q) ∈ S. Then, there exists a bisimulation that contains the pair (p, q); thus, (p, q) ∈ ∼.
## A syntax for LTSs
![](../../Pasted%20image%2020250414091521.png)
![](images/Pasted%20image%2020250414091521.png)
![](../../Pasted%20image%2020250414091528.png)
![](images/Pasted%20image%2020250414091528.png)
The only ingredients we used to write down an LTS are:
- sequential composition (of an action and a process)
@ -117,7 +117,7 @@ For every identifier (denoted with capital letters A,B,..), we shall assume a un
Let us denote with P{b1/x1 . . . bn/xn} the process obtained from P by replacing name xi with name bi, for every i = 1,..., n.
![](../../Pasted%20image%2020250414092202.png)
![](images/Pasted%20image%2020250414092202.png)
>[!def]
>The set of non-deterministic processes is given by the following grammar:
@ -133,7 +133,9 @@ We shall usually omit tail occurrences of ‘.0’ and, for example, simply writ
From the syntax to the LTS We have shown how it is possible, starting from an LTS, to generate a corresponding process
It is also possible the inverse translation and then the two formalisms do coincide; the rules that have to be used in this translation are:
![](../../Pasted%20image%2020250414093017.png)
examples
![](images/Pasted%20image%2020250414093017.png)
#### Examples
![](images/Pasted%20image%2020250414152221.png)
![](images/Pasted%20image%2020250414152234.png)
![](images/Pasted%20image%2020250414152247.png)
![](images/Pasted%20image%2020250414152300.png)