Editorial pass: Gopen + Heilmeier alignment

TACTICAL (sentence-level):
- Applied issue-point positioning (old info → new info)
- Strengthened verb choices, reduced nominalizations
- Eliminated unnecessary passive constructions
- Improved topic string coherence across sentences
- Split overly complex sentences for clarity

OPERATIONAL (paragraph-level):
- Strengthened transitions between subsections
- Improved paragraph flow within sections
- Enhanced coherence within related paragraphs
- Clarified relationships between ideas

STRATEGIC (document-level):
- Tightened Heilmeier question alignment
- Improved section-to-section linkages
- Made explicit connections clearer
- Ensured each section clearly answers its Heilmeier questions

Focus: clarity and impact improvements without nitpicking.

1-goals-and-outcomes/research_statement_v1.tex

@@ -2,18 +2,18 @@
 This research develops autonomous control systems that provide mathematical guarantees of safe and correct behavior.
 
 % INTRODUCTORY PARAGRAPH Hook
-Nuclear reactors today require human operators who follow detailed written procedures and switch between control objectives as plant conditions change.
+Nuclear reactors today require human operators to follow detailed written procedures and switch between control objectives as plant conditions change.
 % Gap
-Small modular reactors face a fundamental economic challenge: per-megawatt staffing costs 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 per-megawatt staffing costs 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 human operators.
 
 % APPROACH PARAGRAPH Solution
-This research unifies formal methods with control theory to produce hybrid control systems correct by construction.
+This research unifies formal methods with control theory to produce hybrid control systems that are correct by construction.
 % Rationale
-Human operators already work this way—using discrete logic to switch 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.
+Human operators already work this way—they use discrete logic to switch 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.
 % 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. 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. 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.
+Control objectives classify continuous modes 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, enabling 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 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 that provide mathematic
 % INTRODUCTORY PARAGRAPH Hook
 Nuclear power plants demand 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 per-megawatt staffing costs 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 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 economic viability. Autonomous control could manage complex operational sequences without constant supervision—but only if it provides safety assurance equal to or exceeding human operators.
 
 % APPROACH PARAGRAPH Solution
-This research unifies formal methods with control theory to produce hybrid control systems correct by construction.
+This research unifies formal methods with control theory to produce hybrid control systems that are correct by construction.
 % Rationale
-Human operators already work this way—using discrete logic to switch between continuous control modes. Formal methods generate provably correct switching logic from written requirements but cannot verify continuous dynamics. Control theory verifies continuous behavior but cannot prove discrete switching correctness. End-to-end correctness requires both.
+Human operators already work this way—they use discrete logic to switch between continuous control modes. Formal methods generate provably correct switching logic from written requirements but cannot verify continuous dynamics. Control theory verifies continuous behavior but 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. These steps transform 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. These steps transform operating procedures into logical specifications that constrain continuous dynamics, producing autonomous controllers that are provably free from design defects. 
 
 The University of Pittsburgh Cyber Energy Center provides access to industry collaboration and Emerson control hardware. This ensures solutions align with practical implementation requirements.
 

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

@@ -14,7 +14,7 @@ Current practice rests on two critical components: procedures and operators. Pro
 
 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, while 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}. 
 
-Procedure development rests on expert judgment and simulator validation—not formal verification. 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 time, or that transitions between procedure sets maintain safety invariants.
+Procedure development rests on expert judgment and simulator validation—not formal verification. 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. No proof verifies that required actions complete within available time. No proof guarantees 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
@@ -31,9 +31,9 @@ Highly automated systems already handle reactor protection: automatic trips on s
 
 \subsection{Human Factors in Nuclear Accidents}
 
-The previous subsection established that procedures lack formal verification despite rigorous development, representing only half the reliability challenge. Even perfect procedures cannot guarantee safe operation when executed imperfectly.
+The previous subsection established that 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. While procedures define what to do, operators determine when and how to act. This discretion introduces persistent failure modes that training 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 that training cannot eliminate.
 
 Current-generation nuclear power plants employ over 3,600 active NRC-licensed
 reactor operators in the United States~\cite{operator_statistics}. These
@@ -43,7 +43,7 @@ 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. 
+Human error persistently contributes to nuclear safety incidents despite decades of training and procedure improvements. Training cannot eliminate this persistence. This motivates 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}. 
 
@@ -63,11 +63,11 @@ limitations are fundamental to human-driven control, not remediable defects.
 
 \subsection{Formal Methods}
 
-The previous subsections established two fundamental limitations: procedures lack formal verification, and human operators introduce persistent reliability issues that training cannot eliminate. Both represent fundamental constraints—not remediable defects.
+The previous subsections established two fundamental limitations. First, procedures lack formal verification. Second, human operators introduce persistent reliability issues that training cannot eliminate. Both represent fundamental constraints—not remediable defects.
 
-Formal methods could eliminate these limitations by providing mathematical guarantees of correctness, yet even the most advanced formal methods applications in nuclear control leave a critical verification gap.
+Formal methods could eliminate these limitations by providing mathematical guarantees of correctness. Yet even the most advanced formal methods applications in nuclear control leave a critical verification gap.
 
-This subsection examines two approaches illustrating this gap. HARDENS verified discrete logic without continuous dynamics, while differential dynamic logic handles hybrid verification only post-hoc. Each demonstrates the current state of formal methods and reveals the verification gap this research addresses.
+This subsection examines two approaches that illustrate this gap. HARDENS verified discrete logic without continuous dynamics. Differential dynamic logic handles hybrid verification only post-hoc. Each demonstrates the current state of formal methods. Each reveals the verification gap this research addresses.
 
 \subsubsection{HARDENS: Formal Methods in Nuclear Control}
 
@@ -162,8 +162,8 @@ This section addressed two Heilmeier questions: What has been done? What are the
 
 \textbf{What has been done?} Three approaches currently exist, each with fundamental limitations. First, human operators provide operational flexibility but introduce persistent reliability constraints that training cannot eliminate. Second, HARDENS verified discrete logic but omitted continuous dynamics. Third, 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, and post-hoc verification cannot scale to system design.
+\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.
 
-This verification gap is clear and consequential. Economic pressures demand autonomous control; technical maturity now enables it. 
+This verification gap is both clear and consequential. Economic pressures demand autonomous control. Technical maturity now enables it. 
 
-Section 3 addresses the next two Heilmeier questions—What is new? Why will it succeed?—presenting the technical approach that closes this gap.
+Section 3 addresses the next two Heilmeier questions—What is new? Why will it succeed?—by presenting the technical approach that closes this gap.

3-research-approach/v3.tex

@@ -23,13 +23,13 @@ This section presents the complete technical approach for synthesizing provably
 % ----------------------------------------------------------------------------
 % 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION
 % ----------------------------------------------------------------------------
-Previous approaches verified either discrete switching logic or continuous control behavior—never both simultaneously. Engineers validate continuous controllers through extensive simulation trials and test discrete switching logic through simulated control room testing and human factors research. Neither method provides rigorous guarantees; both consume enormous resources.
+Previous approaches verified either 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 by composing formal methods with control-theoretic verification and formalizing reactor operations as hybrid automata.
 
 Hybrid system verification faces a fundamental challenge: discrete transitions change the governing vector field, creating discontinuities that traditional verification techniques cannot handle directly.
 
-This methodology decomposes the problem by verifying discrete switching logic and continuous mode behavior separately, then composing them to guarantee correctness for 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.
+This methodology decomposes the problem. It verifies discrete switching logic and continuous mode behavior separately, then composes them to guarantee correctness 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.
 
@@ -58,7 +58,7 @@ where:
 
 A HAHACS requires this tuple together with proof artifacts demonstrating that the control system's actual implementation satisfies its intended behavior.
 
-\textbf{What is new in this research?} Existing approaches verify either discrete logic or continuous dynamics—never both compositionally. Section 2 established this limitation: reactive synthesis, reachability analysis, and barrier certificates exist independently but have never been integrated into a systematic design methodology that spans from procedures to verified implementation.
+\textbf{What is new in this research?} Existing approaches verify either discrete logic or continuous dynamics—never both compositionally. Section 2 established this limitation. Reactive synthesis, reachability analysis, and barrier certificates exist independently. No one has integrated them into a systematic design methodology spanning from procedures to verified implementation.
 
 Three innovations enable compositional verification:
 
@@ -70,11 +70,11 @@ Three innovations enable compositional verification:
 
 \textbf{Why will it succeed?} Three factors ensure practical feasibility.
 
-First, \textit{existing structure}: Nuclear procedures already decompose operations into discrete phases with explicit transition criteria. The approach formalizes this existing structure without imposing artificial abstractions, enabling domain experts to adopt the methodology without formal methods training.
+First, \textit{existing structure}: Nuclear procedures already decompose operations into discrete phases with explicit transition criteria. The approach formalizes this existing structure without imposing artificial abstractions. Domain experts can adopt the methodology without formal methods training.
 
-Second, \textit{bounded complexity}: Mode-level verification checks each mode against local contracts, avoiding global hybrid system analysis. This decomposition bounds computational complexity by transforming an intractable global problem into tractable local verifications.
+Second, \textit{bounded complexity}: Mode-level verification checks each mode against local contracts, avoiding global hybrid system analysis. This decomposition bounds computational complexity. It transforms an intractable global problem into tractable local verifications.
 
-Third, \textit{industrial validation}: The Emerson collaboration provides domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility, ensuring solutions address real deployment constraints—not just theoretical correctness.
+Third, \textit{industrial validation}: The Emerson collaboration provides domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility. This ensures solutions address real deployment constraints—not just theoretical correctness.
 
 These factors combine to demonstrate feasibility on production control systems with realistic reactor models—not merely in principle. Figure~\ref{fig:hybrid_automaton} illustrates the hybrid structure for a simplified reactor startup sequence.
 
@@ -289,9 +289,9 @@ Reactive synthesis produces discrete mode-switching logic from procedures. This
 
 \subsection{Continuous Control Modes}
 
-Reactive synthesis produces a provably correct discrete controller that determines when to switch between modes. However, hybrid control requires more than correct mode switching: the continuous dynamics executing within each discrete mode must also verify against requirements.
+Reactive synthesis produces a provably correct discrete controller that determines when to switch between modes. This solves half the hybrid control problem. The other half remains: the continuous dynamics executing within each discrete mode must also verify against requirements.
 
-Control objectives determine the verification approach. Modes classify into three types—transitory, stabilizing, and expulsory—each requiring different verification tools matched to its distinct purpose. This subsection describes each type and its verification method. 
+Control objectives determine the verification approach. This work classifies modes into three types: transitory, stabilizing, and expulsory. Each type requires different verification tools matched to its distinct purpose. This subsection describes each type and its verification method. 
 
 This methodology's scope requires clarification. This work verifies continuous controllers but does not synthesize them. The distinction parallels model checking in software verification. Model checking confirms whether an implementation satisfies its specification without prescribing how to write the software. Engineers design continuous controllers using standard control theory techniques. This work assumes that capability exists. The contribution lies in the verification framework. It confirms that candidate controllers compose correctly with the discrete layer to produce a safe hybrid system.
 
@@ -441,9 +441,11 @@ controller.
 
 \subsubsection{Expulsory Modes}
 
-Transitory and stabilizing modes handle nominal operations—transitory modes move the plant between conditions while stabilizing modes maintain it within regions. Both assume the plant dynamics match the design model.
+Transitory and stabilizing modes handle nominal operations. Transitory modes move the plant between conditions. Stabilizing modes maintain it within regions. Both assume the plant dynamics match the design model.
 
-Expulsory modes address a different scenario: situations where the plant deviates from expected behavior due to component failures, sensor degradation, or unanticipated disturbances. For expulsory modes, robustness matters more than 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.
+Real systems deviate from design models. Component failures occur. Sensors degrade. Unanticipated disturbances arise. Expulsory modes address these off-nominal scenarios.
+
+For expulsory modes, robustness matters more than optimality. The control objective shifts from reaching targets or maintaining regions to driving the plant to a safe shutdown state. This must succeed 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.
 
@@ -521,29 +523,29 @@ outcomes can best align with customer needs.
 
 This section addressed two critical Heilmeier questions: What is new? Why will it succeed?
 
-\textbf{What is new?} Three innovations enable compositional verification by integrating reactive synthesis, reachability analysis, and barrier certificates: 
+\textbf{What is new?} Three innovations enable compositional verification by integrating reactive synthesis, reachability analysis, and barrier certificates. 
 
-First, \textit{contract-based decomposition} inverts traditional global analysis—discrete synthesis defines verification contracts that bound continuous verification. 
+First, \textit{contract-based decomposition} inverts traditional global analysis. Discrete synthesis defines verification contracts that bound continuous verification. 
 
-Second, \textit{mode classification} matches continuous modes to appropriate verification tools, enabling mode-local analysis with provable composition guarantees. 
+Second, \textit{mode classification} matches continuous modes to appropriate verification tools. This enables mode-local analysis with provable composition guarantees. 
 
 Third, \textit{procedure-driven structure} leverages existing procedural decomposition to avoid intractable state explosion.
 
 Section 2 established that prior work verified discrete logic or continuous dynamics—never both compositionally. These three innovations enable what global analysis cannot: compositional verification spanning from procedures to verified implementation.
 
-\textbf{Why will it succeed?} Three factors ensure practical feasibility: 
+\textbf{Why will it succeed?} Three factors ensure practical feasibility. 
 
-\textit{Existing structure}: Nuclear procedures already decompose operations into discrete phases with explicit transition criteria, allowing formalization without artificial abstractions. 
+\textit{Existing structure}: Nuclear procedures already decompose operations into discrete phases with explicit transition criteria. This allows formalization without artificial abstractions. 
 
-\textit{Bounded complexity}: Mode-level verification bounds each problem locally, avoiding the state explosion that makes global hybrid system analysis intractable. 
+\textit{Bounded complexity}: Mode-level verification bounds each problem locally. This avoids the state explosion that makes global hybrid system analysis intractable. 
 
-\textit{Industrial validation}: Emerson collaboration provides domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility, ensuring solutions address real deployment constraints.
+\textit{Industrial validation}: Emerson collaboration provides domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility. This ensures solutions address real deployment constraints.
 
-With the complete technical methodology established, Sections 2 and 3 have addressed the first four Heilmeier questions—what has been done, what limits current practice, what is new, and why it will succeed. 
+With the complete technical methodology established, Sections 2 and 3 have addressed the first four Heilmeier questions: what has been done, what limits current practice, what is new, and why it will succeed. 
 
-Three questions remain: How will success be measured? What could prevent success? Who cares and what difference will this work make? 
+Three questions remain. How will success be measured? What could prevent success? Who cares and what difference will this work make? 
 
-Section 4 addresses metrics for success, Section 5 identifies what could prevent success, and Section 6 explains who cares and what difference this work will make.
+Section 4 addresses metrics for success. Section 5 identifies what could prevent success. Section 6 explains who cares and what difference this work will make.
 
 %%% NOTES (Section 5):
 % - Get specific details on ARCADE interface from Emerson collaboration

4-metrics-of-success/v1.tex

@@ -6,9 +6,9 @@ Section 3 established the technical approach: compositional verification bridges
 
 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), where system components operate successfully in a relevant laboratory environment. 
+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. It explicitly measures the gap between academic proof-of-concept and practical deployment. This section explains why TRLs appropriately measure success. It then defines specific criteria for each level from TRL 3 through TRL 5.
+TRL advancement provides the most appropriate success metric because it explicitly measures the gap between academic proof-of-concept and practical deployment. This section first explains why TRLs appropriately measure success. It then defines specific criteria for each level from TRL 3 through TRL 5.
 
 Technology Readiness Levels provide the ideal success metric for work bridging academic proof-of-concept and practical deployment. 
 

5-risks-and-contingencies/v1.tex

@@ -2,11 +2,11 @@
 
 \textbf{Heilmeier Question: What could prevent success?}
 
-Section 4 defined success as reaching TRL 5 through component validation, system integration, and hardware demonstration, assuming critical technical challenges can be overcome.
+Section 4 defined success as reaching TRL 5 through component validation, system integration, and hardware demonstration. This assumes critical technical challenges can be overcome.
 
-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, viable mitigation strategies, and contingency plans that preserve research value even when core assumptions fail. 
+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. Each has viable mitigation strategies. Each has contingency plans that preserve research value even when core assumptions fail. 
 
-The staged project structure ensures partial success yields publishable results. It clearly identifies remaining barriers to deployment, even when full success proves elusive.
+The staged project structure ensures partial success yields publishable results. It clearly identifies remaining barriers to deployment—even when full success proves elusive.
 
 \subsection{Computational Tractability of Synthesis}
 
@@ -26,9 +26,9 @@ If computational tractability becomes the limiting factor, we reduce scope to a
 
 \subsection{Discrete-Continuous Interface Formalization}
 
-The first risk addressed practical constraints: whether synthesis can complete within reasonable time bounds. The second risk proves more fundamental: whether boolean guard conditions in temporal logic can map cleanly to continuous state boundaries required for mode transitions. 
+The first risk addressed practical constraints: whether synthesis can complete within reasonable time bounds. The second risk proves more fundamental. Can boolean guard conditions in temporal logic 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 reasoning about differential equations and reachable sets. Guard conditions requiring complex nonlinear predicates may resist boolean abstraction. This would make synthesis intractable. Continuous safety regions that cannot be expressed as conjunctions of verifiable constraints would similarly create insurmountable verification challenges. 
+This interface represents the fundamental challenge of hybrid systems: relating discrete switching logic to continuous dynamics. Temporal logic operates on boolean predicates. Continuous control requires reasoning about differential equations and reachable sets. Guard conditions requiring complex nonlinear predicates may resist boolean abstraction, making synthesis intractable. Continuous safety regions that cannot be expressed as conjunctions of verifiable constraints would similarly create insurmountable verification challenges. 
 
 The risk extends beyond static interface definition to dynamic behavior across transitions. Barrier certificates may fail to exist for proposed transitions. Continuous modes may be unable to guarantee convergence to discrete transition boundaries.