Tactical edits: sentence-level improvements (Gopen principles)

- Broke up long sentences for clarity
- Improved topic-stress positioning
- Reduced passive constructions
- Enhanced readability across sections 1-3

Sections edited: research_statement_v1, v1 (goals), v2 (state-of-art), v3 (approach)

1-goals-and-outcomes/research_statement_v1.tex

@@ -2,18 +2,18 @@
 This research develops autonomous control systems with mathematical guarantees of safe and correct behavior.
 
 % INTRODUCTORY PARAGRAPH Hook
-Extensively trained human operators control nuclear reactors today, following detailed written procedures and switching between control objectives as plant conditions change.
+Human operators control nuclear reactors today. They follow detailed written procedures and switch between control objectives as plant conditions change.
 % Gap
-Small modular reactors face a fundamental economic challenge: staffing costs per megawatt far exceed those of conventional plants, threatening economic viability. Autonomous control could manage complex operational sequences without constant supervision—but only if it provides safety assurance equal to or exceeding that of human operators.
+Small modular reactors face a fundamental economic challenge: their staffing costs per megawatt far exceed those of conventional plants. This threatens economic viability. Autonomous control could manage complex operational sequences without constant supervision—but only if it provides safety assurance equal to or exceeding that of human operators.
 
 % APPROACH PARAGRAPH Solution
-Formal methods from computer science unify with control theory to produce hybrid control systems that are correct by construction.
+This research unifies formal methods from computer science with control theory to produce hybrid control systems correct by construction.
 % Rationale
-Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic but cannot verify continuous dynamics. Control theory verifies continuous behavior but cannot prove discrete logic correctness. Both are required for end-to-end correctness.
+Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic but cannot verify continuous dynamics. Control theory verifies continuous behavior but cannot prove discrete logic correctness. End-to-end correctness requires both.
 % Hypothesis and Technical Approach
-Three stages bridge this gap. First, NASA's Formal Requirements Elicitation Tool (FRET) translates written operating procedures into temporal logic specifications, structuring requirements by scope, condition, component, timing, and response. Realizability checking exposes conflicts and ambiguities before implementation begins. Second, reactive synthesis generates deterministic automata provably correct by construction. Third, reachability analysis verifies that continuous controllers—designed by engineers using standard control theory—satisfy each discrete mode's requirements.
+Three stages bridge this gap. First, NASA's Formal Requirements Elicitation Tool (FRET) translates written operating procedures into temporal logic specifications. FRET structures requirements by scope, condition, component, timing, and response. Realizability checking exposes conflicts and ambiguities before implementation begins. Second, reactive synthesis generates deterministic automata provably correct by construction. Third, reachability analysis verifies that continuous controllers satisfy each discrete mode's requirements. Engineers design these controllers using standard control theory.
 
-Continuous modes classify by control objective into three types: transitory modes drive the plant between conditions, stabilizing modes maintain operation within regions, and expulsory modes ensure safety under failures. Barrier certificates and assume-guarantee contracts prove mode transitions are safe, enabling local verification without global trajectory analysis. This methodology demonstrates on an Emerson Ovation control system—the industrial platform nuclear power plants already use.
+Continuous modes classify by control objective into three types. Transitory modes drive the plant between conditions. Stabilizing modes maintain operation within regions. Expulsory modes ensure safety under failures. Barrier certificates and assume-guarantee contracts prove mode transitions are safe. This enables local verification without global trajectory analysis. The methodology demonstrates on an Emerson Ovation control system—the industrial platform nuclear power plants already use.
 % Pay-off
 This approach manages complex nuclear power operations autonomously while maintaining safety guarantees. It directly addresses the economic constraints threatening small modular reactor viability.
 

1-goals-and-outcomes/v1.tex

@@ -6,16 +6,16 @@ This research develops autonomous hybrid control systems with mathematical guara
 % INTRODUCTORY PARAGRAPH Hook
 Nuclear power plants require the highest levels of control system reliability. Control system failures risk economic losses, service interruptions, or radiological release.
 % Known information
-Extensively trained human operators control nuclear plants today, following detailed written procedures and strict regulatory requirements. They switch between control modes based on plant conditions and procedural guidance.
+Extensively trained human operators control nuclear plants today. They follow detailed written procedures and strict regulatory requirements. They switch between control modes based on plant conditions and procedural guidance.
 % Gap
-This reliance on human operators prevents autonomous control and creates a fundamental economic challenge for next-generation reactor designs. Small modular reactors face staffing costs per megawatt far exceeding those of conventional plants, threatening economic viability. Autonomous control could manage complex operational sequences without constant supervision—but only if it provides safety assurance equal to or exceeding that of human operators.
+This reliance on human operators prevents autonomous control. It creates a fundamental economic challenge for next-generation reactor designs. Small modular reactors face staffing costs per megawatt far exceeding those of conventional plants. This threatens economic viability. Autonomous control could manage complex operational sequences without constant supervision—but only if it provides safety assurance equal to or exceeding that of human operators.
 
 % APPROACH PARAGRAPH Solution
 Formal methods unify with control theory to produce hybrid control systems that are correct by construction.
 % Rationale
-Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic from written requirements but cannot verify the continuous dynamics governing transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. Both are required for end-to-end correctness.
+Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic from written requirements. However, they cannot verify the continuous dynamics governing transitions. Control theory verifies continuous behavior. However, it cannot prove discrete switching correctness. Both are required for end-to-end correctness.
 % Hypothesis
-Two steps close this gap. First, reactive synthesis generates discrete mode transitions directly from written operating procedures. Second, reachability analysis verifies continuous behavior against discrete requirements. This approach transforms operating procedures into logical specifications that constrain continuous dynamics, producing autonomous controllers provably free from design defects. 
+Two steps close this gap. First, reactive synthesis generates discrete mode transitions directly from written operating procedures. Second, reachability analysis verifies continuous behavior against discrete requirements. This approach transforms operating procedures into logical specifications. These specifications constrain continuous dynamics, producing autonomous controllers provably free from design defects. 
 
 The University of Pittsburgh Cyber Energy Center provides access to industry collaboration and Emerson control hardware, ensuring solutions align with practical implementation requirements.
 
@@ -32,9 +32,9 @@ If successful, this approach produces three concrete outcomes:
     discrete control logic from these specifications. Structured intermediate
     representations bridge natural language procedures and mathematical logic.
     % Outcome
-    Control system engineers generate verified mode-switching controllers
+    Control system engineers can generate verified mode-switching controllers
-    directly from regulatory procedures without formal methods expertise,
+    directly from regulatory procedures. They need no formal methods expertise.
-    lowering the barrier to high-assurance control systems.
+    This lowers the barrier to high-assurance control systems.
 
     % OUTCOME 2 Title
   \item \textbf{Verify continuous control behavior across mode transitions.}

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

@@ -2,7 +2,7 @@
 
 \textbf{Heilmeier Questions: What has been done? What are the limits of current practice?} 
 
-No current approach provides autonomous control with end-to-end correctness guarantees. Human-centered operation cannot eliminate reliability limits. Formal methods verify discrete or continuous behavior—never both. 
+No current approach provides end-to-end correctness guarantees for autonomous control. Human-centered operation cannot eliminate reliability limits. Formal methods verify discrete or continuous behavior—never both. 
 
 Three subsections structure this analysis: reactor operators and their operating procedures, fundamental limitations of human-based operation, and formal methods approaches that verify discrete logic or continuous dynamics but not both together.
 
@@ -10,11 +10,11 @@ Section 3 addresses the verification gap these limits establish.
 
 \subsection{Current Reactor Procedures and Operation}
 
-Current practice rests on two critical components: procedures and operators. Procedures define what must be done; operators execute those procedures. This subsection examines procedures—their hierarchy, development process, and role in defining operational modes. The following subsection examines operators—their reliability limits and contribution to accidents.
+Current practice rests on two critical components: procedures and operators. Procedures define what must be done. Operators execute those procedures. This subsection examines procedures—their hierarchy, development process, and role in defining operational modes. The following subsection examines operators—their reliability limits and contribution to accidents.
 
 Nuclear plant procedures form a strict 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. Extensive Damage Mitigation Guidelines (EDMGs) cover catastrophic damage. All procedures must comply with 10 CFR 50.34(b)(6)(ii). NUREG-0899 provides development guidance~\cite{NUREG-0899, 10CFR50.34}. 
 
-Expert judgment and simulator validation—not formal verification—form the basis for procedure development. Regulations mandate rigorous assessment: 10 CFR 55.59~\cite{10CFR55.59} requires technical evaluation, simulator validation testing, and biennial review. Yet key safety properties escape formal verification: no mathematical proof confirms that procedures cover all possible plant states, that required actions complete within available timeframes, or that transitions between procedure sets maintain safety invariants.
+Expert judgment and simulator validation—not formal verification—form the basis for procedure development. Regulations mandate rigorous assessment. Specifically, 10 CFR 55.59~\cite{10CFR55.59} requires technical evaluation, simulator validation testing, and biennial review. Yet key safety properties escape formal verification. No mathematical proof confirms that procedures cover all possible plant states. No proof confirms that required actions complete within available timeframes. No proof confirms that transitions between procedure sets maintain safety invariants.
 
 \textbf{LIMITATION:} \textit{Procedures lack formal verification of correctness
 and completeness.} No proof exists that procedures cover all
@@ -32,7 +32,7 @@ Safety systems already employ extensive automation. Reactor Protection Systems t
 
 Procedures lack formal verification despite rigorous development. This represents only half the reliability challenge: even perfect procedures cannot guarantee safe operation when humans execute them imperfectly.
 
-Human operators—the second pillar of current practice—introduce reliability limitations independent of procedure quality. Procedures define what to do; operators determine when and how to act. This discretion introduces persistent failure modes that training alone cannot eliminate.
+Human operators—the second pillar of current practice—introduce reliability limitations independent of procedure quality. Procedures define what to do. Operators determine when and how to act. This discretion introduces persistent failure modes. Training alone cannot eliminate these failures.
 
 Current-generation nuclear power plants employ over 3,600 active NRC-licensed
 reactor operators in the United States~\cite{operator_statistics}. These
@@ -42,7 +42,11 @@ shift supervisors~\cite{10CFR55}. Staffing typically requires at least two ROs
 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. This persistence cannot be trained away. It motivates the need for formal automated control with mathematical safety guarantees. Under 10 CFR Part 55, operators hold legal authority to make critical decisions. This includes authority to depart from normal regulations during emergencies. The Three Mile Island (TMI) accident demonstrated how personnel error, design 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 guarantees nothing. This tension between operational flexibility and safety assurance remains unresolved: the person responsible for reactor safety often becomes the root cause of failure.
+Human error persistently contributes to nuclear safety incidents despite decades of improvements in training and procedures. This persistence cannot be trained away. It motivates the need for formal automated control with mathematical safety guarantees. 
+
+Under 10 CFR Part 55, operators hold legal authority to make critical decisions. This includes authority to depart from normal regulations during emergencies. The Three Mile Island (TMI) accident demonstrated how personnel error, design 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 does not guarantee safety—not without formally verifying that operators can fulfill this responsibility. This tension between operational flexibility and safety assurance remains unresolved. The person responsible for reactor safety often becomes the root cause of failure.
 
 Multiple independent analyses converge on a striking statistic: human error accounts for 70--80\% of nuclear power plant events~\cite{WNA2020}. Equipment failures account for only 20\%. More significantly, human factors—poor safety management and safety culture—caused all severe accidents at nuclear power plants: Three Mile Island, Chernobyl, and Fukushima Daiichi~\cite{hogberg_root_2013}. A detailed analysis
 of 190 events at Chinese nuclear power plants from
@@ -153,12 +157,12 @@ design loop for complex systems like nuclear reactor startup procedures.
 
 \subsection{Summary: The Verification Gap}
 
-This section answered two Heilmeier questions: What has been done? What are the limits of current practice?
+This section addressed two Heilmeier questions: What has been done? What are the limits of current practice?
 
 \textbf{What has been done?} Three approaches currently exist, each with fundamental limitations. Human operators provide operational flexibility but introduce persistent reliability limitations. HARDENS verified discrete logic but omitted continuous dynamics. Differential dynamic logic expresses hybrid properties but requires post-design expert analysis. None addresses both discrete and continuous verification compositionally.
 
 \textbf{What are the limits of current practice?} A clear verification gap emerges: no existing methodology synthesizes provably correct hybrid controllers from operational procedures with verification integrated into design. Current approaches verify discrete logic or continuous dynamics—never both compositionally. Training improvements cannot overcome human reliability limits. Post-hoc verification cannot scale to system design.
 
-\textbf{Why now?} Two forces create urgency. First, economic necessity demands solutions: small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants. Second, technical maturity enables solutions: formal methods tools have matured sufficiently to enable compositional hybrid verification. These forces converge to make this work both necessary and achievable.
+\textbf{Why now?} Two forces create urgency. First, economic necessity: small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants. Second, technical maturity: formal methods tools have matured sufficiently to enable compositional hybrid verification. These forces converge to make this work both necessary and achievable.
 
-The verification gap is clear. The timing is right. Section 3 closes this gap, establishing what is new and why the approach will succeed.
+The verification gap is clear. The timing is right. Section 3 addresses this gap, establishing what is new and why the approach will succeed.

3-research-approach/v3.tex

@@ -25,11 +25,11 @@ This section presents the complete technical approach for synthesizing provably
 % ----------------------------------------------------------------------------
 Previous approaches verified discrete switching logic or continuous control behavior—never both simultaneously. Engineers validate continuous controllers through extensive simulation trials. They test discrete switching logic through simulated control room testing and human factors research. Neither method provides rigorous guarantees. Both consume enormous resources.
 
-This approach bridges that gap, composing formal methods from computer science with control-theoretic verification and formalizing reactor operations as hybrid automata.
+This approach bridges that gap. It composes formal methods from computer science with control-theoretic verification. It formalizes reactor operations as hybrid automata.
 
 Hybrid system verification faces a fundamental challenge: discrete transitions change the governing vector field. These discontinuities cannot be handled directly by traditional verification techniques.
 
-This methodology decomposes the problem. It verifies discrete switching logic and continuous mode behavior separately, then composes them to establish guarantees for 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.
+This methodology decomposes the problem. It verifies discrete switching logic and continuous mode behavior separately. It then composes them to establish guarantees for the complete hybrid system. This two-layer approach mirrors reactor operations. Discrete supervisory logic determines which control mode is active. Continuous controllers govern plant behavior within each mode.
 
 Hybrid systems require mathematical formalization. This work draws on automata theory, temporal logic, and control theory to provide that description.
 
@@ -394,9 +394,9 @@ appropriate to the fidelity of the reactor models available.
 
 \subsubsection{Stabilizing Modes}
 
-Transitory modes answer the question "can we reach the target?" by driving the system toward exit conditions. Reachability analysis provides the verification tool.
+Transitory modes drive the system toward exit conditions. Reachability analysis verifies whether the target can be reached.
 
-Stabilizing modes address a fundamentally different question: "will we stay within bounds?" These modes maintain the system within a desired operating region indefinitely. Examples include steady-state power operation, hot standby, and load-following at constant power level. This different control objective requires a different verification approach.
+Stabilizing modes address a different question: will the system stay within bounds? These modes maintain the system within a desired operating region indefinitely. Examples include steady-state power operation, hot standby, and load-following at constant power level. This different control objective requires a different verification approach.
 
 Reachability analysis answers "can the system reach a target?" Stabilizing modes instead ask "does the system stay within bounds?" Barrier certificates provide the appropriate verification tool for this question.
 Barrier certificates analyze the dynamics of the system to determine whether
@@ -445,9 +445,9 @@ controller.
 
 \subsubsection{Expulsory Modes}
 
-The first two mode types handle nominal operations: transitory modes move the plant between conditions using reachability analysis, while stabilizing modes maintain the plant within regions using barrier certificates. Both assume the plant dynamics match the design model.
+The first two mode types handle nominal operations. Transitory modes move the plant between conditions using reachability analysis. Stabilizing modes maintain the plant within regions using barrier certificates. Both assume the plant dynamics match the design model.
 
-Expulsory modes address a fundamentally different scenario: situations where the plant deviates from expected behavior. This deviation may result from component failures, sensor degradation, or unanticipated disturbances. Here, robustness matters more than optimality.
+Expulsory modes address a different scenario: situations where the plant deviates from expected behavior. This deviation may result from component failures, sensor degradation, or unanticipated disturbances. Here, robustness matters more than optimality.
 
 Expulsory controllers prioritize robustness over optimality. The control objective shifts from reaching targets or maintaining regions to driving 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.
 
@@ -526,7 +526,7 @@ 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 section answered two critical Heilmeier questions: What is new? Why will it succeed?
+This section addressed two critical Heilmeier questions: What is new? Why will it succeed?
 
 \textbf{What is new?} Three innovations enable compositional verification integrating reactive synthesis, reachability analysis, and barrier certificates: 
 

4-metrics-of-success/v1.tex

@@ -2,7 +2,7 @@
 
 \textbf{Heilmeier Question: How will success be measured?}
 
-Section 3 established the technical approach, answering what is new—compositional verification bridging discrete synthesis with continuous control—and why it will succeed—existing procedural structure, bounded complexity, and industrial validation. This section addresses the next Heilmeier question: How will success be measured? 
+Section 3 established the technical approach: compositional verification bridges discrete synthesis with continuous control. The approach will succeed because it leverages existing procedural structure, bounds computational complexity, and validates against industrial hardware. This section addresses the next Heilmeier question: How will success be measured? 
 
 Success is measured by Technology Readiness Level advancement from fundamental concepts (TRL 2--3) to validated prototype demonstration (TRL 5). At TRL 5, system components operate successfully in a relevant laboratory environment. TRL advancement provides the most appropriate success metric because it explicitly measures the gap between academic proof-of-concept and practical deployment. This section explains why TRLs measure success appropriately, then defines specific criteria for each level from TRL 3 through TRL 5.
 

5-risks-and-contingencies/v1.tex

@@ -6,6 +6,8 @@ Section 4 defined success as reaching TRL 5 through component validation, system
 
 Every research plan rests on assumptions that might prove false. Three primary risks could prevent reaching TRL 5: computational tractability of synthesis and verification, complexity of the discrete-continuous interface, and completeness of procedure formalization.
 
+Each risk has identifiable early warning indicators and viable mitigation strategies. 
+
 Each risk carries associated early warning indicators and contingency plans that preserve research value even when core assumptions fail. The staged project structure ensures that partial success yields publishable results and clearly identifies remaining barriers to deployment, even when full success proves elusive.
 
 \subsection{Computational Tractability of Synthesis}

6-broader-impacts/v1.tex

@@ -6,7 +6,7 @@ Sections 2 through 5 established the complete technical research plan: what has
 
 The technical plan is complete. This section addresses the remaining Heilmeier questions, connecting technical methodology to economic and societal impact: who cares, why now, and what difference this work will make.
 
-\textbf{Who cares?} Three stakeholder groups face the same economic constraint: high operating costs driven by staffing requirements. The nuclear industry faces uncompetitive per-megawatt costs for small modular reactors. Datacenter operators need hundreds of megawatts of continuous clean power for AI infrastructure. Clean energy advocates need nuclear power to be economically competitive with fossil alternatives. All three require this research to succeed.
+\textbf{Who cares?} Three stakeholder groups face the same economic constraint—high operating costs driven by staffing requirements. The nuclear industry faces uncompetitive per-megawatt costs for small modular reactors. Datacenter operators need hundreds of megawatts of continuous clean power for AI infrastructure. Clean energy advocates need nuclear power to be economically competitive with fossil alternatives. All three stakeholders require autonomous control with safety guarantees.
 
 \textbf{What difference will it make?} This research directly addresses a \$21--28 billion annual cost barrier, enabling economically viable small modular reactors for datacenter power and establishing a generalizable framework for safety-critical autonomous systems across critical infrastructure.