Editorial pass: tactical, operational, and strategic improvements

TACTICAL (sentence-level):
- Improved topic-stress positioning throughout (moved known info to sentence start, new info to stress position)
- Strengthened verb choices (replaced weak verbs with stronger alternatives)
- Fixed awkward passive constructions
- Improved sentence flow and readability

OPERATIONAL (paragraph/section):
- Enhanced transitions between subsections with connecting phrases
- Improved coherence within sections (esp. state-of-the-art formal methods transitions)
- Strengthened logical progression between major subsections

STRATEGIC (document-level):
- Reinforced Heilmeier catechism alignment at section boundaries
- Improved section-to-section linkages (sections 3→4, 4→5, 5→6)
- Made explicit connections between sections and their assigned Heilmeier questions
- Strengthened the narrative arc from methodology through metrics to risks to impact

1-goals-and-outcomes/research_statement_v1.tex

@@ -4,7 +4,7 @@ This research develops autonomous control systems with mathematical guarantees o
 % INTRODUCTORY PARAGRAPH Hook
 Extensively trained operators manage nuclear reactors by following detailed written procedures. Plant conditions guide their decisions when they switch between control objectives.
 % Gap
-Small modular reactors face a fundamental economic challenge: their per-megawatt staffing costs significantly exceed those of conventional plants, threatening their viability. Autonomous control systems must manage complex operational sequences safely—without constant supervision—while providing assurance equal to or exceeding that of human-operated systems.
+Small modular reactors face a fundamental economic challenge: their per-megawatt staffing costs significantly exceed those of conventional plants, threatening viability. Autonomous control systems must manage complex operational sequences safely—without constant supervision—while providing assurance equal to or exceeding that of human-operated systems.
 
 % APPROACH PARAGRAPH Solution
 We combine formal methods from computer science with control theory to
@@ -16,7 +16,7 @@ generate provably correct switching logic but cannot handle continuous dynamics
 during transitions. Control theory verifies continuous behavior but
 cannot prove the correctness of discrete switching decisions. 
 % Hypothesis and Technical Approach
-Our methodology bridges this gap in three stages. First, we translate written
+Our methodology bridges this gap through three stages. First, we translate written
 operating procedures into temporal logic specifications using NASA's Formal
 Requirements Elicitation Tool (FRET). FRET structures requirements into scope,
 condition, component, timing, and response elements. Realizability
@@ -24,11 +24,11 @@ checking identifies conflicts and ambiguities before implementation.
 Second, reactive synthesis generates deterministic automata that are provably
 correct by construction.
 Third, we design continuous controllers for each discrete mode using standard
-control theory and verify them using reachability analysis. We classify continuous modes by their transition objectives. Assume-guarantee contracts and barrier certificates prove that mode transitions occur safely. This approach enables local verification of continuous modes
+control theory and verify them using reachability analysis. We classify continuous modes by their transition objectives. Assume-guarantee contracts and barrier certificates prove that mode transitions occur safely. Local verification of continuous modes
-without requiring global trajectory analysis across the entire hybrid system. An
+becomes possible without requiring global trajectory analysis across the entire hybrid system. This methodology is demonstrated on an
-Emerson Ovation control system demonstrates this methodology. 
+Emerson Ovation control system. 
 % Pay-off
-Autonomous control therefore manages complex nuclear
+Autonomous control can then manage complex nuclear
 power operations while maintaining safety guarantees, directly addressing the economic constraints threatening small modular reactor viability.
 
 % OUTCOMES PARAGRAPHS

1-goals-and-outcomes/v1.tex

@@ -6,7 +6,7 @@ systems with mathematical guarantees of safe and correct behavior.
 
 % INTRODUCTORY PARAGRAPH Hook
 Nuclear power plants require the highest levels of control system reliability.
-Control system failures risk significant economic losses, service interruptions,
+Control system failures risk economic losses, service interruptions,
 or radiological release.
 % Known information
 Nuclear plant operations rely on extensively trained human operators
@@ -16,10 +16,10 @@ manage reactor control. Plant conditions and procedural guidance inform their de
 This reliance on human operators prevents autonomous control and
 creates a fundamental economic challenge for next-generation reactor designs.
 Small modular reactors face per-megawatt staffing costs that far
-exceed those of conventional plants, threatening their economic viability.
+exceed those of conventional plants, threatening economic viability.
-The nuclear industry needs autonomous control systems that manage complex
+The nuclear industry needs autonomous control systems that can manage complex
 operational sequences safely without constant human supervision while providing
-assurance equal to or exceeding human-operated systems.
+assurance equal to or exceeding that of human-operated systems.
 
 % APPROACH PARAGRAPH Solution
 We combine formal methods with control theory to build hybrid control
@@ -27,15 +27,14 @@ systems that are correct by construction.
 % Rationale
 Hybrid systems mirror how operators work: discrete
 logic switches between continuous control modes. Existing formal methods
-generate provably correct switching logic from written requirements but cannot handle continuous dynamics during transitions between modes.
+generate provably correct switching logic from written requirements but cannot handle continuous dynamics during transitions.
 Control theory verifies continuous behavior but cannot prove the correctness of discrete switching decisions. This gap prevents end-to-end correctness guarantees.
 % Hypothesis
 Our approach closes this gap by synthesizing discrete mode transitions directly
 from written operating procedures and verifying continuous behavior between
 transitions. We formalize existing procedures into logical
-specifications and verify continuous dynamics against transition requirements. This approach produces autonomous controllers that are provably free from design
+specifications and verify continuous dynamics against transition requirements. This approach produces autonomous controllers provably free from design
-defects. We conduct this work within the University of Pittsburgh Cyber Energy Center,
+defects. The University of Pittsburgh Cyber Energy Center provides access to industry collaboration and Emerson control hardware, ensuring that solutions developed here align with practical implementation
-which provides access to industry collaboration and Emerson control hardware. Solutions developed here align with practical implementation
 requirements.
 
 % OUTCOMES PARAGRAPHS
@@ -86,8 +85,8 @@ If this research is successful, we will be able to do the following:
 % IMPACT PARAGRAPH Innovation
 These three outcomes—procedure translation, continuous verification, and hardware demonstration—establish a complete methodology from regulatory documents to deployed systems.
 
-\textbf{What is new:} We unify discrete synthesis with continuous verification to enable end-to-end correctness guarantees for hybrid systems.
+\textbf{What is new?} We unify discrete synthesis with continuous verification to enable end-to-end correctness guarantees for hybrid systems.
-Formal methods verify discrete logic. Control theory verifies
+Formal methods verify discrete logic; control theory verifies
 continuous dynamics. No existing methodology bridges both with compositional
 guarantees. This work establishes that bridge by treating discrete specifications
 as contracts that continuous controllers must satisfy, enabling independent
@@ -105,4 +104,13 @@ costs through increased autonomy. This research provides the tools to
 achieve that autonomy while maintaining the exceptional safety record the
 nuclear industry requires.
 
-The following sections systematically answer the Heilmeier Catechism questions that define this research: Section 2 examines the state of the art, establishing what has been done and what remains impossible with current approaches. Section 3 presents our hybrid control synthesis methodology, demonstrating what is new and why it will succeed where prior work has not. Section 4 defines how we measure success through Technology Readiness Level advancement from analytical concepts to hardware demonstration. Section 5 identifies risks that could prevent success and establishes contingencies. Section 6 addresses who cares and why now, examining the economic imperative driving autonomous nuclear control and the broader impact on safety-critical systems. Section 8 provides the research schedule and deliverables, answering how long this work will take.
+The following sections systematically answer the Heilmeier Catechism questions that define this research: 
+\begin{itemize}
+  \item \textbf{Section 2 (State of the Art):} What has been done? What are the limits of current practice?
+  \item \textbf{Section 3 (Research Approach):} What is new? Why will it succeed where prior work has not?
+  \item \textbf{Section 4 (Metrics for Success):} How do we measure success?
+  \item \textbf{Section 5 (Risks and Contingencies):} What could prevent success?
+  \item \textbf{Section 6 (Broader Impacts):} Who cares? Why now? What difference will it make?
+  \item \textbf{Section 8 (Schedule):} How long will it take?
+\end{itemize}
+This structure ensures each section explicitly addresses its assigned questions while building toward a complete research plan.

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

@@ -5,7 +5,7 @@
 \subsection{Current Reactor Procedures and Operation}
 
 Nuclear plant procedures form a hierarchy: normal operating procedures govern routine operations, abnormal operating procedures handle off-normal conditions, Emergency Operating Procedures (EOPs) manage design-basis accidents, Severe Accident Management Guidelines (SAMGs) address beyond-design-basis events, and Extensive Damage Mitigation Guidelines (EDMGs) cover catastrophic damage scenarios. These procedures must comply with 10 CFR 50.34(b)(6)(ii); NUREG-0899
-provides development guidance~\cite{NUREG-0899, 10CFR50.34}. Their development relies on expert judgment and simulator validation—not formal verification. Technical evaluation, simulator validation testing, and biennial review under 10 CFR 55.59~\cite{10CFR55.59} assess procedures rigorously. However, this rigor cannot provide formal verification of key safety properties. No mathematical proof exists that procedures cover all possible plant states, that required actions complete within available timeframes, or that transitions between procedure sets maintain safety invariants.
+provides development guidance~\cite{NUREG-0899, 10CFR50.34}. However, their development relies on expert judgment and simulator validation—not formal verification. Technical evaluation, simulator validation testing, and biennial review under 10 CFR 55.59~\cite{10CFR55.59} assess procedures rigorously, but this rigor cannot provide formal verification of key safety properties. No mathematical proof exists that procedures cover all possible plant states, that required actions complete within available timeframes, or that transitions between procedure sets maintain safety invariants.
 
 \textbf{LIMITATION:} \textit{Procedures lack formal verification of correctness
 and completeness.} Current procedure development relies on expert judgment and
@@ -22,7 +22,7 @@ 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
-alone. Safety systems, by contrast, already employ implemented automation. Reactor
+alone. Safety systems, by contrast, already employ automation. Reactor
 Protection Systems trip automatically on safety signals with millisecond
 response times, and engineered safety features actuate automatically on accident
 signals without requiring operator action.
@@ -37,7 +37,7 @@ startup/shutdown sequences, mode transitions, and procedure implementation.
 
 \subsection{Human Factors in Nuclear Accidents}
 
-Procedures lack formal verification despite rigorous development. This subsection examines the second pillar of current practice: the human operators who execute these procedures. Procedures define what to do; human operators determine when and how to apply them. This approach introduces fundamental reliability limitations.
+Procedures lack formal verification despite rigorous development, but this represents only half the reliability challenge. The second pillar of current practice—human operators who execute these procedures—introduces additional reliability limitations. Procedures define what to do; human operators determine when and how to apply them. Even perfectly written procedures cannot eliminate human error.
 
 Current-generation nuclear power plants employ over 3,600 active NRC-licensed
 reactor operators in the United States~\cite{operator_statistics}. These
@@ -48,21 +48,21 @@ and one SRO for current-generation units~\cite{10CFR50.54}. Becoming a reactor
 operator requires several years of training.
 
 Human error persistently contributes to nuclear safety incidents despite decades
-of improvements in training and procedures, motivating formal automated control with mathematical safety guarantees.
+of improvements in training and procedures. This persistence motivates formal automated control with mathematical safety guarantees.
 Under 10 CFR Part 55, operators hold legal authority to make critical decisions,
 including departing from normal regulations during emergencies. The Three Mile
 Island (TMI) accident demonstrated how personnel error, design
-deficiencies, and component failures combined to cause partial meltdown. Operators
+deficiencies, and component failures combine to cause disaster. Operators
 misread confusing and contradictory indications, then shut off the emergency water
 system~\cite{Kemeny1979}. The President's Commission on TMI identified a
 fundamental ambiguity: placing responsibility for safe power plant operations on
 the licensee without formally verifying that operators can fulfill this
 responsibility does not guarantee safety. This tension between operational
-flexibility and safety assurance remains unresolved: the person responsible for
+flexibility and safety assurance remains unresolved—the person responsible for
 reactor safety often becomes the root cause of failures.
 
 Multiple independent analyses converge on a striking statistic: human error accounts for 70--80\% of
-nuclear power plant events, versus approximately
+nuclear power plant events, compared to approximately
 20\% for equipment failures~\cite{WNA2020}. More significantly, poor safety management and safety
 culture—primarily human factors—caused
 all severe accidents at nuclear power plants: Three Mile Island, Chernobyl, and
@@ -80,18 +80,17 @@ limitations are fundamental to human-driven control, not remediable defects.
 
 \subsection{Formal Methods}
 
-Procedures lack formal verification, and human operators introduce persistent reliability issues. Formal methods offer an alternative: mathematical guarantees of correctness that eliminate both human error and procedural ambiguity. This subsection examines recent formal methods applications in nuclear control and identifies the verification gap that remains for autonomous hybrid systems.
+The limitations are now clear: procedures lack formal verification, and human operators introduce persistent reliability issues despite four decades of training improvements. Formal methods offer an alternative approach: mathematical guarantees of correctness that eliminate both human error and procedural ambiguity. This subsection examines recent formal methods applications in nuclear control and identifies the verification gap that remains for autonomous hybrid systems.
 
-\subsubsection{HARDENS}
+\subsubsection{HARDENS: The State of Formal Methods in Nuclear Control}
 
 The High Assurance Rigorous Digital Engineering for Nuclear Safety (HARDENS)
 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
+HARDENS addressed a fundamental dilemma: existing U.S. nuclear control
-rooms rely on analog technologies from the 1950s--60s. This technology is
+rooms rely on analog technologies from the 1950s--60s. This technology incurs significant risk and
-obsolete compared to modern control systems and incurs significant risk and
+cost compared to modern control systems. The NRC contracted Galois, a formal methods firm, to demonstrate that
-cost. The NRC contracted Galois, a formal methods firm, to demonstrate that
 Model-Based Systems Engineering and formal methods could design, verify, and
 implement a complex protection system meeting regulatory criteria at a fraction
 of typical cost. The project delivered a Reactor Trip System (RTS)
@@ -151,9 +150,9 @@ under harsh environments, human-system interaction in realistic
 operational contexts, and regulatory acceptance of formal methods as
 primary assurance evidence.
 
-\subsubsection{Sequent Calculus and Differential Dynamic Logic}
+\subsubsection{Differential Dynamic Logic: Post-Hoc Hybrid Verification}
 
-HARDENS verified discrete control logic but omitted continuous dynamics—a fundamental limitation for hybrid systems. Other researchers pursued a complementary approach: extending temporal logics to handle hybrid systems directly. This work produced differential dynamic logic (dL). dL introduces two additional operators
+HARDENS verified discrete control logic but omitted continuous dynamics—a fundamental limitation for hybrid systems. Recognizing this gap, other researchers pursued a complementary approach: extending temporal logics to handle hybrid systems directly. This work produced differential dynamic logic (dL). 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 region. In this way, it is a safety
@@ -186,8 +185,10 @@ design loop for complex systems like nuclear reactor startup procedures.
 
 \subsection{Summary: The Verification Gap}
 
+This section answered two Heilmeier questions:
+
 \textbf{What has been done?} Human operators provide operational flexibility but introduce persistent reliability limitations—four decades of training improvements have failed to eliminate them. Formal methods provide correctness guarantees but have not scaled to complete hybrid control design. HARDENS verified discrete logic without continuous dynamics. Differential dynamic logic expresses hybrid properties but requires post-design expert analysis and does not scale to system synthesis.
 
-\textbf{What are the limits of current practice?} No existing methodology synthesizes provably correct hybrid controllers from operational procedures with verification integrated into the design process. This gap—between discrete-only formal methods and post-hoc hybrid verification—prevents autonomous nuclear control with end-to-end correctness guarantees. Closing this gap enables autonomous control that addresses the economic constraints threatening small modular reactor viability while maintaining the safety assurance the nuclear industry requires.
+\textbf{What are the limits of current practice?} No existing methodology synthesizes provably correct hybrid controllers from operational procedures with verification integrated into the design process. This gap—between discrete-only formal methods and post-hoc hybrid verification—prevents autonomous nuclear control with end-to-end correctness guarantees.
 
-Section 3 presents our methodology for bridging this gap through compositional hybrid verification, establishing what is new and why it will succeed.
+The economic imperative is clear: small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants. The technical capability gap is equally clear: current approaches verify either discrete logic or continuous dynamics, never both compositionally. Section 3 presents our methodology for bridging this gap, establishing what is new and why it will succeed where prior work has not.

3-research-approach/v3.tex

@@ -15,9 +15,9 @@
 % ----------------------------------------------------------------------------
 % 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION
 % ----------------------------------------------------------------------------
-Previous approaches to autonomous control verified either discrete switching logic or continuous control behavior—never both simultaneously. Continuous controllers rely on extensive simulation trials for validation. Discrete switching logic undergoes simulated control room testing and human factors research. Neither method provides rigorous guarantees of control system behavior despite consuming enormous resources. HAHACS bridges this gap by composing formal methods from computer science with control-theoretic verification, formalizing reactor operations using hybrid automata.
+Previous approaches to autonomous control verified either discrete switching logic or continuous control behavior—never both simultaneously. Continuous controllers rely on extensive simulation trials for validation; discrete switching logic undergoes simulated control room testing and human factors research. Neither method provides rigorous guarantees of control system behavior despite consuming enormous resources. HAHACS bridges this gap by composing formal methods from computer science with control-theoretic verification to formalize reactor operations using hybrid automata.
 
-Hybrid system verification faces a fundamental challenge: the interaction between discrete and continuous dynamics. Discrete transitions change the governing vector field, creating discontinuities in system behavior. Traditional verification techniques—designed for purely discrete or purely continuous systems—cannot handle this interaction directly. Our methodology decomposes the problem: we verify discrete switching logic and continuous mode behavior separately, then compose them to reason about the complete hybrid system. This two-layer approach mirrors reactor operations, where discrete supervisory logic determines which control mode is active, and continuous controllers govern plant behavior within each mode.
+Hybrid system verification faces a fundamental challenge: the interaction between discrete and continuous dynamics. Discrete transitions change the governing vector field, creating discontinuities in system behavior. Traditional verification techniques—designed for purely discrete or purely continuous systems—cannot handle this interaction directly. Our methodology decomposes the problem by verifying discrete switching logic and continuous mode behavior separately, then composes them to reason about the complete hybrid system. This two-layer approach mirrors reactor operations: discrete supervisory logic determines which control mode is active, while continuous controllers govern plant behavior within each mode.
 
 Building a high-assurance hybrid autonomous control system (HAHACS) requires
 a mathematical description of the system. This work draws on
@@ -52,7 +52,7 @@ where:
 
 Creating a HAHACS requires constructing such a tuple together with proof artifacts that demonstrate the control system's actual implementation satisfies its intended behavior.
 
-\textbf{What is new?} Reactive synthesis, reachability analysis, and barrier certificates each exist independently. Our contribution is the architecture that composes them into a complete methodology for hybrid control synthesis. The novelty lies in three innovations. First, we use discrete synthesis to define entry/exit/safety contracts that bound continuous verification, inverting the traditional approach of verifying a complete hybrid system globally. Second, we classify continuous modes by objective (transitory, stabilizing, expulsory) to select appropriate verification tools, enabling mode-local analysis with provable composition. Third, we leverage existing procedural structure to avoid global hybrid system analysis, making the approach tractable for complex systems like nuclear reactor startup. No prior work integrates these techniques into a systematic design methodology from procedures to verified implementation.
+\textbf{What is new?} Reactive synthesis, reachability analysis, and barrier certificates each exist independently. Our contribution is the architecture that composes them into a complete methodology for hybrid control synthesis. Three innovations provide the novelty. First, discrete synthesis defines entry/exit/safety contracts that bound continuous verification, inverting the traditional approach of verifying a complete hybrid system globally. Second, continuous modes are classified by objective (transitory, stabilizing, expulsory) to select appropriate verification tools, enabling mode-local analysis with provable composition. Third, existing procedural structure is leveraged to avoid global hybrid system analysis, making the approach tractable for complex systems like nuclear reactor startup. No prior work integrates these techniques into a systematic design methodology from procedures to verified implementation.
 
 \textbf{Why will it succeed?} Three factors ensure practical feasibility. First, nuclear procedures already decompose operations into discrete phases with explicit transition criteria—we formalize existing structure rather than impose artificial abstractions. Second, mode-level verification avoids the state explosion that makes global hybrid system analysis intractable, keeping computational complexity bounded by verifying each mode against local contracts. Third, the Emerson collaboration provides both domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility. We demonstrate feasibility on production control systems with realistic reactor models, not merely prove it in principle.
 
@@ -101,8 +101,8 @@ Creating a HAHACS requires constructing such a tuple together with proof artifac
     
   \end{tikzpicture}
   \caption{Simplified hybrid automaton for reactor startup. Each discrete state 
-    $q_i$ has associated continuous dynamics $f_i$. Guard conditions on 
+    $q_i$ has associated continuous dynamics $f_i$. Guard conditions 
-    transitions (e.g., $T_{avg} > T_{min}$) are predicates over continuous 
+    (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.}
@@ -120,18 +120,18 @@ Creating a HAHACS requires constructing such a tuple together with proof artifac
 
 \subsection{System Requirements, Specifications, and Discrete Controllers}
 
-The eight-tuple definition formalizes discrete modes, continuous dynamics, guards, and invariants. This subsection shows how to construct such systems from existing operational knowledge. Nuclear operations already possess a natural hybrid structure that maps directly to this automaton formalism.
+The eight-tuple hybrid automaton formalism provides a mathematical framework for describing discrete modes, continuous dynamics, guards, and invariants. This subsection shows how to construct such systems from existing operational knowledge rather than imposing artificial abstractions. Nuclear operations already possess a natural hybrid structure that maps directly to this automaton formalism.
 
 Human control of nuclear power divides into three scopes: strategic,
 operational, and tactical. Strategic control represents high-level,
-long-term decision making for the plant. This level has objectives that are
+long-term decision making for the plant. Objectives at this level 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 is the
+long, often spanning months or years. The lowest level—the
-tactical level: the individual control of pumps, turbines, and
+tactical level—controls individual components: pumps, turbines, and
 chemistry. Nuclear power
-plants today have already automated tactical control somewhat, generally considered ``automatic control'' when autonomous.
+plants today have already automated tactical control somewhat; such automation is generally considered ``automatic control.''
-These controls are almost always continuous systems with a direct impact on the
+These controls are almost always continuous systems with direct impact on the
 physical state of the plant. Tactical control objectives include maintaining
 pressurizer level, maintaining core temperature, or adjusting reactivity with a
 chemical shim.
@@ -251,15 +251,14 @@ coolant pressure drops, the system initiates shutdown within bounded time'').
 
 We will use FRET (Formal Requirements Elicitation Tool) to build these temporal logic statements. NASA developed FRET for high-assurance timed systems. FRET provides an intermediate language between temporal logic and natural language, enabling rigid definitions of temporal behavior through syntax accessible to engineers without formal methods expertise. This accessibility is crucial for industrial feasibility: reducing required expert knowledge makes these tools adoptable by the current workforce.
 
-A key feature of FRET is the ability to start with logically imprecise
+FRET's key feature is its 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
+specifications for a HAHACS. This approach provides two distinct benefits. First, it draws a direct link from design documentation to digital system
-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
+are insufficient. Human operators may still use these procedures, making any
-room for interpretation is a weakness that must be addressed.
+room for interpretation a weakness that must be addressed.
 
 (Some examples of where FRET has been used and why it will be successful here)
 %%% NOTES (Section 2):
@@ -272,6 +271,8 @@ room for interpretation is a weakness that must be addressed.
 % 3. DISCRETE CONTROLLER SYNTHESIS
 % ----------------------------------------------------------------------------
 
+\subsection{Discrete Controller Synthesis}
+
 With system requirements defined as temporal logic specifications, we now build
 the discrete control system through reactive synthesis.
 Reactive synthesis automates the creation of reactive programs from temporal logic specifications.
@@ -280,25 +281,20 @@ an output. Our systems fit this model: the current discrete state and
 status of guard conditions form the input; the next discrete
 state forms the output. 
 
-Reactive synthesis solves the following problem: given an LTL formula $\varphi$
+Reactive synthesis solves a fundamental 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
+controller can exist. This realizability check provides immediate value: an
 unrealizable specification indicates conflicting or impossible requirements in
-the original procedures. 
+the original procedures, catching errors before implementation. 
 
-Reactive synthesis offers a decisive advantage: the discrete automaton requires no human engineering of its implementation. The resultant automaton is correct by construction, eliminating human error at the implementation stage entirely. Human designers focus their effort where it belongs: on specifying system behavior. This has two critical implications. First, it makes discrete controller creation tractable. The reasons the controller
+Reactive synthesis offers a decisive advantage: the discrete automaton requires no human engineering of its implementation. The resultant automaton is correct by construction, eliminating human error at the implementation stage entirely. Human designers can focus their effort where it belongs: on specifying system behavior rather than implementing switching logic. This shift has two critical implications. First, it provides complete traceability. The reasons the controller
-changes between modes can be traced back to the specification and thus to any
+changes between modes trace back through specifications to requirements, establishing clear liability and justification for system
-requirements, providing a trace for liability and justification of system
+behavior. Second, it replaces probabilistic human judgment with deterministic guarantees. Human operators cannot eliminate error from discrete control decisions; humans are intrinsically fallible. By defining system behavior using temporal logics and synthesizing the controller using deterministic
-behavior. Second, discrete control decisions made by humans depend on the
+algorithms, strategic decisions always follow operating procedures exactly—no exceptions, no deviations, no human factors.
-human operator operating correctly. Humans are intrinsically probabilistic
-and 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.
 
 (Talk about how one would go from a discrete automaton to actual code)
 
@@ -318,9 +314,9 @@ according to operating procedures.
 
 Reactive synthesis produces a provably correct discrete controller from operating procedures. This discrete controller determines when to switch between modes—but hybrid control requires more. The continuous dynamics executing within each discrete mode must also be verified to ensure the complete system behaves correctly.
 
-This subsection describes the continuous control modes that execute within each discrete state and explains how we verify they satisfy the requirements imposed by the discrete layer. Three mode types—transitory, stabilizing, and expulsory—require different verification approaches. 
+This subsection describes the continuous control modes that execute within each discrete state and explains how we verify they satisfy the requirements imposed by the discrete layer. The verification approach depends on control objectives. We classify modes into three types—transitory, stabilizing, and expulsory—each requiring different verification tools matched to their distinct purposes. 
 
-This methodology's scope regarding continuous controller design requires clarification. This work verifies continuous controllers—it does not synthesize them. The distinction parallels model checking in software verification: model checking verifies whether a given implementation satisfies its specification without prescribing how to write the software. We assume engineers can design continuous controllers using standard control theory techniques. Our contribution is the verification framework that confirms candidate controllers compose correctly with the discrete layer to produce a safe hybrid system.
+This methodology's scope regarding continuous controller design requires clarification: this work verifies continuous controllers but does not synthesize them. The distinction parallels model checking in software verification. Model checking verifies whether a given implementation satisfies its specification without prescribing how to write the software. We assume engineers can design continuous controllers using standard control theory techniques. Our contribution is the 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
@@ -328,14 +324,16 @@ discrete state are 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
+discrete state $q_i$ and the associated guards. 
+
+This partitioning of the
 continuous state space among several discrete vector fields has traditionally
 posed 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
+These issues are circumvented by designing the hybrid system from the bottom up
 with verification in mind. The discrete transitions define each continuous
 control mode's input and output sets clearly \textit{a priori}.
 
@@ -384,7 +382,7 @@ dynamics $\dot{x} = f(x, u(x))$, the controller must satisfy:
 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 provides the natural verification tool for transitory modes.
 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:
@@ -402,9 +400,7 @@ reachable within time horizon $T$:
 \]
 
 The discrete controller defines clear boundaries in continuous state
-space, making the verification problem for each transitory mode well-posed. We know
+space, making the verification problem for each transitory mode well-posed. The possible initial conditions, target conditions, and safety envelope are all known. The verification task then confirms that the candidate
-the possible initial conditions, the target conditions, and the
-safety envelope. The verification task confirms that the candidate
 continuous controller achieves the objective from all possible starting points.
 
 Several tools exist for computing reachable sets of hybrid
@@ -427,7 +423,7 @@ appropriate to the fidelity of the reactor models available.
 
 \subsubsection{Stabilizing Modes}
 
-Transitory modes drive the system toward exit conditions. Stabilizing modes, in contrast, maintain the system within a desired operating region indefinitely rather than drive it toward an exit condition. Examples include steady-state power operation, hot standby, and load-following at constant power level. Reachability analysis may not suit validation of stabilizing modes. Instead, we use barrier certificates.
+Transitory modes drive the system toward exit conditions. Stabilizing modes, in contrast, maintain the system within a desired operating region indefinitely. Examples include steady-state power operation, hot standby, and load-following at constant power level. The different control objective requires a different verification approach: reachability analysis answers "can the system reach a target?" while stabilizing modes must prove "does the system stay within bounds?" Barrier certificates provide the appropriate tool.
 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 exactly matches what defines the validity of a
@@ -436,7 +432,7 @@ stabilizing continuous control mode.
 Formally, 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 parallels Lyapunov functions for
-stability: rather than computing trajectories explicitly, we find a certificate
+stability: rather than computing trajectories explicitly, we seek 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
 barrier certificate condition requires:
@@ -479,7 +475,7 @@ controller.
 
 \subsubsection{Expulsory Modes}
 
-Transitory and stabilizing modes handle nominal operations. Expulsory modes handle off-nominal conditions. When the plant deviates from expected behavior, expulsory modes take over to ensure safety. These continuous controllers 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.
+Transitory and stabilizing modes handle nominal operations under the assumption that plant dynamics match the design model. When the plant deviates from expected behavior—through component failures, sensor degradation, or unanticipated disturbances—expulsory modes take over to ensure safety. These continuous controllers prioritize robustness over 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.
 
 Proving controller correctness through reachability and barrier certificates makes detecting physical failures straightforward. The controller cannot be incorrect for the nominal plant model. When an invariant is violated, the plant dynamics must have changed. The HAHACS identifies faults when continuous controllers violate discrete boundary conditions—a direct consequence of verified nominal control modes. Unexpected behavior implies off-nominal conditions.
 
@@ -556,7 +552,13 @@ 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.
 
-This methodology—from procedure formalization through discrete synthesis to continuous verification and hardware implementation—establishes the complete research approach. We have shown what is new (compositional hybrid verification integrated into the design process) and why it will succeed (leveraging existing procedural structure, mode-level analysis, and industrial collaboration). Section 4 defines how we measure success: not through theoretical contributions alone, but through Technology Readiness Level advancement that demonstrates both correctness and practical implementability.
+This section answered two Heilmeier questions:
+
+\textbf{What is new?} Reactive synthesis, reachability analysis, and barrier certificates are integrated into a compositional architecture for hybrid control synthesis. The methodology inverts traditional approaches by using discrete synthesis to define verification contracts, classifies continuous modes to select appropriate verification tools, and leverages existing procedural structure to avoid intractable global analysis.
+
+\textbf{Why will it succeed?} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria—the methodology formalizes existing structure rather than imposing artificial abstractions. Mode-level verification avoids state explosion by bounding each verification problem locally. The Emerson collaboration provides domain expertise to validate procedure formalization and industrial hardware to demonstrate practical implementation.
+
+Having established the complete methodology—from procedure formalization through discrete synthesis to continuous verification and hardware implementation—the next question becomes: how do we measure success? Section 4 addresses this question by defining Technology Readiness Level advancement as the primary metric, demonstrating both theoretical correctness and practical implementability as the system progresses from component validation to integrated hardware testing.
 
 %%% NOTES (Section 5):
 % - Get specific details on ARCADE interface from Emerson collaboration

4-metrics-of-success/v1.tex

@@ -9,12 +9,12 @@ system components operate successfully in a relevant laboratory environment.
 This section explains why TRL advancement provides the most appropriate success
 metric and defines specific criteria for TRL 5.
 
-Technology Readiness Levels provide the ideal success metric: they
+Technology Readiness Levels provide the ideal success metric by
-explicitly measure the gap between academic proof-of-concept and practical
+explicitly measuring the gap between academic proof-of-concept and practical
 deployment—precisely what this work aims to bridge. Academic metrics like
 papers published or theorems proved cannot capture practical feasibility.
 Empirical metrics like simulation accuracy or computational speed cannot
-demonstrate theoretical rigor. Only TRLs measure both simultaneously.
+demonstrate theoretical rigor. TRLs alone measure both simultaneously.
 Advancing from TRL 3 to TRL 5 requires maintaining theoretical rigor while
 progressively demonstrating practical feasibility. Formal verification must
 remain valid as the system moves from individual components to integrated
@@ -82,11 +82,11 @@ development status indicates progress toward TRL 3. Synthesis results and
 verification coverage indicate progress toward TRL 4. Simulation performance
 metrics and hardware integration milestones indicate progress toward TRL 5. The
 research plan will be revised only when new data invalidates fundamental
-assumptions. This research succeeds if it achieves TRL 5 by demonstrating a
+assumptions. This research succeeds by achieving TRL 5: demonstrating a
 complete autonomous hybrid controller with formal correctness guarantees
 operating on industrial control hardware through hardware-in-the-loop testing in
 a relevant laboratory environment. This establishes both theoretical validity
 and practical feasibility, proving the methodology produces verified
 controllers implementable with current technology.
 
-TRL advancement provides clear success criteria, but reaching TRL 5 depends on several critical assumptions. If these assumptions prove false, the research may stall at lower readiness levels. The next section identifies the primary risks, their early warning indicators, and contingency plans that preserve research value even if core assumptions fail.
+This section established how we measure success: TRL advancement from 2--3 to 5 demonstrates both theoretical correctness and practical feasibility. However, reaching TRL 5 depends on several critical assumptions. If these assumptions prove false, the research may stall at lower readiness levels despite sound methodology. Section 5 addresses the Heilmeier question \textbf{What could prevent success?} by identifying the primary risks, their early warning indicators, and contingency plans that preserve research value even if core assumptions fail.

5-risks-and-contingencies/v1.tex

@@ -13,14 +13,13 @@ publishable results while clearly identifying remaining barriers to deployment.
 
 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 complexity, creating the risk that
+synthesis scales exponentially with specification complexity. Temporal logic specifications derived from complete startup procedures may
-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 us from demonstrating the
+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
 computationally intractable. Either barrier would constitute a fundamental
-obstacle to achieving our research objectives.
+obstacle to achieving research objectives.
 
 Several indicators would provide early warning of computational tractability
 problems. Synthesis times exceeding 24 hours for simplified procedure subsets
@@ -37,8 +36,8 @@ minimal viable startup sequence covering only cold shutdown to criticality to lo
 
 \subsection{Discrete-Continuous Interface Formalization}
 
-Computational tractability represents one dimension of risk. A more fundamental challenge represents the second critical assumption: mapping boolean guard
+Computational tractability addresses whether synthesis can complete within practical time bounds—a practical constraint. The second risk is more fundamental: whether boolean guard
-conditions in temporal logic to continuous state boundaries required for mode
+conditions in temporal logic can map cleanly to continuous state boundaries required for mode
 transitions. This interface represents the fundamental challenge of hybrid
 systems: relating discrete switching logic to continuous dynamics. Temporal
 logic operates on boolean predicates, while continuous control requires
@@ -149,4 +148,6 @@ extensions, ensuring they address industry-wide practices rather than specific
 quirks.
 
 
-These risks and contingencies demonstrate that while the research faces real challenges, each has identifiable early indicators and viable mitigation strategies. The staged approach ensures valuable contributions even if core assumptions prove invalid: partial success yields publishable results that clearly identify remaining barriers to deployment. With risks addressed and contingencies established, the next section examines broader impacts: who cares about this work and why it matters now.
+This section addressed the Heilmeier question: \textbf{What could prevent success?} Four primary risks—computational tractability, discrete-continuous interface complexity, procedure formalization completeness, and hardware integration—each have identifiable early indicators and viable mitigation strategies. The staged approach ensures valuable contributions even if core assumptions prove invalid: partial success yields publishable results that clearly identify remaining barriers to deployment.
+
+With technical feasibility established through the methodology (Section 3), success metrics defined (Section 4), and risks addressed with contingency plans (Section 5), the research plan is complete from a technical perspective. Section 6 now addresses the remaining Heilmeier questions that establish broader impact: \textbf{Who cares?} \textbf{Why now?} \textbf{What difference will it make?}

6-broader-impacts/v1.tex

@@ -7,8 +7,8 @@ economic challenge. Recent interest in powering artificial intelligence
 infrastructure has renewed focus on small modular reactors (SMRs), particularly
 for hyperscale datacenters requiring hundreds of megawatts of continuous power.
 Deploying SMRs at datacenter sites minimizes transmission losses and
-eliminates emissions from hydrocarbon-based alternatives. Nuclear power
+eliminates emissions. However, nuclear power
-economics at this scale, however, demand careful attention to operating costs.
+economics at this scale demand careful attention to operating costs.
 
 The U.S. Energy Information Administration's Annual Energy Outlook
 2022 projects advanced nuclear power entering service in 2027 will cost
@@ -28,17 +28,17 @@ to \$21--28 billion annually for projected datacenter demand.
 control, making small modular reactors economically viable for datacenter power.
 
 Current nuclear operations require full control room staffing for each
-reactor—whether large conventional units or small modular designs. For large reactors producing 1,000+ MW, staffing costs spread across substantial output. Small modular reactors producing 50-300 MW face the same staffing requirements with far lower output, making the per-megawatt cost prohibitive. These staffing requirements drive the economic challenge
+reactor—whether large conventional units or small modular designs. For large reactors producing 1,000+ MW, staffing costs spread across substantial output. Small modular reactors producing 50-300 MW face the same staffing requirements with far lower output, making per-megawatt costs prohibitive. These staffing requirements drive the economic challenge
 that threatens SMR deployment for datacenter applications. Synthesizing provably correct hybrid controllers from formal
 specifications automates routine operational sequences that currently require
-constant human oversight. A fundamental shift from direct operator
+constant human oversight. This enables a fundamental shift from direct operator
-control to supervisory monitoring becomes possible, where operators oversee multiple autonomous
+control to supervisory monitoring, where operators oversee multiple autonomous
 reactors rather than manually controlling individual units.
 
 The correct-by-construction methodology is critical for this transition.
 Traditional automation approaches cannot provide sufficient safety guarantees
 for nuclear applications, where regulatory requirements and public safety
-concerns demand the highest levels of assurance. Formally verifying both the
+concerns demand the highest levels of assurance. By formally verifying both the
 discrete mode-switching logic and the continuous control behavior, this research
 will produce controllers with mathematical proofs of correctness. These
 guarantees enable automation to safely handle routine operations---startup
@@ -73,7 +73,7 @@ establish both the technical feasibility and regulatory pathway for broader
 adoption across critical infrastructure.
 
 
-These broader impacts answer the final Heilmeier questions: 
+This section answered three Heilmeier questions: 
 
 \textbf{Who cares?} The nuclear industry, datacenter operators, and anyone facing high operating costs from staffing-intensive safety-critical control. 
 
@@ -81,4 +81,4 @@ These broader impacts answer the final Heilmeier questions:
 
 \textbf{What difference will it make?} Enabling autonomous control with mathematical safety guarantees addresses a \$21--28 billion annual cost barrier while establishing a generalizable framework for safety-critical autonomous systems.
 
-The next section presents the timeline for achieving these outcomes through a structured 24-month research plan.
+Section 8 addresses the final Heilmeier question—how long will it take?—presenting a structured 24-month research plan with milestones tied to Technology Readiness Level advancement.

8-schedule/v1.tex

@@ -2,10 +2,9 @@
 
 \textbf{How long will it take?} This research will be conducted over six
 trimesters (24 months) of full-time effort following the proposal defense in
-Spring 2026. All work uses existing computational and experimental resources
+Spring 2026. The University of Pittsburgh Cyber Energy Center and NRC
-available through the University of Pittsburgh Cyber Energy Center and NRC
+Fellowship provide all computational and experimental resources. The work progresses
-Fellowship funding. The work progresses
+sequentially through three main research thrusts, culminating in
-sequentially through three main research thrusts before culminating in
 integrated demonstration and validation.
 
 The first semester (Spring 2026) focuses on Thrust 1, translating startup