1f3afde500
A .DS_Store A Presentations/.DS_Store A Presentations/20251215-Emerson-Pres/.DS_Store A Presentations/20251215-Emerson-Pres/ERLM_SABO_DRAFT_PRES.pdf A Presentations/20251215-Emerson-Pres/ERLM_SABO_FINAL_PRES.pdf A Presentations/20251215-Emerson-Pres/actual-presentation-outline.md A Presentations/20251215-Emerson-Pres/bouncing_ball_hybrid.py A Presentations/20251215-Emerson-Pres/images/.DS_Store
40 lines
1.8 KiB
TeX
40 lines
1.8 KiB
TeX
% Thrust 3: Continuous Verification
|
|
\begin{frame}{Thrust 3: Continuous controllers verified using three complementary techniques}
|
|
|
|
\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: Continuous Verification Visualization}\\[0.3cm]
|
|
Top: Three mode types with phase portraits\\
|
|
\textbf{Stabilizing} (attractor) | \textbf{Transitory} (flow) | \textbf{Expulsory} (escape)\\[0.3cm]
|
|
Middle: State space diagram showing\\
|
|
reachable sets at boundaries\\[0.3cm]
|
|
Bottom: Barrier certificate illustration\\
|
|
Safe set with vector field showing\\
|
|
all trajectories stay inside or exit correctly
|
|
};
|
|
\end{tikzpicture}
|
|
\end{center}
|
|
|
|
%SPEAKER NOTES: See comments below
|
|
%
|
|
\textbf{Three Types of Continuous Modes:}
|
|
1. Stabilizing: Stay in current mode (e.g., full-power operation)
|
|
2. Transitory: Drive toward next mode (e.g., startup heatup)
|
|
3. Expulsory: Force to safe mode (e.g., SCRAM)
|
|
|
|
\textbf{Three Verification Techniques:}
|
|
1. Reachability Analysis: Compute reachable state sets, verify boundary conditions met
|
|
2. Assume-Guarantee: Local verification, global guarantees. Each mode verified independently
|
|
3. Barrier Certificates: Prove safe set forward invariance, guarantee transitions occur correctly
|
|
|
|
\textbf{Key Innovation:} Design continuous controllers after synthesizing automaton
|
|
- Automaton defines transition boundaries
|
|
- Design each mode to satisfy its local transitions
|
|
- Compositional verification avoids intractable global analysis
|
|
|
|
Output: Verified continuous modes + discrete automaton = Complete hybrid controller
|
|
% (End of speaker notes)
|
|
\end{frame}
|