1-goals-and-outcomes/goals.tex

@@ -12,65 +12,69 @@ behavior.\splitnote{Clear thesis statement. Gets right to it.}
 
 % INTRODUCTORY PARAGRAPH Hook
 Nuclear power plants require the highest levels of control system reliability,
-where failures can result in significant economic losses, service
-interruptions, or radiological
-release.\splitnote{Stakes established immediately — good hook.}
+where failures can result in significant economic losses, service interruptions,
+or radiological release.\splitnote{Stakes established immediately — good hook.}
 % Known information
-Currently, nuclear plant operations rely on extensively trained human
-operators who follow detailed written procedures and strict regulatory
-requirements to manage reactor control. These operators make critical
-decisions about when to switch between different control modes based on their
-interpretation of plant conditions and procedural guidance.
+Currently, nuclear plant operations rely on extensively trained human operators
+who follow detailed written procedures and strict regulatory requirements to
+manage reactor control. These operators make critical decisions about when to
+switch between different control modes based on their interpretation of plant
+conditions and procedural guidance.
 % Gap
-\oldt{This reliance on human operators prevents autonomous control
-capabilities and creates a fundamental economic challenge for next-generation
-reactor designs.} \newt{This reliance on human operators prevents autonomous
-control and creates a fundamental economic barrier for next-generation
-reactor designs.} Small modular reactors face per-megawatt staffing costs
-far exceeding those of conventional plants, threatening their economic
-viability.
+This reliance on human operators prevents autonomous control capabilities and
+creates a fundamental economic challenge for next-generation reactor 
+designs.
+\splitinline{The ``and'' here joins two distinct issues (autonomy barrier + 
+economics). Consider making the causal link explicit: ``This reliance on human 
+operators not only prevents autonomous control capabilities but also 
+creates...'' or split into two sentences.}
+Small modular reactors, in particular, face per-megawatt staffing costs far
+exceeding those of conventional plants and threaten their economic viability.
 
 % Critical Need
-\oldt{What is needed is a method to create autonomous control systems that
-safely manage complex operational sequences with the same assurance as
-human-operated systems, but without constant human supervision.}
-\newt{Autonomous control systems must safely manage complex operational
-sequences with the same assurance as human-operated systems, but without
-constant human supervision.}
+What is needed is a method to create autonomous control systems that safely
+manage complex operational sequences with the same assurance as human-operated
+systems, but without constant human supervision.
+\splitinline{``What is needed is'' — Gopen would call this a weak topic 
+position. The sentence buries the subject. Try: ``Autonomous control systems 
+must safely manage complex operational sequences...'' Puts the actor in the 
+topic position.}
 % APPROACH PARAGRAPH Solution
 To address this need, we will combine formal methods with control theory to
 build hybrid control systems that are correct by construction.
 % Rationale
 Hybrid systems use discrete logic to switch between continuous control modes,
-mirroring how operators change control strategies. Existing formal methods
-can generate provably correct switching logic from written requirements, but
-they cannot handle the continuous dynamics that occur during transitions
-between modes. Meanwhile, traditional control theory can verify continuous
-behavior but lacks tools for proving correctness of discrete switching
+mirroring how operators change control strategies. Existing formal methods can
+generate provably correct switching logic from written requirements, but they
+cannot handle the continuous dynamics that occur during transitions between
+modes. Meanwhile, traditional control theory can verify continuous behavior but
+lacks tools for proving correctness of discrete switching 
 decisions.\splitnote{Excellent setup of the gap — shows why neither approach 
 alone is sufficient.}
 % Hypothesis
 By synthesizing discrete mode transitions directly from written operating
-procedures and verifying continuous behavior between transitions, we can
-create hybrid control systems with end-to-end correctness guarantees. If
-existing procedures can be formalized into logical specifications and
-continuous dynamics verified against transition requirements, then autonomous
-controllers can be built that are provably free from design
+procedures and verifying continuous behavior between transitions, we can create
+hybrid control systems with end-to-end correctness guarantees. If existing
+procedures can be formalized into logical specifications and continuous dynamics
+verified against transition requirements, then autonomous controllers can be
+built that are provably free from design 
 defects.\splitnote{Hypothesis is clear and testable.}
 % Pay-off
-\oldt{This approach will enable autonomous control in nuclear power plants
-while maintaining the high safety standards required by the industry.
+This approach will enable autonomous control in nuclear power plants while
+maintaining the high safety standards required by the industry.
 
 % Qualifications
-This work is conducted within the University of Pittsburgh Cyber Energy
-Center, which provides access to industry collaboration and Emerson control
-hardware, ensuring that developed solutions align with practical
-implementation requirements.} \newt{This approach will enable autonomous
-control in nuclear power plants while maintaining the high safety standards
-required by the industry. The University of Pittsburgh Cyber Energy Center's
-partnership with Emerson provides access to industry-standard control
-hardware, ensuring that developed solutions align with practical
-implementation requirements from the outset.}
+This work is conducted within the University of Pittsburgh Cyber Energy Center,
+which provides access to industry collaboration and Emerson control hardware,
+ensuring that developed solutions align with practical implementation
+requirements.
+\splitinline{This qualifications paragraph feels orphaned here. It's important 
+context but reads as an afterthought. Consider integrating it into the 
+approach paragraph (``...demonstrated on Emerson hardware through our 
+partnership with the Cyber Energy Center'') or moving to a ``Why This Will 
+Succeed'' framing later.}
+
+
 
 % OUTCOMES PARAGRAPHS
 If this research is successful, we will be able to do the following:
@@ -81,30 +85,27 @@ If this research is successful, we will be able to do the following:
   \item \textbf{Translate written procedures into verified control logic.}
     % Strategy
     We will develop a methodology for converting existing written operating
-    procedures into formal specifications that can be automatically
-    synthesized into discrete control logic. This process will use structured
-    intermediate representations to bridge natural language procedures and
-    mathematical logic.
+    procedures into formal specifications that can be automatically synthesized
+    into discrete control logic. This process will use structured intermediate
+    representations to bridge natural language procedures and mathematical
+    logic.
     % Outcome
-    \oldt{Control system engineers will generate verified mode-switching
-    controllers directly from regulatory procedures without formal methods
-    expertise, lowering the barrier to high-assurance control systems.}
-    \newt{This will lower the barrier to high-assurance control systems by
-    generating verified mode-switching controllers directly from regulatory
-    procedures.}\dasinline{Same comment as in executive summary. Might not be
-    true and is not the point.}
+    Control system engineers will generate verified mode-switching controllers
+    directly from regulatory procedures without formal methods 
+    expertise,\dasinline{Same comment as in executive
+    summary. Might not be true and is not the point.}
+    lowering the barrier to high-assurance control systems.
 
     % OUTCOME 2 Title
   \item \textbf{Verify continuous control behavior across mode transitions.}
     % Strategy
     We will establish methods for analyzing continuous control modes to ensure
     they satisfy discrete transition requirements. Using classical control
-    theory for linear systems and reachability analysis for nonlinear
-    dynamics, we will verify that each continuous mode safely reaches its
-    intended transitions.
-    % Outcome
-    Engineers will design continuous controllers using standard practices
-    while iterating to ensure broader system correctness, proving that mode
+    theory for linear systems and reachability analysis for nonlinear dynamics,
+    we will verify that each continuous mode safely reaches its intended
+    transitions.
+    Engineers will design continuous controllers using standard practices while
+    iterating to ensure broader system correctness, proving that mode
     transitions occur safely and at the correct times.
 
     % OUTCOME 3  Title
@@ -120,8 +121,8 @@ If this research is successful, we will be able to do the following:
     operation'' — concrete and impressive scope.}
     % Outcome
     We will demonstrate that autonomous hybrid control can be realized in the
-    nuclear industry with current equipment, establishing a path toward
-    reduced operator staffing while maintaining safety.
+    nuclear industry with current equipment, establishing a path toward reduced
+    operator staffing while maintaining safety.
 
 \end{enumerate}
 
@@ -131,17 +132,15 @@ verification to enable end-to-end correctness guarantees for hybrid
 systems.\splitnote{Clear ``what's new'' statement.}
 % Outcome Impact
 If successful, control engineers will create autonomous controllers from
-existing procedures with mathematical proof of correct behavior.
-High-assurance autonomous control will become practical for safety-critical
-applications.
+existing procedures with mathematical proof of correct behavior. High-assurance
+autonomous control will become practical for safety-critical applications.
 % Impact/Pay-off
-\oldt{This capability is essential for the economic viability of
-next-generation nuclear power. Small modular reactors offer a promising
-solution to growing energy demands, but their success depends on reducing
-per-megawatt operating costs through increased autonomy. This research will
-provide the tools to achieve that autonomy while maintaining the exceptional
-safety record the nuclear industry requires.} \newt{This research will
-provide the tools to achieve that autonomy while maintaining the exceptional
-safety record the nuclear industry
-requires.}\dasinline{This paragraph is literally the same as the rest of the
-GO. Does not belong here and feels very redundant.}
+This capability is essential for the economic viability of next-generation
+nuclear power. Small modular reactors offer a promising solution to growing
+energy demands, but their success depends on reducing per-megawatt operating
+costs through increased autonomy.\dasinline{This paragraph is literally
+the same as the rest of the GO. Does not belong here
+and feels very redundant.} This research will provide the tools to
+achieve that autonomy while maintaining the exceptional safety record the
+nuclear industry requires.\splitnote{Strong closing --- ties technical work to 
+real-world impact and economic necessity.}

1-goals-and-outcomes/research-statement.tex

@@ -1,79 +1,85 @@
 % GOAL PARAGRAPH
 The goal of this research is to develop a methodology for creating autonomous
-\oldt{control systems with event-driven control laws that have guarantees of
-safe and correct behavior.} \newt{hybrid control systems with mathematical
-guarantees of safe and correct behavior.}\splitnote{Strong, direct opening.
-Sets scope immediately.}
+control systems with event-driven control laws that have guarantees of safe and
+correct behavior.\splitnote{Strong, direct opening. Sets scope immediately.}
 \dasinline{Title needs updated to High Assurance Hybrid
 Control Systems. Maybe removal of `formal'?}
 
 % INTRODUCTORY PARAGRAPH Hook
 Nuclear power relies on extensively trained operators who follow detailed
-written procedures to manage reactor control. Based on these procedures and
-\oldt{operators'} \newt{their} interpretation of plant conditions,
-\oldt{operators} \newt{they} make critical decisions about when to switch
-between control objectives.
+written procedures to manage reactor control.\dasinline{Why is there any
+hyphenation at all? Why not full justification?} Based on these procedures and
+\oldt{operators'} \newt{their} interpretation of plant conditions, \oldt{operators} \newt{they} make critical decisions
+about when to switch between control objectives.
+\splitinline{Consider: ``operators'' appears 3x in two sentences. Maybe: 
+``Based on these procedures and their interpretation of plant conditions, 
+they make critical decisions...''}
 % Gap
-\oldt{But, reliance} \newt{This reliance} on human operators has created an
-economic challenge for next-generation nuclear power plants. Small modular
-reactors face significantly higher per-megawatt staffing costs than
-conventional plants.\dasinline{Obvious but source required.} Autonomous
-control systems \oldt{are needed that can} \newt{must} safely manage complex
+\oldt{But, reliance} \newt{This reliance} on human operators has created an economic challenge for
+next-generation nuclear power plants.
+\splitinline{``But, reliance'' — the comma after ``But'' is unusual. Either 
+drop it or restructure: ``However, this reliance...'' or ``This reliance, 
+however, has created...''}
+\dasinline{Or just straight up ``this reliance''.
+Right to the topic.}
+Small modular reactors face significantly higher per-megawatt staffing costs 
+than conventional 
+plants.\dasinline{Obvious but source required.} Autonomous control systems \oldt{are
+needed that can} \newt{must} safely manage complex 
 operational sequences with the same assurance as human-operated systems, but 
 without constant supervision.
+\splitinline{``are needed that can'' --- passive. Try: ``Autonomous control 
+systems must safely manage...''}
 
 % APPROACH PARAGRAPH Solution
-To address this need, we will combine formal methods from computer science
-with control theory \oldt{to build hybrid control systems that are correct by
-construction.} \newt{to build hybrid control systems that are correct by
-construction, leveraging the extensive domain knowledge already embedded in
-existing operating procedures and safety analyses.}
+To address this need, we will combine formal methods from computer science with
+control theory to build hybrid control systems that are correct by 
+construction.\splitnote{Clear statement of approach.}\dasinline{Add
+``and leverage existing domain knowledge'' or similar.
+Industry knowledge can be reused here --- less like
+starting from scratch.}
 % Rationale
 Hybrid systems use discrete logic to switch between continuous control modes,
 similar to how operators change control strategies. Existing formal methods
-generate provably correct switching logic but cannot handle continuous
-dynamics during transitions, while traditional control theory verifies
-continuous behavior but lacks tools for proving discrete switching
+generate provably correct switching logic but cannot handle continuous dynamics
+during transitions, while traditional control theory verifies continuous
+behavior but lacks tools for proving discrete switching 
 correctness.\splitnote{Nice parallel structure showing the gap.}
-
 % Hypothesis and Technical Approach
 We will bridge this gap through a three-stage methodology. First, we will
-translate written operating procedures into temporal logic specifications
-using NASA's Formal Requirements Elicitation Tool (FRET). \oldt{which
-structures requirements into scope, condition, component, timing, and
-response elements. This structured approach enables realizability checking to
-identify conflicts and ambiguities in procedures before implementation.}
-\newt{FRET structures requirements into scope, condition, component, timing,
-and response elements, enabling realizability checking that identifies
-conflicts and ambiguities in procedures before implementation.}
-\dasinline{Had to read this twice.}
-Second, we will synthesize discrete mode switching logic using reactive
-synthesis \oldt{to generate deterministic automata that are provably correct
-by construction.} \newt{to produce deterministic automata that are correct by
-construction.}\dasinline{Also had to read this twice. A lot of
+translate written operating procedures into temporal logic specifications using
+NASA's Formal Requirements Elicitation Tool (FRET), which structures
+requirements into scope, condition, component, timing, and response elements.
+This structured approach enables realizability checking to identify conflicts
+and ambiguities in procedures before 
+implementation.\dasinline{Had to read this twice.} Second, we will synthesize
+discrete mode switching logic using reactive 
+synthesis\dasinline{Also had to read this twice. A lot of
 jargon. Check topic stress.}
-Third, we will develop continuous controllers for each discrete mode using
-standard control theory and reachability analysis. We will classify
-continuous modes based on their transition objectives \oldt{, and then employ
-assume-guarantee contracts and barrier certificates to prove that mode
-transitions occur safely and as defined by the deterministic automata.}
-\newt{and verify safe mode transitions using barrier certificates and
-reachability analysis.}\dasinline{I don't think I ever mention this phrase
-again specifically. Might be a dogwhistle to other work unintentionally. Must
-be careful.}
-
-This compositional approach enables local verification of continuous modes
-without requiring global trajectory analysis across the entire hybrid system.
-\oldt{We will demonstrate this on an Emerson Ovation control system.}
-\newt{We will validate this methodology through hardware-in-the-loop testing
-on an Emerson Ovation distributed control system, made possible through the
-University of Pittsburgh Cyber Energy Center's industry partnership.}
-\dasinline{Where did this come from? Needs context.}
-
+to generate deterministic automata that are provably
+correct by construction. Third, we will develop continuous
+controllers for each discrete mode using standard control theory and
+reachability analysis. We will classify continuous modes based on their
+transition objectives, and then employ assume-guarantee contracts\dasinline{I don't think
+I ever mention this phrase again specifically. Might be a
+dogwhistle to other work unintentionally. Must be
+careful.} and barrier
+certificates to prove that mode transitions occur safely and as defined by the
+deterministic automata. This compositional approach enables local verification
+of continuous modes without requiring global trajectory analysis across the
+entire hybrid system. We will demonstrate this on an Emerson Ovation control 
+system.\dasinline{Where did this come from? Needs context.}
+\splitinline{This paragraph is dense. Consider breaking after the three 
+stages, then a new paragraph for the compositional verification point and 
+Emerson demo.}
 % Pay-off
-This approach \oldt{will demonstrate autonomous control can be used for}
-\newt{enables autonomous management of} complex nuclear power operations
-while maintaining safety guarantees.
+This approach \oldt{will demonstrate autonomous control can be used for} \newt{enables autonomous management of} complex
+nuclear power operations while maintaining safety 
+guarantees.
+\splitinline{``can be used for'' — weak. Try: ``...will demonstrate that 
+autonomous control can manage complex nuclear power operations while 
+maintaining safety guarantees.'' Or even stronger: ``...enables autonomous 
+management of complex nuclear power operations with safety guarantees.''}
 
 % OUTCOMES PARAGRAPHS
 If this research is successful, we will be able to do the following:
@@ -85,15 +91,15 @@ If this research is successful, we will be able to do the following:
     into formal specifications. These specifications will be synthesized into
     discrete control logic using reactive synthesis tools.     
     % Outcome
-    \oldt{Control engineers will be able to generate mode-switching
-    controllers from regulatory procedures with little formal methods
-    expertise, reducing barriers to high-assurance control systems.}
-    \newt{This will reduce barriers to high-assurance control systems by
-    generating verified mode-switching controllers directly from regulatory
-    procedures.}\dasinline{This may not be true, and perhaps does not belong.}
+    Control engineers will be able to generate mode-switching controllers from
+    regulatory procedures with little formal methods 
+    expertise,\dasinline{This may not be true, and perhaps
+    does not belong.} reducing
+    barriers to high-assurance control 
+    systems.\splitnote{Good practical framing --- emphasizes accessibility.}
 
     % OUTCOME 2 Title
-  \item \textit{Verify continuous control behavior across mode transitions.}
+  \item \textit{Verify continuous control behavior across mode transitions. }
     % Strategy
     We will develop methods using reachability analysis to ensure continuous 
     control modes satisfy discrete transition requirements. 
@@ -104,18 +110,18 @@ If this research is successful, we will be able to do the following:
 
     % OUTCOME 3  Title
   \item \textit{Demonstrate autonomous reactor startup control with safety
-    guarantees.}
+    guarantees. }
     % Strategy
     We will implement this methodology on a small modular reactor simulation
-    using industry-standard control hardware.
-    % Outcome
-    \oldt{Control engineers will be able to achieve autonomy without
-    retraining costs or developing new equipment by implementing
-    high-assurance autonomous controls on industrial platforms they already
-    use.} \newt{Without retraining costs or new equipment, control engineers
-    will be able to implement high-assurance autonomous controls on industrial
-    platforms they already use.}\dasinline{Flip the clauses. Put retraining
-    and new equipment before the comma, end with building HAHACs with control
-    hardware they already use. That's the more important part.}
+    using industry-standard control hardware.     % Outcome
+    Control engineers will be able to \oldt{implement high-assurance autonomous
+    controls on industrial platforms they already use, enabling users to
+    achieve autonomy without retraining costs or developing new 
+    equipment.} \newt{achieve autonomy without retraining costs or developing new equipment by implementing high-assurance autonomous controls on industrial platforms they already use.}\splitnote{Strong industrial grounding --- the ``platforms they 
+    already use'' point is compelling for 
+    adoption.}\dasinline{Flip the clauses. Put retraining
+    and new equipment before the comma, end with building
+    HAHACs with control hardware they already use.
+    That's the more important part.}
 
 \end{enumerate}

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

@@ -1,303 +1,269 @@
 \section{State of the Art and Limits of Current Practice}
 
 The principal aim of this research is to create autonomous reactor control
-systems that are tractably safe. \oldt{To understand what is being automated,
-we must first understand how nuclear reactors are operated today. This section
-examines reactor operators and the operating procedures we aim to leverage,
-then investigates limitations of human-based operation, and concludes with
-current formal methods approaches to reactor control systems.}
-\newt{Understanding what is being automated requires understanding how
-nuclear reactors are operated today. This section examines reactor operating
-procedures, investigates limitations of human-based operation, and reviews
-current formal methods approaches to reactor control
-systems.}\dasinline{Don't like ``we'' here. Sounds like ``we're going on an
-adventure!'' and feels jocular. Maybe: ``To motivate this proposal, the
-state of the art of nuclear reactor control, blah, and blah, are discussed
-in this section.''}
+systems that are tractably safe. To understand what is being automated, we must
+first understand how nuclear reactors are operated today. This section examines
+reactor operators and the operating procedures we aim to leverage, then
+investigates limitations of human-based operation, and concludes with current
+formal methods approaches to reactor control 
+systems.\splitnote{Good roadmap --- tells reader exactly what's 
+coming.}\dasinline{Don't like ``we'' here. Sounds like
+``we're going on an adventure!'' and feels jocular.
+Maybe: ``To motivate this proposal, the state of
+the art of nuclear reactor control, blah, and blah,
+are discussed in this section.''}
 
 \subsection{Current Reactor Procedures and Operation}
 
-\oldt{Nuclear plant procedures exist in a hierarchy: normal operating
-procedures for routine operations, abnormal operating procedures for
-off-normal conditions, Emergency Operating Procedures (EOPs) for
-design-basis accidents, Severe Accident Management Guidelines (SAMGs) for
-beyond-design-basis events, and Extensive Damage Mitigation Guidelines
-(EDMGs) for catastrophic damage scenarios.} \newt{Nuclear plant operations
-are governed by a hierarchy of written procedures, ranging from normal
-operating procedures for routine operations to Emergency Operating
-Procedures (EOPs) for design-basis accidents and Severe Accident Management
-Guidelines (SAMGs) for beyond-design-basis events. These procedures exist
-because reactor operation requires deterministic responses to a wide range
-of plant conditions, from routine power changes to catastrophic
-failures.}\dasinline{This sentence is MASSIVE. Why is there 6 lines
-describing different types of procedures? WHO CARES? Need a sentence after
-saying why we have these procedures.} These procedures must comply with 10
-CFR 50.34(b)(6)(ii) and are developed using guidance from
-NUREG-0899~\cite{NUREG-0899, 10CFR50.34}, but their development relies
-fundamentally on expert judgment and simulator validation rather than formal
-verification.
+Nuclear plant procedures exist in a hierarchy: normal operating procedures for
+routine operations, abnormal operating procedures for off-normal conditions,
+Emergency Operating Procedures (EOPs) for design-basis accidents, Severe
+Accident Management Guidelines (SAMGs) for beyond-design-basis events, and
+Extensive Damage Mitigation Guidelines (EDMGs) for catastrophic damage
+scenarios.\dasinline{This sentence is MASSIVE. Why is
+there 6 lines describing different types of
+procedures? WHO CARES? Need a sentence after saying
+why we have these procedures.} These procedures must comply with 10 CFR 50.34(b)(6)(ii) and are
+developed using guidance from NUREG-0899~\cite{NUREG-0899, 10CFR50.34}, but their
+development relies fundamentally on expert judgment and simulator validation
+rather than formal verification. Procedures undergo technical evaluation,
+simulator validation testing, and biennial review as part of operator
+requalification under 10 CFR 55.59~\cite{10CFR55.59}. Despite this rigor,
+procedures fundamentally lack formal verification of key safety 
+properties.\dasinline{Does the audience know what formal
+verification is at this point? Probably, but should
+say differently. Maybe `exhaustive' or
+`definitive'.} No
+mathematical proof exists that procedures cover all possible plant states, that
+required actions can be completed within available timeframes, or that
+transitions between procedure sets maintain safety 
+invariants.\splitsuggest{This paragraph is doing a lot. Consider splitting: 
+first paragraph on the hierarchy and compliance, second on the lack of formal 
+verification. The ``No mathematical proof exists...'' sentence is powerful and 
+deserves emphasis.}
 
-Procedures undergo technical evaluation, simulator validation testing, and
-biennial review as part of operator requalification under 10 CFR
-55.59~\cite{10CFR55.59}. Despite this rigor, procedures fundamentally lack
-\oldt{formal verification of key safety properties.} \newt{exhaustive
-verification of key safety properties.}\dasinline{Does the audience know
-what formal verification is at this point? Probably, but should say
-differently. Maybe `exhaustive' or `definitive'.} No mathematical proof
-exists that procedures cover all possible plant states, that required actions
-can be completed 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
+simulator validation. No mathematical proof exists that procedures cover all
+possible plant states, that required actions can be completed within available
+timeframes, or that transitions between procedure sets maintain safety
+invariants. Paper-based procedures cannot ensure correct application, and even
+computer-based procedure systems lack the formal guarantees that automated
+reasoning could provide.\splitpolish{This repeats the ``No mathematical 
+proof exists...'' sentence almost verbatim from the paragraph above. Either 
+cut it from the paragraph or from the LIMITATION box.}
 
-\textbf{LIMITATION:} \textit{Procedures lack exhaustive verification of
-correctness and completeness.} \oldt{Current procedure development relies on
-expert judgment and simulator validation. No mathematical proof exists that
-procedures cover all possible plant states, that required actions can be
-completed within available timeframes, or that transitions between procedure
-sets maintain safety invariants. Paper-based procedures cannot ensure correct
-application, and even computer-based procedure systems lack the formal
-guarantees that automated reasoning could provide.} \newt{Paper-based
-procedures cannot ensure correct application, and even computer-based
-procedure systems lack the guarantees that automated reasoning could
-provide.}\splitpolish{This repeats the ``No mathematical proof exists...''
-sentence almost verbatim from the paragraph above. Either cut it from the
-paragraph or from the LIMITATION box.}
+Nuclear plants operate with multiple control modes: automatic control, where the
+reactor control system maintains target parameters through continuous reactivity
+adjustment; manual control, where operators directly manipulate the reactor; and
+various intermediate modes. In typical pressurized water reactor operation, the
+reactor control system automatically maintains a floating average temperature
+and compensates for power demand changes through reactivity feedback loops
+alone. Safety systems, by contrast, operate with implemented automation. Reactor
+Protection Systems trip automatically on safety signals with millisecond
+response times, and engineered safety features actuate automatically on accident
+signals without operator action required.
 
-Nuclear plants operate with multiple control modes: automatic control, where
-the reactor control system maintains target parameters through continuous
-reactivity adjustment; manual control, where operators directly manipulate
-the reactor; and various intermediate modes. In typical pressurized water
-reactor operation, the reactor control system automatically maintains a
-floating average temperature and compensates for power demand changes through
-reactivity feedback loops alone. Safety systems, by contrast, operate with
-implemented automation. Reactor Protection Systems trip automatically on
-safety signals with millisecond response times, and engineered safety
-features actuate automatically on accident signals without operator action
-required.
-
-\oldt{The division between automated and human-controlled functions reveals
-the fundamental challenge of hybrid control. Highly automated systems handle
-reactor protection---automatic trips on safety parameters, emergency core
-cooling actuation, containment isolation, and basic process
-control~\cite{WRPS.Description, gentillon_westinghouse_1999}. Human
-operators, however, retain control of strategic decision-making: power level
-changes, startup/shutdown sequences, mode transitions, and procedure
-implementation.} \newt{This division between automated and human-controlled
-functions is itself the hybrid control problem. Automated systems handle
-reactor protection: trips on safety parameters, emergency core cooling
+\dasinline{After reading the next sentence, ``key safety''
+can honestly just be a semicolon.}
+\dasinline{Not sure what the challenge actually is
+as this paragraph is written. What's the point?}
+The division between automated and human-controlled functions reveals the
+fundamental challenge of hybrid control. Highly automated systems handle reactor
+protection---automatic trips on safety parameters, emergency core cooling
 actuation, containment isolation, and basic process
-control~\cite{WRPS.Description, gentillon_westinghouse_1999}. Human
-operators retain control of everything else: power level changes,
+control~\cite{WRPS.Description, gentillon_westinghouse_1999}. Human operators,
+however, retain control of strategic decision-making: power level changes,
 startup/shutdown sequences, mode transitions, and procedure 
-implementation.}\dasinline{After reading the next sentence, ``key safety''
-can honestly just be a semicolon.}\dasinline{Not sure what the challenge
-actually is as this paragraph is written. What's the
-point?}\splitnote{This is the key insight — the hybrid nature is already
-there, just not formally verified.}
+implementation.\splitnote{This is the key insight — the hybrid nature is 
+already there, just not formally verified.}
 
 \subsection{Human Factors in Nuclear Accidents}
 
-\oldt{Current-generation nuclear power plants employ over 3,600 active
-NRC-licensed reactor operators in the United
-States~\cite{operator_statistics}. These operators divide into Reactor
-Operators (ROs), who manipulate reactor controls, and Senior Reactor
-Operators (SROs), who direct plant operations and serve as 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.} \newt{Nuclear plant staffing
-requires at least two Reactor Operators (ROs) and one Senior Reactor
-Operator (SRO) per unit~\cite{10CFR50.54}, with operators requiring several
-years of training and NRC licensing under 10 CFR Part
-55~\cite{10CFR55}.}\dasinline{Why is this here? Should this be in broader
-impacts about running out of ROs? As it is here I have no idea why this is
-here.}
+Current-generation nuclear power plants employ over 3,600 active NRC-licensed
+reactor operators in the United 
+States~\cite{operator_statistics}.\dasinline{Why is this here? Should this
+be in broader impacts about running out of ROs?
+As it is here I have no idea why this is here.} These
+operators divide into Reactor Operators (ROs), who manipulate reactor controls,
+and Senior Reactor Operators (SROs), who direct plant operations and serve as
+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.
 
-The persistent role of human error in nuclear safety incidents---despite
-decades of improvements in training and procedures---provides the most
-compelling motivation for formal automated control with mathematical safety
-guarantees.\splitnote{Strong thesis for this subsection.} Operators hold
-legal authority under 10 CFR Part 55 to make critical
-decisions~\cite{10CFR55},\dasinline{Cite.} including departing from normal
-regulations during emergencies. \oldt{The Three Mile Island (TMI) accident}
-\newt{This authority itself introduces risk. The Three Mile Island (TMI)
-accident}\dasinline{Needs a connector here. Like ``But this can in and of
-itself prime plants for an accident.'' Then continue.} demonstrated how a
-combination of personnel error, design deficiencies, and component failures
-led to partial meltdown when operators misread confusing and contradictory
-readings and 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
-formal verification that operators can fulfill this responsibility does not
-guarantee safety. This tension between operational flexibility and safety
-assurance remains unresolved: the person responsible for reactor safety is
-often the root cause of failures.\splitnote{``the person responsible for
-reactor safety is often the root cause of failures'' — devastating summary.
-Very effective.}
+The persistent role of human error in nuclear safety incidents---despite decades
+of improvements in training and procedures---provides the most compelling
+motivation for formal automated control with mathematical safety 
+guarantees.\splitnote{Strong thesis for this subsection.}
+Operators hold legal authority under 10 CFR Part 55 to make critical 
+decisions,\dasinline{Cite.}
+including departing from normal regulations during emergencies. 
+\dasinline{Needs a connector here. Like ``But this can
+in and of itself prime plants for an accident.''
+Then continue.}The Three Mile
+Island (TMI) accident demonstrated how a combination of personnel error, design
+deficiencies, and component failures led to partial meltdown when operators
+misread confusing and contradictory readings and 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 formal verification that operators can fulfill this
+responsibility does not guarantee safety. This tension between operational
+flexibility and safety assurance remains unresolved: the person responsible for
+reactor safety is often the root cause of 
+failures.\splitnote{``the person responsible for reactor safety is often the 
+root cause of failures'' — devastating summary. Very effective.}
 
 Multiple independent analyses converge on a striking statistic: 70--80\% of
-nuclear power plant events are attributed to human error, versus
-approximately 20\% to equipment failures~\cite{WNA2020}. More significantly,
-the root cause of all severe accidents at nuclear power plants---Three Mile
-Island, Chernobyl, and Fukushima Daiichi---has been identified as poor
-safety management and safety culture: primarily human
-factors~\cite{hogberg_root_2013}. A detailed analysis of 190 events at
-Chinese nuclear power plants from
-2007--2020~\cite{zhang_analysis_2025} found that 53\% of events involved
-active errors, while 92\% were associated with latent
-errors---organizational and systemic weaknesses that create conditions for
+nuclear power plant events are attributed to human error, versus approximately
+20\% to equipment failures~\cite{WNA2020}. More significantly, the root cause of
+all severe accidents at nuclear power plants---Three Mile Island, Chernobyl, and
+Fukushima Daiichi---has been identified as poor safety management and safety
+culture: primarily human factors~\cite{hogberg_root_2013}. A detailed analysis
+of 190 events at Chinese nuclear power plants from
+2007--2020~\cite{zhang_analysis_2025} found that 53\% of events involved active
+errors, while 92\% were associated with latent errors---organizational and
+systemic weaknesses that create conditions for 
 failure.\splitnote{Strong empirical grounding. The Chinese plant data is a 
 nice addition — shows this isn't just a Western regulatory perspective.}
 
 
-\textbf{LIMITATION:} \textit{Human factors impose fundamental reliability
-limits that cannot be overcome through training alone.} The persistent human
-error contribution despite four decades of improvements demonstrates that
-these limitations are fundamental rather than a remediable part of
-human-driven control.\splitnote{Well-stated. The ``four decades'' point
-drives it home.}
+\textbf{LIMITATION:} \textit{Human factors impose fundamental reliability limits
+that cannot be overcome through training alone.} The persistent human
+error contribution despite four decades of improvements demonstrates that these
+limitations are fundamental rather than a remediable part of human-driven 
+control.\splitnote{Well-stated. The ``four decades'' point drives it home.}
 
 \subsection{Formal Methods}
 \subsubsection{HARDENS}
 
 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}.
+project represents the most advanced application of formal methods to nuclear
+reactor control systems to date~\cite{Kiniry2024}.
 
-HARDENS aimed to address a fundamental dilemma: existing U.S. nuclear
-control rooms rely on analog technologies from the
-1950s--60s.\dasinline{Source?} This technology is obsolete compared to
-modern control systems and incurs significant risk and 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)
-implementation with full traceability from \oldt{NRC Request for Proposals
-and IEEE standards through formal architecture specifications to verified
-software.} \newt{regulatory requirements through formal architecture
-specifications to verified software.}\dasinline{Wordsmith this to remove the
-RFP and IEEE standards language. Should just say requirements.}
+HARDENS aimed to address a fundamental dilemma: existing U.S. nuclear control
+rooms rely on analog technologies from the 1950s--60s.\dasinline{Source?}
+This technology is
+obsolete compared to modern control systems and incurs significant risk and
+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)
+implementation with full traceability from NRC Request for Proposals and IEEE
+standards through formal architecture specifications to verified 
+software.\dasinline{Wordsmith this to remove the RFP and
+IEEE standards language. Should just say
+requirements.}
 
-\oldt{HARDENS employed formal methods tools and techniques across the
-verification hierarchy.} \newt{HARDENS employed formal methods tools at
-every level of system development, from high-level requirements through
-executable models to generated code.}\dasinline{Zero discussion about what
-the verification hierarchy is. What is a specification or a requirement to
-someone who hasn't heard of one before?} High-level specifications used
-Lando, SysMLv2, and FRET (NASA Formal Requirements Elicitation Tool) to
-capture stakeholder requirements, domain engineering, certification
-requirements, and safety requirements. Requirements were analyzed for
-consistency, completeness, and realizability using SAT and SMT solvers.
-Executable formal models used Cryptol to create a behavioral model of the
-entire RTS, including all subsystems, components, and limited digital twin
+HARDENS employed formal methods tools and techniques across the verification
+hierarchy.\dasinline{Zero discussion about what the
+verification hierarchy is. What is a specification
+or a requirement to someone who hasn't heard of
+one before?} High-level specifications used Lando, SysMLv2, and FRET (NASA Formal
+Requirements Elicitation Tool) to capture stakeholder requirements, domain
+engineering, certification requirements, and safety requirements. Requirements
+were analyzed for consistency, completeness, and realizability using SAT and SMT
+solvers. Executable formal models used Cryptol to create a behavioral model of
+the entire RTS, including all subsystems, components, and limited digital twin
 models of sensors, actuators, and compute infrastructure. Automatic code
 synthesis generated verifiable C implementations and SystemVerilog hardware
-implementations directly from Cryptol models---eliminating the traditional
-gap between specification and implementation where errors commonly
+implementations directly from Cryptol models---eliminating the traditional gap
+between specification and implementation where errors commonly 
 arise.\splitnote{Good technical depth on HARDENS toolchain.}
 
-\oldt{Despite its accomplishments, HARDENS has a fundamental limitation
-directly relevant to hybrid control synthesis: the project addressed only
-discrete digital control logic without modeling or verifying continuous
-reactor dynamics. The Reactor Trip System specification and verification
-covered discrete state transitions (trip/no-trip decisions), digital sensor
-input processing through discrete logic, and discrete actuation outputs
-(reactor trip commands). The project did not address continuous dynamics of
-nuclear reactor physics. Real reactor safety depends on the interaction
-between continuous processes---temperature, pressure, neutron flux---evolving
-in response to discrete control decisions. HARDENS verified the discrete
-controller in isolation but not the closed-loop hybrid system behavior.}
-\newt{Despite these accomplishments, HARDENS addressed only discrete digital
-control logic. The Reactor Trip System verification covered discrete state
-transitions, digital sensor processing, and discrete actuation outputs. It
-did not model or verify continuous reactor dynamics. Real reactor safety
-depends on the interaction between continuous processes---temperature,
-pressure, neutron flux---evolving in response to discrete control decisions.
-HARDENS verified the discrete controller in isolation but not the
-closed-loop hybrid system behavior.}\dasinline{Edit these to more clearly
-separate the context from the limit. The limitation should be in the
-limitation.}\splitnote{Clear articulation of the gap your work fills.}
+Despite its accomplishments, HARDENS has a fundamental limitation directly
+relevant to hybrid control synthesis: the project addressed only discrete
+digital control logic without modeling or verifying continuous reactor 
+dynamics.\dasinline{Edit these to more clearly separate
+the context from the limit. The limitation should
+be in the limitation.}
+The Reactor Trip System specification and verification covered discrete state
+transitions (trip/no-trip decisions), digital sensor input processing through
+discrete logic, and discrete actuation outputs (reactor trip commands). The
+project did not address continuous dynamics of nuclear reactor physics. Real
+reactor safety depends on the interaction between continuous
+processes---temperature, pressure, neutron flux---evolving in response to
+discrete control decisions. HARDENS verified the discrete controller in
+isolation but not the closed-loop hybrid system 
+behavior.\splitnote{Clear articulation of the gap your work fills.}
 
-\textbf{LIMITATION:} \textit{HARDENS addressed discrete control logic
-without continuous dynamics or hybrid system verification.} Verifying
-discrete control logic alone provides no guarantee that the closed-loop
-system exhibits desired continuous behavior such as stability, convergence to
-setpoints, or maintained safety margins.
+\textbf{LIMITATION:} \textit{HARDENS addressed discrete control logic without
+continuous dynamics or hybrid system verification.} Verifying discrete control
+logic alone provides no guarantee that the closed-loop system exhibits desired
+continuous behavior such as stability, convergence to setpoints, or maintained
+safety margins.
 
 HARDENS produced a demonstrator system at Technology Readiness Level 2--3
-(analytical proof of concept with laboratory breadboard validation) rather
-than a deployment-ready system validated through extended operational
-testing. The NRC Final Report explicitly notes~\cite{Kiniry2024} that all
-material is considered in development, not a finalized product, and that
-``The demonstration of its technical soundness was to be at a level
-consistent with satisfaction of the current regulatory criteria, although
-with no explicit demonstration of how regulatory requirements are
-met.''\dasinline{Check this quote. Absolutely damning for HARDENS if true
-and hilarious Galois said this.} The project did not include deployment in
-actual nuclear facilities, testing with real reactor systems under
-operational conditions, side-by-side validation with operational analog RTS
-systems, systematic failure mode testing, NRC licensing review, or human
-factors validation with licensed operators in realistic control room
-scenarios.
+(analytical proof of concept with laboratory breadboard validation) rather than
+a deployment-ready system validated through extended operational testing. The
+NRC Final Report explicitly notes~\cite{Kiniry2024} that all material is
+considered in development, not a finalized product, and that ``The demonstration
+of its technical soundness was to be at a level consistent with satisfaction of
+the current regulatory criteria, although with no explicit demonstration of how
+regulatory requirements are 
+met.''\dasinline{Check this quote. Absolutely damning
+for HARDENS if true and hilarious Galois said
+this.} The project did not include deployment in
+actual nuclear facilities, testing with real reactor systems under operational
+conditions, side-by-side validation with operational analog RTS systems,
+systematic failure mode testing (radiation effects, electromagnetic
+interference, temperature extremes), NRC licensing review, or human factors
+validation with licensed operators in realistic control room scenarios.
 
 \textbf{LIMITATION:} \textit{HARDENS achieved TRL 2--3 without experimental
-validation.} \oldt{While formal verification provides mathematical
-correctness guarantees for the implemented discrete logic, the gap between
-formal verification and actual system deployment involves myriad practical
-considerations: integration with legacy systems, long-term reliability under
-harsh environments, human-system interaction in realistic operational
-contexts, and regulatory acceptance of formal methods as primary assurance
-evidence.} \newt{The gap between formal verification and actual system
-deployment remains wide: integration with legacy systems, long-term
-reliability under harsh environments, human-system interaction, and
-regulatory acceptance of formal methods as primary assurance
-evidence.}\dasinline{Same as before. Separate limit from context better.}
+validation.}\dasinline{Same as before. Separate limit
+from context better.} While formal verification provides mathematical correctness
+guarantees for the implemented discrete logic, the gap between formal
+verification and actual system deployment involves myriad practical
+considerations: integration with legacy systems, long-term reliability
+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}
-\oldt{There has been additional work to do verification of hybrid systems by
-extending the temporal logics directly.} \newt{A separate line of work
-extends temporal logics to verify hybrid systems
-directly.}\dasinline{Need to introduce temporal logic and FRET here first.}
-The result has been the field of 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 \oldt{ivariant} \newt{invariant} being
-enforced for the system.\splitfix{Typo: ``ivariant'' should be
-``invariant''} The second operator, the diamond operator
-\(<\alpha>\phi\) says that for the region \(\phi\), there is at least one
-trajectory of \(\alpha\) that enters that region. This is a declaration of a
+There has been additional work to do verification of hybrid systems by extending
+the temporal logics 
+directly.\dasinline{Need to introduce temporal logic
+and FRET here first.} The result has been the field of 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
+ivariant being enforced for the system.\splitfix{Typo: ``ivariant'' should be 
+``invariant''} The second operator, the diamond
+operator \(<\alpha>\phi\) says that for the region \(\phi\), there is at least
+one trajectory of \(\alpha\) that enters that region. This is a declaration of a
 liveness property. 
 
 %source: https://symbolaris.com/logic/dL.html
 
-While dL allows for the specification of these liveness and safety
-properties, actually proving them for a given hybrid system is quite
-difficult. Automated proof assistants such as KeYmaera X exist to help
-develop proofs of systems using dL, but so far have been insufficient for
-reasonably complex hybrid systems. The main issue behind creating system
-proofs using dL is state space explosion and non-terminating solutions.
+While dL allows for the specification of these liveness and safety properties,
+actually proving them for a given hybrid system is quite difficult. Automated
+proof assistants such as KeYmaera X exist to help develop proofs of systems
+using dL, but so far have been insufficient for reasonably complex hybrid
+systems. The main issue behind creating system proofs using dL is state space
+explosion and non-terminating 
+solutions.\splitsuggest{Consider adding a concrete example here — ``For 
+instance, a system with N modes and M continuous state variables...'' to give 
+readers a sense of the scaling problem.}
 %Source: that one satellite tracking paper that has the problem with the
 %gyroscopes overloding and needing to dump speed all the time
-Approaches have been made to alleviate these issues for nuclear power
-contexts using contract and decomposition based methods, \oldt{but are far
-from a complete methodology to design systems with.} \newt{but do not yet
-constitute a complete design methodology.}\splitpolish{``but are far from a
-complete methodology to design systems with'' — awkward ending preposition.}
+Approaches have been made to alleviate
+these issues for nuclear power contexts using contract and decomposition based
+methods, but are far from a complete methodology to design systems 
+with.\splitpolish{``but are far from a complete methodology to design systems 
+with'' — awkward ending preposition. Try: ``but remain far from a complete 
+design methodology'' or ``but do not yet constitute a complete design 
+methodology.''}
 %source: Manyu's thesis. 
 Instead, these approaches have been used on systems that have been designed a
 priori, and require expert knowledge to create the system proofs. 
 
 %Maybe a limitation here? Something about dL doesn't scale or help in design
-%very much, so the limitation is that logic based hybrid system approaches
-%have not been used in the DESIGN of autonomous controllers, only in the
-%analysis of systems that already exist.
-
-\textbf{LIMITATION:} \textit{Differential dynamic logic has been used for
-post-hoc analysis of existing systems, not for the constructive design of
-autonomous controllers.} Current dL-based approaches verify systems that
-have already been designed, requiring expert knowledge to construct proofs.
-They have not been applied to the synthesis of new controllers from
-operational requirements.\splitinline{Your comment here is spot-on. You
-should add a LIMITATION box: \textit{Differential dynamic logic has been
-used for post-hoc analysis of existing systems, not for the constructive
-design of autonomous controllers.} This is exactly the gap you're filling —
-you're doing synthesis, not just verification.}
+%very much, so the limitation is that logic based hybrid system approaches have
+%not been used in the DESIGN of autonomous controllers, only in the analysis of
+%systems that already exist.
+\splitinline{Your comment here is spot-on. You should add a LIMITATION box: 
+\textit{Differential dynamic logic has been used for post-hoc analysis of 
+existing systems, not for the constructive design of autonomous controllers.} 
+This is exactly the gap you're filling — you're doing synthesis, not just 
+verification.}

4-metrics-of-success/metrics.tex

@@ -6,36 +6,33 @@ demonstration. This work begins at TRL 2--3 and aims to reach TRL 5, where
 system components operate successfully in a relevant laboratory 
 environment.\splitnote{TRL as primary metric is smart — speaks industry 
 language.}
-This section explains why TRL advancement provides the most appropriate
-success metric and defines the specific criteria required to achieve TRL 5.
+This section explains why TRL advancement provides the most appropriate success
+metric and defines the specific criteria required to achieve TRL 5.
 
-\oldt{Technology Readiness Levels provide the ideal success metric because
-they explicitly measure 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. TRLs measure both dimensions
-simultaneously.} \newt{TRLs measure the gap between academic
-proof-of-concept and practical deployment, which is precisely what this work
-aims to bridge. Academic metrics alone cannot capture practical feasibility,
-and empirical metrics alone cannot demonstrate theoretical rigor. TRLs
-measure both simultaneously.}\dasinline{Chop. No likey.}\splitnote{Good
-framing — explains why other metrics are insufficient.} 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 hardware testing.
+Technology Readiness Levels provide the ideal success metric because they
+explicitly measure the gap between academic proof-of-concept and 
+practical\dasinline{Chop. No likey.}
+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. TRLs measure both dimensions 
+simultaneously.\splitnote{Good framing — explains why other metrics are 
+insufficient.}
+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
+hardware testing.
 
 The nuclear industry requires extremely high assurance before deploying new
 control technologies. Demonstrating theoretical correctness alone is
 insufficient for adoption; conversely, showing empirical performance without
-formal guarantees fails to meet regulatory requirements. TRLs capture this
-dual requirement naturally. Each level represents both increased practical
-maturity and sustained theoretical validity. Furthermore, TRL assessment
-forces explicit identification of remaining barriers to deployment. The
-nuclear industry already uses TRLs for technology assessment, making this
-metric directly relevant to potential adopters. Reaching TRL 5 provides a
-clear answer to industry questions about feasibility and maturity that
-academic publications alone cannot.
+formal guarantees fails to meet regulatory requirements. TRLs capture this dual
+requirement naturally. Each level represents both increased practical maturity
+and sustained theoretical validity. Furthermore, TRL assessment forces explicit
+identification of remaining barriers to deployment. The nuclear industry already
+uses TRLs for technology assessment, making this metric directly relevant to
+potential adopters. Reaching TRL 5 provides a clear answer to industry questions
+about feasibility and maturity that academic publications alone cannot.
 
 Moving from current state to target requires achieving three intermediate
 levels, each representing a distinct validation milestone:
@@ -48,8 +45,8 @@ temporal logic specifications that pass realizability analysis. A discrete
 automaton must be synthesized with interpretable structure. At least one
 continuous controller must be designed with reachability analysis proving
 transition requirements are satisfied. Independent review must confirm that
-specifications match intended procedural behavior. This proves the
-fundamental approach on a simplified startup sequence.
+specifications match intended procedural behavior. This proves the fundamental
+approach on a simplified startup sequence.
 
 \paragraph{TRL 4 \textit{Laboratory Testing of Integrated Components}}
 
@@ -60,44 +57,41 @@ must exist for all discrete modes. Verification must be complete for all mode
 transitions using reachability analysis, barrier certificates, and
 assume-guarantee contracts. The integrated controller must execute complete
 startup sequences in software simulation with zero safety violations across
-multiple consecutive runs. This proves that formal correctness guarantees can
-be maintained throughout system integration.
+multiple consecutive runs. This proves that formal correctness guarantees can be
+maintained throughout system integration.
 
 \paragraph{TRL 5 \textit{Laboratory Testing in Relevant Environment}}
 
 For this research, TRL 5 means demonstrating the verified controller on
-industrial control hardware through hardware-in-the-loop testing. The
-discrete automaton must be implemented on the Emerson Ovation control system
-and verified to match synthesized specifications exactly. Continuous
-controllers must execute at required rates. The ARCADE interface must
-establish stable real-time communication between the Emerson Ovation hardware
-and SmAHTR simulation. Complete autonomous startup sequences must execute via
-hardware-in-the-loop across the full operational envelope. The controller
-must handle off-nominal scenarios to validate that expulsory modes function
-correctly. For example, simulated sensor failures must trigger appropriate
-fault detection and mode transitions, and loss-of-cooling scenarios must
-activate SCRAM procedures as specified. Graded responses to minor
-disturbances are outside this work's scope\oldt{.}\newt{, as they require
-runtime optimization under uncertainty that extends beyond the
-correct-by-construction verification framework presented
-here.}\splitsuggest{Consider noting why graded responses are out of scope —
-is it time, complexity, or scope creep? Brief justification helps.} Formal
-verification results must remain valid, with discrete behavior matching
+industrial control hardware through hardware-in-the-loop testing. The discrete
+automaton must be implemented on the Emerson Ovation control system and verified
+to match synthesized specifications exactly. Continuous controllers must execute
+at required rates. The ARCADE interface must establish stable real-time
+communication between the Emerson Ovation hardware and SmAHTR simulation.
+Complete autonomous startup sequences must execute via hardware-in-the-loop
+across the full operational envelope. The controller must handle off-nominal
+scenarios to validate that expulsory modes function correctly. For example,
+simulated sensor failures must trigger appropriate fault detection and mode
+transitions, and loss-of-cooling scenarios must activate SCRAM procedures as
+specified. Graded responses to minor disturbances are outside this work's 
+scope.\splitsuggest{Consider noting why graded responses are out of scope — 
+is it time, complexity, or scope creep? Brief justification helps.}
+Formal verification results must remain valid, with discrete behavior matching
 specifications and continuous trajectories remaining within verified bounds.
-This proves that the methodology produces verified controllers implementable
-on industrial hardware.
+This proves that the methodology produces verified controllers implementable on
+industrial hardware.
 
 Progress will be assessed quarterly through collection of specific data
 comparing actual results against TRL advancement criteria. Specification
 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
+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
 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 that the methodology
-produces verified controllers and that implementation is achievable with
-current technology.\splitnote{Clear success criteria. Committee will know
-exactly what ``done'' looks like.}
+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 that the methodology produces verified
+controllers and that implementation is achievable with current 
+technology.\splitnote{Clear success criteria. Committee will know exactly 
+what ``done'' looks like.}

5-risks-and-contingencies/risks.tex

@@ -1,11 +1,9 @@
 \section{Risks and Contingencies}
 
-This research relies on several critical assumptions that, if invalidated,
-would require scope adjustment or methodological
-revision.\splitnote{Honest acknowledgment of risks with clear contingencies
-— committee will appreciate this.} The primary risks to successful
-completion fall into four categories: computational tractability of synthesis
-and verification, complexity of the discrete-continuous interface,
+This research relies on several critical assumptions that, if invalidated, would
+require scope adjustment or methodological revision.\splitnote{Honest acknowledgment of risks with clear contingencies — committee will appreciate this.} The primary risks to
+successful completion fall into four categories: computational tractability of
+synthesis and verification, complexity of the discrete-continuous interface,
 completeness of procedure formalization, and hardware-in-the-loop integration
 challenges. Each risk has associated indicators for early detection and
 contingency plans that preserve research value even if core assumptions prove
@@ -17,23 +15,22 @@ 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 risk
-that temporal logic specifications derived from complete startup procedures
-may produce automata with thousands of states. Such large automata would
-require synthesis times exceeding days or weeks, preventing demonstration of
-the complete methodology within project timelines. Reachability analysis for
+synthesis scales exponentially with specification complexity, creating risk that
+temporal logic specifications derived from complete startup procedures may
+produce automata with thousands of states. Such large automata would require
+synthesis times exceeding days or weeks, preventing demonstration of the
+complete methodology within project timelines. Reachability analysis for
 continuous modes with high-dimensional state spaces may similarly prove
 computationally intractable. Either barrier would constitute a fundamental
 obstacle to achieving the research objectives.
 
 Several indicators would provide early warning of computational tractability
 problems. Synthesis times exceeding 24 hours for simplified procedure subsets
-would suggest complete procedures are intractable. Generated automata
-containing more than 1,000 discrete states would indicate the discrete state
-space is too large for efficient verification. Specifications flagged as
-unrealizable by \oldt{FRET or Strix} \newt{realizability checking
-tools}\dasinline{Strix may not be the reactive synth tool anymore. Be more
-general.} would reveal fundamental conflicts in the formalized procedures.
+would suggest complete procedures are intractable. Generated automata containing
+more than 1,000 discrete states would indicate the discrete state space is too
+large for efficient verification. Specifications flagged as unrealizable by FRET
+or Strix\dasinline{Strix may not be the reactive synth
+tool anymore. Be more general.} would reveal fundamental conflicts in the formalized procedures.
 Reachability analysis failing to converge within reasonable time bounds would
 show that continuous mode verification cannot be completed with available
 computational resources.
@@ -41,130 +38,122 @@ computational resources.
 The contingency plan for computational intractability is to reduce scope to a
 minimal viable startup sequence. This reduced sequence would cover only cold
 shutdown to criticality to low-power hold, omitting power ascension and other
-operational phases. The subset would still demonstrate the complete
-methodology while reducing computational burden. The research contribution
-would remain valid even with reduced scope, proving that formal hybrid
-control synthesis is achievable for safety-critical nuclear applications. The
-limitation to simplified operational sequences would be explicitly documented
-as a constraint rather than a failure.
+operational phases. The subset would still demonstrate the complete methodology
+while reducing computational burden. The research contribution would remain
+valid even with reduced scope, proving that formal hybrid control synthesis is
+achievable for safety-critical nuclear applications. The limitation to
+simplified operational sequences would be explicitly documented as a constraint
+rather than a failure.
 
 \subsection{Discrete-Continuous Interface Formalization}
 
 The second critical assumption concerns the mapping between boolean guard
-conditions in temporal logic and 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.
-\oldt{Guard conditions requiring complex nonlinear predicates may resist
-boolean abstraction, making synthesis intractable.} \newt{Some guard
-conditions may require complex nonlinear predicates that cannot be cleanly
-expressed as boolean combinations of simple threshold checks, making
-synthesis intractable.}\dasinline{What does this mean?} 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,
-or continuous modes may be unable to guarantee convergence to discrete
-transition boundaries.
+conditions in temporal logic and 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, making
+synthesis intractable.\dasinline{What does this mean?} 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, or continuous modes may be unable to guarantee convergence
+to discrete transition boundaries.
 
 Early indicators of interface formalization problems would appear during both
-synthesis and verification phases. Guard conditions requiring complex
-nonlinear predicates that resist boolean abstraction would suggest
-fundamental misalignment between discrete specifications and continuous
-realities. Continuous safety regions that cannot be expressed as conjunctions
-of half-spaces or polynomial inequalities would indicate the interface
-between discrete guards and continuous invariants is too complex. Failure to
-construct barrier certificates proving safety across mode transitions would
-reveal that continuous dynamics cannot be formally related to discrete
-switching logic. Reachability analysis showing that continuous modes cannot
-reach intended transition boundaries from all possible initial conditions
-would demonstrate the synthesized discrete controller is incompatible with
-achievable continuous behavior.
+synthesis and verification phases. Guard conditions requiring complex nonlinear
+predicates that resist boolean abstraction would suggest fundamental misalignment
+between discrete specifications and continuous realities. Continuous safety
+regions that cannot be expressed as conjunctions of half-spaces or polynomial
+inequalities would indicate the interface between discrete guards and continuous
+invariants is too complex. Failure to construct barrier certificates proving
+safety across mode transitions would reveal that continuous dynamics cannot be
+formally related to discrete switching logic. Reachability analysis showing that
+continuous modes cannot reach intended transition boundaries from all possible
+initial conditions would demonstrate the synthesized discrete controller is
+incompatible with achievable continuous behavior.
 
-The primary contingency for interface complexity is restricting continuous
-modes to operate within polytopic invariants. Polytopes are state regions
-defined as intersections of linear half-spaces, which map directly to boolean
-predicates through linear inequality checks. This restriction ensures
-tractable synthesis while maintaining theoretical rigor, though at the cost
-of limiting expressiveness compared to arbitrary nonlinear regions. The
-discrete-continuous interface remains well-defined and verifiable with
-polytopic restrictions, providing a clear fallback position that preserves
-the core methodology. Conservative over-approximations offer an alternative
-approach: a nonlinear safe region can be inner-approximated by a polytope,
-sacrificing operational flexibility to maintain formal guarantees. The
-three-mode classification already structures the problem to minimize complex
-transitions, with critical safety properties concentrated in expulsory modes
-that can receive additional design attention.
+The primary contingency for interface complexity is restricting continuous modes
+to operate within polytopic invariants. Polytopes are state regions defined as
+intersections of linear half-spaces, which map directly to boolean predicates
+through linear inequality checks. This restriction ensures tractable synthesis
+while maintaining theoretical rigor, though at the cost of limiting
+expressiveness compared to arbitrary nonlinear regions. The discrete-continuous
+interface remains well-defined and verifiable with polytopic restrictions,
+providing a clear fallback position that preserves the core methodology.
+Conservative over-approximations offer an alternative approach: a nonlinear safe
+region can be inner-approximated by a polytope, sacrificing operational
+flexibility to maintain formal guarantees. The three-mode classification already
+structures the problem to minimize complex transitions, with critical safety
+properties concentrated in expulsory modes that can receive additional design
+attention.
 
 Mitigation strategies focus on designing continuous controllers with discrete
 transitions as primary objectives from the outset. Rather than designing
 continuous control laws independently and verifying transitions post-hoc, the
 approach uses transition requirements as design constraints. Control barrier
-functions provide a systematic method to synthesize controllers that
-guarantee forward invariance of safe sets and convergence to transition
-boundaries. This design-for-verification approach reduces the likelihood that
-interface complexity becomes insurmountable. Focusing verification effort on
-expulsory modes---where safety is most critical---allows more complex
-analysis to be applied selectively rather than uniformly across all modes,
-concentrating computational resources where they matter most for safety
-assurance.
+functions provide a systematic method to synthesize controllers that guarantee
+forward invariance of safe sets and convergence to transition boundaries. This
+design-for-verification approach reduces the likelihood that interface
+complexity becomes insurmountable. Focusing verification effort on expulsory
+modes---where safety is most critical---allows more complex analysis to be
+applied selectively rather than uniformly across all modes, concentrating
+computational resources where they matter most for safety assurance.
 
 \subsection{Procedure Formalization Completeness}
 
 The third assumption is that existing startup procedures contain sufficient
-detail and clarity for translation into temporal logic specifications.
-Nuclear operating procedures, while extensively detailed, were written for
-human operators who bring contextual understanding and adaptive reasoning to
-their interpretation. Procedures may contain implicit knowledge, ambiguous
-directives, or references to operator judgment that resist formalization in
-current specification languages. Underspecified timing constraints, ambiguous
-condition definitions, or gaps in operational coverage would cause synthesis
-to fail or produce incorrect automata. The risk is not merely that
-formalization is difficult, but that current procedures fundamentally lack
-the precision required for autonomous control, revealing a gap between
-human-oriented documentation and machine-executable specifications.
+detail and clarity for translation into temporal logic specifications. Nuclear
+operating procedures, while extensively detailed, were written for human
+operators who bring contextual understanding and adaptive reasoning to their
+interpretation. Procedures may contain implicit knowledge, ambiguous directives,
+or references to operator judgment that resist formalization in current
+specification languages. Underspecified timing constraints, ambiguous condition
+definitions, or gaps in operational coverage would cause synthesis to fail or
+produce incorrect automata. The risk is not merely that formalization is
+difficult, but that current procedures fundamentally lack the precision required
+for autonomous control, revealing a gap between human-oriented documentation and
+machine-executable specifications.
 
-Several indicators would reveal formalization completeness problems early in
-the project. FRET realizability checks failing due to underspecified
-behaviors or conflicting requirements would indicate procedures do not form a
-complete specification. Multiple valid interpretations of procedural steps
-with no clear resolution would demonstrate procedure language is
-insufficiently precise for automated synthesis. Procedures referencing
-``operator judgment,'' ``as appropriate,'' or similar discretionary language
-for critical decisions would explicitly identify points where human reasoning
-cannot be directly formalized. Domain experts unable to provide crisp answers
-to specification questions about edge cases would suggest the procedures
-themselves do not fully define system behavior, relying instead on operator
-training and experience to fill gaps.
+Several indicators would reveal formalization completeness problems early in the
+project. FRET realizability checks failing due to underspecified behaviors or
+conflicting requirements would indicate procedures do not form a complete
+specification. Multiple valid interpretations of procedural steps with no clear
+resolution would demonstrate procedure language is insufficiently precise for
+automated synthesis. Procedures referencing ``operator judgment,'' ``as
+appropriate,'' or similar discretionary language for critical decisions would
+explicitly identify points where human reasoning cannot be directly formalized.
+Domain experts unable to provide crisp answers to specification questions about
+edge cases would suggest the procedures themselves do not fully define system
+behavior, relying instead on operator training and experience to fill gaps.
 
 The contingency plan treats inadequate specification as itself a research
 contribution rather than a project failure. Documenting specific ambiguities
 encountered would create a taxonomy of formalization barriers: timing
-underspecification, missing preconditions, discretionary actions, and
-undefined failure modes. Each category would be analyzed to understand why
-current procedure-writing practices produce these gaps and what specification
-languages would need to address them. Proposed extensions to FRETish or
-similar specification languages would demonstrate how to bridge the gap
-between current procedures and the precision needed for autonomous control.
-The research output would shift from ``here is a complete autonomous
-controller'' to ``here is what formal autonomous control requires that
-current procedures do not provide, and here are language extensions to bridge
-that gap.'' This contribution remains valuable to both the nuclear industry
-and formal methods community, establishing clear requirements for
-next-generation procedure development and autonomous control specification
-languages.
+underspecification, missing preconditions, discretionary actions, and undefined
+failure modes. Each category would be analyzed to understand why current
+procedure-writing practices produce these gaps and what specification languages
+would need to address them. Proposed extensions to FRETish or similar
+specification languages would demonstrate how to bridge the gap between current
+procedures and the precision needed for autonomous control. The research output
+would shift from ``here is a complete autonomous controller'' to ``here is what
+formal autonomous control requires that current procedures do not provide, and
+here are language extensions to bridge that gap.'' This contribution remains
+valuable to both the nuclear industry and formal methods community, establishing
+clear requirements for next-generation procedure development and autonomous
+control specification languages.
 
 Early-stage procedure analysis with domain experts provides the primary
 mitigation strategy. Collaboration through the University of Pittsburgh Cyber
 Energy Center enables identification and resolution of ambiguities before
-synthesis attempts, rather than discovering them during failed synthesis
-runs. Iterative refinement with reactor operators and control engineers can
-clarify procedural intent before formalization begins, reducing the risk of
-discovering insurmountable specification gaps late in the project. Comparison
-with procedures from multiple reactor designs---pressurized water reactors,
-boiling water reactors, and advanced designs---may reveal common patterns and
-standard ambiguities amenable to systematic resolution. This cross-design
-analysis would strengthen the generalizability of any proposed specification
-language extensions, ensuring they address industry-wide practices rather
-than specific quirks.
+synthesis attempts, rather than discovering them during failed synthesis runs.
+Iterative refinement with reactor operators and control engineers can clarify
+procedural intent before formalization begins, reducing the risk of discovering
+insurmountable specification gaps late in the project. Comparison with
+procedures from multiple reactor designs---pressurized water reactors, boiling
+water reactors, and advanced designs---may reveal common patterns and standard
+ambiguities amenable to systematic resolution. This cross-design analysis would
+strengthen the generalizability of any proposed specification language
+extensions, ensuring they address industry-wide practices rather than specific
+quirks.

6-broader-impacts/impacts.tex

@@ -2,80 +2,72 @@
 
 Nuclear power presents both a compelling application domain and an urgent
 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 would minimize
-transmission losses and eliminate emissions from hydrocarbon-based
-alternatives. However, nuclear power economics at this scale demand careful
-attention to operating costs.
+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 would minimize transmission losses and
+eliminate emissions from hydrocarbon-based alternatives. However, nuclear power
+economics at this scale demand careful attention to operating costs.
 
-\oldt{According to the U.S. Energy Information Administration's Annual
-Energy Outlook 2022, advanced nuclear power entering service in 2027 is
-projected to cost \$88.24 per megawatt-hour~\cite{eia_lcoe_2022}. Datacenter
-electricity demand is projected to reach 1,050 terawatt-hours annually by
-2030~\cite{eesi_datacenter_2024}. If this demand were supplied by nuclear
-power, the total annual cost of power generation would exceed \$92 billion.
-Within this figure, operations and maintenance represents a substantial
-component. The EIA estimates that fixed O\&M costs alone account for \$16.15
-per megawatt-hour, with additional variable O\&M costs embedded in fuel and
-operating expenses~\cite{eia_lcoe_2022}. Combined, O\&M-related costs
-represent approximately 23--30\% of the total levelized cost of electricity,
-translating to \$21--28 billion annually for projected datacenter demand.}
-\newt{[DANE: Verify these figures are current. Check EIA Annual Energy
-Outlook 2024/2025 for updated LCOE projections. The \$88.24/MWh,
-\$16.15/MWh O\&M, and datacenter demand projections may have newer
-sources.]}\dasinline{Check all of this math and update if newer sources
-exist.}
+According to the U.S. Energy Information 
+Administration's\dasinline{Check all of this math and
+update if newer sources exist.} Annual Energy Outlook
+2022, advanced nuclear power entering service in 2027 is projected to cost
+\$88.24 per megawatt-hour~\cite{eia_lcoe_2022}. Datacenter electricity demand is
+projected to reach 1,050 terawatt-hours annually by
+2030~\cite{eesi_datacenter_2024}. If this demand were supplied by nuclear power,
+the total annual cost of power generation would exceed \$92 billion. Within this
+figure, operations and maintenance represents a substantial component. The EIA
+estimates that fixed O\&M costs alone account for \$16.15 per megawatt-hour,
+with additional variable O\&M costs embedded in fuel and operating
+expenses~\cite{eia_lcoe_2022}. Combined, O\&M-related costs represent
+approximately 23--30\% of the total levelized cost of electricity, translating
+to \$21--28 billion annually for projected datacenter demand.
 
 This research directly addresses the multi-billion-dollar O\&M cost challenge
 through high-assurance autonomous control. Current nuclear operations require
-full control room staffing for each reactor, whether large conventional units
-or small modular designs. These staffing requirements drive the high O\&M
-costs that make nuclear power economically challenging, particularly for
-smaller reactor designs where the same staffing overhead must be spread
-across lower power output. Synthesizing provably correct hybrid controllers
-from formal specifications can automate routine operational sequences that
-currently require constant human oversight. This enables a fundamental shift
-from direct operator control to supervisory monitoring, where operators
-oversee multiple autonomous reactors rather than manually controlling
-individual units.
+full control room staffing for each reactor, whether large conventional units or
+small modular designs. These staffing requirements drive the high O\&M costs
+that make nuclear power economically challenging, particularly for smaller
+reactor designs where the same staffing overhead must be spread across lower
+power output. Synthesizing provably correct hybrid controllers from formal
+specifications can automate routine operational sequences that currently require
+constant human oversight. This enables a fundamental shift from direct operator
+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
-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 sequences, power level changes, and normal operational
-transitions---that currently require human operators to follow written
-procedures. Operators will remain in supervisory roles to handle off-normal
-conditions and provide authorization for major operational changes, but the
-routine cognitive burden of procedure execution shifts to provably correct
-automated systems that are much cheaper to operate.
+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
+sequences, power level changes, and normal operational transitions---that
+currently require human operators to follow written procedures. Operators will
+remain in supervisory roles to handle off-normal conditions and provide
+authorization for major operational changes, but the routine cognitive burden of
+procedure execution shifts to provably correct automated systems that are much
+cheaper to operate.
 
 SMRs represent an ideal deployment target for this technology. Nuclear
-Regulatory Commission certification requires extensive documentation of
-control procedures, operational requirements, and safety analyses written in
-structured natural language. As described in our approach, these regulatory
-documents can be translated into temporal logic specifications using tools
-like FRET, then synthesized into discrete switching logic using reactive
-synthesis tools, and finally verified using reachability analysis and barrier
-certificates for the continuous control modes. The infrastructure of
-requirements and specifications already exists as part of the licensing
-process, creating a direct pathway from existing regulatory documentation to
-formally verified autonomous controllers.
+Regulatory Commission certification requires extensive documentation of control
+procedures, operational requirements, and safety analyses written in structured
+natural language. As described in our approach, these regulatory documents can
+be translated into temporal logic specifications using tools like FRET, then
+synthesized into discrete switching logic using reactive synthesis tools, and
+finally verified using reachability analysis and barrier certificates for the
+continuous control modes. The infrastructure of requirements and specifications
+already exists as part of the licensing process, creating a direct pathway from
+existing regulatory documentation to formally verified autonomous controllers.
 
-Beyond reducing operating costs for new reactors, this research will
-establish a generalizable framework for autonomous control of safety-critical
-systems. The methodology of translating operational procedures into formal
-specifications, synthesizing discrete switching logic, and verifying
-continuous mode behavior applies to any hybrid system with documented
-operational requirements. Potential applications include chemical process
-control, aerospace systems, and autonomous transportation, where similar
-economic and safety considerations favor increased autonomy with provable
-correctness guarantees. Demonstrating this approach in nuclear power---one of
-the most regulated and safety-critical
-domains\splitnote{``If it works here, it works anywhere — strong closing
-argument.}---will establish both the technical feasibility and regulatory
-pathway for broader adoption across critical infrastructure.
+Beyond reducing operating costs for new reactors, this research will establish a
+generalizable framework for autonomous control of safety-critical systems. The
+methodology of translating operational procedures into formal specifications,
+synthesizing discrete switching logic, and verifying continuous mode behavior
+applies to any hybrid system with documented operational requirements. Potential
+applications include chemical process control, aerospace systems, and autonomous
+transportation, where similar economic and safety considerations favor increased
+autonomy with provable correctness guarantees. Demonstrating this approach in
+nuclear power---one of the most regulated and safety-critical domains\splitnote{``If it works here, it works anywhere — strong closing argument.}---will
+establish both the technical feasibility and regulatory pathway for broader
+adoption across critical infrastructure.