diff --git a/3-research-approach/approach.tex b/3-research-approach/approach.tex index 661abbf..1c6e898 100644 --- a/3-research-approach/approach.tex +++ b/3-research-approach/approach.tex @@ -421,12 +421,9 @@ We classify continuous controllers into three types based on their objectives: transitory, stabilizing, and expulsory. Each type has distinct verification requirements that determine which formal methods tools are appropriate. -\dasinline{ - \begin{itemize} - \item Add figure showing the relationship between entry/exit/safety sets - \item Mention assume guarantee compositional stuff and how that fits in here - \end{itemize} -} +\dasinline{(1) Add figure showing the relationship between entry/exit/safety +sets. (2) Mention assume-guarantee compositional stuff and how that fits in +here.} \subsubsection{Transitory Modes} @@ -673,7 +670,7 @@ The Emerson collaboration strengthens this work in two ways. Access to system experts at Emerson ensures that implementation details of the Ovation platform are handled correctly. Direct industry collaboration also provides an immediate pathway for technology transfer and alignment with practical -deployment requirements.}\splitnote{Kapuria 2025 validates hybrid control on +deployment requirements.\splitnote{Kapuria 2025 validates hybrid control on SmAHTR: formal verification (d$\mathcal{L}$ + reachability, pp.37-70) proved safe PHX maintenance scenario, then Simulink demo confirmed (pp.70-72). This two-tier approach (formal proof + simulation validation) strengthens your