## 5 Comparative Study  
### Previous Research  
In previous research, we developed a methodology to specify smart IoT systems probabilistically with dTP-Calculus for their nondeterministic operational requirements and verify smart IoT systems with GTS logic for their safety and security requirements [11]. The previous research was motivated by the fact that the probabilistic process algebra for smart IoT systems is suitable to predict and control the nondeterministic behavior of the systems. However, the existing probabilistic process algebra, such as PCCS (Probabilistic Calculus of Communicating Systems), PACSR (Probabilistic Algebra of Communicating Shared Resources), PALOMA (Process Algebra for Located Markovian Agents), are based only on static probabilistic models of unconditional nondeterministic choice operations, resulting a lack of probabilistic analytical methods for nondeterministic probabilistic behavior of the systems as follows [27; 28; 29]:  
* PCCS only relies on discrete probability models;
* PACSR only relies on discrete probability models, similar to PCCS;
* PALOMA only focuses exponential probability distribution models. In other words, they are not suitable to predict and control the nondeterministic behavior of the systems based on the dynamic probabilistic models. In order to overcome the limitations, our previous research focused on developing a new process algebra, namely, dTP-Calculus, with dynamic probability property of a choice operation in order to specify the probabilistic operational requirements of smart IoT systems and to verify probabilistic safety and security requirements of the systems for the probabilistic operational requirements. In this way, the nondeterministic behavior of the systems can be both predicted and controlled probabilistically in dynamically incremental manners. The target characteristics of the research for dTP-Calculus were as follows:  
* Specification of nondeterministic behavior--the behavior of processes in a system is specified with probability so that the system become probabilistically predictable and controllable;
* Verification of probabilistic requirements--the safety and security requirements can be both analyzed and verified probabilistically;
* Control of nondeterministic behavior--the nondeterministic behavior of a system becomes controllable with dynamically controllable probability. This approach shows that dTP-Calculus is a very effective method to specify, analyze, verify and to evaluate the requirements of smart IoT systems in smart cities. Especially in case where the probabilistic operational requirements of the systems do not satisfy the probabilistic safety and security requirements of the systems, the probabilities for the operational requirements have to be modified to an arbitrary level so that the safety and security requirements can be satisfied probabilistically. \begin{table}
\begin{tabular}{c c c c c c} \hline \hline \multicolumn{2}{c}{**Requirements**} & \multicolumn{2}{c}{**Va Probabilities**} & \multicolumn{2}{c}{**System Probabilities**} & \multicolumn{2}{c}{**Verification Results**} \\ \hline \multirow{3}{*}{\(R^{Sc}\)} & \(R^{Sc}_{1}\) & 0.35 & 0.66 & O & Satisfied \\ \cline{2-6}  & \(R^{Sc}_{2}\) & 0.40 & 0.66 & O & Satisfied \\ \cline{2-6}  & \(R^{Sc}_{3}\) & 0.30 & 0.66 & O & Satisfied \\ \hline \multirow{3}{*}{\(R^{Sf}\)} & \(R^{Sf}_{1}\) & 0.50 & 0.65 & O & Satisfied \\ \cline{2-6}  & \(R^{Sf}_{2}\) & 0.30 & 0.66 & O & Satisfied \\ \cline{1-1} \cline{2-6}  & \(R^{Sf}_{3}\) & 0.20 & 0.66 & O & Satisfied \\ \hline \hline \end{tabular}
\end{table} 
Table 26: Validation results for the probabilistic requirements (multiple improvements). The previous research shows the feasibility of the approach to overcome the limitation, but the arbitrariness to find the degree of the probabilities to satisfy the requirements was not properly handled in the approach.