danesabo/Thesis
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Editorial pass: tactical, operational, and strategic improvements

Browse Source 
Tactical (sentence-level):
- Applied Gopen's principles: improved topic-stress positioning, stronger verbs
- Reduced passive voice and unnecessary modifiers
- Split long sentences for clarity and emphasis
- Tightened redundant phrasing throughout

Operational (paragraph/section):
- Added explicit transitions between subsections
- Improved flow within paragraphs (e.g., control scopes example)
- Created parallel structure for related concepts
- Enhanced coherence in State of the Art section

Strategic (document-level):
- Strengthened value proposition (higher vs same assurance)
- Improved Heilmeier alignment (why now, what's new, why it will succeed)
- Better linkage between State of the Art gap and research goals
- Connected economic motivation more explicitly throughout
This commit is contained in:
Split 2026-03-09 12:19:07 -04:00
parent 00c14339e0
commit ab627264ac
7 changed files with 103 additions and 107 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

42
1-goals-and-outcomes/research_statement_v1.tex
View File

@ -1,16 +1,15 @@
% GOAL PARAGRAPH
This research develops a methodology for creating autonomous control systems
that guarantee safe and correct behavior through event-driven control laws.
that guarantee safe and correct behavior.
% INTRODUCTORY PARAGRAPH Hook
Nuclear power plants rely on extensively trained operators who follow detailed
written procedures to manage reactor control. These operators interpret plant
conditions and make critical decisions about when to switch between control
conditions and decide when to switch between control
objectives.
% Gap
Next-generation nuclear power plants face an economic challenge from this
reliance on human operators. Small modular reactors face per-megawatt
staffing costs significantly exceeding those of conventional plants. These
Next-generation nuclear power plants face an economic challenge: small modular reactors incur per-megawatt
staffing costs that significantly exceed those of conventional plants. These
economic constraints demand autonomous control systems that can safely manage
complex operational sequences without constant supervision while maintaining the
same assurance as human-operated systems.
@ -19,25 +18,24 @@ same assurance as human-operated systems.
We combine formal methods from computer science with control theory to
build hybrid control systems that are correct by construction.
% Rationale
Hybrid systems mirror how operators change control strategies: they use discrete
logic to switch between continuous control modes. Existing formal methods
Hybrid systems mirror how operators work: discrete
logic switches between continuous control modes. Existing formal methods
generate provably correct switching logic but cannot handle continuous dynamics
during transitions. Traditional control theory verifies continuous behavior but
during transitions. Control theory verifies continuous behavior but
lacks tools for proving discrete switching correctness.
% Hypothesis and Technical Approach
A three-stage methodology bridges this gap. First, we translate written
operating procedures into temporal logic specifications using NASA's Formal
Requirements Elicitation Tool (FRET). FRET structures requirements into scope,
condition, component, timing, and response elements, enabling realizability
checking that identifies conflicts and ambiguities before implementation.
condition, component, timing, and response elements. Realizability
checking then identifies conflicts and ambiguities before implementation.
Second, reactive synthesis generates deterministic automata that are provably
correct by construction for discrete mode switching logic.
Third, we develop continuous controllers for each discrete mode using standard
control theory and reachability analysis. We classify continuous modes based on
correct by construction.
Third, we design continuous controllers for each discrete mode using standard
control theory and verify them using reachability analysis. We classify continuous modes based on
their transition objectives, then employ assume-guarantee contracts and barrier
certificates to prove that mode transitions occur safely as the
deterministic automata specify. Local verification of continuous modes becomes
possible without global trajectory analysis across the entire hybrid system. An
certificates to prove that mode transitions occur safely. This enables local verification of continuous modes
without global trajectory analysis across the entire hybrid system. An
Emerson Ovation control system will demonstrate this methodology.
% Pay-off
This approach demonstrates that autonomous control can manage complex nuclear
@ -54,18 +52,18 @@ If this research is successful, we will be able to do the following:
discrete control logic from these specifications.
% Outcome
Control engineers will generate mode-switching controllers from regulatory
procedures with minimal formal methods expertise, reducing barriers to
procedures with minimal formal methods expertise. This reduces barriers to
high-assurance control systems.
% OUTCOME 2 Title
\item \textit{Verify continuous control behavior across mode transitions.}
% Strategy
Reachability analysis will ensure continuous control modes satisfy discrete
Reachability analysis will verify that continuous control modes satisfy discrete
transition requirements.
% Outcome
Engineers will design continuous controllers using standard practices while
ensuring system correctness, proving that mode transitions occur safely at
the right times.
maintaining formal correctness guarantees. Mode transitions will provably occur safely and at
the correct times.
% OUTCOME 3 Title
\item \textit{Demonstrate autonomous reactor startup control with safety
@ -75,7 +73,7 @@ If this research is successful, we will be able to do the following:
will implement this methodology.
% Outcome
Control engineers will implement high-assurance autonomous controls on
industrial platforms they already use, enabling autonomy without retraining
costs or developing new equipment.
industrial platforms they already use. This enables autonomy without retraining
costs or new equipment development.
\end{enumerate}

39
1-goals-and-outcomes/v1.tex
View File

@ -9,38 +9,38 @@ Nuclear power plants require the highest levels of control system reliability.
Failures can result in significant economic losses, service interruptions,
or radiological release.
% Known information
Currently, nuclear plant operations rely on extensively trained human operators
Nuclear plant operations rely on extensively trained human operators
who follow detailed written procedures and strict regulatory requirements to
manage reactor control. These operators make critical decisions about when to
manage reactor control. These operators decide when to
switch between different control modes based on their interpretation of plant
conditions and procedural guidance.
% Gap
This reliance on human operators prevents autonomous control capabilities and
This reliance on human operators prevents autonomous control and
creates a fundamental economic challenge for next-generation reactor designs.
Small modular reactors face per-megawatt staffing costs far
exceeding those of conventional plants, threatening their economic viability.
% Critical Need
The nuclear industry needs autonomous control systems that safely manage complex
operational sequences without constant human supervision while maintaining the
same assurance as human-operated systems.
operational sequences without constant human supervision while maintaining
higher assurance than human-operated systems.
% APPROACH PARAGRAPH Solution
We combine formal methods with control theory to build hybrid control
systems that are correct by construction.
% Rationale
Hybrid systems mirror how operators change control strategies: they use discrete
logic to switch between continuous control modes. Existing formal methods
Hybrid systems mirror how operators work: discrete
logic switches between continuous control modes. Existing formal methods
generate provably correct switching logic from written requirements but cannot
handle the continuous dynamics occurring during transitions between modes.
Traditional control theory verifies continuous behavior but lacks tools for
handle the continuous dynamics during transitions between modes.
Control theory verifies continuous behavior but lacks tools for
proving correctness of discrete switching decisions. This gap between discrete
and continuous verification prevents end-to-end correctness guarantees.
% Hypothesis
Our approach closes this gap by synthesizing discrete mode transitions directly
from written operating procedures and verifying continuous behavior between
transitions. If we can formalize existing procedures into logical
specifications and verify continuous dynamics against transition requirements,
we can build autonomous controllers provably free from design
transitions. Formalizing existing procedures into logical
specifications and verifying continuous dynamics against transition requirements
enables us to build autonomous controllers provably free from design
defects.
% Pay-off
This approach enables autonomous control in nuclear power plants while
@ -73,14 +73,13 @@ If this research is successful, we will be able to do the following:
% OUTCOME 2 Title
\item \textbf{Verify continuous control behavior across mode transitions.}
% Strategy
We will establish methods for analyzing continuous control modes to ensure
We will establish methods for analyzing continuous control modes to verify
they satisfy discrete transition requirements. Classical control theory for
linear systems and reachability analysis for nonlinear dynamics will verify
that each continuous mode safely reaches its intended transitions.
% Outcome
Engineers will design continuous controllers using standard practices while
iterating to ensure broader system correctness, proving that mode
transitions occur safely and at the correct times.
maintaining formal correctness guarantees. Mode transitions will provably occur safely and at the correct times.
% OUTCOME 3 Title
\item \textbf{Demonstrate autonomous reactor startup control with safety
@ -105,15 +104,15 @@ documents to deployed systems.
\textbf{The key innovation} unifies discrete synthesis with continuous
verification to enable end-to-end correctness guarantees for hybrid systems.
While formal methods can verify discrete logic and control theory can verify
continuous dynamics, no existing methodology bridges both with compositional
guarantees. This work establishes that bridge. It treats discrete specifications
as contracts that continuous controllers must satisfy, enabling independent
Formal methods can verify discrete logic. Control theory can verify
continuous dynamics. No existing methodology bridges both with compositional
guarantees. This work establishes that bridge by treating discrete specifications
as contracts that continuous controllers must satisfy. This enables independent
verification of each layer while guaranteeing correct composition.
% Outcome Impact
If successful, control engineers will create autonomous controllers from
existing procedures with mathematical proof of correct behavior. High-assurance
existing procedures with mathematical proofs of correct behavior. High-assurance
autonomous control will become practical for safety-critical applications.
% Impact/Pay-off
This capability is essential for the economic viability of next-generation

34
2-state-of-the-art/v2.tex
View File

@ -2,8 +2,8 @@
This research aims to create autonomous reactor control systems that are
tractably safe. Understanding what we automate requires understanding how
nuclear reactors operate today. This section examines reactor operators and the
operating procedures we will leverage, investigates limitations of human-based
nuclear reactors operate today. This section examines reactor operators and their
operating procedures, investigates limitations of human-based
operation, and reviews current formal methods approaches to reactor
control systems.
@ -15,8 +15,8 @@ Emergency Operating Procedures (EOPs) for design-basis accidents, Severe
Accident Management Guidelines (SAMGs) for beyond-design-basis events, and
Extensive Damage Mitigation Guidelines (EDMGs) for catastrophic damage
scenarios. These procedures must comply with 10 CFR 50.34(b)(6)(ii). NUREG-0899
provides guidance for their development~\cite{NUREG-0899, 10CFR50.34}, but their
development relies fundamentally on expert judgment and simulator validation
provides guidance for their development~\cite{NUREG-0899, 10CFR50.34}. Their
development, however, relies on expert judgment and simulator validation
rather than formal verification. Procedures undergo technical evaluation,
simulator validation testing, and biennial review as part of operator
requalification under 10 CFR 55.59~\cite{10CFR55.59}. Despite this rigor,
@ -56,7 +56,7 @@ startup/shutdown sequences, mode transitions, and procedure implementation.
\subsection{Human Factors in Nuclear Accidents}
The preceding subsection established how nuclear plants currently operate:
through written procedures executed by human operators. This subsection examines
through written procedures executed by human operators. Having established current practice, we now examine
why this human-centered approach poses fundamental limitations.
Current-generation nuclear power plants employ over 3,600 active NRC-licensed
@ -67,8 +67,8 @@ shift supervisors~\cite{10CFR55}. Staffing typically requires at least two ROs
and one SRO for current-generation units~\cite{10CFR50.54}. Becoming a reactor
operator requires several years of training.
Human error persistently plays a role in nuclear safety incidents despite decades
of improvements in training and procedures. This provides the most compelling
Human error persistently contributes to nuclear safety incidents despite decades
of improvements in training and procedures. This provides compelling
motivation for formal automated control with mathematical safety guarantees.
Operators hold legal authority under 10 CFR Part 55 to make critical decisions,
including departing from normal regulations during emergencies. The Three Mile
@ -95,16 +95,17 @@ systemic weaknesses that create conditions for failure.
\textbf{LIMITATION:} \textit{Human factors impose fundamental reliability limits
that cannot be overcome through training alone.} The persistent human
error contribution despite four decades of improvements demonstrates that these
limitations are fundamental rather than a remediable part of human-driven control.
that training alone cannot overcome.} Four decades of improvements have not eliminated human
error. These
limitations are fundamental to human-driven control, not remediable defects.
\subsection{Formal Methods}
The persistent human error problem motivates exploring formal methods to
provide mathematical guarantees of correctness that human-centered approaches
Having established that human error imposes fundamental reliability limits,
we now turn to formal methods as an alternative approach.
Formal methods provide mathematical guarantees of correctness that human-centered approaches
cannot achieve. This subsection examines recent formal methods work in nuclear
control and identifies limitations for autonomous hybrid systems.
control and identifies their limitations for autonomous hybrid systems.
\subsubsection{HARDENS}
@ -152,7 +153,8 @@ logic alone provides no guarantee that the closed-loop system exhibits desired
continuous behavior such as stability, convergence to setpoints, or maintained
safety margins.
HARDENS produced a demonstrator system at Technology Readiness Level 2--3
Beyond the technical limitation of omitting continuous dynamics, HARDENS also faced
deployment maturity constraints. The project produced a demonstrator system at Technology Readiness Level 2--3
(analytical proof of concept with laboratory breadboard validation) rather than
a deployment-ready system validated through extended operational testing. The
NRC Final Report explicitly notes~\cite{Kiniry2024} that all material is
@ -213,7 +215,7 @@ design loop for complex systems like nuclear reactor startup procedures.
\subsection{Summary: The Verification Gap}
Current practice reveals a fundamental gap. Human operators provide operational
flexibility but introduce persistent reliability limitations. Formal
flexibility but introduce persistent reliability limitations that four decades of training improvements have not eliminated. Formal
methods provide correctness guarantees but have not scaled to complete hybrid
control design.
@ -224,4 +226,4 @@ correct hybrid controllers from operational procedures with verification
integrated into the design process.
This gap—between discrete-only formal methods and post-hoc hybrid
verification—defines the challenge this research addresses.
verification—defines the challenge this research addresses. Closing this gap enables autonomous nuclear control with mathematical safety guarantees, addressing the economic constraints that threaten small modular reactor viability.

83
3-research-approach/v3.tex
View File

@ -16,14 +16,13 @@
% 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION
% ----------------------------------------------------------------------------
Previous approaches to autonomous control verified discrete switching logic or
continuous control behavior, but not both simultaneously. Today's continuous
controller validation consists of extensive simulation trials. Human operators
drive discrete switching logic for routine operation; their evaluation includes
simulated control room testing and human factors research. Neither method
continuous control behavior, but not both simultaneously. Continuous
controller validation relies on extensive simulation trials. Discrete switching logic evaluation
uses simulated control room testing and human factors research. Neither method
provides rigorous guarantees of control system behavior despite being
extremely resource intensive. HAHACS bridges this gap by composing formal
methods from computer science with control-theoretic verification and
formalizing reactor operations using the framework of hybrid automata.
methods from computer science with control-theoretic verification, then
formalizing reactor operations using hybrid automata.
The challenge of hybrid system verification lies in the interaction between
discrete and continuous dynamics. Discrete transitions change the governing
@ -74,16 +73,16 @@ The creation of a HAHACS amounts to the construction of such a tuple together
with proof artifacts demonstrating that the intended behavior of the control
system is satisfied by its actual implementation.
\textbf{What is new:} This approach is tractable now because the infrastructure
\textbf{What is new:} The infrastructure
for each component has matured, but no existing work composes them for
end-to-end hybrid system verification. The novelty lies in the architecture
connecting discrete synthesis with continuous verification through well-defined
interfaces.
\textbf{Why it will succeed:} By defining
entry, exit, and safety conditions at the discrete level first, we transform the
\textbf{Why it will succeed:} Defining
entry, exit, and safety conditions at the discrete level first transforms the
intractable problem of global hybrid verification into a collection of local
verification problems with clear interfaces. Verification operates per mode
verification problems with clear interfaces. Verification then operates per mode
rather than on the full hybrid system, keeping analysis tractable even for
complex reactor operations. Nuclear procedures already define discrete boundaries
between operating regimes, providing the natural decomposition this methodology
@ -153,8 +152,8 @@ requires.
\subsection{System Requirements, Specifications, and Discrete Controllers}
The hybrid system mathematical framework defined above provides the foundation.
Now we establish how to construct such systems from existing operational knowledge.
The preceding section established the mathematical framework for hybrid systems.
This section establishes how to construct such systems from existing operational knowledge.
The key insight: nuclear operations already possess a natural hybrid structure
that maps directly to the automaton formalism.
@ -176,17 +175,19 @@ The level of control linking these two extremes is the operational control
scope. Operational control is the primary responsibility of human operators
today. Operational control takes the current strategic objective and implements
tactical control objectives to drive the plant towards strategic goals. In this
way, it bridges high-level and low-level goals. A strategic goal may be to
way, it bridges high-level and low-level goals.
Consider an example: a strategic goal may be to
perform refueling at a certain time, while the tactical level of the plant is
currently focused on maintaining a certain core temperature. The operational
level issues the shutdown procedure, using several smaller tactical goals along
the way to achieve this objective. Thus, the combination of the operational and
the way to achieve this objective.
This structure reveals why the combination of the operational and
tactical levels fundamentally forms a hybrid controller. The tactical level is
the continuous evolution of the plant according to the control input and control
law, while the operational level is a discrete state evolution that determines
which tactical control law to apply.
%Say something about autonomous control systems near here?
which tactical control law to apply. This operational level is precisely what we target for autonomous control.
\begin{figure}
@ -233,10 +234,10 @@ manuals to perform their control with strict procedures on what control to
implement at a given time. These procedures are the key to the operational
control scope.
The method of constructing a HAHACS in this proposal leverages two key
observations about current practice. First, the operational scope control is
effectively discrete control. Second, the rules for implementing this control
are described prior to their implementation in operating procedures. Before
Constructing a HAHACS leverages two key
observations about current practice. First, operational scope control is
effectively discrete control. Second, operating procedures describe the rules for implementing this control
before implementation. Before
constructing a HAHACS, we must completely describe its intended behavior. The
behavior of any control system originates in requirements: statements about what
the system must do, must not do, and under what conditions. For nuclear systems,
@ -261,14 +262,13 @@ Discrete mode transitions include predicates that are Boolean functions over the
continuous state space: $p_i: \mathcal{X} \rightarrow \{\text{true},
\text{false}\}$. These predicates formalize conditions like ``coolant
temperature exceeds 315°C'' or ``pressurizer level is between 30\% and 60\%.''
Critically, we do not impose this discrete abstraction artificially. Operating
We do not impose this discrete abstraction artificially. Operating
procedures for nuclear systems already define go/no-go conditions as discrete
predicates. These thresholds come from design basis safety analysis and have
been validated over decades of operational experience. Our methodology assumes
this domain knowledge exists and provides a framework to formalize it. This is
why the approach is feasible for nuclear applications specifically: the hard
work of defining safe operating boundaries has already been done by generations
of nuclear engineers.
predicates. Design basis safety analysis determined these thresholds, and decades of operational experience have
validated them. Our methodology assumes
this domain knowledge exists and provides a framework to formalize it. The approach is feasible for nuclear applications because generations
of nuclear engineers have already done the hard
work of defining safe operating boundaries.
Linear temporal logic (LTL) is particularly well-suited for
specifying reactive systems. LTL formulas are built from atomic propositions
@ -317,14 +317,14 @@ room for interpretation is a weakness that must be addressed.
% 3. DISCRETE CONTROLLER SYNTHESIS
% ----------------------------------------------------------------------------
Once system requirements are defined as temporal logic specifications, we use
them to build the discrete control system. To do this, reactive synthesis tools
are employed. Reactive synthesis is a field in computer science that deals with
Having defined system requirements as temporal logic specifications, we now use
them to build the discrete control system through reactive synthesis.
Reactive synthesis is a field in computer science that deals with
the automated creation of reactive programs from temporal logic specifications.
A reactive program is one that, for a given state, takes an input and produces
an output. Our systems fit exactly this mold: the current discrete state and
status of guard conditions are the input, while the output is the next discrete
state.
A reactive program takes an input for a given state and produces
an output. Our systems fit this model: the current discrete state and
status of guard conditions form the input; the next discrete
state is the output.
Reactive synthesis solves the following problem: given an LTL formula $\varphi$
that specifies desired system behavior, automatically construct a finite-state
@ -371,8 +371,8 @@ according to operating procedures.
The discrete controller synthesized above is provably correct. Now we turn to the
continuous dynamics executing within each discrete mode.
Synthesizing the discrete operational controller completes only half of an
autonomous controller. These control systems are hybrid: they have both discrete and
The discrete operational controller, while provably correct, represents only half of an
autonomous controller. Hybrid control systems require both discrete and
continuous components. This section describes the continuous control modes that
execute within each discrete state, and how we verify that they satisfy the
requirements imposed by the discrete layer. It is important to clarify the scope
@ -434,7 +434,7 @@ requirements that determine which formal methods tools are appropriate.
\subsubsection{Transitory Modes}
Transitory modes are continuous controllers designed to move
The first mode type, transitory modes, moves
the plant from one discrete operating condition to another. Their purpose is to
execute transitions: starting from entry conditions, reach exit conditions,
and maintain safety invariants throughout. Examples include power ramp-up sequences,
@ -494,11 +494,8 @@ appropriate to the fidelity of the reactor models available.
\subsubsection{Stabilizing Modes}
Transitory modes drive the system toward exit conditions. Stabilizing modes, in
contrast, maintain the system within a desired operating region.
Stabilizing modes are continuous controllers designed to maintain a particular
discrete state indefinitely. Rather than driving the system toward an
Transitory modes drive the system toward exit conditions. Stabilizing modes, the second type,
maintain the system within a desired operating region indefinitely. Rather than driving the system toward an
exit condition, they keep the system within a safe operating region. Examples
include steady-state power operation, hot standby, and load-following at
constant power level. Reachability analysis for stabilizing modes may not be a

4
4-metrics-of-success/v1.tex
View File

@ -9,9 +9,9 @@ system components operate successfully in a relevant laboratory environment.
This section explains why TRL advancement provides the most appropriate success
metric and defines the specific criteria required to achieve TRL 5.
Technology Readiness Levels provide the ideal success metric because they
Technology Readiness Levels provide the ideal success metric: they
explicitly measure the gap between academic proof-of-concept and practical
deployment---precisely what this work aims to bridge. Academic metrics like
deployment, precisely what this work aims to bridge. Academic metrics like
papers published or theorems proved cannot capture practical feasibility.
Empirical metrics like simulation accuracy or computational speed cannot
demonstrate theoretical rigor. TRLs measure both dimensions simultaneously.

4
5-risks-and-contingencies/v1.tex
View File

@ -1,8 +1,8 @@
\section{Risks and Contingencies}
This research relies on several critical assumptions that, if invalidated, would
require scope adjustment or methodological revision. The primary risks to
successful completion fall into four categories: computational tractability of
require scope adjustment or methodological revision. Four primary risks could prevent
successful completion: 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

4
6-broader-impacts/v1.tex
View File

@ -1,8 +1,8 @@
\section{Broader Impacts}
\textbf{Who cares:} The nuclear industry, datacenter operators, and clean energy
\textbf{Who cares and why now:} The nuclear industry, datacenter operators, and clean energy
advocates all face the same economic constraint: high operating costs driven by
staffing requirements.
staffing requirements. Recent AI infrastructure demands have made this constraint urgent.
Nuclear power presents both a compelling application domain and an urgent
economic challenge. Recent interest in powering artificial intelligence