## 2 Theoretical Background
### dTP-Calculus
#### 2.1.2 dTP-Calculus Syntax  
Table 3 shows the full syntax of dTP-Calculus. Note that \(P,~{}Q,~{}and~{}E\) imply a process, respectively, and \(A\) indicates an action that a process performs. \begin{table}
\begin{tabular}{c c c c} \hline \hline
**Movements** & **Request** & **Permision** & **Results** \\ \hline _Get_ & \(B=get~{}A\) & \(A=B~{}get\) & \(B~{}get~{}A\) \\ \hline _Put_ & \(B=put~{}A\) & \(A=B~{}put\) & \(B~{}put~{}A\) \\ \hline \hline \end{tabular}
\end{table} 
Table 2: _Cont._ \begin{table}
\begin{tabular}{c c c c} \hline \hline
**Construct** & & **Name** & **Index** \\ \hline \hline \(P=~{}A\) & Action & (1) \\ \(|~{}A^{per,~{}n}_{t,no,d}|\) & Timed Action & (2) \\ \(|~{}P^{per,~{}n}_{[r,no,d]}\) & Timed Process & (3) \\ \(|~{}P_{(pri,n)}\) & Priority & (4) \\ \(|~{}P[Q]\) & Nesting & (5) \\ \(|~{}P(ch)\) & Channel & (6) \\ \(|~{}P+Q\) & Choice & (7) \\ \(|~{}P\{pc\}+_{F}Q\{pc\}\) & Probabilistic Choice & (8) \\ \(|~{}P\parallel Q\) & Parallel & (9) \\ \(|~{}P\backslash E\) & Exception & (10) \\ \(|~{}A.P\) & Sequence & (11) \\ \(F=~{}D\) & Discrete Distribution & (12) \\ \(|~{}N(\mu,\sigma)\) & Normal Distribution & (13) \\ \(|~{}Ex(\lambda)\) & Exponential & (14) \\ \(|~{}U(l,u)\) & Uniform Distribution & (15) \\ \(A=~{}\phi\) & Empty & (16) \\ \(|~{}ch(\overline{msg})\) & Send & (17) \\ \(|~{}ch(msg)\) & Receive & (18) \\ \(|~{}M\) & Movement & (19) \\ \(|~{}C\) & Control & (20) \\ \(M=~{}m^{pri}(k)~{}P\) & Movement Request & (21) \\ \(|~{}P~{}m(k)\) & Movement & (22) \\ \(m=~{}in\) & In Movement & (23) \\ \(|~{}get\) & Out Movement & (24) \\ \(|~{}out\) & Get Movement & (25) \\ \(|~{}put\) & Put Movement & (26) \\ \(C=~{}new~{}P\) & Create Process & (27) \\ \(|~{}kill~{}P\) & Kill Process & (28) \\ \(|~{}exit\) & Exit Process & (29) \\ \hline \hline \end{tabular}
\end{table} 
Table 3: dTP-Calculus syntax. It is one of the actions for \(A\) shown in (1) and (16) of the table: null (empty (16)), communication (send (17), receive (18)), movement ((19): (23)-(26)), control ((20): (27)-(29)). 1. [label=()] 2. Empty (16)--It represents a null action, where no action occurs. 3. Communication (send (17), receive (18))--It represents a synchronous communication between sender and receiver. In order to perform a communication between two processes, a set of synchronous actions, that is, send and receive, must occur in an overlapping time between them through a communication channel with the same type of message. 4. Movement (19)--It represents a movement interaction between a requesting process (21) and a permitting process (22). In order to perform a movement, the request action for the movement from the requesting process must be granted by the corresponding permitting action for the movement from the permitting process. There are a total of four types of such actions in dTP-Calculus--_In_ (23), _Out_ (24), _Get_ (25), and _Put_ (26). 5. Control (20)--It represents a set of control actions as follows: 1. [label=()] 2. _New_ (27)--It represents an action for a process to create its child process. The child process cannot have a priority that is higher than that of the parent. 3. _Kill_ (28)--It represents an action for a process to terminate another process. The former must have a priority that is higher than that of the latter. 4. _Exit_ (29)--It represents an action for a process to terminate itself. The child processes with less priorities will be terminated in depth-first order. If there is any child process with a higher priority, this action must be propagated until the child process terminates. 3. Timed Action (2)--It represents a time action, where the action is specified with the temporal properties [_r_, \(t\), \(e\), _d_], representing _ready time_, _timeout_, _execution time_, and _deadline_, respectively, and the recursion properties \(p\) and \(n\), representing the period and number of repetitions, respectively. 4. Timed Process (3)--This is the same notion for a process, instead of an action. 5. Priority (4)--It represents the priority that has been stated in the previous subsection.