Obsidian/Presentations/20251215-Emerson-Pres/sections/11_key_insight.tex

% Key Insight
\begin{frame}{Key Insight: Automaton-first design makes verification tractable}

  \begin{center}
    \begin{tikzpicture}
      \draw[thick, fill=gray!20] (0,0) rectangle (12,7);
      \node[align=center, text width=10cm] at (6,3.5) {
        \textbf{FIGURE: Traditional vs Our Approach}\\[0.3cm]
        LEFT (red X): Traditional approach\\
        Tangled spaghetti diagram showing\\
        monolithic verification problem\\
        Label: ``Intractable''\\[0.3cm]
        RIGHT (green check): Our approach\\
        Clean modular diagram:\\
        Automaton $\rightarrow$ Local modes $\rightarrow$ Compose\\
        Each module verified independently\\
        Label: ``Tractable''
      };
    \end{tikzpicture}
  \end{center}

  %SPEAKER NOTES: See comments below
%
    \textbf{Traditional Approach (Intractable):}
    - Design everything at once
    - Verify entire trajectory through all modes
    - Computationally intractable for complex systems

    \textbf{Our Approach (Tractable):}
    1. Synthesize Discrete Automaton (tells us what boundaries to verify)
    2. Define Transition Boundaries (from automaton structure)
    3. Design Continuous Modes Locally (each controller designed for its specific job)
    4. Verify Each Mode Independently (local verification is tractable)
    5. Compose via Assume-Guarantee (interface contracts guarantee composition)

    \textbf{Key Message:} Decomposition is the key to tractable verification
% (End of speaker notes)
\end{frame}