## 2 Theoretical Background
### Probabilistic Equivalences
#### 2.2.1 Probabilistic Process Equivalences  
Process \(P\) is defined as \(P=(S,T)\), where \(S\), \(T\) are two sets of states and transitions between two states, represented by \(S=\left\{s_{1},\cdots,s_{f_{s}}\right\}\) and \(T=\left\{t_{1},\cdots,t_{f_{t}}\right\}\), where each \(t=\left\langle s_{i},s_{j}\right\rangle\) and \(s_{i},s_{j}\in S\). For example, Process \(R\) is defined as follows in dTP-Calculus. \(R\) is defined as two sets of states and transitions between states. Note that the diagram for the process is shown for this example only since the diagram is obvious and will be shown in the ITS (In-The-Small) model of the SAVE (Specification, Analysis, Verification, Evaluation) tool in the following implementation section. \begin{table}
\begin{tabular}{c c c} \hline
**Type** & **Rules** & **Index** \\ \hline Choice1 & \(P+P=P\) & (1) \\ \hline Choice2 & \(P+Q=Q+P\) & (2) \\ \hline Choice3 & \((P+Q)+R=P+(Q+R)\) & (3) \\ \hline Parallel1 & \(P|\phi=P\) & (4) \\ \hline Parallel2 & \(P|Q=Q|P\) & (5) \\ \hline Parallel3 & \((P|Q)|R=P|(Q|R)\) & (6) \\ \hline Nesting1 & \(P|\phi|=P\) & (7) \\ \hline Nesting2 & \(R[P]+R[Q]=R[P+Q]\) & (8) \\ \hline Distributive1 & \(P|(Q+R)=(P|Q)+(P|R)\) & (9) \\ \hline Distributive2 & \((a_{1}+a_{2}).P=a_{1}.P+a_{2}.P\) & (10) \\ \hline \end{tabular}
\end{table} 
Table 5: dTP-Calculus rules. If two processes \(P_{i}\) and \(P_{j}\) are identical, that is, \(P_{i}=(S_{i},T_{i})\), \(P_{j}=(S_{j},T_{j})\), \(S_{i}=S_{j}\), and \(T_{i}=T_{j}\), then two processes are _equivalent_, that is, \(P_{i}=P_{j}\). For example, Processes \(R_{1}\) and \(R_{2}\) are defined as follows in dTP-Calculus and the two processes are identical, that is, \(R_{1}=R_{2}\):  
\[ \begin{array}{l}R1=P\ put.B\ get.B\ put.C\ get.exit;\\ R2=P\ put.B\ get.B\ put.C\ get.exit.\end{array} \]  
Process \(P\) is defined to be _probabilistic_, if Process \(P=(S,T^{p})\), where \(S\) and \(T^{p}\) are two sets of states and transitions between two states, represented by \(S=\left\{s_{1},\cdots,s_{f_{s}}\right\}\) and \(T^{p}=\left\{t_{1}^{p},\cdots,t_{f_{s}}^{p}\right\}\), where, for each \(t_{i}^{p}=\left\langle s_{j},s_{k}\right\rangle^{p}\) and \(s_{i},s_{j}\in S\), \(p\) is the probability of the successful transition between \(s_{i}\) and \(s_{j}\). For example, Process \(P\) is defined as follows in dTP-Calculus and \(R\) is defined as two sets of states and transitions between states, especially a choice operation with probability:  
\[P=\left(PB\left(\overline{\mathit{Send}\ R1}\right)\{0.5\}.put\ R1.put\ R2+ \mathit{{}_{D}PB}\left(\overline{\mathit{Send}\ R2}\right)\{0.5\}.put\ R2. put\ R1\right).exit;\]  
If two probabilistic processes \(P_{i}\) and \(P_{j}\) are probabilistically identical, that is, \(P_{i}=(S_{i},T_{i}^{p})\), \(P_{j}=(S_{j},T_{j}^{p})\), \(S_{i}=S_{j}\), and \(T_{i}^{p}=T_{j}^{p}\), then the two processes are _probabilistically equivalent_, that is, \(P_{i}\sim P_{j}\). For example, Processes \(P_{1}\) and \(P_{2}\) are defined as follows in dTP-Calculus and the two processes are probabilistically identical, that is, \(P_{1}\sim P_{2}\), especially with respect to the choice operations with the same probabilities:  
\[ \begin{array}{l}P1=\left(PB\left(\overline{\mathit{Send}\ R1}\right)\{0.5 \}.put\ R1.put\ R2+\mathit{{}_{D1}PB}\left(\overline{\mathit{Send}\ R2} \right)\{0.5\}.put\ R2.put\ R1\right).exit;\\ P2=\left(PB\left(\overline{\mathit{Send}\ R1}\right)\{0.5\}.put\ R1.put\ R2+ \mathit{{}_{D2}PB}\left(\overline{\mathit{Send}\ R2}\right)\{0.5\}.put\ R2. put\ R1\right).exit.\end{array} \]  
If the difference between two probabilities \(p_{i}\) and \(p_{j}\) are within \(\Delta^{+_{D}}\), then the two processes are within the _permissible probability_ range, that is, \(P_{i}\Delta^{+_{D}}P_{j}\). For example, Processes \(P_{1}\) and \(P_{2}\) are identical, but not probabilistic, and the permissible range for \(P_{1}\) and \(P_{2}\) is defined as follows: \(P_{1}\left([0.5+_{D_{1}}0.5]\right)\Delta^{<0.4>}P_{2}\left([0.9+_{D_{2}}0.1]\right).\)  
\[