An n-ary semaphore S(n)(p,v) is a process used to ensure that there are no more than n istances of the same activity concurrently in execution. An activity is started by action p and is terminated by action v.

The specification of a unary semaphore is the following:
$$S^{(1)} \triangleq p \cdot S_{1}^{(1)}$$
$$S_{1}^{(1)} \triangleq p \cdot S_{1}^{(1)}$$
The specification of a binary semaphore is the following:
$$S_{}^{(2)} \triangleq p \cdot S_{1}^{(2)}$$
$$S_{1}^{(2)} \triangleq p \cdot S_{1}^{(2)}+v\cdot S^{(2)}$$
$$S_{2}^{(2)} \triangleq v \cdot S_{1}^{(2)}$$

If we consider S(2) as the specification of the expected behavior of a binary semaphore and S(1) | S(1) as its concrete implementation, we can show that $$S^{(1)}|S^{(1)} \space \textasciitilde \space S^{2}$$
This means that the implementation and the specification do coincide. To show this equivalence, it suffices to show that following relation is a bisimulation:
![](../../Pasted%20image%2020250415082906.png)

## Restrictions
**Proposition:** $a.P \textbackslash a ∼ 0$
*Proof:*
- S = {(a.P\a , 0)} is a bisimulation

Which challenges can (a.P)\a have?
- a.P can only perform a (and become P)
- however, because of restriction, a.P\a is stuck

 No challenge from a.P\a, nor from 0 -> bisimilar!

**Proposition:** $\bar{a}.P \textbackslash a ∼ 0$
*Proof is similar.*

## Idempotency of Sum
**Proposition:** $α.P+α.P+M ∼ α.P+M$
*Proof:*
$$S = \{ (α.P+α.P+M , α.P+M) \}$$
Is it a bisimulation?
NO: the problem is that, for example:
- α.P+α.P+M –α–> P
- α.P+M –α–> P
- BUT (P,P) in general does NOT belong to S!

So we can try with $$S = \{ (α.P+α.P+M , α.P+M) \} ∪ \{(P,P)\}$$
But it is not yet a bisimulation. 
P –β–> P’ (challenge and reply), but we don't have (P', P') in S.

So let's try with: $$S = \{ (α.P+α.P+M , α.P+M) \} ∪ Id$$
Let's go!