\section{Research Approach} % ============================================================================ % STRUCTURE (maps to Thesis.RA tasks): % 1. Introduction + Hybrid Systems Definition (Task 34) % 2. System Requirements and Specifications (Task 35) % 3. Discrete Controller Synthesis (Task 36) % 4. Continuous Controllers Overview (Task 37) % 4.1 Transitory Modes (Task 38) % 4.2 Stabilizing Modes (Task 39) % 4.3 Expulsory Modes (Task 40) % 5. Industrial Implementation (Task 41) % ============================================================================ % ---------------------------------------------------------------------------- % 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION % ---------------------------------------------------------------------------- \oldt{Previous approaches to autonomous control have verified discrete switching logic or continuous control behavior, but not both simultaneously. Validation of continuous controllers today consists of extensive simulation trials. Discrete switching logic for routine operation has been driven by human operators, whose evaluation includes simulated control room testing and human factors research. Neither method, despite being extremely resource intensive, provides rigorous guarantees of control system behavior. HAHACS bridges this gap by composing formal methods from computer science with control-theoretic verification, formalizing reactor operations using the framework of hybrid automata.} \newt{HAHACS bridges the gap between discrete and continuous verification by composing formal methods from computer science with control-theoretic verification, formalizing reactor operations using the framework of hybrid automata.}\dasinline{Honestly just get rid of this whole paragraph.} The challenge of hybrid system verification lies in the interaction between discrete and continuous dynamics. Discrete transitions change the \oldt{governing} \newt{active}\dasinline{Governing what? People? Whos in Whoville?} vector field, creating discontinuities in the system's behavior. Traditional verification techniques designed for purely discrete or purely continuous systems cannot handle this interaction directly.\splitpolish{Missing space before ``Our}\dasinline{This whole paragraph should just be after the definition of the tuple. First sentence can stay, but all this explanation should move.} Our methodology addresses this challenge through decomposition. We verify discrete switching logic and continuous mode behavior separately, then compose these guarantees to reason about the complete hybrid system.\splitsuggest{Compositional verification claim needs citation. See assume-guarantee literature (Henzinger, Alur). None of the NEEDS\_REVIEWED papers directly prove this composition is sound for your specific approach.} This two-layer approach mirrors the structure of reactor operations themselves: discrete supervisory logic determines which control mode is active, while continuous controllers govern plant behavior within each mode. To build a high-assurance hybrid autonomous control system (HAHACS), we must first establish a mathematical description of the system. This work draws on automata theory, temporal logic, and control theory. A hybrid system is a dynamical system that has both continuous and discrete states. The specific type of system discussed in this proposal is a continuous autonomous hybrid system. This means that the system does not have external input and that continuous states do not change instantaneously when discrete states change. For our systems of interest, the continuous states are physical quantities that are always Lipschitz continuous. This nomenclature is borrowed from the Handbook on Hybrid Systems Control \cite{HANDBOOK ON HYBRID SYSTEMS}, but is redefined here for convenience: \begin{equation} H = (\mathcal{Q}, \mathcal{X}, \mathbf{f}, Init, \mathcal{G}, \delta, \mathcal{R}, Inv) \end{equation} where: \begin{itemize} \item $\mathcal{Q}$: the set of discrete states (modes) of the system \item $\mathcal{X} \subseteq \mathbb{R}^n$: the continuous state space \item $\mathbf{f}: \mathcal{Q} \times \mathcal{X} \rightarrow \mathbb{R}^n$: vector fields defining the continuous dynamics for each discrete mode $q_i$ \item $Init \subseteq \mathcal{Q} \times \mathcal{X}$: the set of initial states \item $\mathcal{G}$: guard conditions that define when discrete state transitions may occur \item $\delta: \mathcal{Q} \times \mathcal{G} \rightarrow \mathcal{Q}$: the discrete state transition function \item $\mathcal{R}$: reset maps that define any instantaneous changes to continuous state upon discrete transitions \item $Inv$: safety invariants on the continuous dynamics \end{itemize} The creation of a HAHACS amounts to the construction of such a tuple together with proof artifacts demonstrating that the intended behavior of the control system is satisfied by its actual implementation.\oldt{}\newt{ In concrete terms, this means producing a discrete automaton whose transitions are provably correct, continuous controllers whose behavior is verified against transition requirements, and formal evidence linking the two.}\dasinline{Add a sentence explaining what this actually means.} This approach is tractable now because the infrastructure for each component has matured. The novelty is not in the individual pieces, but in the architecture that connects them.\splitnote{This is your key insight --- the novelty is compositional, not component-level.} By defining entry, exit, and safety conditions at the discrete level first, we transform the intractable problem of global hybrid verification into a collection of local verification problems with clear interfaces. Verification is performed per mode rather than on the full hybrid system, keeping the analysis tractable even for complex reactor operations. \begin{figure} \centering \begin{tikzpicture}[ state/.style={ circle, draw=black, thick, minimum size=2.2cm, fill=blue!10, align=center, font=\small }, trans/.style={ ->, thick, >=stealth }, guard/.style={ font=\scriptsize, align=center, fill=white, inner sep=2pt }, dynamics/.style={ font=\scriptsize\itshape, text=blue!70!black } ] % States \node[state] (q0) at (0,0) {$q_0$\\Cold\\Shutdown}; \node[state] (q1) at (5,0) {$q_1$\\Heatup}; \node[state] (q2) at (10,0) {$q_2$\\Power\\Operation}; \node[state, fill=red!15] (q3) at (5,-3.5) {$q_3$\\SCRAM}; % Normal transitions \draw[trans] (q0) -- node[guard, above] {$T_{avg} > T_{min}$} (q1); \draw[trans] (q1) -- node[guard, above] {$T_{avg} \in [T_{op} \pm \delta]$\\$P > P_{crit}$} (q2); % Fault transitions \draw[trans, red!70!black] (q1) -- node[guard, left, text=red!70!black] {$\neg Inv_1$} (q3); \draw[trans, red!70!black] (q2) to[bend left=20] node[guard, right, text=red!70!black] {$\neg Inv_2$} (q3); % Recovery transition \draw[trans, dashed] (q3) to[bend left=30] node[guard, below] {Manual reset} (q0); % Self-loops indicating staying in mode \draw[trans] (q2) to[loop right] node[guard, right] {$Inv_2$} (q2); % Dynamics labels below states \node[dynamics] at (0,-1.4) {$\dot{x} = f_0(x)$}; \node[dynamics] at (6,-1.2) {$\dot{x} = f_1(x)$}; \node[dynamics] at (10,-1.4) {$\dot{x} = f_2(x)$}; \node[dynamics] at (5,-4.9) {$\dot{x} = f_3(x)$}; \end{tikzpicture} \dasinline{Figure dynamics show control inputs u, but these systems are autonomous. What's up with that?} \caption{Simplified hybrid automaton for reactor startup. Each discrete state $q_i$ has associated continuous dynamics $f_i$. Guard conditions on transitions (e.g., $T_{avg} > T_{min}$) are predicates over continuous state. Invariant violations ($\neg Inv_i$) trigger transitions to the SCRAM state. The operational level manages discrete transitions; the tactical level executes continuous control within each mode.} \label{fig:hybrid_automaton} \end{figure} %%% NOTES (Section 1): % - May want to clarify the "no external input" claim with a footnote about % strategic inputs (e.g., remote start/stop commands) % - The reset map R is often identity for physical systems; clarify if needed % ---------------------------------------------------------------------------- % 2. SYSTEM REQUIREMENTS AND SPECIFICATIONS % ---------------------------------------------------------------------------- \subsection{System Requirements, Specifications, and Discrete Controllers} Human control of nuclear power can be divided into three different scopes: strategic, operational, and tactical. Strategic control is high-level and long-term decision making for the plant. This level has objectives that are complex and economic in scale, such as managing labor needs and supply chains to optimize scheduled maintenance and downtime. The time scale at this level is long, often spanning months or years. The lowest level of control is the tactical level. This is the individual control of pumps, turbines, and chemistry. Tactical control has already been somewhat automated in nuclear power plants today, and is generally considered ``automatic control'' when autonomous. These controls are almost always continuous systems with a direct impact on the physical state of the plant.\dasinline{This should be written to be clear this isn't an exhaustive list.} Tactical control objectives include\oldt{}\newt{, but are not limited to,} maintaining pressurizer level, maintaining core temperature, or adjusting reactivity with a chemical shim. The level of control \oldt{linking} \newt{linking these two extremes of}\dasinline{Linking of these two extremes. Don't even say control here.} \oldt{these two extremes is the} operational control scope. Operational control is the primary responsibility of human operators today. Operational control takes the current strategic objective and implements tactical control objectives to drive the plant towards strategic goals. In this way, it bridges high-level and low-level goals. A strategic goal may be to perform refueling at a certain time, while the tactical level of the plant is currently focused on maintaining a certain core temperature. The operational level issues the shutdown procedure, using several smaller tactical goals along the way to achieve this \oldt{objective.} \newt{strategic objective.}\dasinline{This STRATEGIC objective.} Thus, the combination of the operational and tactical levels fundamentally forms a hybrid controller. The tactical level is the continuous evolution of the plant according to the control input and control law, while the operational level is a discrete state evolution that determines which tactical control law to apply. %Say something about autonomous control systems near here? \begin{figure} \centering \begin{tikzpicture}[scale=0.8] % Pyramid layers \fill[blue!30!white] (0,4) -- (2,4) -- (1,5.) -- cycle; \fill[blue!20!white] (-1.5,2.5) -- (3.5,2.5) -- (2,4) -- (0,4) -- cycle; \fill[blue!10!white] (-3,1) -- (5,1) -- (3.5,2.5) -- (-1.5,2.5) -- cycle; % Labels inside pyramid \node[font=\small\bfseries] at (1,4.5) {Strategic}; \node[font=\small\bfseries] at (1,3.1) {Operational}; \node[font=\small\bfseries] at (1,1.6) {Tactical}; % Descriptions to the right \node[anchor=west, font=\small, text width=8cm] at (5.5,4.6) {\textit{Long-term planning:} maintenance scheduling, capacity planning, economic dispatch}; \node[anchor=west, font=\small, text width=8cm] at (5.5,3.1) {\textit{Discrete decisions:} startup/shutdown sequences, power level changes, mode transitions}; \node[anchor=west, font=\small, text width=8cm] at (5.5,1.6) {\textit{Continuous control:} temperature regulation, pressure control, load following}; % Bracket showing HAHACS scope (simple line with text) \draw[thick] (5.0,1.0) -- (-3.5,1) -- (-3.5,4) -- (2.0,4) -- cycle; \node[font=\small, align=center, rotate=90] at (-4.2,2.5) {HAHACS scope}; \end{tikzpicture} \caption{Control scope hierarchy in nuclear power operations. Strategic control (long-term planning) remains with human management. HAHACS addresses the operational level (discrete mode switching) and tactical level (continuous control within modes), which together form a hybrid control system.} \label{fig:strat_op_tact} \end{figure} \oldt{This operational control level is the main reason for the requirement of human operators in nuclear control today. The hybrid nature of this control system makes it difficult to prove that a controller will perform according to strategic requirements, as unified infrastructure for building and verifying hybrid systems does not currently exist. Humans have been used for this layer because their general intelligence has been relied upon as a safe way to manage the hybrid nature of this system.} \newt{The hybrid nature of this control problem is the reason human operators remain essential. Because unified infrastructure for building and verifying hybrid systems does not currently exist, the operational layer has relied on human general intelligence to manage the interaction between discrete decisions and continuous dynamics.}\dasinline{This operational control level is the main reason\ldots Add a sentence why. Because the hybrid dynamics have previously been `unknowable', it's been assumed that a human operator could figure it out on the fly. Or similar.} \oldt{But these operators use prescriptive operating manuals to perform their control with strict procedures on what control to implement at a given time.} \newt{However, human factors research has sought to minimize the need for general human reasoning by creating extremely prescriptive operating manuals with strict procedures dictating what control to implement at a given time.}\dasinline{Say but human factors has been seeking to eliminate the need for general human behavior by creating extremely prescriptive operating manuals. This is our leverage.} These procedures are the key to the operational control scope. The method of constructing a HAHACS in this proposal leverages two key observations about current practice. First, the operational scope control is effectively discrete control. Second, the rules for implementing this control are described prior to their implementation in operating procedures. Before constructing a HAHACS, we must completely describe its intended behavior. The behavior of any control system originates in requirements: statements about what the system must do, must not do, and under what conditions. For nuclear systems, these requirements derive from multiple sources including regulatory mandates, design basis analyses, and operating procedures. The challenge is formalizing these requirements with sufficient precision that they can serve as the foundation for autonomous control system synthesis and verification. We can build these requirements using temporal logic.\dasinline{We definitely need some temporal logic juice in the SOTA.} Temporal logic is a powerful set of semantics for building systems with complex but deterministic behavior. Temporal logic extends classical propositional logic with operators that express properties over time. Using temporal logic, we can make statements relating discrete control modes to one another and define all the requirements of a HAHACS. The guard conditions $\mathcal{G}$ are defined by determining boundary conditions between discrete states and specifying their behavior, while continuous mode invariants can also be expressed as temporal logic statements. These specifications form the basis of any proofs about a HAHACS and constitute the fundamental truth statements about what the behavior of the system is designed to be. Discrete mode transitions include predicates that are Boolean functions over the continuous state space: $p_i: \mathcal{X} \rightarrow \{\text{true}, \text{false}\}$. These predicates formalize conditions like ``coolant temperature exceeds 315\textdegree{}C'' or ``pressurizer level is between 30\% and 60\%.'' Critically, we do not impose this discrete abstraction artificially. Operating procedures for nuclear systems already define go/no-go conditions as discrete predicates. These thresholds come from design basis safety analysis and have been validated over decades of operational experience. Our methodology assumes this domain knowledge exists and provides a framework to formalize it. This is why the approach is feasible for nuclear applications specifically: the hard work of defining safe operating boundaries has already been done by generations of nuclear engineers. Linear temporal logic (LTL) is particularly well-suited for\dasinline{Some of this could be in SOTA vs here. Examples in nuclear space should be in RA, but the general idea of temporal logic and where it came from in the context of computers could be in SOTA.} specifying reactive systems. LTL formulas are built from atomic propositions (our discrete predicates) using Boolean connectives and temporal operators. The key temporal operators are: \begin{itemize} \item $\mathbf{X}\phi$ (next): $\phi$ holds in the next state \item $\mathbf{G}\phi$ (globally): $\phi$ holds in all future states \item $\mathbf{F}\phi$ (finally): $\phi$ holds in some future state \item $\phi \mathbf{U} \psi$ (until): $\phi$ holds until $\psi$ becomes true \end{itemize} These operators allow us to express safety properties (``the reactor never enters an unsafe configuration''), liveness properties (``the system eventually reaches operating temperature''), and response properties (``if coolant pressure drops, the system initiates shutdown within bounded time'').% \splitsuggest{CAUTION: Katis 2022 (Table 1, p.2) notes FRET realizability checking does NOT support liveness properties. Your ``eventually reaches operating temperature'' example may need alternative verification approach.} To build these temporal logic statements, an intermediary tool called FRET is planned to be used. FRET stands for Formal Requirements Elicitation Tool, and was developed by NASA to build high-assurance timed systems. FRET is an intermediate language between temporal logic and natural language that allows for rigid definitions of temporal behavior while using a syntax accessible to engineers without formal methods expertise. This benefit is crucial for the feasibility of this methodology in industry. By reducing the expert knowledge required to use these tools, their adoption with the current workforce becomes easier. A key feature of FRET is the ability to start with logically imprecise statements and consecutively refine them into well-posed specifications. We can use this to our advantage by directly importing operating procedures and design requirements into FRET in natural language, then iteratively refining them into specifications for a HAHACS. This has two distinct benefits. First, it allows us to draw a direct link from design documentation to digital system implementation. Second, it clearly demonstrates where natural language documents are insufficient. These procedures may still be used by human operators, so any room for interpretation is a weakness that must be addressed.\splitnote{FRET has been validated: Katis 2022 (pp.1-2, Section 0.3) demonstrates FRET's FRETish template system with 160 distinct patterns; Pressburger 2023 (pp.17, Section 1) shows successful application to Lift+Cruise case study with 53 requirements formalized and iteratively refined---strong evidence your approach is feasible.} (Some examples of where FRET has been used and why it will be successful here) %%% NOTES (Section 2): % - Add concrete FRET example showing requirement $\rightarrow$ FRETish % $\rightarrow$ LTL % - Discuss hysteresis and how to prevent mode chattering near boundaries % - Address sensor noise and measurement uncertainty in threshold definitions % - Consider numerical precision issues when creating discrete automata % ---------------------------------------------------------------------------- % 3. DISCRETE CONTROLLER SYNTHESIS % ---------------------------------------------------------------------------- Once system requirements are defined as temporal logic specifications, we use them to build the discrete control system. To do this, reactive synthesis tools are employed. Reactive synthesis is a field in computer science that deals with the automated creation of reactive programs from temporal logic specifications. A reactive program is one that, for a given state, takes an input and produces an output. Our systems fit exactly this mold: the current discrete state and status of guard conditions are the input, while the output is the next discrete state. Reactive synthesis solves the following problem: given an LTL formula $\varphi$ that specifies desired system behavior, automatically construct a finite-state machine (strategy) that produces outputs in response to environment inputs such that all resulting execution traces satisfy $\varphi$. If such a strategy exists, the specification is called \emph{realizable}. The synthesis algorithm either produces a correct-by-construction controller or reports that no such controller can exist. This realizability check is itself valuable: an unrealizable specification indicates conflicting or impossible requirements in the original procedures.\splitnote{Realizability is proven valuable: Katis 2022 (pp.7-10) shows FRET diagnosis found 8 minimal unrealizable cores in infusion pump case; Pressburger 2023 (pp.19-21) shows unrealizability revealed under-specification (missing stay requirements in LPC aircraft), driving iterative refinement---this suggests your synthesis approach will help engineers catch requirement errors early.} The main advantage of reactive synthesis is that at no point in the production of the discrete automaton is human engineering of the implementation required. The resultant automaton is correct by construction. This method of construction eliminates the possibility of human error at the implementation stage entirely. \oldt{Instead, the effort on the human designer is directed at the specification of system behavior itself. This has two critical implications. First, it makes the creation of the discrete controller tractable. The reasons the controller changes between modes can be traced back to the specification and thus to any requirements, which provides a trace for liability and justification of system behavior. Second, discrete control decisions made by humans are reliant on the human operator operating correctly. Humans are intrinsically probabilistic creatures who cannot eliminate human error. By defining the behavior of this system using temporal logics and synthesizing the controller using deterministic algorithms, we are assured that strategic decisions will always be made according to operating procedures.} \newt{The effort shifts entirely to specifying correct behavior rather than implementing it. This has two critical implications. First, every mode transition can be traced back through the specification to its originating requirement, providing a clear liability and justification chain. Second, by defining system behavior in temporal logic and synthesizing the controller using deterministic algorithms, discrete control decisions become provably consistent with operating procedures.}\dasinline{Some goofy issue-point stuff going on in this paragraph.}\splitnote{Strix (Luttenberger 2020, pp.1-3) is a practical reactive synthesis tool winning SYNTCOMP competitions; handles LTL specs for systems with large state spaces. Strix uses parity games and forward-explorative construction (pp.7-8) to scale---recommend as your synthesis backend for nuclear procedures.}\splitsuggest{Consider discussing scalability: Strix handles large alphabets better (v19.07 update, p.30), but still struggles with very large specifications. Document expected spec size for SmAHTR startup procedures to set expectations.} (Talk about how one would go from a discrete automaton to actual code)\splitnote{GR(1) fragment (Maoz \& Ringert 2015, pp.1-4) is tractable LTL subset for synthesis: wins SYNTCOMP competitions (p.13). Luttenberger 2020 (Strix tool, pp.1-3) handles full LTL via parity games, achieving 4000+ state specs efficiently (p.5). Your nuclear procedures should fit GR(1) since they're reactive (environment inputs = plant state, outputs = mode transitions). This suggests synthesis will be practical for SmAHTR scale.} (Examples of reactive synthesis in the wild)\splitfix{Need to verify your LTL specs fit GR(1) or full LTL needed---if full LTL required, computational cost grows but Strix may handle it (confirm scalability claim with specific spec size estimates for startup/shutdown procedures).} %%% NOTES (Section 3): % - Mention computational complexity of synthesis (doubly exponential worst % case) % - Discuss how specification structure affects synthesis tractability % - Reference GR(1) fragment as a tractable subset commonly used in practice % - May want to include an example automaton figure % ---------------------------------------------------------------------------- % 4. CONTINUOUS CONTROLLERS % ---------------------------------------------------------------------------- \subsection{Continuous Control Modes} The synthesis of the discrete operational controller is only half of an autonomous controller. These control systems are hybrid, with both discrete and continuous components. This section describes the continuous control modes that execute within each discrete state, and how we verify that they satisfy the requirements imposed by the discrete layer. It is important to clarify the scope of this methodology with respect to continuous controller design. This work \oldt{verifies} \newt{will verify}\dasinline{Verb tense: ``will verify''.} continuous controllers; it does not synthesize them. The distinction parallels model checking in software verification: model checking does not tell engineers how to write correct software, but it verifies whether a given implementation satisfies its specification. Similarly, we assume that continuous controllers can be designed using standard control theory techniques. Our contribution is a verification framework that confirms candidate controllers compose correctly with the discrete layer to produce a safe hybrid system. The operational control scope defines go/no-go decisions that determine what kind of continuous control to implement. The entry or exit conditions of a discrete state are themselves the guard conditions $\mathcal{G}$ that define the boundaries for each continuous controller's allowed state-space region. These continuous controllers all share a common state space, but each individual continuous control mode operates within its own partition defined by the discrete state $q_i$ and the associated guards. This partitioning of the continuous state space among several discrete vector fields has traditionally been a difficult problem for validation and verification. The discontinuity of the vector fields at discrete state interfaces makes reachability analysis computationally expensive, and analytic solutions often become intractable \cite{MANYUS THESIS}. We circumvent these issues by designing our hybrid system from the bottom up with verification in mind. Each continuous control mode has an input set and output set clearly defined by our discrete transitions \textit{a priori}. Consider that we define the continuous state space as $\mathcal{X}$. Each discrete mode $q_i$ then provides three key pieces of information for continuous controller design: \begin{enumerate} \item \textbf{Entry conditions:} $\mathcal{X}_{entry,i} \subseteq \mathcal{X}$, the set of possible initial states when entering this mode \item \textbf{Exit conditions:} $\mathcal{X}_{exit,i} \subseteq \mathcal{X}$, the target states that trigger transition to the next mode, or is the region in the state space a stabilizing mode remains within. \item \textbf{Safety invariants:} $\mathcal{X}_{safe,i} \subseteq \mathcal{X}$, the envelope of safe states during operation in this mode. These are derived from invariants \(Inv\). \end{enumerate} These sets come directly from the discrete controller synthesis and define precise objectives for continuous control.\dasinline{This SOUNDS like assume-guarantee stuff. Maybe make that connection formal and cite it?} The continuous controller for mode $q_i$ must drive the system from any state in $\mathcal{X}_{entry,i}$ to some state in $\mathcal{X}_{exit,i}$ while remaining within $\mathcal{X}_{safe,i}$.\splitnote{This compositional approach is formalized in Kapuria 2025 (pp.17-24, Section 2.4): component proofs via differential cuts reduce state-space (DC rule, p.20), then system proof composes via differential invariants (DI rule, pp.22-24). Kapuria proves SmAHTR safety by verifying 6 components in isolation then system---your three-mode structure maps perfectly to this decomposition, reducing verification complexity from curse of dimensionality.} We classify continuous controllers into three types based on their objectives: transitory, stabilizing, and expulsory.\splitnote{This three-mode taxonomy is elegant --- maps verification tools to control objectives cleanly.} Each type has distinct verification requirements that determine which formal methods tools are appropriate. %%% NOTES (Section 4): % - Add figure showing the relationship between entry/exit/safety sets % - Discuss how standard control techniques (LQR, MPC, PID) fit into this % framework % - Mention assume-guarantee reasoning for compositional verification % ---------------------------------------------------------------------------- % 4.1 TRANSITORY MODES % ---------------------------------------------------------------------------- \subsubsection{Transitory Modes} Transitory modes are continuous controllers designed to move the plant from one discrete operating condition to another. Their purpose is to execute transitions: starting from entry conditions, reach exit conditions, and maintain safety invariants throughout. Examples include power ramp-up sequences, cooldown procedures, and load-following maneuvers. The control objective for a transitory mode can be stated formally. Given entry conditions $\mathcal{X}_{entry}$, exit conditions $\mathcal{X}_{exit}$, safety invariant $\mathcal{X}_{safe}$, and closed-loop dynamics $\dot{x} = f(x, u(x))$, the controller must satisfy: \[ \forall x_0 \in \mathcal{X}_{entry}: \exists T > 0: x(T) \in \mathcal{X}_{exit} \land \forall t \in [0,T]: x(t) \in \mathcal{X}_{safe} \] That is, from any valid entry state, the trajectory must eventually reach the exit condition without ever leaving the safe region. Verification of transitory modes uses reachability analysis. Reachability analysis computes the set of all states reachable from a given initial set under the system dynamics. For a transitory mode to be valid, the reachable set from $\mathcal{X}_{entry}$ must satisfy two conditions: \begin{enumerate} \item The reachable set eventually intersects $\mathcal{X}_{exit}$ (the mode achieves its objective) \item The reachable set never leaves $\mathcal{X}_{safe}$ (safety is maintained throughout the transition) \end{enumerate} Formally, if $\text{Reach}(\mathcal{X}_{entry}, f, [0,T])$ denotes the states reachable within time horizon $T$: \[ \text{Reach}(\mathcal{X}_{entry}, f_i, [0,T]) \subseteq \mathcal{X}_{safe} \land \text{Reach}(\mathcal{X}_{entry}, f_i, [0,T]) \cap \mathcal{X}_{exit} \neq \emptyset \] \textcolor{blue}{Because the discrete controller defines clear boundaries in continuous state space, the verification problem for each transitory mode is well-posed. We know the possible initial conditions, we know the target conditions, and we know the safety envelope. The verification task is to confirm that the candidate continuous controller achieves the objective from all possible starting points.} Several tools exist for computing reachable sets of hybrid systems, including CORA, Flow*, SpaceEx, and JuliaReach. The choice of tool depends on the structure of the continuous dynamics. Linear systems admit efficient polyhedral or ellipsoidal reachability computations. Nonlinear systems require more conservative over-approximations using techniques such as Taylor models or polynomial zonotopes. For this work, we will select tools appropriate to the fidelity of the reactor models available.\splitnote{Your toolset is well-justified: SpaceEx (Frehse 2011, pp.3-6) handles hybrid automata via support functions; Flow* (Chen 2013) uses Taylor models for nonlinear dynamics; JuliaReach (Bogomolov 2019, pp.1-2) offers flexible set representations (zonotopes, boxes). Kapuria 2025 (pp.11-12, Section 2.2) uses Flow* successfully for SmAHTR reachability with reactor models showing state-space constraints (e.g., temp 673--677\textdegree{}C, Figures 6, 16--20). This validates your tool choices for nuclear systems.}\splitnote{Critical finding from Kapuria 2025: decomposition-based verification (pp.17-24, Section 2.4) proves component safety in isolation using reachability, THEN composes to system proof via differential invariants---your three-mode taxonomy maps cleanly to component verification, reducing complexity from monolithic analysis.} %%% NOTES (Section 4.1): % - Add timing constraints discussion: what if the transition takes too long? % - Consider timed reachability for systems with deadline requirements % - Mention that the Mealy machine perspective unifies this: continuous system % IS the transition, entry/exit conditions are the discrete states % ---------------------------------------------------------------------------- % 4.2 STABILIZING MODES % ---------------------------------------------------------------------------- \subsubsection{Stabilizing Modes} Stabilizing modes are continuous controllers with an objective of maintaining a particular discrete state indefinitely. Rather than driving the system toward an exit \oldt{condition,} \newt{state,}\dasinline{``mode'' --- ``condition'' here sounds goofy.} they keep the system within a safe operating region. Examples include steady-state power operation, hot standby, and load-following at constant power level. Reachability analysis for stabilizing modes may not be a suitable approach to validation. Instead, we plan to use barrier certificates. Barrier certificates analyze the dynamics of the system to determine whether flux across a given boundary exists. They evaluate whether any trajectory leaves a given boundary. This definition is exactly what defines the validity of a stabilizing continuous control mode. A barrier certificate (or control barrier function) is a scalar function $B: \mathcal{X} \rightarrow \mathbb{R}$ that certifies forward invariance of a safe set. The idea is analogous to Lyapunov functions for stability: rather than computing trajectories explicitly, we find a certificate function whose properties guarantee the desired behavior. For a safe set $\mathcal{C} = \{x : B(x) \geq 0\}$ and dynamics $\dot{x} = f(x,u)$, the\dasinline{Should clarify that the safe set C is not the entire continuous region. It's just the boundary of the region.} barrier certificate condition requires: \[ \forall x \in \partial\mathcal{C}: \dot{B}(x) = \nabla B(x) \cdot f(x,u(x)) \geq 0 \] This condition states that on the boundary of the safe set (where $B(x) = 0$), the time derivative of $B$ is non-negative. Geometrically, this means the vector field points inward or tangent to the boundary, never outward. If this condition holds, no trajectory starting inside $\mathcal{C}$ can ever leave. Because the design of the discrete controller defines careful boundaries in continuous state space, the barrier is known prior to designing the continuous controller. This eliminates the search for an appropriate barrier and minimizes complication in validating stabilizing continuous control modes. The discrete specifications tell us what region must be invariant; the barrier certificate confirms that the candidate controller achieves this invariance. Finding barrier certificates can be formulated as a sum-of-squares (SOS) optimization problem for polynomial systems, or solved using satisfiability modulo theories (SMT) solvers for broader classes of dynamics. The key advantage is that the verification is independent of how the controller was designed. Standard control techniques can be used to build continuous controllers, and barrier certificates provide a separate check that the result satisfies the required invariants. This also allows for the checking of control modes with different models than they are designed for. For example, a lower fidelity model can be used for controller design, but a higher fidelity model can be used for the actual validation of that stabilizing controller.\splitnote{SOS methods proven effective: Papachristodoulou 2021 (SOSTOOLS v4, pp.1-2) solves barrier certificate optimization via SOS constraints---tool integrates with MATLAB. Borrmann 2015 (pp.4-8) demonstrates control barrier certificates for multi-agent systems, showing how discrete boundaries (mode guards) can inform barrier design. Your claim that discrete specs eliminate barrier search is novel and well-supported by these foundations.}\splitnote{Hauswirth 2024 (pp.1-3) shows optimization-based robust feedback controllers can serve as alternative verification method---suggests barrier certificates + reachability provide complementary guarantees for your stabilizing modes.} %%% NOTES (Section 4.2): % - Clarify relationship between barrier certificates and Lyapunov stability % - Discuss what happens at mode boundaries: barrier for this mode vs guard % for transition % - Mention tools: SOSTOOLS, dReal, barrier function synthesis methods % ---------------------------------------------------------------------------- % 4.3 EXPULSORY MODES % ---------------------------------------------------------------------------- \subsubsection{Expulsory Modes} Expulsory modes are continuous controllers responsible for ensuring safety when failures occur. They are designed for robustness rather than optimality. The control objective is to drive the plant to a safe shutdown state from potentially anywhere in the state space, under degraded or uncertain dynamics. Examples include emergency core cooling, reactor SCRAM sequences, and controlled depressurization procedures. We can detect that physical failures exist because our physical controllers have been previously proven correct by reachability and barrier certificates. We know our controller cannot be incorrect for the nominal plant model, so if an invariant is violated, we know the plant dynamics have changed. \oldt{The HAHACS can identify that a fault occurred because a discrete boundary condition was violated by the continuous physical controller.} \newt{}\dasinline{This says the same thing as the sentence right before it.} This is a direct consequence of having verified the nominal continuous control modes: unexpected behavior implies off-nominal conditions. The mathematical formulation for expulsory mode verification differs from transitory modes in two key ways. First, the entry conditions may be the entire state space (or a large, conservatively bounded region) rather than a well-defined entry set. The failure may occur at any point during operation. Second, the dynamics include parametric uncertainty representing failure modes: \[ \dot{x} = f(x, u, \theta), \quad \theta \in \Theta_{failure} \] where $\Theta_{failure}$ captures the range of possible degraded plant% \splitsuggest{GAP: None of the NEEDS\_REVIEWED papers directly address reachability with parametric uncertainty for failure mode analysis. SpaceEx handles nondeterministic inputs (Frehse 2011, p.4) but not parametric plant uncertainty. Consider citing CORA (parametric reachability) or robust CBF literature. This may require additional references beyond current collection.} behaviors identified through failure mode and effects analysis (FMEA) or traditional safety analysis. We verify expulsory modes using reachability analysis with parametric uncertainty. The verification condition requires that for all parameter values within the uncertainty set, trajectories from the expanded entry region reach the safe shutdown state: \[ \forall \theta \in \Theta_{failure}: \text{Reach}(\mathcal{X}_{current}, f_\theta, [0,T]) \subseteq \mathcal{X}_{shutdown} \] This is more conservative than nominal reachability, accounting for the fact that we cannot know exactly which failure mode is active. Traditional safety analysis techniques inform the construction of $\Theta_{failure}$. Probabilistic risk assessment, FMEA, and design basis accident analysis identify credible failure scenarios and their effects on plant dynamics. The expulsory mode must handle the worst-case dynamics within this envelope. This is where conservative controller design is appropriate as safety margins will matter more than performance during emergency shutdown.\splitnote{Parametric uncertainty approach validated: Kapuria 2025 (pp.82-120, Sections 5) verifies SmAHTR resiliency against UCAs with uncertain dynamics (e.g., PHX secondary flow shutdown, resonating turbine flow). Uses reachability + Z3 SMT solver (pp.23-24, Section 2.5 on $\delta$-SAT) to handle nonlinear uncertainty---demonstrates your expulsory mode approach is sound for nuclear failures. Shows safety can be proven even when controller deviates from nominal (pp.85-107, UCA 1 analysis).}\splitsuggest{Kapuria 2025 reveals practical challenge: determining $\Theta_{\text{failure}}$ bounds is non-trivial. Recommend documenting failure mode selection process (FMEA $\rightarrow$ parametric bounds) to make expulsory mode design repeatable for other reactor sequences.} %%% NOTES (Section 4.3): % - Discuss sensor failures vs actual plant failures % - Address unmodeled disturbances that aren't failures % - How much parametric uncertainty is enough? Need methodology for bounds % - Mention graceful degradation: graded responses vs immediate SCRAM % ---------------------------------------------------------------------------- % 5. INDUSTRIAL IMPLEMENTATION % ---------------------------------------------------------------------------- \subsection{Industrial Implementation} The methodology described above must be validated on realistic systems using industrial-grade hardware to demonstrate practical feasibility. This research will leverage the University of Pittsburgh Cyber Energy Center's partnership with Emerson to implement and test the HAHACS methodology on production control equipment. Emerson's Ovation distributed control system is widely deployed in power generation facilities, including nuclear plants. The Ovation platform provides a realistic target for demonstrating that formally synthesized controllers can execute on industrial hardware meeting timing and reliability requirements. The discrete automaton produced by reactive synthesis will be compiled to run on Ovation controllers, with verification that the implemented behavior matches the synthesized specification exactly. For the continuous dynamics, we will use a small modular reactor simulation.\dasinline{Are we REALLY going to do this? Maybe not.} The SmAHTR (Small modular Advanced High Temperature Reactor) model provides a relevant testbed for startup and shutdown procedures. The ARCADE (Advanced Reactor Control Architecture Development Environment) interface will establish communication between the Emerson Ovation hardware and the reactor simulation, enabling hardware-in-the-loop testing of the complete hybrid controller. \oldt{Working with Emerson on such an implementation is an incredible advantage for the success and impact of this work. We will directly address the gap of verification and validation methods for these systems and industry adoption by forming a two-way exchange of knowledge between the laboratory and commercial environments. This work stands to be successful with Emerson implementation because we will have access to system experts at Emerson to help with the fine details of using the Ovation system. At the same time, we will have the benefit of transferring technology directly to industry with a direct collaboration in this research, while getting an excellent perspective of how our research outcomes can align best with customer needs.} \newt{The Emerson collaboration strengthens this work in two ways. Access to system experts at Emerson ensures that implementation details of the Ovation platform are handled correctly. Direct industry collaboration provides an immediate pathway for technology transfer and alignment with practical deployment requirements.}\splitnote{Kapuria 2025 validates hybrid control on SmAHTR: formal verification (d$\mathcal{L}$ + reachability, pp.37-70) proved safe PHX maintenance scenario, then Simulink demo confirmed (pp.70-72). This two-tier approach (formal proof + simulation validation) strengthens your Emerson demo plan for credibility.}\splitsuggest{Consider documenting integration points: ARCADE interface must guarantee formal synthesis outputs map 1:1 to Ovation code. Pressburger 2023 (pp.22-23) notes manual integration risks---automate code generation from formal specs to minimize this gap.} %%% NOTES (Section 5): % - Get specific details on ARCADE interface from Emerson collaboration % - Mention what startup sequence will be demonstrated (cold shutdown % $\rightarrow$ criticality $\rightarrow$ low power?) % - Discuss how off-nominal scenarios will be tested (sensor failures, % simulated component degradation) % - Reference Westinghouse relationship if relevant