## 2 Theoretical Background
### Probabilistic Equivalences
#### 2.2.2 Probabilistic System Equivalences  
System \(S\) is defined to be a set of processes, that is, \(S=\left\{P_{k}|1\leq k\leq n\right\}\). For example, System \(P_{1}B_{1}C_{1}\) is defined as follows in dTP-Calculus, and its system view is shown as well:  
\[ \begin{array}{l}P_{1}B_{1}C_{1}=P_{1}[R1\parallel R2]\parallel B_{1} \parallel C_{1}\\ P_{1}=\left(PB\Big{(}\overline{\mathit{Send}\ R1}\Big{)}.\mathit{put}\ R1. \mathit{put}\ R2+\ PB\Big{(}\overline{\mathit{Send}\ R2}\Big{)}.\mathit{put}\ R2. \mathit{put}\ R1\right).\mathit{exit};\\ B_{1}=\left(PB(\mathit{Send}\ R1).\mathit{get}\ R1.\mathit{get}\ R2+\ PB(\mathit{Send}\ R2).\mathit{get}\ R2. \mathit{get}\ R2).\\ (CB(\mathit{Send}\ R1).\mathit{put}\ R1.\mathit{put}\ R2+\ CB(\mathit{Send} \ R2).\mathit{put}\ R2.\mathit{put}\ R1).\mathit{exit};\\ C_{1}=\left(CB\Big{(}\overline{\mathit{Send}\ R1}\Big{)}.\mathit{get}\ R1. \mathit{get}\ R2+\ CB\Big{(}\overline{\mathit{Send}\ R2}\Big{)}.\mathit{get} \ R2.\mathit{get}\ R1\right).\mathit{exit};\\ R1=P_{1}\ put.B_{1}\ get.B_{1}put.C_{1}\ get.exit;\\ R2=P_{1}\ put.B_{1}\ get.B_{1}\ put.C_{1}\ get.exit.\end{array} \]  
If two systems \(S_{i}=\left\{P_{i,k}|1\leq k\leq n\right\}\) and \(S_{j}=\left\{P_{j,k}\big{|}1\leq k\leq n\right\}\) are identical, that is, \(P_{i,k}=P_{j,k}\) for \(1\leq k\leq n\), then two systems are _equivalent_, that is, \(S_{i}=S_{j}\). For example, System \(P_{2}B_{2}C_{2}\) is defined as follows, and it is identical to \(P_{1}B_{1}C_{1}\) in the above example: \(P_{1}B_{1}C_{1}=P_{2}B_{2}C_{2}\), since \(P_{1}=P_{2}\), \(B_{1}=B_{2}\), and \(C_{1}=C_{2}\). \[ \begin{array}{l}P_{2}B_{2}C_{2}=P_{2}[R1\parallel R2]\parallel B_{2} \parallel C_{2}\\ P_{2}=\left(PB\Big{(}\overline{\mathit{Send}\ R1}\Big{)}.\mathit{put}\ R1. \mathit{put}\ R2+PB\Big{(}\overline{\mathit{Send}\ R2}\Big{)}.\mathit{put}\ R2.\mathit{put}\ R1\right).\mathit{exit};\\ B_{2}=\left(PB(\mathit{Send}\ R1).\mathit{get}\ R1.\mathit{get}\ R2+PB( \mathit{Send}\ R2).\mathit{get}\ R2.\mathit{get}\ R2).\\ (CB(\mathit{Send}\ R1).\mathit{put}\ R1.\mathit{put}\ R2+CB(\mathit{Send} \ R2).\mathit{put}\ R2.\mathit{put}\ R1).\mathit{exit};\\ C_{2}=\left(CB\Big{(}\overline{\mathit{Send}\ R1}\Big{)}.\mathit{get}\ R1. \mathit{get}\ R2+CB\Big{(}\overline{\mathit{Send}\ R2}\Big{)}.\mathit{get} \ R2.\mathit{get}\ R1\right).\mathit{exit};\\ R1=P_{2}\ put.B_{2}\ get.B_{2}\ put.C_{2}\ get.exit;\\ R2=P_{2}\ put.B_{2}\ get.B_{2}\ put.C_{2}\ get.exit.\end{array} \]  
System \(S\) is defined to be _probabilistic_ if \(S=\left\{P_{k}|1\leq k\leq n\right\}\) and at least one of the processes \(P_{k}\) for \(1\leq k\leq n\) is probabilistic. For example, System \(P_{1}^{\prime}B_{1}^{\prime}C_{1}^{\prime}\) is defined below as a probabilistic system since Processes \(P_{1}^{\prime}\), \(B_{1}^{\prime}\) and \(C_{1}^{\prime}\) are defined as probabilistic processes. \[ \begin{array}{l}P_{1}^{\prime}B_{1}^{\prime}C_{1}^{\prime}=P_{1}^{\prime}[R1 \parallel R2]\parallel B_{1}^{\prime}\parallel C_{1}^{\prime}\\ P_{1}^{\prime}=\left(PB\Big{(}\overline{\mathit{Send}\ R1}\Big{)}\{0.6\}. \mathit{put}\ R1.\mathit{put}\ R2\ +_{D}\ PB\Big{(}\overline{\mathit{Send}\ R2}\Big{)}\{0.4\}.\mathit{put}\ R2. \mathit{put}\ R1\right).\mathit{exit};\\ B_{1}^{\prime}=\left(PB(\mathit{Send}\ R1)\{0.7\}.\mathit{get}\ R1.\mathit{get} \ R2\ +_{D}\ PB(\mathit{Send}\ R2)\{0.3\}.\mathit{get}\ R2.\mathit{get}\ R2).\\ (CB(\mathit{Send}\ R1)\{0.5\}.\mathit{put}\ R1.\mathit{put}\ R2\ +_{D}\ CB(\mathit{Send}\ R2)\{0.5\}. \mathit{put}\ R2.\mathit{put}\ R1).\mathit{exit};\\ C_{1}^{\prime}=\left(CB\Big{(}\overline{\mathit{Send}\ R1}\Big{)}\{0.8\}. \mathit{get}\ R1.\mathit{get}\ R2\ +_{D}CB\Big{(}\overline{\mathit{Send}\ R2}\Big{)}\{0.2\}.\mathit{get}\ R2. \mathit{get}\ R1\right).\mathit{exit};\\ R1=P_{1}^{\prime}\ put.B_{1}^{\prime}\ get.B_{1}^{\prime}\ put.C_{1}^{\prime}\ get.exit;\\ R2=P_{1}^{\prime}\ put.B_{1}^{\prime}\ get.B_{1}^{\prime}\ put.C_{1}^{\prime}\ get.exit. \end{array}