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