\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.
