1-goals-and-outcomes/goals.tex

@@ -2,13 +2,8 @@
 
 % GOAL PARAGRAPH
 The goal of this research is to develop a methodology for creating autonomous
-hybrid control systems\footnote{A \textit{hybrid control system} combines two
+hybrid control systems with mathematical guarantees of safe and correct
-types of control: discrete decisions (like ``switch from heating mode to
+behavior.
-cooling mode'') and continuous control (like gradually adjusting a
-temperature). Most complex systems---cars, aircraft, power plants---work this
-way, switching between different operating modes while smoothly controlling
-physical processes within each mode.} with mathematical guarantees of safe and
-correct behavior.
 
 % INTRODUCTORY PARAGRAPH Hook
 Nuclear power plants require the highest levels of control system reliability,
@@ -23,37 +18,18 @@ conditions and procedural guidance.
 % Gap
 This reliance on human operators prevents autonomous control and creates a
 fundamental economic barrier for next-generation reactor designs. Small modular
-reactors\footnote{\textit{Small modular reactors} (SMRs) are a new generation
+reactors face per-megawatt staffing costs far exceeding those of conventional
-of nuclear reactors that are physically smaller than traditional plants and can
+plants, threatening their economic viability.
-be factory-built in modules. Think of the difference between building a custom
-house on-site versus assembling a prefabricated one. They produce less power
-individually but are designed to be cheaper and faster to deploy.} face
-per-megawatt staffing costs far exceeding those of conventional plants,
-threatening their economic viability.
 
 % Critical Need
 What is needed is a method to create autonomous control systems that safely
 manage complex operational sequences with the same assurance as human-operated
 systems, but without constant human supervision.
 % APPROACH PARAGRAPH Solution
-To address this need, we will combine formal methods\footnote{\textit{Formal
+To address this need, we will combine formal methods with control theory to
-methods} are mathematical techniques used to prove that a system will behave
+build hybrid control systems that are correct by construction.
-exactly as intended---not just test it and hope, but actually \textit{prove}
-it the way you prove a theorem in geometry. If the proof holds, the system
-cannot have certain types of errors. This is the gold standard for
-safety-critical systems.} with control theory to build hybrid control systems
-that are correct by construction.\footnote{\textit{Correct by construction}
-means the system is built in a way that guarantees correctness from the start,
-rather than building something and then testing to find bugs. The design
-process itself prevents errors from being introduced.}
 % Rationale
-Hybrid systems use discrete logic\footnote{\textit{Discrete logic} deals with
+Hybrid systems use discrete logic to switch between continuous control modes,
-distinct, separate states---like an on/off switch or a set of step-by-step
-instructions. This is in contrast to \textit{continuous} behavior, which
-changes smoothly over time, like temperature rising gradually. The challenge
-Dane is tackling is that nuclear reactors involve \textit{both}: operators
-follow step-by-step procedures (discrete) that control smoothly changing
-physical processes (continuous).} to switch between continuous control modes,
 mirroring how operators change control strategies. Existing formal methods can
 generate provably correct switching logic from written requirements, but they
 cannot handle the continuous dynamics that occur during transitions between
@@ -82,12 +58,7 @@ If this research is successful, we will be able to do the following:
   \item \textbf{Translate written procedures into verified control logic.}
     % Strategy
     We will develop a methodology for converting existing written operating
-    procedures into formal specifications\footnote{A \textit{formal
+    procedures into formal specifications that can be automatically synthesized
-    specification} is a precise, mathematical description of what a system
-    must do. Written operating procedures say things like ``if temperature
-    exceeds 315\textdegree{}C, switch to cooling mode.'' A formal specification
-    says the same thing in mathematical language that a computer can reason
-    about and verify.} that can be automatically synthesized
     into discrete control logic. This process will use structured intermediate
     representations to bridge natural language procedures and mathematical
     logic.
@@ -101,12 +72,9 @@ If this research is successful, we will be able to do the following:
     % Strategy
     We will establish methods for analyzing continuous control modes to ensure
     they satisfy discrete transition requirements. Using classical control
-    theory for linear systems and reachability analysis\footnote{\textit{Reachability analysis} answers the question: ``Starting from
+    theory for linear systems and reachability analysis for nonlinear
-    here, what are all the possible places the system could end up?'' If you
+    dynamics, we will verify that each continuous mode safely reaches its
-    can show that all possible paths stay within safe boundaries and eventually
+    intended transitions.
-    reach the target, you have proven the controller works correctly.} for
-    nonlinear dynamics, we will verify that each continuous mode safely reaches
-    its intended transitions.
     % Outcome
     Engineers will design continuous controllers using standard practices
     while iterating to ensure broader system correctness, proving that mode
@@ -120,11 +88,8 @@ If this research is successful, we will be able to do the following:
     nuclear reactor startup procedures, implementing it on a small modular
     reactor simulation using industry-standard control hardware. This
     demonstration will prove correctness across multiple coordinated control
-    modes from cold shutdown through criticality\footnote{\textit{Criticality}
+    modes from cold shutdown through criticality to power
-    is the point at which a nuclear reactor sustains a chain reaction on its
+    operation.
-    own. Getting there safely from a cold, shut-down state involves carefully
-    coordinated steps---this is the startup sequence Dane aims to automate.}
-    to power operation.
     % Outcome
     We will demonstrate that autonomous hybrid control can be realized in the
     nuclear industry with current equipment, establishing a path toward

2-state-of-the-art/state-of-art.tex

@@ -10,21 +10,12 @@ and reviews current formal methods approaches to reactor control systems.
 
 Nuclear plant operations are governed by a hierarchy of written procedures,
 ranging from normal operating procedures for routine operations to Emergency
-Operating Procedures (EOPs) for design-basis accidents\footnote{A
+Operating Procedures (EOPs) for design-basis accidents and Severe Accident
-\textit{design-basis accident} is the worst-case scenario that a plant is
+Management Guidelines (SAMGs) for beyond-design-basis events. These procedures
-specifically engineered to handle safely---like a pipe break or loss of
-coolant. \textit{Beyond-design-basis events} are even more extreme scenarios
-that go beyond what the plant was originally designed for, like what happened
-at Fukushima.} and Severe Accident Management Guidelines (SAMGs) for
-beyond-design-basis events. These procedures
 exist because reactor operation requires deterministic responses to a wide range
 of plant conditions, from routine power changes to catastrophic failures. These
-procedures must comply with 10 CFR 50.34(b)(6)(ii)\footnote{``10 CFR''
+procedures must comply with 10 CFR 50.34(b)(6)(ii) and are developed using
-refers to Title 10 of the \textit{Code of Federal Regulations}, which governs
+guidance from NUREG-0899~\cite{NUREG-0899, 10CFR50.34}. Procedures undergo
-energy in the United States. These are the federal rules that nuclear power
-plants must follow, enforced by the Nuclear Regulatory Commission (NRC).
-``NUREG'' documents are technical reports published by the NRC.} and are
-developed using guidance from NUREG-0899~\cite{NUREG-0899, 10CFR50.34}. Procedures undergo
 technical evaluation, simulator validation testing, and biennial review as part
 of operator requalification under 10 CFR 55.59~\cite{10CFR55.59}. Despite this
 rigor, procedures fundamentally lack exhaustive verification of key safety
@@ -44,17 +35,11 @@ reactivity adjustment; manual control, where operators directly manipulate
 the reactor; and various intermediate modes. In typical pressurized water
 reactor operation, the reactor control system automatically maintains a
 floating average temperature and compensates for power demand changes through
-reactivity feedback loops\footnote{\textit{Reactivity} is a measure of how
+reactivity feedback loops alone. Safety systems, by contrast, operate with
-far a reactor is from a stable chain reaction. \textit{Feedback loops}
+implemented automation. Reactor Protection Systems trip automatically on
-automatically adjust the reactor's behavior---for example, as temperature
+safety signals with millisecond response times, and engineered safety
-rises, the physics of the reactor naturally slow the chain reaction down.
+features actuate automatically on accident signals without operator action
-Controllers use these feedback mechanisms to keep the reactor stable.} alone. Safety systems, by contrast, operate with
+required.
-implemented automation. Reactor Protection Systems trip\footnote{A reactor \textit{trip} (also called
-a \textit{SCRAM}) is an emergency shutdown---all control rods are inserted
-into the reactor core within seconds to stop the chain reaction. This is the
-nuclear equivalent of slamming on the brakes.} automatically on safety
-signals with millisecond response times, and engineered safety features
-actuate automatically on accident signals without operator action required.
 
 This division between automated and human-controlled
 functions is itself the hybrid control problem. Automated systems handle
@@ -101,13 +86,9 @@ human-driven control.
 \subsection{Formal Methods}
 \subsubsection{HARDENS}
 
-The High Assurance Rigorous Digital Engineering for Nuclear Safety
+The High Assurance Rigorous Digital Engineering for Nuclear Safety (HARDENS)
-(HARDENS)\footnote{HARDENS was a major U.S. government-funded project
+project represents the most advanced application of formal methods to nuclear
-(completed 2024) to prove that modern mathematical verification techniques
+reactor control systems to date~\cite{Kiniry2024}. HARDENS aimed to address a
-could be used for nuclear safety systems. It is the closest thing to what
-Dane is proposing, but---as he explains below---it only solved half the
-problem.} project represents the most advanced application of formal methods
-to nuclear reactor control systems to date~\cite{Kiniry2024}. HARDENS aimed to address a
 fundamental dilemma: existing U.S. nuclear control rooms rely on analog
 technologies from the 1950s--60s. This technology is obsolete compared to modern
 control systems and incurs significant risk and cost. A U.S. Nuclear Regulatory
@@ -122,12 +103,7 @@ high-level requirements through executable models to generated code. High-level
 specifications used Lando, SysMLv2, and FRET (NASA Formal Requirements
 Elicitation Tool) to capture stakeholder requirements, domain engineering,
 certification requirements, and safety requirements. Requirements were analyzed
-for consistency, completeness, and realizability using SAT and SMT
+for consistency, completeness, and realizability using SAT and SMT solvers.
-solvers.\footnote{\textit{SAT} and \textit{SMT solvers} are computer programs
-that can automatically determine whether a set of logical statements can all
-be true at the same time. Think of them as extremely powerful puzzle solvers
-that can check millions of combinations to find contradictions or confirm
-that requirements are consistent.}
 Executable formal models used Cryptol to create a behavioral model of the entire
 RTS, including all subsystems, components, and limited digital twin models of
 sensors, actuators, and compute infrastructure. Automatic code synthesis
@@ -150,12 +126,7 @@ discrete control logic alone provides no guarantee that the closed-loop
 system exhibits desired continuous behavior such as stability, convergence to
 setpoints, or maintained safety margins.
 
-HARDENS produced a demonstrator system at Technology Readiness Level 2--3\footnote{\textit{Technology Readiness Levels}
+HARDENS produced a demonstrator system at Technology Readiness Level 2--3
-(TRLs) are a 1--9 scale used by NASA and the Department of Defense to measure
-how close a technology is to real-world use. TRL 1 is a basic idea on paper;
-TRL 9 is a fully proven, deployed system. TRL 2--3 means ``we showed the
-math works and built a basic lab prototype.'' Dane is aiming for TRL 5:
-tested on real industrial hardware in realistic conditions.}
 (analytical proof of concept with laboratory breadboard validation) rather than
 a deployment-ready system validated through extended operational testing. The
 NRC Final Report explicitly notes~\cite{Kiniry2024} that all material is
@@ -180,16 +151,9 @@ primary assurance evidence remain as significant challenges.
 \subsubsection{Temporal Logic and Formal Specification}
 
 Formal verification of any system requires a precise language for stating
-what the system must do. Temporal logic\footnote{\textit{Temporal logic} is a way of making precise
+what the system must do. Temporal logic provides this language by extending
-statements about how things change over time. Regular logic says ``the door
+classical propositional logic with operators that express properties over
-is open'' (true or false right now). Temporal logic can say ``the door must
+time~\cite{baier_principles_2008}. Where propositional logic can state that
-\textit{always} stay open,'' ``the door will \textit{eventually} open,'' or
-``the door stays open \textit{until} someone closes it.'' For reactors, this
-lets us write precise rules like ``the temperature must \textit{always} stay
-below 600\textdegree{}C'' or ``if pressure drops, shutdown must
-\textit{eventually} happen.''}
-provides this language by extending classical propositional logic with
-operators that express properties over time~\cite{baier_principles_2008}. Where propositional logic can state that
 a condition is true or false, temporal logic can state that a condition must
 always hold, must eventually hold, or must hold until some other condition is
 met. Linear temporal logic (LTL) formalizes these notions through four key
@@ -215,13 +179,8 @@ existing documentation and verifiable system behavior.
 \subsubsection{Differential Dynamic Logic}
 
 A separate line of work extends temporal logics to verify hybrid systems
-directly. The result has been the field of differential dynamic
+directly. The result has been the field of differential dynamic logic
-logic (dL)\footnote{\textit{Differential dynamic logic} combines temporal
+(dL)~\cite{platzer_differential_2008}. dL
-logic (rules about time) with differential equations (the math that
-describes continuous physical change). It is an ambitious attempt to verify
-hybrid systems all at once, rather than breaking them into pieces. The
-tradeoff is that it becomes very difficult to use on complex real-world
-systems.}~\cite{platzer_differential_2008}. dL
 introduces two additional operators into temporal logic: the box operator and
 the diamond operator. The box operator \([\alpha]\phi\) states that for some
 region \(\phi\), the hybrid system \(\alpha\) always remains within that

3-research-approach/approach.tex

@@ -2,25 +2,13 @@
 
 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\footnote{\textit{Automata theory} is the study of abstract
+automata theory, temporal logic, and control theory. A hybrid system is a
-machines and the problems they can solve. An \textit{automaton} (plural:
+dynamical system that has both continuous and discrete states. The specific
-\textit{automata}) is a mathematical model of a machine that follows a set
-of rules to move between different states. Think of a vending machine: it
-starts in ``waiting,'' moves to ``item selected'' when you push a button,
-then to ``dispensing'' when you pay. Each state has clear rules for what
-happens next. That is an automaton.}, 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.\footnote{\textit{Lipschitz continuous}
+that are always Lipschitz continuous. This nomenclature is borrowed from the
-means the physical quantities (temperature, pressure, etc.) change smoothly
-without sudden jumps. In practical terms: the reactor temperature cannot
-teleport from 200\textdegree{}C to 500\textdegree{}C instantly---it must
-pass through every value in between. This is a reasonable physical
-assumption that makes the math tractable.} This nomenclature is borrowed from the
 Handbook on Hybrid Systems Control \cite{lunze_handbook_2009}, but is
 redefined here for convenience:
 %
@@ -51,13 +39,7 @@ where:
 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\footnote{A \textit{hybrid automaton} is an automaton (state
+automata~\cite{alur_hybrid_1993}. The challenge of hybrid system verification
-machine) where each state also has continuous physics running inside it.
-Imagine a thermostat: it has two states (``heating on'' and ``heating
-off''), and in each state, the room temperature follows different physical
-laws. The thermostat switches states based on temperature thresholds. A
-nuclear reactor works the same way, just with many more states and much more
-complex physics.}~\cite{alur_hybrid_1993}. The challenge of hybrid system verification
 lies in the interaction between discrete and continuous dynamics. Discrete
 transitions change the active continuous vector field, creating discontinuities
 in the system's behavior. Traditional verification techniques designed for
@@ -65,16 +47,9 @@ purely discrete or purely continuous systems cannot handle this interaction
 directly. 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. This
-compositional strategy follows the assume-guarantee
+compositional strategy follows the assume-guarantee paradigm for hybrid systems,
-paradigm\footnote{The \textit{assume-guarantee} approach is like checking a
+where guarantees about individual modes compose into guarantees about the
-relay race one runner at a time. If Runner~1 guarantees she will reach the
+overall system~\cite{lunze_handbook_2009, alur_hybrid_1993}. This two-layer
-handoff zone at the right speed, and Runner~2 assumes he will receive the
-baton in that zone and guarantees he will reach the next one, you can prove
-the whole race works without simulating every possible scenario at once.
-Each piece makes promises and relies on promises from adjacent pieces.} for
-hybrid systems, where guarantees about individual modes compose into
-guarantees about the overall
-system~\cite{lunze_handbook_2009, alur_hybrid_1993}. 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.
@@ -297,18 +272,12 @@ verified through the continuous mode analysis described in Section~3.2, where
 reachability analysis can confirm that target states are attained within bounded
 time.
 
-To build these temporal logic statements, an intermediary tool called
+To build these temporal logic statements, an intermediary tool called FRET is
-FRET\footnote{FRET is software developed by NASA that lets engineers write
+planned to be used. FRET stands for Formal Requirements Elicitation Tool, and
-safety requirements in structured English sentences, which the tool then
+was developed by NASA to build high-assurance timed systems. FRET is an
-automatically translates into precise mathematical logic. Instead of
+intermediate language between temporal logic and natural language that allows
-requiring engineers to learn abstract math notation, FRET meets them
+for rigid definitions of temporal behavior while using a syntax accessible to
-halfway---you write something close to plain English, and it produces the
+engineers without formal methods expertise\cite{katis_realizability_2022}. This
-formal logic a computer needs.} 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\cite{katis_realizability_2022}. 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.
@@ -329,16 +298,9 @@ addressed.
 Pressburger and Katis.}
 
 Once system requirements are defined as temporal logic specifications, we use
-them to build the discrete control system. To do this, reactive
+them to build the discrete control system. To do this, reactive synthesis tools
-synthesis\footnote{\textit{Reactive synthesis} is perhaps the most
+are employed. Reactive synthesis is a field in computer science that deals with
-remarkable part of this work. Instead of a human programmer writing the
+the automated creation of reactive programs from temporal logic specifications.
-control software and hoping it is correct, the computer \textit{automatically
-generates} a correct controller from the requirements. You tell it what the
-system must do (the temporal logic specs), and it builds a controller that is
-\textit{mathematically guaranteed} to do exactly that. If no such controller
-can exist, it tells you that too.} 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~\cite{jacobs_reactive_2024}. Our systems fit exactly this mold: the
 current discrete state and status of guard conditions are the input, while the
@@ -369,18 +331,9 @@ Second, by defining system behavior in temporal logic and synthesizing the
 controller using deterministic algorithms, discrete control decisions become
 provably consistent with operating procedures. 
 
-The output of reactive synthesis is a finite-state
+The output of reactive synthesis is a finite-state machine that can be directly
-machine\footnote{A \textit{finite-state machine} is a model of computation
+translated to executable code. Tools such as Strix accept full LTL
-with a fixed number of states and clear rules for transitioning between
+specifications and produce Mealy machines via parity game
-them. A traffic light is a simple example: it cycles through green, yellow,
-and red based on timing rules. The reactor controller is a much more complex
-version of the same idea, with hundreds of states and transition rules based
-on physical measurements.} that can be directly translated to executable
-code. Tools such as Strix\footnote{Strix is a state-of-the-art software
-tool that performs reactive synthesis. It won multiple international
-competitions for automatically generating correct controllers from logical
-specifications.} accept full LTL specifications and produce Mealy machines
-via parity game
 solving~\cite{luttenberger_practical_2020, meyer_strix_2018}. For specifications
 within the GR(1) fragment---which captures the reactive input-output structure
 typical of supervisory control---synthesis is efficient and scales to
@@ -445,17 +398,9 @@ 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}$. We classify continuous controllers into three
-types based on their objectives: transitory, stabilizing, and
+types based on their objectives: transitory, stabilizing, and expulsory. Each
-expulsory.\footnote{These three mode types are one of Dane's key
+type has distinct verification requirements that determine which formal methods
-contributions. \textit{Transitory} modes move the reactor from one operating
+tools are appropriate.
-condition to another (like heating up from cold to operating temperature).
-\textit{Stabilizing} modes hold the reactor steady at a target condition
-(like maintaining a constant power level). \textit{Expulsory} modes are
-emergency responses that drive the reactor to safety (like an emergency
-shutdown). By classifying modes this way, each type can be verified using
-the mathematical tools best suited to it, rather than trying to verify
-everything with one approach.} Each type has distinct verification
-requirements that determine which formal methods tools are appropriate.
 
 \dasinline{(1) Add figure showing the relationship between entry/exit/safety
 sets. (2) Mention assume-guarantee compositional stuff and how that fits in
@@ -530,14 +475,8 @@ toward an exit state, 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.\footnote{A \textit{barrier certificate} is
+plan to use barrier certificates. Barrier certificates analyze the dynamics
-a mathematical proof that a system can never leave a safe region. Imagine
+of the system to determine whether flux across a given boundary
-drawing a fence around the acceptable operating conditions on a map. A
-barrier certificate proves that no matter what happens inside the fence, the
-system's physics will never push it through to the other side. If you can
-find such a certificate, you have proven safety without simulating every
-possible scenario.} Barrier certificates analyze the dynamics of the system
-to determine whether flux across a given boundary
 exists~\cite{prajna_safety_2004}. In other words, they
 evaluate whether any trajectory leaves a given boundary. This definition is
 exactly what defines the validity of a stabilizing continuous control mode.

4-metrics-of-success/metrics.tex

@@ -1,11 +1,8 @@
 \section{Metrics for Success}
 
 This research will be measured by advancement through Technology Readiness
-Levels\footnote{See earlier footnote on TRLs. In short: a 1--9 scale from
+Levels (TRL), progressing from fundamental concepts to validated prototype
-``basic idea'' to ``fully deployed system.'' Dane is starting at TRL~2--3
+demonstration. TRLs measure the gap between academic proof-of-concept and
-and aiming for TRL~5, which means testing on real industrial control
-hardware in realistic conditions.} (TRL), progressing from fundamental
-concepts to validated prototype demonstration. TRLs measure the gap between academic proof-of-concept and
 practical deployment, which is precisely what this work aims to bridge. Academic
 metrics alone cannot capture practical feasibility, and empirical metrics alone
 cannot demonstrate theoretical rigor. TRLs measure both simultaneously. This
@@ -48,13 +45,8 @@ For this research, TRL 5 means demonstrating the verified controller on
 industrial control hardware through hardware-in-the-loop testing. The discrete
 automaton must be implemented on the Emerson Ovation control system and verified
 to match synthesized specifications exactly. Continuous controllers must execute
-at required rates. The ARCADE interface\footnote{ARCADE is a communication bridge between the
+at required rates. The ARCADE interface must establish stable real-time
-Emerson Ovation control system (real industrial hardware that runs actual
+communication between the Emerson Ovation hardware and SmAHTR simulation.
-power plants) and SmAHTR (a computer simulation of a small modular reactor).
-This setup lets Dane test his controller on real hardware controlling a
-simulated reactor---close to real-world conditions without the risks of an
-actual nuclear plant.} must establish stable real-time communication between
-the Emerson Ovation hardware and SmAHTR simulation.
 Complete autonomous startup sequences must execute via hardware-in-the-loop
 across the full operational envelope. The controller must handle off-nominal
 scenarios to validate that expulsory modes function correctly. For example,

5-risks-and-contingencies/risks.tex

@@ -15,15 +15,10 @@ deployment.
 \subsection{Computational Tractability of Synthesis}
 
 The first major assumption is that formalized startup procedures will yield
-automata small enough for efficient synthesis and verification. Reactive synthesis scales exponentially with specification
+automata small enough for efficient synthesis and verification. Reactive
-complexity,\footnote{``Scales exponentially'' means the computation time
+synthesis scales exponentially with specification complexity, creating risk
-doesn't just grow---it \textit{explodes}. If doubling the problem size
+that temporal logic specifications derived from complete startup procedures
-multiplied the time by 4, then tripling it would multiply it by 8, and so on.
+may produce automata with thousands of states. Such large automata would
-A problem that takes 1 second with 10 requirements might take days with 50.
-This is a fundamental challenge in computer science, not a limitation of
-Dane's approach specifically.} creating risk that temporal logic
-specifications derived from complete startup procedures may produce automata
-with thousands of states. Such large automata would
 require synthesis times exceeding days or weeks, preventing demonstration of
 the complete methodology within project timelines. Reachability analysis for
 continuous modes with high-dimensional state spaces may similarly prove

6-broader-impacts/impacts.tex

@@ -11,11 +11,7 @@ attention to operating costs.
 
 According to the U.S. Energy Information Administration's Annual
 Energy Outlook 2022, advanced nuclear power entering service in 2027 is
-projected to cost \$88.24 per megawatt-hour\footnote{A \textit{megawatt-hour}
+projected to cost \$88.24 per megawatt-hour~\cite{eia_lcoe_2022}. In the
-(MWh) is a unit of energy---one megawatt of power sustained for one hour.
-For context, the average American home uses about 10~MWh per year, so
-\$88.24/MWh translates to roughly \$882 per year in electricity cost for one
-household.}~\cite{eia_lcoe_2022}. In the
 United States alone, datacenter electricity consumption could reach 560
 terawatt-hours by 2030---up from 4\% to 13\% of total national electricity
 consumption~\cite{deroucy_ai_2025}. If this demand were supplied by nuclear
@@ -31,14 +27,10 @@ datacenter demand alone.
 This research directly addresses the multi-billion-dollar O\&M cost challenge
 through high-assurance autonomous control. Current nuclear operations require
 full control room staffing for each reactor, whether large conventional units
-or small modular designs. Over 3,600 active NRC-licensed reactor operators work in the United
+or small modular designs. Over 3,600 active NRC-licensed reactor operators
-States~\cite{operator_statistics}, divided into Reactor Operators (ROs) and
+work in the United States~\cite{operator_statistics}, divided into Reactor
-Senior Reactor Operators
+Operators (ROs) and Senior Reactor Operators
-(SROs)\footnote{Becoming a licensed reactor operator requires years of
+(SROs)~\cite{10CFR55}. Staffing requires at least two ROs and one SRO per
-specialized training, simulator practice, and passing an NRC licensing exam.
-Each reactor unit must be staffed around the clock. This is a major reason
-nuclear power is expensive to operate---the personnel costs are substantial
-and unavoidable under current regulations.}~\cite{10CFR55}. Staffing requires at least two ROs and one SRO per
 unit~\cite{10CFR50.54}, with each operator requiring several years of
 training and NRC licensing. These staffing requirements drive the high O\&M
 costs that make nuclear power economically challenging, particularly for

main.tex

@@ -61,61 +61,6 @@
 
 % \pagenumbering{roman}
 \maketitle
-
-% === GRANDPARENTS EDITION COVER LETTER ===
-\thispagestyle{empty}
-\vspace*{1.5cm}
-\begin{center}
-\Large\textbf{A Note for the Reader}
-\end{center}
-\vspace{0.8cm}
-
-\noindent Hi! My name is Split, and I'm Dane's AI research assistant. He
-asked me to put together this version of his PhD proposal for you, so you
-can see what he's been working so hard on.
-
-\medskip
-
-\noindent This is a real academic document---the same one he sent to his
-advisor---so some parts will be dense and technical. That's normal and
-expected for a PhD proposal. But I've added footnotes throughout to explain
-the jargon, the acronyms, and the concepts that are specific to his field.
-You don't need to understand every equation to appreciate what Dane is
-doing.
-
-\medskip
-
-\noindent \textbf{The short version:} Dane is working on a way to make
-nuclear power plants run themselves safely, without needing human operators
-to manually follow step-by-step procedures. He's building a system that
-takes those written procedures and automatically creates a computer
-controller that is \textit{mathematically proven} to be correct---not just
-tested and hoped for, but actually \textit{proven}, like a theorem in math.
-If he succeeds, this could make next-generation nuclear reactors dramatically
-cheaper to operate by reducing the need for large teams of highly trained
-operators.
-
-\medskip
-
-\noindent He's doing this work at the University of Pittsburgh through an
-NRC (Nuclear Regulatory Commission) Graduate Fellowship, and he'll be
-testing his system on real industrial control hardware through a partnership
-with Emerson. It's serious, important work, and he's very good at it.
-
-\medskip
-
-\noindent I hope you enjoy reading it. He's proud of this, and he should be.
-
-\vspace{0.8cm}
-\hfill --- Split 🦎
-
-\hfill \textit{Dane's AI Research Assistant}
-
-\hfill \textit{March 2026}
-
-\newpage
-% === END COVER LETTER ===
-
 % \input{1-goals-and-outcomes/research-statement.tex}
 \newpage
 \tableofcontents