1-goals-and-outcomes/goals.tex

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

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

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

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

@@ -1,303 +1,269 @@
 \section{State of the Art and Limits of Current Practice}
 
 The principal aim of this research is to create autonomous reactor control
-systems that are tractably safe. \oldt{To understand what is being automated,
+systems that are tractably safe. To understand what is being automated, we must
-we must first understand how nuclear reactors are operated today. This section
+first understand how nuclear reactors are operated today. This section examines
-examines reactor operators and the operating procedures we aim to leverage,
+reactor operators and the operating procedures we aim to leverage, then
-then investigates limitations of human-based operation, and concludes with
+investigates limitations of human-based operation, and concludes with current
-current formal methods approaches to reactor control systems.}
+formal methods approaches to reactor control 
-\newt{Understanding what is being automated requires understanding how
+systems.\splitnote{Good roadmap --- tells reader exactly what's 
-nuclear reactors are operated today. This section examines reactor operating
+coming.}\dasinline{Don't like ``we'' here. Sounds like
-procedures, investigates limitations of human-based operation, and reviews
+``we're going on an adventure!'' and feels jocular.
-current formal methods approaches to reactor control
+Maybe: ``To motivate this proposal, the state of
-systems.}\dasinline{Don't like ``we'' here. Sounds like ``we're going on an
+the art of nuclear reactor control, blah, and blah,
-adventure!'' and feels jocular. Maybe: ``To motivate this proposal, the
+are discussed in this section.''}
-state of the art of nuclear reactor control, blah, and blah, are discussed
-in this section.''}
 
 \subsection{Current Reactor Procedures and Operation}
 
-\oldt{Nuclear plant procedures exist in a hierarchy: normal operating
+Nuclear plant procedures exist in a hierarchy: normal operating procedures for
-procedures for routine operations, abnormal operating procedures for
+routine operations, abnormal operating procedures for off-normal conditions,
-off-normal conditions, Emergency Operating Procedures (EOPs) for
+Emergency Operating Procedures (EOPs) for design-basis accidents, Severe
-design-basis accidents, Severe Accident Management Guidelines (SAMGs) for
+Accident Management Guidelines (SAMGs) for beyond-design-basis events, and
-beyond-design-basis events, and Extensive Damage Mitigation Guidelines
+Extensive Damage Mitigation Guidelines (EDMGs) for catastrophic damage
-(EDMGs) for catastrophic damage scenarios.} \newt{Nuclear plant operations
+scenarios.\dasinline{This sentence is MASSIVE. Why is
-are governed by a hierarchy of written procedures, ranging from normal
+there 6 lines describing different types of
-operating procedures for routine operations to Emergency Operating
+procedures? WHO CARES? Need a sentence after saying
-Procedures (EOPs) for design-basis accidents and Severe Accident Management
+why we have these procedures.} These procedures must comply with 10 CFR 50.34(b)(6)(ii) and are
-Guidelines (SAMGs) for beyond-design-basis events. These procedures exist
+developed using guidance from NUREG-0899~\cite{NUREG-0899, 10CFR50.34}, but their
-because reactor operation requires deterministic responses to a wide range
+development relies fundamentally on expert judgment and simulator validation
-of plant conditions, from routine power changes to catastrophic
+rather than formal verification. Procedures undergo technical evaluation,
-failures.}\dasinline{This sentence is MASSIVE. Why is there 6 lines
+simulator validation testing, and biennial review as part of operator
-describing different types of procedures? WHO CARES? Need a sentence after
+requalification under 10 CFR 55.59~\cite{10CFR55.59}. Despite this rigor,
-saying why we have these procedures.} These procedures must comply with 10
+procedures fundamentally lack formal verification of key safety 
-CFR 50.34(b)(6)(ii) and are developed using guidance from
+properties.\dasinline{Does the audience know what formal
-NUREG-0899~\cite{NUREG-0899, 10CFR50.34}, but their development relies
+verification is at this point? Probably, but should
-fundamentally on expert judgment and simulator validation rather than formal
+say differently. Maybe `exhaustive' or
-verification.
+`definitive'.} No
+mathematical proof exists that procedures cover all possible plant states, that
+required actions can be completed within available timeframes, or that
+transitions between procedure sets maintain safety 
+invariants.\splitsuggest{This paragraph is doing a lot. Consider splitting: 
+first paragraph on the hierarchy and compliance, second on the lack of formal 
+verification. The ``No mathematical proof exists...'' sentence is powerful and 
+deserves emphasis.}
 
-Procedures undergo technical evaluation, simulator validation testing, and
+\textbf{LIMITATION:} \textit{Procedures lack formal verification of correctness
-biennial review as part of operator requalification under 10 CFR
+and completeness.} Current procedure development relies on expert judgment and
-55.59~\cite{10CFR55.59}. Despite this rigor, procedures fundamentally lack
+simulator validation. No mathematical proof exists that procedures cover all
-\oldt{formal verification of key safety properties.} \newt{exhaustive
+possible plant states, that required actions can be completed within available
-verification of key safety properties.}\dasinline{Does the audience know
+timeframes, or that transitions between procedure sets maintain safety
-what formal verification is at this point? Probably, but should say
+invariants. Paper-based procedures cannot ensure correct application, and even
-differently. Maybe `exhaustive' or `definitive'.} No mathematical proof
+computer-based procedure systems lack the formal guarantees that automated
-exists that procedures cover all possible plant states, that required actions
+reasoning could provide.\splitpolish{This repeats the ``No mathematical 
-can be completed within available timeframes, or that transitions between
+proof exists...'' sentence almost verbatim from the paragraph above. Either 
-procedure sets maintain safety invariants.
+cut it from the paragraph or from the LIMITATION box.}
 
-\textbf{LIMITATION:} \textit{Procedures lack exhaustive verification of
+Nuclear plants operate with multiple control modes: automatic control, where the
-correctness and completeness.} \oldt{Current procedure development relies on
+reactor control system maintains target parameters through continuous reactivity
-expert judgment and simulator validation. No mathematical proof exists that
+adjustment; manual control, where operators directly manipulate the reactor; and
-procedures cover all possible plant states, that required actions can be
+various intermediate modes. In typical pressurized water reactor operation, the
-completed within available timeframes, or that transitions between procedure
+reactor control system automatically maintains a floating average temperature
-sets maintain safety invariants. Paper-based procedures cannot ensure correct
+and compensates for power demand changes through reactivity feedback loops
-application, and even computer-based procedure systems lack the formal
+alone. Safety systems, by contrast, operate with implemented automation. Reactor
-guarantees that automated reasoning could provide.} \newt{Paper-based
+Protection Systems trip automatically on safety signals with millisecond
-procedures cannot ensure correct application, and even computer-based
+response times, and engineered safety features actuate automatically on accident
-procedure systems lack the guarantees that automated reasoning could
+signals without operator action required.
-provide.}\splitpolish{This repeats the ``No mathematical proof exists...''
-sentence almost verbatim from the paragraph above. Either cut it from the
-paragraph or from the LIMITATION box.}
 
-Nuclear plants operate with multiple control modes: automatic control, where
+\dasinline{After reading the next sentence, ``key safety''
-the reactor control system maintains target parameters through continuous
+can honestly just be a semicolon.}
-reactivity adjustment; manual control, where operators directly manipulate
+\dasinline{Not sure what the challenge actually is
-the reactor; and various intermediate modes. In typical pressurized water
+as this paragraph is written. What's the point?}
-reactor operation, the reactor control system automatically maintains a
+The division between automated and human-controlled functions reveals the
-floating average temperature and compensates for power demand changes through
+fundamental challenge of hybrid control. Highly automated systems handle reactor
-reactivity feedback loops alone. Safety systems, by contrast, operate with
+protection---automatic trips on safety parameters, emergency core cooling
-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
+control~\cite{WRPS.Description, gentillon_westinghouse_1999}. Human operators,
-operators retain control of everything else: power level changes,
+however, retain control of strategic decision-making: power level changes,
 startup/shutdown sequences, mode transitions, and procedure 
-implementation.}\dasinline{After reading the next sentence, ``key safety''
+implementation.\splitnote{This is the key insight — the hybrid nature is 
-can honestly just be a semicolon.}\dasinline{Not sure what the challenge
+already there, just not formally verified.}
-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}
 
-\oldt{Current-generation nuclear power plants employ over 3,600 active
+Current-generation nuclear power plants employ over 3,600 active NRC-licensed
-NRC-licensed reactor operators in the United
+reactor operators in the United 
-States~\cite{operator_statistics}. These operators divide into Reactor
+States~\cite{operator_statistics}.\dasinline{Why is this here? Should this
-Operators (ROs), who manipulate reactor controls, and Senior Reactor
+be in broader impacts about running out of ROs?
-Operators (SROs), who direct plant operations and serve as shift
+As it is here I have no idea why this is here.} These
-supervisors~\cite{10CFR55}. Staffing typically requires at least two ROs and
+operators divide into Reactor Operators (ROs), who manipulate reactor controls,
-one SRO for current-generation units~\cite{10CFR50.54}. Becoming a reactor
+and Senior Reactor Operators (SROs), who direct plant operations and serve as
-operator requires several years of training.} \newt{Nuclear plant staffing
+shift supervisors~\cite{10CFR55}. Staffing typically requires at least two ROs
-requires at least two Reactor Operators (ROs) and one Senior Reactor
+and one SRO for current-generation units~\cite{10CFR50.54}. Becoming a reactor
-Operator (SRO) per unit~\cite{10CFR50.54}, with operators requiring several
+operator requires several years of training.
-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
+The persistent role of human error in nuclear safety incidents---despite decades
-decades of improvements in training and procedures---provides the most
+of improvements in training and procedures---provides the most compelling
-compelling motivation for formal automated control with mathematical safety
+motivation for formal automated control with mathematical safety 
-guarantees.\splitnote{Strong thesis for this subsection.} Operators hold
+guarantees.\splitnote{Strong thesis for this subsection.}
-legal authority under 10 CFR Part 55 to make critical
+Operators hold legal authority under 10 CFR Part 55 to make critical 
-decisions~\cite{10CFR55},\dasinline{Cite.} including departing from normal
+decisions,\dasinline{Cite.}
-regulations during emergencies. \oldt{The Three Mile Island (TMI) accident}
+including departing from normal regulations during emergencies. 
-\newt{This authority itself introduces risk. The Three Mile Island (TMI)
+\dasinline{Needs a connector here. Like ``But this can
-accident}\dasinline{Needs a connector here. Like ``But this can in and of
+in and of itself prime plants for an accident.''
-itself prime plants for an accident.'' Then continue.} demonstrated how a
+Then continue.}The Three Mile
-combination of personnel error, design deficiencies, and component failures
+Island (TMI) accident demonstrated how a combination of personnel error, design
-led to partial meltdown when operators misread confusing and contradictory
+deficiencies, and component failures led to partial meltdown when operators
-readings and shut off the emergency water system~\cite{Kemeny1979}. The
+misread confusing and contradictory readings and shut off the emergency water
-President's Commission on TMI identified a fundamental ambiguity: placing
+system~\cite{Kemeny1979}. The President's Commission on TMI identified a
-responsibility for safe power plant operations on the licensee without
+fundamental ambiguity: placing responsibility for safe power plant operations on
-formal verification that operators can fulfill this responsibility does not
+the licensee without formal verification that operators can fulfill this
-guarantee safety. This tension between operational flexibility and safety
+responsibility does not guarantee safety. This tension between operational
-assurance remains unresolved: the person responsible for reactor safety is
+flexibility and safety assurance remains unresolved: the person responsible for
-often the root cause of failures.\splitnote{``the person responsible for
+reactor safety is often the root cause of 
-reactor safety is often the root cause of failures'' — devastating summary.
+failures.\splitnote{``the person responsible for reactor safety is often the 
-Very effective.}
+root cause of failures'' — devastating summary. Very effective.}
 
 Multiple independent analyses converge on a striking statistic: 70--80\% of
-nuclear power plant events are attributed to human error, versus
+nuclear power plant events are attributed to human error, versus approximately
-approximately 20\% to equipment failures~\cite{WNA2020}. More significantly,
+20\% to equipment failures~\cite{WNA2020}. More significantly, the root cause of
-the root cause of all severe accidents at nuclear power plants---Three Mile
+all severe accidents at nuclear power plants---Three Mile Island, Chernobyl, and
-Island, Chernobyl, and Fukushima Daiichi---has been identified as poor
+Fukushima Daiichi---has been identified as poor safety management and safety
-safety management and safety culture: primarily human
+culture: primarily human factors~\cite{hogberg_root_2013}. A detailed analysis
-factors~\cite{hogberg_root_2013}. A detailed analysis of 190 events at
+of 190 events at Chinese nuclear power plants from
-Chinese nuclear power plants from
+2007--2020~\cite{zhang_analysis_2025} found that 53\% of events involved active
-2007--2020~\cite{zhang_analysis_2025} found that 53\% of events involved
+errors, while 92\% were associated with latent errors---organizational and
-active errors, while 92\% were associated with latent
+systemic weaknesses that create conditions for 
-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
+\textbf{LIMITATION:} \textit{Human factors impose fundamental reliability limits
-limits that cannot be overcome through training alone.} The persistent human
+that cannot be overcome through training alone.} The persistent human
-error contribution despite four decades of improvements demonstrates that
+error contribution despite four decades of improvements demonstrates that these
-these limitations are fundamental rather than a remediable part of
+limitations are fundamental rather than a remediable part of human-driven 
-human-driven control.\splitnote{Well-stated. The ``four decades'' point
+control.\splitnote{Well-stated. The ``four decades'' point drives it home.}
-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
+project represents the most advanced application of formal methods to nuclear
-nuclear reactor control systems to date~\cite{Kiniry2024}.
+reactor control systems to date~\cite{Kiniry2024}.
 
-HARDENS aimed to address a fundamental dilemma: existing U.S. nuclear
+HARDENS aimed to address a fundamental dilemma: existing U.S. nuclear control
-control rooms rely on analog technologies from the
+rooms rely on analog technologies from the 1950s--60s.\dasinline{Source?}
-1950s--60s.\dasinline{Source?} This technology is obsolete compared to
+This technology is
-modern control systems and incurs significant risk and cost. The NRC
+obsolete compared to modern control systems and incurs significant risk and
-contracted Galois, a formal methods firm, to demonstrate that Model-Based
+cost. The NRC contracted Galois, a formal methods firm, to demonstrate that
-Systems Engineering and formal methods could design, verify, and implement a
+Model-Based Systems Engineering and formal methods could design, verify, and
-complex protection system meeting regulatory criteria at a fraction of
+implement a complex protection system meeting regulatory criteria at a fraction
-typical cost. The project delivered a Reactor Trip System (RTS)
+of typical cost. The project delivered a Reactor Trip System (RTS)
-implementation with full traceability from \oldt{NRC Request for Proposals
+implementation with full traceability from NRC Request for Proposals and IEEE
-and IEEE standards through formal architecture specifications to verified
+standards through formal architecture specifications to verified 
-software.} \newt{regulatory requirements through formal architecture
+software.\dasinline{Wordsmith this to remove the RFP and
-specifications to verified software.}\dasinline{Wordsmith this to remove the
+IEEE standards language. Should just say
-RFP and IEEE standards language. Should just say requirements.}
+requirements.}
 
-\oldt{HARDENS employed formal methods tools and techniques across the
+HARDENS employed formal methods tools and techniques across the verification
-verification hierarchy.} \newt{HARDENS employed formal methods tools at
+hierarchy.\dasinline{Zero discussion about what the
-every level of system development, from high-level requirements through
+verification hierarchy is. What is a specification
-executable models to generated code.}\dasinline{Zero discussion about what
+or a requirement to someone who hasn't heard of
-the verification hierarchy is. What is a specification or a requirement to
+one before?} High-level specifications used Lando, SysMLv2, and FRET (NASA Formal
-someone who hasn't heard of one before?} High-level specifications used
+Requirements Elicitation Tool) to capture stakeholder requirements, domain
-Lando, SysMLv2, and FRET (NASA Formal Requirements Elicitation Tool) to
+engineering, certification requirements, and safety requirements. Requirements
-capture stakeholder requirements, domain engineering, certification
+were analyzed for consistency, completeness, and realizability using SAT and SMT
-requirements, and safety requirements. Requirements were analyzed for
+solvers. Executable formal models used Cryptol to create a behavioral model of
-consistency, completeness, and realizability using SAT and SMT solvers.
+the entire RTS, including all subsystems, components, and limited digital twin
-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
+implementations directly from Cryptol models---eliminating the traditional gap
-gap between specification and implementation where errors commonly
+between specification and implementation where errors commonly 
 arise.\splitnote{Good technical depth on HARDENS toolchain.}
 
-\oldt{Despite its accomplishments, HARDENS has a fundamental limitation
+Despite its accomplishments, HARDENS has a fundamental limitation directly
-directly relevant to hybrid control synthesis: the project addressed only
+relevant to hybrid control synthesis: the project addressed only discrete
-discrete digital control logic without modeling or verifying continuous
+digital control logic without modeling or verifying continuous reactor 
-reactor dynamics. The Reactor Trip System specification and verification
+dynamics.\dasinline{Edit these to more clearly separate
-covered discrete state transitions (trip/no-trip decisions), digital sensor
+the context from the limit. The limitation should
-input processing through discrete logic, and discrete actuation outputs
+be in the limitation.}
-(reactor trip commands). The project did not address continuous dynamics of
+The Reactor Trip System specification and verification covered discrete state
-nuclear reactor physics. Real reactor safety depends on the interaction
+transitions (trip/no-trip decisions), digital sensor input processing through
-between continuous processes---temperature, pressure, neutron flux---evolving
+discrete logic, and discrete actuation outputs (reactor trip commands). The
-in response to discrete control decisions. HARDENS verified the discrete
+project did not address continuous dynamics of nuclear reactor physics. Real
-controller in isolation but not the closed-loop hybrid system behavior.}
+reactor safety depends on the interaction between continuous
-\newt{Despite these accomplishments, HARDENS addressed only discrete digital
+processes---temperature, pressure, neutron flux---evolving in response to
-control logic. The Reactor Trip System verification covered discrete state
+discrete control decisions. HARDENS verified the discrete controller in
-transitions, digital sensor processing, and discrete actuation outputs. It
+isolation but not the closed-loop hybrid system 
-did not model or verify continuous reactor dynamics. Real reactor safety
+behavior.\splitnote{Clear articulation of the gap your work fills.}
-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
+\textbf{LIMITATION:} \textit{HARDENS addressed discrete control logic without
-without continuous dynamics or hybrid system verification.} Verifying
+continuous dynamics or hybrid system verification.} Verifying discrete control
-discrete control logic alone provides no guarantee that the closed-loop
+logic alone provides no guarantee that the closed-loop system exhibits desired
-system exhibits desired continuous behavior such as stability, convergence to
+continuous behavior such as stability, convergence to setpoints, or maintained
-setpoints, or maintained safety margins.
+safety margins.
 
 HARDENS produced a demonstrator system at Technology Readiness Level 2--3
-(analytical proof of concept with laboratory breadboard validation) rather
+(analytical proof of concept with laboratory breadboard validation) rather than
-than a deployment-ready system validated through extended operational
+a deployment-ready system validated through extended operational testing. The
-testing. The NRC Final Report explicitly notes~\cite{Kiniry2024} that all
+NRC Final Report explicitly notes~\cite{Kiniry2024} that all material is
-material is considered in development, not a finalized product, and that
+considered in development, not a finalized product, and that ``The demonstration
-``The demonstration of its technical soundness was to be at a level
+of its technical soundness was to be at a level consistent with satisfaction of
-consistent with satisfaction of the current regulatory criteria, although
+the current regulatory criteria, although with no explicit demonstration of how
-with no explicit demonstration of how regulatory requirements are
+regulatory requirements are 
-met.''\dasinline{Check this quote. Absolutely damning for HARDENS if true
+met.''\dasinline{Check this quote. Absolutely damning
-and hilarious Galois said this.} The project did not include deployment in
+for HARDENS if true and hilarious Galois said
-actual nuclear facilities, testing with real reactor systems under
+this.} The project did not include deployment in
-operational conditions, side-by-side validation with operational analog RTS
+actual nuclear facilities, testing with real reactor systems under operational
-systems, systematic failure mode testing, NRC licensing review, or human
+conditions, side-by-side validation with operational analog RTS systems,
-factors validation with licensed operators in realistic control room
+systematic failure mode testing (radiation effects, electromagnetic
-scenarios.
+interference, temperature extremes), NRC licensing review, or human factors
+validation with licensed operators in realistic control room scenarios.
 
 \textbf{LIMITATION:} \textit{HARDENS achieved TRL 2--3 without experimental
-validation.} \oldt{While formal verification provides mathematical
+validation.}\dasinline{Same as before. Separate limit
-correctness guarantees for the implemented discrete logic, the gap between
+from context better.} While formal verification provides mathematical correctness
-formal verification and actual system deployment involves myriad practical
+guarantees for the implemented discrete logic, the gap between formal
-considerations: integration with legacy systems, long-term reliability under
+verification and actual system deployment involves myriad practical
-harsh environments, human-system interaction in realistic operational
+considerations: integration with legacy systems, long-term reliability
-contexts, and regulatory acceptance of formal methods as primary assurance
+under harsh environments, human-system interaction in realistic
-evidence.} \newt{The gap between formal verification and actual system
+operational contexts, and regulatory acceptance of formal methods as
-deployment remains wide: integration with legacy systems, long-term
+primary assurance evidence.
-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}
-\oldt{There has been additional work to do verification of hybrid systems by
+There has been additional work to do verification of hybrid systems by extending
-extending the temporal logics directly.} \newt{A separate line of work
+the temporal logics 
-extends temporal logics to verify hybrid systems
+directly.\dasinline{Need to introduce temporal logic
-directly.}\dasinline{Need to introduce temporal logic and FRET here first.}
+and FRET here first.} The result has been the field of differential
-The result has been the field of differential dynamic logic (dL). dL
+dynamic logic (dL). dL introduces two additional operators
-introduces two additional operators into temporal logic: the box operator and
+into temporal logic: the box operator and the diamond operator. The box operator
-the diamond operator. The box operator \([\alpha]\phi\) states that for some
+\([\alpha]\phi\) states that for some region \(\phi\), the hybrid system
-region \(\phi\), the hybrid system \(\alpha\) always remains within that
+\(\alpha\) always remains within that region. In this way, it is a safety
-region. In this way, it is a safety \oldt{ivariant} \newt{invariant} being
+ivariant being enforced for the system.\splitfix{Typo: ``ivariant'' should be 
-enforced for the system.\splitfix{Typo: ``ivariant'' should be
+``invariant''} The second operator, the diamond
-``invariant''} The second operator, the diamond operator
+operator \(<\alpha>\phi\) says that for the region \(\phi\), there is at least
-\(<\alpha>\phi\) says that for the region \(\phi\), there is at least one
+one trajectory of \(\alpha\) that enters that region. This is a declaration of a
-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
+While dL allows for the specification of these liveness and safety properties,
-properties, actually proving them for a given hybrid system is quite
+actually proving them for a given hybrid system is quite difficult. Automated
-difficult. Automated proof assistants such as KeYmaera X exist to help
+proof assistants such as KeYmaera X exist to help develop proofs of systems
-develop proofs of systems using dL, but so far have been insufficient for
+using dL, but so far have been insufficient for reasonably complex hybrid
-reasonably complex hybrid systems. The main issue behind creating system
+systems. The main issue behind creating system proofs using dL is state space
-proofs using dL is state space explosion and non-terminating solutions.
+explosion and non-terminating 
+solutions.\splitsuggest{Consider adding a concrete example here — ``For 
+instance, a system with N modes and M continuous state variables...'' to give 
+readers a sense of the scaling problem.}
 %Source: that one satellite tracking paper that has the problem with the
 %gyroscopes overloding and needing to dump speed all the time
-Approaches have been made to alleviate these issues for nuclear power
+Approaches have been made to alleviate
-contexts using contract and decomposition based methods, \oldt{but are far
+these issues for nuclear power contexts using contract and decomposition based
-from a complete methodology to design systems with.} \newt{but do not yet
+methods, but are far from a complete methodology to design systems 
-constitute a complete design methodology.}\splitpolish{``but are far from a
+with.\splitpolish{``but are far from a complete methodology to design systems 
-complete methodology to design systems with'' — awkward ending preposition.}
+with'' — awkward ending preposition. Try: ``but remain far from a complete 
+design methodology'' or ``but do not yet constitute a complete design 
+methodology.''}
 %source: Manyu's thesis. 
 Instead, these approaches have been used on systems that have been designed a
 priori, and require expert knowledge to create the system proofs. 
 
 %Maybe a limitation here? Something about dL doesn't scale or help in design
-%very much, so the limitation is that logic based hybrid system approaches
+%very much, so the limitation is that logic based hybrid system approaches have
-%have not been used in the DESIGN of autonomous controllers, only in the
+%not been used in the DESIGN of autonomous controllers, only in the analysis of
-%analysis of systems that already exist.
+%systems that already exist.
-
+\splitinline{Your comment here is spot-on. You should add a LIMITATION box: 
-\textbf{LIMITATION:} \textit{Differential dynamic logic has been used for
+\textit{Differential dynamic logic has been used for post-hoc analysis of 
-post-hoc analysis of existing systems, not for the constructive design of
+existing systems, not for the constructive design of autonomous controllers.} 
-autonomous controllers.} Current dL-based approaches verify systems that
+This is exactly the gap you're filling — you're doing synthesis, not just 
-have already been designed, requiring expert knowledge to construct proofs.
+verification.}
-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,36 +6,33 @@ demonstration. This work begins at TRL 2--3 and aims to reach TRL 5, where
 system components operate successfully in a relevant laboratory 
 environment.\splitnote{TRL as primary metric is smart — speaks industry 
 language.}
-This section explains why TRL advancement provides the most appropriate
+This section explains why TRL advancement provides the most appropriate success
-success metric and defines the specific criteria required to achieve TRL 5.
+metric and defines the specific criteria required to achieve TRL 5.
 
-\oldt{Technology Readiness Levels provide the ideal success metric because
+Technology Readiness Levels provide the ideal success metric because they
-they explicitly measure the gap between academic proof-of-concept and
+explicitly measure the gap between academic proof-of-concept and 
-practical deployment---precisely what this work aims to bridge. Academic
+practical\dasinline{Chop. No likey.}
-metrics like papers published or theorems proved cannot capture practical
+deployment---precisely what this work aims to bridge. Academic metrics like
-feasibility. Empirical metrics like simulation accuracy or computational
+papers published or theorems proved cannot capture practical feasibility.
-speed cannot demonstrate theoretical rigor. TRLs measure both dimensions
+Empirical metrics like simulation accuracy or computational speed cannot
-simultaneously.} \newt{TRLs measure the gap between academic
+demonstrate theoretical rigor. TRLs measure both dimensions 
-proof-of-concept and practical deployment, which is precisely what this work
+simultaneously.\splitnote{Good framing — explains why other metrics are 
-aims to bridge. Academic metrics alone cannot capture practical feasibility,
+insufficient.}
-and empirical metrics alone cannot demonstrate theoretical rigor. TRLs
+Advancing from TRL 3 to TRL 5 requires maintaining theoretical rigor while
-measure both simultaneously.}\dasinline{Chop. No likey.}\splitnote{Good
+progressively demonstrating practical feasibility. Formal verification must
-framing — explains why other metrics are insufficient.} Advancing from TRL 3
+remain valid as the system moves from individual components to integrated
-to TRL 5 requires maintaining theoretical rigor while progressively
+hardware testing.
-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
+formal guarantees fails to meet regulatory requirements. TRLs capture this dual
-dual requirement naturally. Each level represents both increased practical
+requirement naturally. Each level represents both increased practical maturity
-maturity and sustained theoretical validity. Furthermore, TRL assessment
+and sustained theoretical validity. Furthermore, TRL assessment forces explicit
-forces explicit identification of remaining barriers to deployment. The
+identification of remaining barriers to deployment. The nuclear industry already
-nuclear industry already uses TRLs for technology assessment, making this
+uses TRLs for technology assessment, making this metric directly relevant to
-metric directly relevant to potential adopters. Reaching TRL 5 provides a
+potential adopters. Reaching TRL 5 provides a clear answer to industry questions
-clear answer to industry questions about feasibility and maturity that
+about feasibility and maturity that academic publications alone cannot.
-academic publications alone cannot.
 
 Moving from current state to target requires achieving three intermediate
 levels, each representing a distinct validation milestone:
@@ -48,8 +45,8 @@ temporal logic specifications that pass realizability analysis. A discrete
 automaton must be synthesized with interpretable structure. At least one
 continuous controller must be designed with reachability analysis proving
 transition requirements are satisfied. Independent review must confirm that
-specifications match intended procedural behavior. This proves the
+specifications match intended procedural behavior. This proves the fundamental
-fundamental approach on a simplified startup sequence.
+approach on a simplified startup sequence.
 
 \paragraph{TRL 4 \textit{Laboratory Testing of Integrated Components}}
 
@@ -60,44 +57,41 @@ must exist for all discrete modes. Verification must be complete for all mode
 transitions using reachability analysis, barrier certificates, and
 assume-guarantee contracts. The integrated controller must execute complete
 startup sequences in software simulation with zero safety violations across
-multiple consecutive runs. This proves that formal correctness guarantees can
+multiple consecutive runs. This proves that formal correctness guarantees can be
-be maintained throughout system integration.
+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
+industrial control hardware through hardware-in-the-loop testing. The discrete
-discrete automaton must be implemented on the Emerson Ovation control system
+automaton must be implemented on the Emerson Ovation control system and verified
-and verified to match synthesized specifications exactly. Continuous
+to match synthesized specifications exactly. Continuous controllers must execute
-controllers must execute at required rates. The ARCADE interface must
+at required rates. The ARCADE interface must establish stable real-time
-establish stable real-time communication between the Emerson Ovation hardware
+communication between the Emerson Ovation hardware and SmAHTR simulation.
-and SmAHTR simulation. Complete autonomous startup sequences must execute via
+Complete autonomous startup sequences must execute via hardware-in-the-loop
-hardware-in-the-loop across the full operational envelope. The controller
+across the full operational envelope. The controller must handle off-nominal
-must handle off-nominal scenarios to validate that expulsory modes function
+scenarios to validate that expulsory modes function correctly. For example,
-correctly. For example, simulated sensor failures must trigger appropriate
+simulated sensor failures must trigger appropriate fault detection and mode
-fault detection and mode transitions, and loss-of-cooling scenarios must
+transitions, and loss-of-cooling scenarios must activate SCRAM procedures as
-activate SCRAM procedures as specified. Graded responses to minor
+specified. Graded responses to minor disturbances are outside this work's 
-disturbances are outside this work's scope\oldt{.}\newt{, as they require
+scope.\splitsuggest{Consider noting why graded responses are out of scope — 
-runtime optimization under uncertainty that extends beyond the
+is it time, complexity, or scope creep? Brief justification helps.}
-correct-by-construction verification framework presented
+Formal verification results must remain valid, with discrete behavior matching
-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
+This proves that the methodology produces verified controllers implementable on
-on industrial hardware.
+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.
+metrics and hardware integration milestones indicate progress toward TRL 5. The
-The research plan will be revised only when new data invalidates fundamental
+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
+operating on industrial control hardware through hardware-in-the-loop testing in
-testing in a relevant laboratory environment. This establishes both
+a relevant laboratory environment. This establishes both theoretical validity
-theoretical validity and practical feasibility, proving that the methodology
+and practical feasibility, proving that the methodology produces verified
-produces verified controllers and that implementation is achievable with
+controllers and that implementation is achievable with current 
-current technology.\splitnote{Clear success criteria. Committee will know
+technology.\splitnote{Clear success criteria. Committee will know exactly 
-exactly what ``done'' looks like.}
+what ``done'' looks like.}

5-risks-and-contingencies/risks.tex

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

6-broader-impacts/impacts.tex

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