157 lines
7.8 KiB
Markdown
157 lines
7.8 KiB
Markdown
The equivalence studied up to now is quite discriminating, in the sense that it distinguishes, for example, τ.P and τ.τ.P.
|
||
|
||
- If an external observer can count the number of non-observable actions (i.e., the τ’s), this distinction makes sense.
|
||
- If we assume that an observer cannot access any internal information of the system, then this distinction is not acceptable.
|
||
|
||
The idea of the new equivalence is to ignore (some) τ’s:
|
||
- a visible action must be replied to with the same action, possibly together with some internal actions
|
||
- an internal action must be replied to by a (possibly empty) sequence of internal actions.
|
||
|
||
We define the relation $\implies$ as:
|
||
|
||
$P \implies P'$ if and only if there exist $P_{0}, P_{1},\dots,P_{k}$ (for $k \geq 0$) such that $P=P_{0} \xrightarrow{\tau} P_{1} \xrightarrow{\tau}\dots\xrightarrow{\tau}Pk=P'$
|
||
|
||
relation $\xRightarrow{\hat{\alpha}}$:
|
||
- if $\alpha=\tau$ then $\xRightarrow{\hat{\alpha}}\triangleq\implies$
|
||
- otherwise $\xRightarrow{\hat{\alpha}}\triangleq\implies\xrightarrow{\alpha}\implies$
|
||
|
||
S is a weak simulation if and only if $$\forall(p, q) \in S \space \forall p \xrightarrow{\alpha} p' \exists q' \space s.t. \space q\xRightarrow{\hat{\alpha}}q' \space and \space (p', q') \in S$$
|
||
A relation S is called weak bisimulation if both $S$ and $S^{-1}$ are weak simulations.
|
||
We say that p and q are weakly bisimilar, written $p \approx q$, if there exists a weak bisimulation $S$ such that $(p, q) \in S$.
|
||
|
||
**Prop:**
|
||
$\approx$ is a
|
||
1. equivalence
|
||
2. congruence
|
||
3. weak bisimulation
|
||
4. $\sim \subset \approx$
|
||
|
||
#### Examples of weakly bisimilar processes
|
||
|
||
|
||
**Theorem:** given any process P and any sum M, N, then:
|
||
1. $P \approx \tau.{P}$
|
||
2. $M+N+\tau.N \approx M + \tau.N$
|
||
3. $M+\alpha.P+\alpha.(N+\tau.P) \approx M + \alpha.(N + \tau.P)$
|
||
|
||
*Proof:*
|
||
take the symmetric closure of the following relations, that can be easily shown to be weak simulations:
|
||
1. $S = \{ (P,\tau.P )\}\cup Id$
|
||
2. $S=\{ (M+N+\tau.N,M+\tau.N )\}\cup Id$
|
||
3. $S=\{ ((M+\alpha.P+\alpha.(N+\tau.P), M+\alpha.(N+\tau.P)) \} \cup Id$
|
||
|
||
#### Weak bisimilarity abstracts from any $\tau$
|
||
|
||
|
||
**There exists no weak bisimulation S that contains (P, Q).**
|
||
*Proof:*
|
||
By contr. suppose that a bisimulation exists
|
||
Since Q −τ→ b.0, there must exist a P’ such that P ⇒ P and (P,b.0) ∈ S The only P that satisfies P ⇒ P’ is P itself
|
||
hence it should be (P,b.0) ∈ S
|
||
|
||
Contradiction: P can perform a whereas b.0 cannot !!
|
||
Similarly, P/R and Q/R are NOT weakly bisimilar
|
||
|
||
### EXAMPLE: Factory
|
||
A factory can handle three kinds of works: easy (E), medium (M), difficult (D).
|
||
|
||
An activity of the factory consists in receiving in input a work (of any kind) and in producing in output a manufactured work.
|
||
|
||
The given specification of an activity is the following:
|
||
$$A\triangleq i_{E}.A'+i_{M}. A'+i_{D}.A'$$
|
||
$$A' \triangleq \bar{o}.A$$
|
||
where actions $i_{E}, i_{M}, i_{D}$ represents they input, and $\bar{o}$ represents the production of an output.
|
||
|
||
The factory is given by the parallel composition of two activities:
|
||
$$Factory \triangleq A|A$$
|
||
|
||
A possible implementation of this specification is obtained by having two workers that perform in parallel different kinds of work.
|
||
- For easy works, they don’t use any machinery
|
||
- For medium works, they can use either a special or a general machine
|
||
- For difficult works, they have to use the special machine.
|
||
There is only one special and only one general machine that the workers have to share.
|
||
|
||
|
||
|
||
where rg and rs are used to require the general/special machine, lg and ls are used to leave the general/special machine, and S and G implement a semaphore on the two different machines.
|
||
|
||
The resulting system is given by:
|
||
$$Workers \triangleq (W|W|G|S) \setminus_{\{rg,rs,lg,ls \}}$$
|
||
We now want to show that:
|
||
$$Factory \approx Workers$$
|
||
i.e., that the specification and the implementation of the factory behave the same (apart from internal actions).
|
||
|
||
Let N denote {rg,rs,lg,ls} and x,y ∊ {E,M,D}
|
||
We can prove that the following relation is a weak bisimulation:
|
||
|
||
|
||
This is a family of relations:
|
||
- 3 pairs of the second form (one for every x)
|
||
- 9 pairs of the fifth form (one for every x and y)
|
||
- 3 pairs of the sixth form
|
||
- 3 pairs of the seventh form
|
||
|
||
Furthermore, **we should also consider commutativity** of parallel in pairs of the second, third, fourth, sixth, seventh and eighth form.
|
||
|
||
Thus, R is actually made up of 1+6+2+2+9+6+6+2 = 34 pairs.
|
||
*exercise: write down the LTSs*
|
||
|
||
### EXAMPLE: Lottery
|
||
We want to model a lottery L where we can select any ball from a bag that contains n balls; after every extraction, the extracted ball is put back in the bag and the procedure is repeated.
|
||
|
||
The specification is: $$L \triangleq \tau.\bar{p_{1}}L+\tau.\bar{p_{2}}.L+\dots+\tau.\bar{p_{n}}.L$$
|
||
where $\tau$'s represent ball extractions and $\tilde{p_{i}}$ is the action that communicates with the value of the extracted ball. The LTS resulting from this specification is:
|
||
|
||
|
||
We now build a system with n components, one for every ball.
|
||
|
||
Every component can be in three states:
|
||
- A (waiting for being habilitated to extraction)
|
||
- B (habilitated, with the possibility of being extracted or of habilitating the next component)
|
||
- C (extracted, waiting to externally communicate its value and start the process again): $$A_{i}=a_{i}.B_{i} \quad B_{i}=\tau.C_{i}+\bar{a}_{(i \space mod \space n)+1}.A_{i} \quad C_{i}=\bar{p}_{i}.B_{i}$$
|
||
In pratica ogni volta o estrae di nuovo "se stesso" oppure "abilita" il componente successivo.
|
||
|
||
Implementation: $$Impl \triangleq (B_{1}|A_{2}|\dots|An)\setminus_{\{ a_{1}\dots an \}}$$
|
||
basically we need to have an initially habilitated process, which can be any (the first one in our case).
|
||
|
||
This will generate the LTS:
|
||
|
||
|
||
Is the implementation correct w.r.t. the given specification? Yes.
|
||
Weak bisimilarity $L \approx L_{i}$
|
||
$$R \triangleq \{ (L, L_{i})\space|\space 0<i\leq n\} \space \cup \space \{\bar{p_{i}}.L,L'_{i} \space | \space 0<i<n \}$$
|
||
is a weak bisimulation, trust me bro.
|
||
|
||
### EXAMPLE: Scheduler
|
||
We have a set of processes Pi (for 0 < i ≤ n) that must repeatedly perform at certain
|
||
task.
|
||
|
||
A scheduler has to guarantee that processes cyclically start their task, starting from P1.
|
||
Executions of different processes may overlap but the scheduler has to guarantee that
|
||
every process Pi completes his performance before starting another one (with the
|
||
same index i).
|
||
|
||
Every process Pi requires to start its task via action $a_i$ and signals to the scheduler its
|
||
termination via action $b_i$
|
||
- the scheduler has to guarantee that the a’s cyclically occur, starting with $a_1$, and, for every i, the ai’s must alternate with the bi’s, starting with $a_i$.
|
||
|
||
The specification is:
|
||
if $i \in X$ then:
|
||
$$S_{i,X}=\sum_{j \in X}b_{j}.S_{i,X-\{ j \}}$$
|
||
otherwise: $$S_{i,X}=a_{i}.S_{(i \space mod \space n)+1,X\cup \{ i \}} + \sum_{j \in X}b_{j}.S_{i,X-\{ j \}}$$
|
||
Starting config $S_{1,\{ \}}$
|
||
LTS for $n=2$:
|
||
|
||
|
||
We can try to implement the scheduler in the following way:
|
||
$$A_{i}=a_{i}.B_{i} \quad B_{i}=\bar{c}_{(i \space mod \space n)+1}.C_{i} \quad C_{i}=b_{i}.D_{i} \quad D_{i}=c_{i}.A_{i}$$
|
||
- actions of kind $\bar{c}$ are needed to signal to the next process (i.e., with the next index) that it can start working
|
||
- actions of kind $c$ are needed to receive from the previous process such a signal
|
||
- such actions implement a token ring; the token is initially given to the first process: $$S=(A_{1}|D_{2}|\dots|D_{n})\setminus _{\{ c_{1}\dots cn \}}$$
|
||
|
||
Is the implementation correct? Or, in other words, $S ≈ S_{1,∅}$?
|
||
No (ci sono rimasto male anche io).
|
||
|
||
Ma il fatto è che questo porta a questo LTS:
|
||
|
||
|