## 2 Literature Review
### Limitations on Current Techniques  
The prospective verification analysis is limited in extent by the potential user machine interaction model to establish the correct user behavior. Works such as these researcher [18] express the user machine interaction with an account of a formal description and they are not well reinforce the relation with user machine interaction. Correspondingly, they [20] established awareness of the link to unobservable and uncontrollable events for user but it had some weak points. Further, they [5] investigated and analyzed the human machine interaction through a formal model representation using predicate and proposition. All the provided practices do not have the non-deterministic behavior or choices lie at any state.  
Moreover, currently we cannot generate the interface when the system has more than one user and machine all of which are interlinked with the supervisor as we described the limitation in Table 1. We are also interested to investigate the supervisor interface. \((\sum_{M}^{com})_{choice=1}\), \((\sum_{M}^{obs})\) and \((\sum_{M}^{int})\) have already evaluated in [19] the user domain while the supervisor's perspective still needs to be considered. Further, \((\sum_{M}^{com})_{choice>1}\) and \((\sum_{M}^{com^{\prime}})_{choice>1}\) events are still not being investigated by scientists.  
\begin{table}
\begin{tabular}{c c c c c c c c c} \hline \hline
**\#User and Machine** & **User** & **Choice** & **Event** & **Controllability** & **Observability** & **Supervisor Model** & **Supervisor Machine** & **Publication** \\ \hline Only 1 & \(M1\)\({}^{\frac{10}{33}}_{\text{M}}\) L1 & 1 & \((\sum_{\text{M}}^{\text{out}})_{\text{,chiter}=1}\) & Yes & Yes & No & No & [26] \\  & User operation & & & & & & & \\ \hline Only 1 & \(L2\)\({}^{\frac{10}{33}}_{\text{M}}\) M1 & - & \(\sum_{\text{M}}^{\text{out}}\) & No & Yes & No & No & [20] \\  & Machine operation & & & & & & & \\ \hline \multirow{6}{*}{Only 1} & \(L2\)\({}^{\frac{10}{33}}_{\text{M}}\) M2 & \multirow{6}{*}{-} & \(\sum_{\text{M}}^{\text{out}}\) & No & No & No & No & [20, 26] \\  & \(M2\)\({}^{\frac{10}{33}}_{\text{M}}\) M3 & - & \(\sum_{\text{M}}^{\text{out}}\) & No & No & No & No & [20, 26] \\  & \(M3\)\({}^{\frac{10}{33}}_{\text{M}}\) M2 & \multirow{6}{*}{-} & \(\sum_{\text{M}}^{\text{out}}\) & No & No & No & No & [20, 26] \\  & Machine operation & & & & & & & \\ \hline \multirow{6}{*}{\(>\)1 can be used} & \(L2\)\({}^{\frac{10}{33}}_{\text{M}}\) M1 & \multirow{6}{*}{\(>\)1} & \multirow{6}{*}{\(\sum_{\text{M}}^{\text{out}}\)} & \multirow{6}{*}{Yes} & Yes & No & No & *** \\  & \(L2\)\({}^{\frac{10}{33}}_{\text{M}}\) M2 & & & & & & & \\  & User operation & & & & & & & \\ \hline \multirow{6}{*}{\(>\)1 can be used} & \(N_{00}\)\({}^{\frac{10}{33}}_{\text{M}}\) L1 & 1 ** & \((\sum_{\text{M}}^{\text{out}})_{\text{,chiter}=1}\) & Yes & Yes & Yes & Yes & *** \\  & Supervisor operation & & & & & & & \\ \hline \hline \end{tabular} Note. – Previously model can support only one user and machine so we used \(\eta_{1}\) = representation. Now, we changed the representation because of more than one user and machine from \(\eta_{1}\) + to \(\eta_{1}\) (user or machine = 1, operation = 1). “ Supervisor will deliver the instruction to user for proceeding the user operations. Also, depend upon supervisor model; supervisor may have one or more than one choice to execute her/his task, “Controllution.  
\end{table}
Table 1: Event execution based on criteria of observability and controllability through user and machine operation.