Edit Impacts: flag economic figures for Dane to verify with updated sources

1-goals-and-outcomes/goals.tex

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

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

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

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

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

4-metrics-of-success/metrics.tex

@@ -6,33 +6,36 @@ 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
+This section explains why TRL advancement provides the most appropriate
-metric and defines the specific criteria required to achieve TRL 5.
+success metric and defines the specific criteria required to achieve TRL 5.
 
-Technology Readiness Levels provide the ideal success metric because they
+\oldt{Technology Readiness Levels provide the ideal success metric because
-explicitly measure the gap between academic proof-of-concept and 
+they explicitly measure the gap between academic proof-of-concept and
-practical\dasinline{Chop. No likey.}
+practical deployment---precisely what this work aims to bridge. Academic
-deployment---precisely what this work aims to bridge. Academic metrics like
+metrics like papers published or theorems proved cannot capture practical
-papers published or theorems proved cannot capture practical feasibility.
+feasibility. Empirical metrics like simulation accuracy or computational
-Empirical metrics like simulation accuracy or computational speed cannot
+speed cannot demonstrate theoretical rigor. TRLs measure both dimensions
-demonstrate theoretical rigor. TRLs measure both dimensions 
+simultaneously.} \newt{TRLs measure the gap between academic
-simultaneously.\splitnote{Good framing — explains why other metrics are 
+proof-of-concept and practical deployment, which is precisely what this work
-insufficient.}
+aims to bridge. Academic metrics alone cannot capture practical feasibility,
-Advancing from TRL 3 to TRL 5 requires maintaining theoretical rigor while
+and empirical metrics alone cannot demonstrate theoretical rigor. TRLs
-progressively demonstrating practical feasibility. Formal verification must
+measure both simultaneously.}\dasinline{Chop. No likey.}\splitnote{Good
-remain valid as the system moves from individual components to integrated
+framing — explains why other metrics are insufficient.} Advancing from TRL 3
-hardware testing.
+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
+formal guarantees fails to meet regulatory requirements. TRLs capture this
-requirement naturally. Each level represents both increased practical maturity
+dual requirement naturally. Each level represents both increased practical
-and sustained theoretical validity. Furthermore, TRL assessment forces explicit
+maturity and sustained theoretical validity. Furthermore, TRL assessment
-identification of remaining barriers to deployment. The nuclear industry already
+forces explicit identification of remaining barriers to deployment. The
-uses TRLs for technology assessment, making this metric directly relevant to
+nuclear industry already uses TRLs for technology assessment, making this
-potential adopters. Reaching TRL 5 provides a clear answer to industry questions
+metric directly relevant to potential adopters. Reaching TRL 5 provides a
-about feasibility and maturity that academic publications alone cannot.
+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:
@@ -45,8 +48,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
+specifications match intended procedural behavior. This proves the
-approach on a simplified startup sequence.
+fundamental approach on a simplified startup sequence.
 
 \paragraph{TRL 4 \textit{Laboratory Testing of Integrated Components}}
 
@@ -57,41 +60,44 @@ 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
+multiple consecutive runs. This proves that formal correctness guarantees can
-maintained throughout system integration.
+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
+industrial control hardware through hardware-in-the-loop testing. The
-automaton must be implemented on the Emerson Ovation control system and verified
+discrete automaton must be implemented on the Emerson Ovation control system
-to match synthesized specifications exactly. Continuous controllers must execute
+and verified to match synthesized specifications exactly. Continuous
-at required rates. The ARCADE interface must establish stable real-time
+controllers must execute at required rates. The ARCADE interface must
-communication between the Emerson Ovation hardware and SmAHTR simulation.
+establish stable real-time communication between the Emerson Ovation hardware
-Complete autonomous startup sequences must execute via hardware-in-the-loop
+and SmAHTR simulation. Complete autonomous startup sequences must execute via
-across the full operational envelope. The controller must handle off-nominal
+hardware-in-the-loop across the full operational envelope. The controller
-scenarios to validate that expulsory modes function correctly. For example,
+must handle off-nominal scenarios to validate that expulsory modes function
-simulated sensor failures must trigger appropriate fault detection and mode
+correctly. For example, simulated sensor failures must trigger appropriate
-transitions, and loss-of-cooling scenarios must activate SCRAM procedures as
+fault detection and mode transitions, and loss-of-cooling scenarios must
-specified. Graded responses to minor disturbances are outside this work's 
+activate SCRAM procedures as specified. Graded responses to minor
-scope.\splitsuggest{Consider noting why graded responses are out of scope — 
+disturbances are outside this work's scope\oldt{.}\newt{, as they require
-is it time, complexity, or scope creep? Brief justification helps.}
+runtime optimization under uncertainty that extends beyond the
-Formal verification results must remain valid, with discrete behavior matching
+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
 specifications and continuous trajectories remaining within verified bounds.
-This proves that the methodology produces verified controllers implementable on
+This proves that the methodology produces verified controllers implementable
-industrial hardware.
+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
+metrics and hardware integration milestones indicate progress toward TRL 5.
-research plan will be revised only when new data invalidates fundamental
+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
+operating on industrial control hardware through hardware-in-the-loop
-a relevant laboratory environment. This establishes both theoretical validity
+testing in a relevant laboratory environment. This establishes both
-and practical feasibility, proving that the methodology produces verified
+theoretical validity and practical feasibility, proving that the methodology
-controllers and that implementation is achievable with current 
+produces verified controllers and that implementation is achievable with
-technology.\splitnote{Clear success criteria. Committee will know exactly 
+current technology.\splitnote{Clear success criteria. Committee will know
-what ``done'' looks like.}
+exactly what ``done'' looks like.}

5-risks-and-contingencies/risks.tex

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

6-broader-impacts/impacts.tex

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