Dane Sabo
02832ba45e
M Writing/ERLM/main.aux M Writing/ERLM/main.bbl M Writing/ERLM/main.blg M Writing/ERLM/main.fdb_latexmk M Writing/ERLM/main.fls M Writing/ERLM/main.log M Writing/ERLM/main.pdf M Writing/ERLM/main.synctex.gz
196 lines
11 KiB
TeX
196 lines
11 KiB
TeX
\section{State of the Art and Limits of Current Practice}
|
|
|
|
This research aims to advance high-assurance autonomous hybrid control systems
|
|
by bridging disparate approaches from control theory and computer science. While
|
|
both fields tackle hybrid system verification, they approach the problem from
|
|
fundamentally different perspectives. Control theory emphasizes performance and
|
|
stability, while computer science focuses on correctness through formal
|
|
verification. This gap represents both the primary challenge and the key
|
|
opportunity for intellectual contribution.
|
|
|
|
\subsection{Control Theory and Hybrid Systems}
|
|
|
|
Hybrid systems combine continuous dynamics (`flows') with discrete transitions
|
|
(`jumps'). Following the standard formulation, a hybrid system can be expressed as:
|
|
\begin{align}
|
|
\dot{x}(t) &= f(x(t), q(t), u(t)) \\
|
|
q(k+1) &= \nu(x(k), q(k), u(k))
|
|
\end{align}
|
|
|
|
Here, $f(\cdot)$ defines the continuous dynamics while $\nu(\cdot)$ governs
|
|
discrete transitions. The continuous states $x$, discrete state $q$, and control
|
|
input $u$ interact to produce hybrid behavior. The discrete state $q$ defines
|
|
the current continuous dynamics mode. The only constraint on $\nu(\cdot)$ is
|
|
avoiding Zeno behavior---infinite jumps in finite time. Our focus centers on
|
|
continuous autonomous hybrid systems, where continuous states remain unchanged
|
|
during jumps and no external control input is required. Physical systems
|
|
naturally exhibit this property---a nuclear reactor switching from warm-up to
|
|
load-following control cannot instantaneously change its temperature or rod
|
|
position.
|
|
|
|
An intuitive approach to building hybrid controllers is to stitch together
|
|
multiple simple controllers for different state space regions. This approach
|
|
creates significant verification challenges. Even with linear time-invariant
|
|
modes, global stability cannot be guaranteed using linear control theory alone.
|
|
Instead, researchers have developed Lyapunov-based approaches, though finding
|
|
appropriate Lyapunov functions remains challenging.
|
|
Stability conditions for switched linear systems
|
|
can provide necessary and sufficient conditions using multiple Lyapunov
|
|
functions~\cite{geromel2006stability}, but these methods require
|
|
restrictive assumptions. Individual Lyapunov functions must be monotonically
|
|
nonincreasing at every switching time, which proves impractical for many
|
|
real systems. Common Lyapunov functions face even stricter existence
|
|
conditions, often impossible for systems with fundamentally different
|
|
dynamics across modes~\cite{branicky1998multiple,liberzon2003switching}.
|
|
|
|
\textbf{LIMITATION: Lyapunov-based methods of ensuring stability are
|
|
prohibitively challenging to apply to hybrid control systems.} Finding Lyapunov
|
|
functions to prove stability in the sense of Lyapunov is not practical for
|
|
working with hybrid systems. Additional requirements on the Lyapunov functions
|
|
makes finding appropriate functions extremely difficult.
|
|
|
|
Reachability analysis offers an alternative verification approach by computing
|
|
system output ranges for given inputs. Unlike Lyapunov methods, reachability
|
|
extends naturally to nonlinear systems. Hamilton-Jacobi frameworks established
|
|
the mathematical foundation for computing reachable sets in continuous and
|
|
hybrid systems, enabling formal verification of safety-critical
|
|
applications~\cite{mitchell2005time}.
|
|
|
|
\textbf{LIMITATION: Reachability analysis is not scalable to large hybrid
|
|
systems.} Reachability analysis faces two critical limitations. First,
|
|
computational complexity grows exponentially with state dimension---current
|
|
methods remain limited to 6-8 dimensional systems despite recent algorithmic
|
|
advances. Second, approximation errors compound over long time horizons,
|
|
potentially rendering analysis meaningless for extended trajectories.
|
|
Zonotope-based methods suffer accuracy degradation when propagating across mode
|
|
boundaries, while ellipsoidal methods produce conservative over-approximations
|
|
that become increasingly pessimistic with each mode transition.
|
|
|
|
Recent work on using control barrier functions has improved hybrid system
|
|
verification efforts. Neural network based control barrier function
|
|
approximations achieve 10-100X speedup over classical Hamilton-Jacobi methods
|
|
while maintaining safety guarantees for 7-dimensional autonomous racing
|
|
systems~\cite{yang2024learning}. This breakthrough demonstrates that deep neural
|
|
networks can approximate Hamilton-Jacobi partial differential equations and
|
|
enables application to previously intractable high-dimensional systems, but
|
|
future work must address the explainability problem for neural networks to
|
|
ensure control barrier functions are valid.
|
|
|
|
\subsection{Formal Methods and Reactive Synthesis}
|
|
|
|
Correctness requirements are specified using temporal logic, which captures
|
|
system behaviors through temporal relations. Linear Temporal Logic (LTL)
|
|
provides four fundamental operators: next ($\mathsf{X}$), eventually
|
|
($\mathsf{F}$), globally ($\mathsf{G}$), and until ($\mathsf{U}$).
|
|
Consider a nuclear reactor SCRAM requirement:
|
|
|
|
\vspace{0.2cm}
|
|
|
|
\textit{Natural language}: ``If a high temperature alarm triggers, control
|
|
rods must immediately insert and remain inserted until operator reset.''
|
|
|
|
\vspace{0.2cm}
|
|
|
|
This plain language requirement can be translated into a rigorous logical
|
|
specification.
|
|
|
|
\vspace{0.2cm}
|
|
|
|
\textit{LTL specification}:
|
|
\begin{equation}
|
|
\mathsf{G}(\text{HighTemp} \rightarrow
|
|
\mathsf{X}(\text{RodsInserted} \land
|
|
(\neg\text{RodsWithdrawn} \; \mathsf{U} \; \text{OperatorReset})))
|
|
\end{equation}
|
|
|
|
Once requirements are translated into these logical specifications, they can be
|
|
checked using computational tools. Cyber-physical systems naturally exhibit
|
|
discrete behavior amenable to formal analysis. Systems with finite states can be
|
|
modeled as finite state machines, where all possible states and transitions are
|
|
explicitly enumerable as logical specifications. This enables exhaustive
|
|
verification through model checking---a technique extensively employed in
|
|
high-assurance digital systems and safety-critical software. This mathematical
|
|
framework has been extended to hybrid automata~\cite{alur1993hybrid}, which
|
|
established the standard model combining discrete control graphs with continuous
|
|
dynamics. Hybrid automata bridge program-analysis techniques to hybrid systems
|
|
with infinite state spaces through symbolic model-checking based on reachability
|
|
analysis~\cite{alur1995algorithmic} but are not scalable for the same
|
|
limitations mentioned earlier with other reachability techniques.
|
|
|
|
% Signal Temporal Logic (STL) extends temporal logic to continuous-time signals
|
|
% with quantitative semantics~\cite{donze2010robust}. This enables specification
|
|
% of real-valued signal properties crucial for cyber-physical systems. Recent
|
|
% advances by Su et al. provide the first systematic STL synthesis approach with
|
|
% formal correctness guarantees for hybrid systems~\cite{su2024switching}.
|
|
|
|
NASA's Formal Requirements Elicitation Tool (FRET) bridges natural language
|
|
and mathematical specifications through FRETish---a structured English-like
|
|
language automatically translatable to temporal logic~\cite{giannakopoulou2022fret}.
|
|
FRET enables hierarchical requirement organization, realizability checking for
|
|
specification conflicts, integration with verification tools like CoCoSim, and
|
|
runtime monitoring through their Copilot tool.
|
|
|
|
From realizable specifications, reactive synthesis tools automatically generate
|
|
controllers. The Reactive Synthesis Competition (SYNTCOMP) has driven
|
|
algorithmic improvements for over a decade, with tools like Strix dominating
|
|
recent competitions through efficient parity game
|
|
solving~\cite{meyer2018strix,jacobs2017syntcomp}. Strix is able to translate
|
|
linear temporal logic specifications into deterministic automata automatically
|
|
while maximizing generated automata quality.
|
|
|
|
|
|
\textbf{LIMITATION: Unexplored application of temporal logic requirements in
|
|
nuclear control.} Despite extensive nuclear power documentation and mature
|
|
reactive synthesis tools, little work has combined these for nuclear
|
|
control applications. Nuclear procedures are written in structured natural
|
|
language that maps well to temporal logic, yet the synthesis community has not
|
|
engaged with this domain. This represents a significant unexplored opportunity
|
|
where formal methods could provide immediate practical impact.
|
|
|
|
% \textbf{[NEW CONTENT - Current Tool Capabilities]}
|
|
% Strix has won first place in all LTL tracks since 2018 by combining:
|
|
% \begin{itemize}
|
|
% \item Direct LTL-to-deterministic parity automata translation
|
|
% \item Multi-threaded explicit state solving
|
|
% \item Efficient automata minimization
|
|
% \item Strategy iteration for intermediate games
|
|
% \end{itemize}
|
|
|
|
Hybrid automata extend finite automata by representing discrete states as
|
|
control modes with continuous dynamics. Transitions between nodes indicate
|
|
discrete state changes through $\nu(\cdot)$ execution. This provides intuitive
|
|
graphical representation of mode switching logic. Differential dynamic logic
|
|
(dL) expands this idea and offers the most complete logical foundation for
|
|
hybrid verification. dL introduced two key
|
|
modalities~\cite{platzer2008differential,platzer2017complete}:
|
|
|
|
\begin{itemize}
|
|
\item Box modality $[\alpha]\phi$: for all executions of hybrid system $\alpha$, property $\phi$ holds
|
|
\item Diamond modality
|
|
$\langle\alpha\rangle\phi$: there exists an execution of $\alpha$ where $\phi$ holds
|
|
\end{itemize}
|
|
|
|
These modalities enable direct reasoning about hybrid systems including
|
|
continuous dynamics. The KeYmaera X theorem prover implements dL through
|
|
axiomatic tactical proving, successfully verifying collision avoidance in
|
|
train and aircraft control~\cite{fulton2015keymaera}.
|
|
|
|
\textbf{LIMITATION: There is a high expertise barrier for dL verification, and
|
|
scalability remains an issue.}
|
|
While dL is expressive enough for any hybrid behavior, verification requires
|
|
expertise in differential equations, logical specifications, and sequent
|
|
calculus. The proof effort remains challenging even with automated assistance.
|
|
Users must understand both the mathematical intricacies of their system and
|
|
the logical framework, then guide the prover through complex proof steps.
|
|
This expertise barrier prevents wider adoption despite the framework's
|
|
theoretical completeness.
|
|
|
|
The state of the art reveals a field in transition. Traditional boundaries
|
|
between control theory and formal methods are dissolving through
|
|
learning-based approaches and compositional techniques. While fundamental
|
|
challenges remain---particularly scalability and the theory-practice
|
|
gap---the convergence of approaches promises to enable verification and
|
|
synthesis for systems of unprecedented complexity. The next section
|
|
describes how this research will contribute to bridging these gaps
|
|
through unified synthesis frameworks applied to nuclear reactor control.
|