## 2 Theoretical Background
### dTP-Calculus
#### 2.1.3 dTP-Calculus Semantics  
The semantics of dTP-Calculus are defined by transition rules, as follows:  
\[Transition=\frac{p_{1},\ldots,p_{k}}{q}(r) \tag{1}\]  
Note that \(p_{1},\ldots,p_{k}\) are premises and \(q\) is a conclusion under the side condition \(r\). It implies that the conclusion can be made from the premises under the condition. Table 4 shows the transition rules for all the operations defined by the syntax of dTP-Calculus. Brief descriptions of the rules are provided below. 1. Sequence (1)--Process \(P\) can perform its action without any premise or condition. 2. ChoiceL, ChoiceR (2)--Only the chosen process can perform its own action as a premise without any condition. 3. Probability Choice (3)--Only the chosen process can perform its own action probabilistically as a premise without any condition under a specified probability distribution. 4. ParIL, ParIR (4)--Each process is independent and runs concurrently without interference as a premise without any condition. 5. Parcom (5)--Synchronous communication occurs between two processes, \(P\) and \(Q\). As a result of the communication interaction, each process makes its respective transition, as shown in the premises, without any side condition. 6. NestingO, NestingI (6)--Both nesting and nested processes can perform their own transitions independently, as defined in the premises without any side condition. 7. NestingCom (7)--A synchronous communication interaction is possible between the nesting and nested processes. 8. In (8), Out (9), Get (10), Put (11)--Each movement is defined as a _synchronous_ interaction between a requesting process and a permitting process for the action. As stated, _In_ and _Out_ are for autonomous movements and _Get_ and _Put_ are for heteronomous movements. Note that the inclusion relations are modified as a result of the movements. 9. InP (12), OutP (13), GetP (14), PutP (15)--Each movement is defined as an _asynchronous_ interaction between a requesting process and a permitting process for the action. The difference is that if the request process has a higher priority, it does not have to wait for permission from the permitting process, but it can move asynchronously without permission. 10. TickTimeR (16)--As time ticks with \(\rhd\), the ready time \(r\) and deadline \(d\) are elapsed by the ticks \(\rhd_{t}\). 11. TickTimeTO (17)--As time ticks idly with \(\rhd_{t}\), timeout \(to\) and deadline \(d\) are elapsed by the ticks \(\rhd_{t}\). 12. TickTimeEnd (18)--An action is completed after the execution time \(e\). 13. TickTimeSyncE (19)--As time ticks for the synchronous interaction with \(\rhd_{t}\), the execution time \(e\) and deadline \(d\) are elapsed by the ticks \(\rhd_{t}\). 14. TickTimeAsyncE (20)--As time ticks for the asynchronous interaction with \(\rhd_{t}\), the execution time \(e\) and deadline \(d\) are elapsed by the ticks \(\rhd_{t}\) after ready time \(r\). 15. Timeout (21)--When timeout \(to\) becomes zero, a fault occurs. Exception handler \(P\) should be activated. 16. Deadline (22)--When deadline \(d\) becomes zero, a fault occurs. Exception handler \(P\) should be activated. 17. Period (23)--After recursion, repetition \(n\) is decremented by one. 18. PeriodEnd (24)--If repetition \(n\) becomes zero, the recursion ends.