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

Add Split's editorial comments with color-coded feedback

Browse Source 
Edit mode system:
- \editmode{1} enables comments + wider margins
- \editmode{0} hides all comments for final output

Comment types (color-coded):
- \splitnote{} (green): General observations, good work
- \splitsuggest{} (yellow): Suggestions to consider
- \splitpolish{} (orange): Needs polish, should fix
- \splitfix{} (red): Must fix, not acceptable

Comments added throughout all sections with substantive feedback
on structure, wording, and Gopen-style improvements.

Also fixed typos: 'ivariant' → 'invariant', 'excess' → 'access'
This commit is contained in:
Split 2026-03-09 21:44:23 -04:00
parent a01f42d47c
commit 623f760084
16 changed files with 559 additions and 177 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

40
1-goals-and-outcomes/goals.tex
View File

@ -3,12 +3,12 @@
% GOAL PARAGRAPH % GOAL PARAGRAPH
The goal of this research is to develop a methodology for creating autonomous The goal of this research is to develop a methodology for creating autonomous
hybrid control systems with mathematical guarantees of safe and correct hybrid control systems with mathematical guarantees of safe and correct
behavior.\splitnote{Strong opening — direct and clear. No changes needed.} behavior.\splitnote{Clear thesis statement. Gets right to it.}
% INTRODUCTORY PARAGRAPH Hook % INTRODUCTORY PARAGRAPH Hook
Nuclear power plants require the highest levels of control system reliability, Nuclear power plants require the highest levels of control system reliability,
where failures can result in significant economic losses, service interruptions, where failures can result in significant economic losses, service interruptions,
or radiological release. or radiological release.\splitnote{Stakes established immediately — good hook.}
% Known information % Known information
Currently, nuclear plant operations rely on extensively trained human operators Currently, nuclear plant operations rely on extensively trained human operators
who follow detailed written procedures and strict regulatory requirements to who follow detailed written procedures and strict regulatory requirements to
@ -17,14 +17,21 @@ switch between different control modes based on their interpretation of plant
conditions and procedural guidance. conditions and procedural guidance.
% Gap % Gap
This reliance on human operators prevents autonomous control capabilities and This reliance on human operators prevents autonomous control capabilities and
creates a fundamental economic challenge for next-generation reactor designs.\splitnote{Consider: ``...and creates a fundamental economic challenge'' — the ``and'' makes this feel like two separate issues. Maybe split into two sentences or tighten the causal link?} creates a fundamental economic challenge for next-generation reactor
designs.\splitsuggest{The ``and'' here joins two distinct issues (autonomy
barrier + economics). Consider making the causal link explicit: ``This reliance
on human operators not only prevents autonomous control capabilities but also
creates...'' or split into two sentences.}
Small modular reactors, in particular, face per-megawatt staffing costs far Small modular reactors, in particular, face per-megawatt staffing costs far
exceeding those of conventional plants and threaten their economic viability. exceeding those of conventional plants and threaten their economic viability.
% Critical Need % Critical Need
What is needed is a method to create autonomous control systems that safely What is needed is a method to create autonomous control systems that safely
manage complex operational sequences with the same assurance as human-operated manage complex operational sequences with the same assurance as human-operated
systems, but without constant human supervision.\splitnote{``What is needed is'' — classic Gopen weak opening. Try: ``Autonomous control systems must safely manage...'' — puts the subject in the topic position.} systems, but without constant human supervision.\splitpolish{``What is needed
is'' — Gopen would call this a weak topic position. The sentence buries the
subject. Try: ``Autonomous control systems must safely manage complex
operational sequences...'' Puts the actor in the topic position.}
% APPROACH PARAGRAPH Solution % APPROACH PARAGRAPH Solution
To address this need, we will combine formal methods with control theory to To address this need, we will combine formal methods with control theory to
build hybrid control systems that are correct by construction. build hybrid control systems that are correct by construction.
@ -34,14 +41,17 @@ mirroring how operators change control strategies. Existing formal methods can
generate provably correct switching logic from written requirements, but they generate provably correct switching logic from written requirements, but they
cannot handle the continuous dynamics that occur during transitions between cannot handle the continuous dynamics that occur during transitions between
modes. Meanwhile, traditional control theory can verify continuous behavior but modes. Meanwhile, traditional control theory can verify continuous behavior but
lacks tools for proving correctness of discrete switching decisions. lacks tools for proving correctness of discrete switching
decisions.\splitnote{Excellent setup of the gap — shows why neither approach
alone is sufficient.}
% Hypothesis % Hypothesis
By synthesizing discrete mode transitions directly from written operating By synthesizing discrete mode transitions directly from written operating
procedures and verifying continuous behavior between transitions, we can create procedures and verifying continuous behavior between transitions, we can create
hybrid control systems with end-to-end correctness guarantees. If existing hybrid control systems with end-to-end correctness guarantees. If existing
procedures can be formalized into logical specifications and continuous dynamics procedures can be formalized into logical specifications and continuous dynamics
verified against transition requirements, then autonomous controllers can be verified against transition requirements, then autonomous controllers can be
built that are provably free from design defects. built that are provably free from design
defects.\splitnote{Hypothesis is clear and testable.}
% Pay-off % Pay-off
This approach will enable autonomous control in nuclear power plants while This approach will enable autonomous control in nuclear power plants while
maintaining the high safety standards required by the industry. maintaining the high safety standards required by the industry.
@ -50,9 +60,13 @@ maintaining the high safety standards required by the industry.
This work is conducted within the University of Pittsburgh Cyber Energy Center, This work is conducted within the University of Pittsburgh Cyber Energy Center,
which provides access to industry collaboration and Emerson control hardware, which provides access to industry collaboration and Emerson control hardware,
ensuring that developed solutions align with practical implementation ensuring that developed solutions align with practical implementation
requirements. requirements.\splitsuggest{This qualifications paragraph feels orphaned here.
It's important context but reads as an afterthought. Consider integrating it
into the approach paragraph (``...demonstrated on Emerson hardware through our
partnership with the Cyber Energy Center'') or moving to a ``Why This Will
Succeed'' framing later.}
\splitinline{This qualifications paragraph feels a bit tacked-on here. Consider moving to the end of the Approach section or integrating it more naturally into the ``why it will succeed'' argument.}
% OUTCOMES PARAGRAPHS % OUTCOMES PARAGRAPHS
If this research is successful, we will be able to do the following: If this research is successful, we will be able to do the following:
@ -92,7 +106,9 @@ If this research is successful, we will be able to do the following:
nuclear reactor startup procedures, implementing it on a small modular nuclear reactor startup procedures, implementing it on a small modular
reactor simulation using industry-standard control hardware. This reactor simulation using industry-standard control hardware. This
demonstration will prove correctness across multiple coordinated control demonstration will prove correctness across multiple coordinated control
modes from cold shutdown through criticality to power operation. modes from cold shutdown through criticality to power
operation.\splitnote{``cold shutdown through criticality to power
operation'' — concrete and impressive scope.}
% Outcome % Outcome
We will demonstrate that autonomous hybrid control can be realized in the We will demonstrate that autonomous hybrid control can be realized in the
nuclear industry with current equipment, establishing a path toward reduced nuclear industry with current equipment, establishing a path toward reduced
@ -102,7 +118,8 @@ If this research is successful, we will be able to do the following:
% IMPACT PARAGRAPH Innovation % IMPACT PARAGRAPH Innovation
The innovation in this work is unifying discrete synthesis with continuous The innovation in this work is unifying discrete synthesis with continuous
verification to enable end-to-end correctness guarantees for hybrid systems. verification to enable end-to-end correctness guarantees for hybrid
systems.\splitnote{Clear ``what's new'' statement.}
% Outcome Impact % Outcome Impact
If successful, control engineers will create autonomous controllers from If successful, control engineers will create autonomous controllers from
existing procedures with mathematical proof of correct behavior. High-assurance existing procedures with mathematical proof of correct behavior. High-assurance
@ -113,4 +130,5 @@ nuclear power. Small modular reactors offer a promising solution to growing
energy demands, but their success depends on reducing per-megawatt operating energy demands, but their success depends on reducing per-megawatt operating
costs through increased autonomy. This research will provide the tools to costs through increased autonomy. This research will provide the tools to
achieve that autonomy while maintaining the exceptional safety record the achieve that autonomy while maintaining the exceptional safety record the
nuclear industry requires. nuclear industry requires.\splitnote{Strong closing — ties technical work to
real-world impact and economic necessity.}

46
1-goals-and-outcomes/research-statement.tex
View File

@ -1,29 +1,37 @@
% GOAL PARAGRAPH % GOAL PARAGRAPH
The goal of this research is to develop a methodology for creating autonomous The goal of this research is to develop a methodology for creating autonomous
control systems with event-driven control laws that have guarantees of safe and control systems with event-driven control laws that have guarantees of safe and
correct behavior. correct behavior.\splitnote{Strong, direct opening. Sets scope immediately.}
% INTRODUCTORY PARAGRAPH Hook % INTRODUCTORY PARAGRAPH Hook
Nuclear power relies on extensively trained operators who follow detailed 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. Based on these procedures and
operators' interpretation of plant conditions, operators make critical decisions operators' interpretation of plant conditions, operators make critical decisions
about when to switch between control objectives. about when to switch between control objectives.\splitsuggest{Consider:
``operators'' appears 3x in two sentences. Maybe: ``Based on these procedures
and their interpretation of plant conditions, they make critical decisions...''}
% Gap % Gap
But, reliance on human operators has created an economic challenge for But, reliance on human operators has created an economic challenge for
next-generation nuclear power plants. Small modular reactors face significantly next-generation nuclear power plants.\splitpolish{``But, reliance'' — the comma
higher per-megawatt staffing costs than conventional plants. Autonomous control after ``But'' is unusual. Either drop it or restructure: ``However, this
systems are needed that can safely manage complex operational sequences with the reliance...'' or ``This reliance, however, has created...''} Small modular
same assurance as human-operated systems, but without constant supervision. reactors face significantly higher per-megawatt staffing costs than conventional
plants. Autonomous control systems are needed that can safely manage complex
operational sequences with the same assurance as human-operated systems, but
without constant supervision.\splitsuggest{``are needed that can'' — passive.
Try: ``Autonomous control systems must safely manage...''}
% APPROACH PARAGRAPH Solution % APPROACH PARAGRAPH Solution
To address this need, we will combine formal methods from computer science with To address this need, we will combine formal methods from computer science with
control theory to build hybrid control systems that are correct by construction. control theory to build hybrid control systems that are correct by
construction.\splitnote{Clear statement of approach.}
% Rationale % Rationale
Hybrid systems use discrete logic to switch between continuous control modes, Hybrid systems use discrete logic to switch between continuous control modes,
similar to how operators change control strategies. Existing formal methods similar to how operators change control strategies. Existing formal methods
generate provably correct switching logic but cannot handle continuous dynamics generate provably correct switching logic but cannot handle continuous dynamics
during transitions, while traditional control theory verifies continuous during transitions, while traditional control theory verifies continuous
behavior but lacks tools for proving discrete switching correctness. behavior but lacks tools for proving discrete switching
correctness.\splitnote{Nice parallel structure showing the gap.}
% Hypothesis and Technical Approach % Hypothesis and Technical Approach
We will bridge this gap through a three-stage methodology. First, we will We will bridge this gap through a three-stage methodology. First, we will
translate written operating procedures into temporal logic specifications using translate written operating procedures into temporal logic specifications using
@ -40,10 +48,17 @@ transition objectives, and then employ assume-guarantee contracts and barrier
certificates to prove that mode transitions occur safely and as defined by the certificates to prove that mode transitions occur safely and as defined by the
deterministic automata. This compositional approach enables local verification deterministic automata. This compositional approach enables local verification
of continuous modes without requiring global trajectory analysis across the of continuous modes without requiring global trajectory analysis across the
entire hybrid system. We will demonstrate this on an Emerson Ovation control system. entire hybrid system. We will demonstrate this on an Emerson Ovation control
system.\splitsuggest{This paragraph is dense. Consider breaking after the
three stages, then a new paragraph for the compositional verification point
and Emerson demo.}
% Pay-off % Pay-off
This approach will demonstrate autonomous control can be used for complex This approach will demonstrate autonomous control can be used for complex
nuclear power operations while maintaining safety guarantees. nuclear power operations while maintaining safety
guarantees.\splitpolish{``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 % OUTCOMES PARAGRAPHS
If this research is successful, we will be able to do the following: If this research is successful, we will be able to do the following:
@ -57,13 +72,14 @@ If this research is successful, we will be able to do the following:
% Outcome % Outcome
Control engineers will be able to generate mode-switching controllers from Control engineers will be able to generate mode-switching controllers from
regulatory procedures with little formal methods expertise, reducing regulatory procedures with little formal methods expertise, reducing
barriers to high-assurance control systems. barriers to high-assurance control
systems.\splitnote{Good practical framing — emphasizes accessibility.}
% OUTCOME 2 Title % OUTCOME 2 Title
\item \textit{Verify continuous control behavior across mode transitions. } \item \textit{Verify continuous control behavior across mode transitions. }
% Strategy % Strategy
We will develop methods using reachability analysis to ensure continuous control modes We will develop methods using reachability analysis to ensure continuous
satisfy discrete transition requirements. control modes satisfy discrete transition requirements.
% Outcome % Outcome
Engineers will be able to design continuous controllers using standard Engineers will be able to design continuous controllers using standard
practices while ensuring system correctness and proving mode transitions practices while ensuring system correctness and proving mode transitions
@ -77,6 +93,8 @@ If this research is successful, we will be able to do the following:
using industry-standard control hardware. % Outcome using industry-standard control hardware. % Outcome
Control engineers will be able to implement high-assurance autonomous Control engineers will be able to implement high-assurance autonomous
controls on industrial platforms they already use, enabling users to controls on industrial platforms they already use, enabling users to
achieve autonomy without retraining costs or developing new equipment. achieve autonomy without retraining costs or developing new
equipment.\splitnote{Strong industrial grounding — the ``platforms they
already use'' point is compelling for adoption.}
\end{enumerate} \end{enumerate}

56
2-state-of-the-art/state-of-art.tex
View File

@ -5,7 +5,8 @@ systems that are tractably safe. To understand what is being automated, we must
first understand how nuclear reactors are operated today. This section examines first understand how nuclear reactors are operated today. This section examines
reactor operators and the operating procedures we aim to leverage, then reactor operators and the operating procedures we aim to leverage, then
investigates limitations of human-based operation, and concludes with current investigates limitations of human-based operation, and concludes with current
formal methods approaches to reactor control systems. formal methods approaches to reactor control
systems.\splitnote{Good roadmap — tells reader exactly what's coming.}
\subsection{Current Reactor Procedures and Operation} \subsection{Current Reactor Procedures and Operation}
@ -23,7 +24,11 @@ requalification under 10 CFR 55.59~\cite{10CFR55.59}. Despite this rigor,
procedures fundamentally lack formal verification of key safety properties. No procedures fundamentally lack formal verification of key safety properties. No
mathematical proof exists that procedures cover all possible plant states, that mathematical proof exists that procedures cover all possible plant states, that
required actions can be completed within available timeframes, or that required actions can be completed within available timeframes, or that
transitions between procedure sets maintain safety invariants. transitions between procedure sets maintain safety
invariants.\splitsuggest{This paragraph is doing a lot. Consider splitting:
first paragraph on the hierarchy and compliance, second on the lack of formal
verification. The ``No mathematical proof exists...'' sentence is powerful and
deserves emphasis.}
\textbf{LIMITATION:} \textit{Procedures lack formal verification of correctness \textbf{LIMITATION:} \textit{Procedures lack formal verification of correctness
and completeness.} Current procedure development relies on expert judgment and and completeness.} Current procedure development relies on expert judgment and
@ -32,7 +37,9 @@ possible plant states, that required actions can be completed within available
timeframes, or that transitions between procedure sets maintain safety timeframes, or that transitions between procedure sets maintain safety
invariants. Paper-based procedures cannot ensure correct application, and even invariants. Paper-based procedures cannot ensure correct application, and even
computer-based procedure systems lack the formal guarantees that automated computer-based procedure systems lack the formal guarantees that automated
reasoning could provide. reasoning could provide.\splitpolish{This repeats the ``No mathematical
proof exists...'' sentence almost verbatim from the paragraph above. Either
cut it from the paragraph or from the LIMITATION box.}
Nuclear plants operate with multiple control modes: automatic control, where the Nuclear plants operate with multiple control modes: automatic control, where the
reactor control system maintains target parameters through continuous reactivity reactor control system maintains target parameters through continuous reactivity
@ -51,7 +58,9 @@ protection---automatic trips on safety parameters, emergency core cooling
actuation, containment isolation, and basic process actuation, containment isolation, and basic process
control~\cite{WRPS.Description, gentillon_westinghouse_1999}. Human operators, control~\cite{WRPS.Description, gentillon_westinghouse_1999}. Human operators,
however, retain control of strategic decision-making: power level changes, however, retain control of strategic decision-making: power level changes,
startup/shutdown sequences, mode transitions, and procedure implementation. startup/shutdown sequences, mode transitions, and procedure
implementation.\splitnote{This is the key insight — the hybrid nature is
already there, just not formally verified.}
\subsection{Human Factors in Nuclear Accidents} \subsection{Human Factors in Nuclear Accidents}
@ -65,7 +74,8 @@ operator requires several years of training.
The persistent role of human error in nuclear safety incidents---despite decades The persistent role of human error in nuclear safety incidents---despite decades
of improvements in training and procedures---provides the most compelling of improvements in training and procedures---provides the most compelling
motivation for formal automated control with mathematical safety guarantees. motivation for formal automated control with mathematical safety
guarantees.\splitnote{Strong thesis for this subsection.}
Operators hold legal authority under 10 CFR Part 55 to make critical decisions, Operators hold legal authority under 10 CFR Part 55 to make critical decisions,
including departing from normal regulations during emergencies. The Three Mile including departing from normal regulations during emergencies. The Three Mile
Island (TMI) accident demonstrated how a combination of personnel error, design Island (TMI) accident demonstrated how a combination of personnel error, design
@ -76,7 +86,9 @@ fundamental ambiguity: placing responsibility for safe power plant operations on
the licensee without formal verification that operators can fulfill this the licensee without formal verification that operators can fulfill this
responsibility does not guarantee safety. This tension between operational responsibility does not guarantee safety. This tension between operational
flexibility and safety assurance remains unresolved: the person responsible for flexibility and safety assurance remains unresolved: the person responsible for
reactor safety is often the root cause of failures. reactor safety is often the root cause of
failures.\splitnote{``the person responsible for reactor safety is often the
root cause of failures'' — devastating summary. Very effective.}
Multiple independent analyses converge on a striking statistic: 70--80\% of Multiple independent analyses converge on a striking statistic: 70--80\% of
nuclear power plant events are attributed to human error, versus approximately nuclear power plant events are attributed to human error, versus approximately
@ -87,13 +99,16 @@ culture: primarily human factors~\cite{hogberg_root_2013}. A detailed analysis
of 190 events at Chinese nuclear power plants from of 190 events at 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 active
errors, while 92\% were associated with latent errors---organizational and errors, while 92\% were associated with latent errors---organizational and
systemic weaknesses that create conditions for failure. systemic weaknesses that create conditions for
failure.\splitnote{Strong empirical grounding. The Chinese plant data is a
nice addition — shows this isn't just a Western regulatory perspective.}
\textbf{LIMITATION:} \textit{Human factors impose fundamental reliability limits \textbf{LIMITATION:} \textit{Human factors impose fundamental reliability 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 these error contribution despite four decades of improvements demonstrates that these
limitations are fundamental rather than a remediable part of human-driven control. limitations are fundamental rather than a remediable part of human-driven
control.\splitnote{Well-stated. The ``four decades'' point drives it home.}
\subsection{Formal Methods} \subsection{Formal Methods}
\subsubsection{HARDENS} \subsubsection{HARDENS}
@ -122,7 +137,8 @@ the entire RTS, including all subsystems, components, and limited digital twin
models of sensors, actuators, and compute infrastructure. Automatic code models of sensors, actuators, and compute infrastructure. Automatic code
synthesis generated verifiable C implementations and SystemVerilog hardware synthesis generated verifiable C implementations and SystemVerilog hardware
implementations directly from Cryptol models---eliminating the traditional gap implementations directly from Cryptol models---eliminating the traditional gap
between specification and implementation where errors commonly arise. between specification and implementation where errors commonly
arise.\splitnote{Good technical depth on HARDENS toolchain.}
Despite its accomplishments, HARDENS has a fundamental limitation directly Despite its accomplishments, HARDENS has a fundamental limitation directly
relevant to hybrid control synthesis: the project addressed only discrete relevant to hybrid control synthesis: the project addressed only discrete
@ -134,7 +150,8 @@ project did not address continuous dynamics of nuclear reactor physics. Real
reactor safety depends on the interaction between continuous reactor safety depends on the interaction between continuous
processes---temperature, pressure, neutron flux---evolving in response to processes---temperature, pressure, neutron flux---evolving in response to
discrete control decisions. HARDENS verified the discrete controller in discrete control decisions. HARDENS verified the discrete controller in
isolation but not the closed-loop hybrid system behavior. isolation but not the closed-loop hybrid system
behavior.\splitnote{Clear articulation of the gap your work fills.}
\textbf{LIMITATION:} \textit{HARDENS addressed discrete control logic without \textbf{LIMITATION:} \textit{HARDENS addressed discrete control logic without
continuous dynamics or hybrid system verification.} Verifying discrete control continuous dynamics or hybrid system verification.} Verifying discrete control
@ -172,7 +189,8 @@ dynamic logic (dL). dL introduces two additional operators
into temporal logic: the box operator and the diamond operator. The box operator into temporal logic: the box operator and the diamond operator. The box operator
\([\alpha]\phi\) states that for some region \(\phi\), the hybrid system \([\alpha]\phi\) states that for some region \(\phi\), the hybrid system
\(\alpha\) always remains within that region. In this way, it is a safety \(\alpha\) always remains within that region. In this way, it is a safety
ivariant being enforced for the system. The second operator, the diamond ivariant being enforced for the system.\splitfix{Typo: ``ivariant'' should be
``invariant''} The second operator, the diamond
operator \(<\alpha>\phi\) says that for the region \(\phi\), there is at least operator \(<\alpha>\phi\) says that for the region \(\phi\), there is at least
one trajectory of \(\alpha\) that enters that region. This is a declaration of a one trajectory of \(\alpha\) that enters that region. This is a declaration of a
liveness property. liveness property.
@ -184,12 +202,19 @@ actually proving them for a given hybrid system is quite difficult. Automated
proof assistants such as KeYmaera X exist to help develop proofs of systems proof assistants such as KeYmaera X exist to help develop proofs of systems
using dL, but so far have been insufficient for reasonably complex hybrid using dL, but so far have been insufficient for reasonably complex hybrid
systems. The main issue behind creating system proofs using dL is state space systems. The main issue behind creating system 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 %Source: that one satellite tracking paper that has the problem with the
%gyroscopes overloding and needing to dump speed all the time %gyroscopes overloding and needing to dump speed all the time
Approaches have been made to alleviate Approaches have been made to alleviate
these issues for nuclear power contexts using contract and decomposition based these issues for nuclear power contexts using contract and decomposition based
methods, but are far from a complete methodology to design systems with. methods, but are far from a complete methodology to design systems
with.\splitpolish{``but are far from a complete methodology to design systems
with'' — awkward ending preposition. Try: ``but remain far from a complete
design methodology'' or ``but do not yet constitute a complete design
methodology.''}
%source: Manyu's thesis. %source: Manyu's thesis.
Instead, these approaches have been used on systems that have been designed a Instead, these approaches have been used on systems that have been designed a
priori, and require expert knowledge to create the system proofs. priori, and require expert knowledge to create the system proofs.
@ -198,3 +223,8 @@ priori, and require expert knowledge to create the system proofs.
%very much, so the limitation is that logic based hybrid system approaches have %very much, so the limitation is that logic based hybrid system approaches have
%not been used in the DESIGN of autonomous controllers, only in the analysis of %not been used in the DESIGN of autonomous controllers, only in the analysis of
%systems that already exist. %systems that already exist.
\splitinline{Your comment here is spot-on. You should add a LIMITATION box:
\textit{Differential dynamic logic has been used for post-hoc analysis of
existing systems, not for the constructive design of autonomous controllers.}
This is exactly the gap you're filling — you're doing synthesis, not just
verification.}

8
3-research-approach/approach.tex
View File

@ -30,7 +30,7 @@ The challenge of hybrid system verification lies in the interaction between
discrete and continuous dynamics. Discrete transitions change the governing discrete and continuous dynamics. Discrete transitions change the governing
vector field, creating discontinuities in the system's behavior. Traditional vector field, creating discontinuities in the system's behavior. Traditional
verification techniques designed for purely discrete or purely continuous verification techniques designed for purely discrete or purely continuous
systems cannot handle this interaction directly.Our methodology addresses this systems cannot handle this interaction directly.\splitpolish{Missing space before ``Our} Our methodology addresses this
challenge through decomposition. We verify discrete switching logic and challenge through decomposition. We verify discrete switching logic and
continuous mode behavior separately, then compose these guarantees to reason continuous mode behavior separately, then compose these guarantees to reason
about the complete hybrid system. This two-layer approach mirrors the structure about the complete hybrid system. This two-layer approach mirrors the structure
@ -75,7 +75,7 @@ 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 with proof artifacts demonstrating that the intended behavior of the control
system is satisfied by its actual implementation. This approach is tractable now system is satisfied by its actual implementation. This approach is tractable now
because the infrastructure for each component has matured. The novelty is not in because the infrastructure for each component has matured. The novelty is not in
the individual pieces, but in the architecture that connects them. By defining the individual pieces, but in the architecture that connects them.\splitnote{This is your key insight — the novelty is compositional, not component-level.} By defining
entry, exit, and safety conditions at the discrete level first, we transform the entry, exit, and safety conditions at the discrete level first, we transform the
intractable problem of global hybrid verification into a collection of local intractable problem of global hybrid verification into a collection of local
verification problems with clear interfaces. Verification is performed per mode verification problems with clear interfaces. Verification is performed per mode
@ -404,7 +404,7 @@ $q_i$ must drive the system from any state in $\mathcal{X}_{entry,i}$ to some
state in $\mathcal{X}_{exit,i}$ while remaining within $\mathcal{X}_{safe,i}$. state in $\mathcal{X}_{exit,i}$ while remaining within $\mathcal{X}_{safe,i}$.
We classify continuous controllers into three types based on their objectives: We classify continuous controllers into three types based on their objectives:
transitory, stabilizing, and expulsory. Each type has distinct verification transitory, stabilizing, and expulsory.\splitnote{This three-mode taxonomy is elegant — maps verification tools to control objectives cleanly.} Each type has distinct verification
requirements that determine which formal methods tools are appropriate. requirements that determine which formal methods tools are appropriate.
%%% NOTES (Section 4): %%% NOTES (Section 4):
@ -619,7 +619,7 @@ the success and impact of this work. We will directly address the gap of
verification and validation methods for these systems and industry adoption by verification and validation methods for these systems and industry adoption by
forming a two-way exchange of knowledge between the laboratory and commercial forming a two-way exchange of knowledge between the laboratory and commercial
environments. This work stands to be successful with Emerson implementation environments. This work stands to be successful with Emerson implementation
because we will have excess to system experts at Emerson to help with the fine because we will have access to system experts\splitfix{Typo: ``excess should be ``access} at Emerson to help with the fine
details of using the Ovation system. At the same time, we will have the benefit details of using the Ovation system. At the same time, we will have the benefit
of transferring technology directly to industry with a direct collaboration in of transferring technology directly to industry with a direct collaboration in
this research, while getting an excellent perspective of how our research this research, while getting an excellent perspective of how our research

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

@ -3,7 +3,9 @@
This research will be measured by advancement through Technology Readiness This research will be measured by advancement through Technology Readiness
Levels, progressing from fundamental concepts to validated prototype Levels, progressing from fundamental concepts to validated prototype
demonstration. This work begins at TRL 2--3 and aims to reach TRL 5, where demonstration. This work begins at TRL 2--3 and aims to reach TRL 5, where
system components operate successfully in a relevant laboratory environment. system components operate successfully in a relevant laboratory
environment.\splitnote{TRL as primary metric is smart — speaks industry
language.}
This section explains why TRL advancement provides the most appropriate success This section explains why TRL advancement provides the most appropriate success
metric and defines the specific criteria required to achieve TRL 5. metric and defines the specific criteria required to achieve TRL 5.
@ -12,7 +14,9 @@ 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. papers published or theorems proved cannot capture practical feasibility.
Empirical metrics like simulation accuracy or computational speed cannot Empirical metrics like simulation accuracy or computational speed cannot
demonstrate theoretical rigor. TRLs measure both dimensions simultaneously. demonstrate theoretical rigor. TRLs measure both dimensions
simultaneously.\splitnote{Good framing — explains why other metrics are
insufficient.}
Advancing from TRL 3 to TRL 5 requires maintaining theoretical rigor while Advancing from TRL 3 to TRL 5 requires maintaining theoretical rigor while
progressively demonstrating practical feasibility. Formal verification must progressively demonstrating practical feasibility. Formal verification must
remain valid as the system moves from individual components to integrated remain valid as the system moves from individual components to integrated
@ -68,7 +72,9 @@ across the full operational envelope. The controller must handle off-nominal
scenarios to validate that expulsory modes function correctly. For example, scenarios to validate that expulsory modes function correctly. For example,
simulated sensor failures must trigger appropriate fault detection and mode simulated sensor failures must trigger appropriate fault detection and mode
transitions, and loss-of-cooling scenarios must activate SCRAM procedures as transitions, and loss-of-cooling scenarios must activate SCRAM procedures as
specified. Graded responses to minor disturbances are outside this work's scope. specified. Graded responses to minor disturbances are outside this work's
scope.\splitsuggest{Consider noting why graded responses are out of scope —
is it time, complexity, or scope creep? Brief justification helps.}
Formal verification results must remain valid, with discrete behavior matching Formal verification results must remain valid, with discrete behavior matching
specifications and continuous trajectories remaining within verified bounds. specifications and continuous trajectories remaining within verified bounds.
This proves that the methodology produces verified controllers implementable on This proves that the methodology produces verified controllers implementable on
@ -85,4 +91,6 @@ complete autonomous hybrid controller with formal correctness guarantees
operating on industrial control hardware through hardware-in-the-loop testing in operating on industrial control hardware through hardware-in-the-loop testing in
a relevant laboratory environment. This establishes both theoretical validity a relevant laboratory environment. This establishes both theoretical validity
and practical feasibility, proving that the methodology produces verified and practical feasibility, proving that the methodology produces verified
controllers and that implementation is achievable with current technology. controllers and that implementation is achievable with current
technology.\splitnote{Clear success criteria. Committee will know exactly
what ``done'' looks like.}

2
5-risks-and-contingencies/risks.tex
View File

@ -1,7 +1,7 @@
\section{Risks and Contingencies} \section{Risks and Contingencies}
This research relies on several critical assumptions that, if invalidated, would This research relies on several critical assumptions that, if invalidated, would
require scope adjustment or methodological revision. The primary risks to require scope adjustment or methodological revision.\splitnote{Honest acknowledgment of risks with clear contingencies — committee will appreciate this.} The primary risks to
successful completion fall into four categories: computational tractability of successful completion fall into four categories: computational tractability of
synthesis and verification, complexity of the discrete-continuous interface, synthesis and verification, complexity of the discrete-continuous interface,
completeness of procedure formalization, and hardware-in-the-loop integration completeness of procedure formalization, and hardware-in-the-loop integration

2
6-broader-impacts/impacts.tex
View File

@ -66,6 +66,6 @@ applies to any hybrid system with documented operational requirements. Potential
applications include chemical process control, aerospace systems, and autonomous applications include chemical process control, aerospace systems, and autonomous
transportation, where similar economic and safety considerations favor increased transportation, where similar economic and safety considerations favor increased
autonomy with provable correctness guarantees. Demonstrating this approach in autonomy with provable correctness guarantees. Demonstrating this approach in
nuclear power---one of the most regulated and safety-critical domains---will nuclear power---one of the most regulated and safety-critical domains\splitnote{``If it works here, it works anywhere — strong closing argument.}---will
establish both the technical feasibility and regulatory pathway for broader establish both the technical feasibility and regulatory pathway for broader
adoption across critical infrastructure. adoption across critical infrastructure.

2
8-schedule/schedule.tex
View File

@ -93,4 +93,4 @@ methodology. M5 (Month 20) achieves TRL 5 by demonstrating practical
implementability on industrial hardware. This milestone delivers a conference implementability on industrial hardware. This milestone delivers a conference
paper submission to NPIC\&HMIT or CDC documenting hardware implementation and paper submission to NPIC\&HMIT or CDC documenting hardware implementation and
experimental validation. M6 (Month 24) completes the dissertation documenting experimental validation. M6 (Month 24) completes the dissertation documenting
the entire methodology, experimental results, and research contributions. the entire methodology, experimental results, and research contributions.\splitnote{Clear timeline with publication targets — shows you have a plan.}

240
main.aux
View File

@ -1,70 +1,230 @@
\relax \relax
\@writefile{toc}{\contentsline {section}{Contents}{ii}{}\protected@file@percent } \@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Strong, direct opening. Sets scope immediately.}{i}{}\protected@file@percent }
\pgfsyspdfmark {pgfid1}{10005341}{44941311}
\pgfsyspdfmark {pgfid4}{33755687}{44915575}
\pgfsyspdfmark {pgfid5}{36070152}{44675891}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{yellow!60}{\textcolor {yellow!60}{o}}\ Consider: ``operators'' appears 3x in two sentences. Maybe: ``Based on these procedures and their interpretation of plant conditions, they make critical decisions...''}{i}{}\protected@file@percent }
\pgfsyspdfmark {pgfid6}{15536702}{41140223}
\pgfsyspdfmark {pgfid9}{33755687}{40539187}
\pgfsyspdfmark {pgfid10}{36070152}{40299503}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{orange!50}{\textcolor {orange!50}{o}}\ ``But, reliance'' — the comma after ``But'' is unusual. Either drop it or restructure: ``However, this reliance...'' or ``This reliance, however, has created...''}{i}{}\protected@file@percent }
\pgfsyspdfmark {pgfid11}{24132805}{40189951}
\pgfsyspdfmark {pgfid14}{33755687}{26505721}
\pgfsyspdfmark {pgfid15}{36070152}{26266037}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{yellow!60}{\textcolor {yellow!60}{o}}\ ``are needed that can'' — passive. Try: ``Autonomous control systems must safely manage...''}{i}{}\protected@file@percent }
\pgfsyspdfmark {pgfid16}{11376844}{36388863}
\pgfsyspdfmark {pgfid19}{33755687}{13363545}
\pgfsyspdfmark {pgfid20}{36070152}{13123861}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Clear statement of approach.}{i}{}\protected@file@percent }
\pgfsyspdfmark {pgfid21}{30785862}{34488319}
\pgfsyspdfmark {pgfid24}{33755687}{5421997}
\pgfsyspdfmark {pgfid25}{36070152}{5182313}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Nice parallel structure showing the gap.}{i}{}\protected@file@percent }
\pgfsyspdfmark {pgfid26}{19909561}{29736959}
\pgfsyspdfmark {pgfid29}{33755687}{1936899}
\pgfsyspdfmark {pgfid30}{36070152}{1697215}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{yellow!60}{\textcolor {yellow!60}{o}}\ This paragraph is dense. Consider breaking after the three stages, then a new paragraph for the compositional verification point and Emerson demo.}{i}{}\protected@file@percent }
\pgfsyspdfmark {pgfid31}{29147912}{16433151}
\pgfsyspdfmark {pgfid34}{33755687}{-2439489}
\pgfsyspdfmark {pgfid35}{36070152}{-2679173}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{orange!50}{\textcolor {orange!50}{o}}\ ``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.''}{i}{}\protected@file@percent }
\pgfsyspdfmark {pgfid36}{21883461}{14532607}
\pgfsyspdfmark {pgfid39}{33755687}{-14690375}
\pgfsyspdfmark {pgfid40}{36070152}{-14930059}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Good practical framing — emphasizes accessibility.}{i}{}\protected@file@percent }
\pgfsyspdfmark {pgfid41}{27551156}{7225343}
\pgfsyspdfmark {pgfid44}{33755687}{-38528031}
\pgfsyspdfmark {pgfid45}{36070152}{-38767715}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Strong industrial grounding — the ``platforms they already use'' point is compelling for adoption.}{ii}{}\protected@file@percent }
\pgfsyspdfmark {pgfid46}{15325447}{39239679}
\pgfsyspdfmark {pgfid49}{33755687}{39213943}
\pgfsyspdfmark {pgfid50}{36070152}{38974259}
\@writefile{toc}{\contentsline {section}{Contents}{iii}{}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {1}Goals and Outcomes}{1}{}\protected@file@percent } \@writefile{toc}{\contentsline {section}{\numberline {1}Goals and Outcomes}{1}{}\protected@file@percent }
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Strong opening — direct and clear. No changes needed.}{1}{}\protected@file@percent } \@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Clear thesis statement. Gets right to it.}{1}{}\protected@file@percent }
\pgfsyspdfmark {pgfid1}{25927240}{44563390} \pgfsyspdfmark {pgfid51}{30597830}{44563390}
\pgfsyspdfmark {pgfid4}{38491976}{44537654} \pgfsyspdfmark {pgfid54}{33755687}{44537654}
\pgfsyspdfmark {pgfid5}{40806441}{44297970} \pgfsyspdfmark {pgfid55}{36070152}{44297970}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Consider: ``...and creates a fundamental economic challenge'' — the ``and'' makes this feel like two separate issues. Maybe split into two sentences or tighten the causal link?}{1}{}\protected@file@percent } \@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Stakes established immediately — good hook.}{1}{}\protected@file@percent }
\pgfsyspdfmark {pgfid6}{6549774}{36961214} \pgfsyspdfmark {pgfid56}{11072977}{41712574}
\pgfsyspdfmark {pgfid9}{38491976}{36935478} \pgfsyspdfmark {pgfid59}{33755687}{40308378}
\pgfsyspdfmark {pgfid10}{40806441}{36695794} \pgfsyspdfmark {pgfid60}{36070152}{40068694}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ ``What is needed is'' — classic Gopen weak opening. Try: ``Autonomous control systems must safely manage...'' — puts the subject in the topic position.}{1}{}\protected@file@percent } \@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{yellow!60}{\textcolor {yellow!60}{o}}\ The ``and'' here joins two distinct issues (autonomy barrier + economics). Consider making the causal link explicit: ``This reliance on human operators not only prevents autonomous control capabilities but also creates...'' or split into two sentences.}{1}{}\protected@file@percent }
\pgfsyspdfmark {pgfid11}{10907275}{33160126} \pgfsyspdfmark {pgfid61}{19272391}{36010942}
\pgfsyspdfmark {pgfid14}{38491976}{21872198} \pgfsyspdfmark {pgfid64}{33755687}{35931990}
\pgfsyspdfmark {pgfid15}{40806441}{21632514} \pgfsyspdfmark {pgfid65}{36070152}{35692306}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ This qualifications paragraph feels a bit tacked-on here. Consider moving to the end of the Approach section or integrating it more naturally into the ``why it will succeed'' argument.}{1}{}\protected@file@percent } \@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{orange!50}{\textcolor {orange!50}{o}}\ ``What is needed is'' — Gopen would call this a weak topic position. The sentence buries the subject. Try: ``Autonomous control systems must safely manage complex operational sequences...'' Puts the actor in the topic position.}{1}{}\protected@file@percent }
\pgfsyspdfmark {pgfid16}{20112834}{17337306} \pgfsyspdfmark {pgfid66}{20791156}{31259582}
\pgfsyspdfmark {pgfid69}{33755687}{14768204}
\pgfsyspdfmark {pgfid70}{36070152}{14528520}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Excellent setup of the gap — shows why neither approach alone is sufficient.}{1}{}\protected@file@percent }
\pgfsyspdfmark {pgfid71}{7117565}{23657406}
\pgfsyspdfmark {pgfid74}{33755687}{-3868824}
\pgfsyspdfmark {pgfid75}{36070152}{-4108508}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Hypothesis is clear and testable.}{1}{}\protected@file@percent }
\pgfsyspdfmark {pgfid76}{16705748}{18906046}
\pgfsyspdfmark {pgfid79}{33755687}{-10771970}
\pgfsyspdfmark {pgfid80}{36070152}{-11011654}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{yellow!60}{\textcolor {yellow!60}{o}}\ This qualifications paragraph feels orphaned here. It's important context but reads as an afterthought. Consider integrating it into the approach paragraph (``...demonstrated on Emerson hardware through our partnership with the Cyber Energy Center'') or moving to a ``Why This Will Succeed'' framing later.}{1}{}\protected@file@percent }
\pgfsyspdfmark {pgfid81}{30785862}{14154686}
\pgfsyspdfmark {pgfid84}{33755687}{-14109956}
\pgfsyspdfmark {pgfid85}{36070152}{-14349640}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ ``cold shutdown through criticality to power operation'' — concrete and impressive scope.}{2}{}\protected@file@percent }
\pgfsyspdfmark {pgfid86}{22235661}{34488319}
\pgfsyspdfmark {pgfid89}{33755687}{34462583}
\pgfsyspdfmark {pgfid90}{36070152}{34222899}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Clear ``what's new'' statement.}{2}{}\protected@file@percent }
\pgfsyspdfmark {pgfid91}{27214487}{28884991}
\pgfsyspdfmark {pgfid94}{33755687}{25629745}
\pgfsyspdfmark {pgfid95}{36070152}{25390061}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Strong closing — ties technical work to real-world impact and economic necessity.}{2}{}\protected@file@percent }
\pgfsyspdfmark {pgfid96}{18188851}{21282815}
\pgfsyspdfmark {pgfid99}{33755687}{21257079}
\pgfsyspdfmark {pgfid100}{36070152}{21017395}
\citation{NUREG-0899,10CFR50.34} \citation{NUREG-0899,10CFR50.34}
\citation{10CFR55.59} \citation{10CFR55.59}
\citation{WRPS.Description,gentillon_westinghouse_1999} \citation{WRPS.Description,gentillon_westinghouse_1999}
\@writefile{toc}{\contentsline {section}{\numberline {2}State of the Art and Limits of Current Practice}{3}{}\protected@file@percent }
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Good roadmap — tells reader exactly what's coming.}{3}{}\protected@file@percent }
\pgfsyspdfmark {pgfid101}{13036184}{40762302}
\pgfsyspdfmark {pgfid104}{33755687}{40736566}
\pgfsyspdfmark {pgfid105}{36070152}{40496882}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}Current Reactor Procedures and Operation}{3}{}\protected@file@percent }
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{yellow!60}{\textcolor {yellow!60}{o}}\ 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.}{3}{}\protected@file@percent }
\pgfsyspdfmark {pgfid106}{17724053}{25831016}
\pgfsyspdfmark {pgfid109}{33755687}{25805280}
\pgfsyspdfmark {pgfid110}{36070152}{25565596}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{orange!50}{\textcolor {orange!50}{o}}\ 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.}{3}{}\protected@file@percent }
\pgfsyspdfmark {pgfid111}{27570105}{19179112}
\pgfsyspdfmark {pgfid114}{33755687}{7168252}
\pgfsyspdfmark {pgfid115}{36070152}{6928568}
\citation{operator_statistics} \citation{operator_statistics}
\citation{10CFR55} \citation{10CFR55}
\citation{10CFR50.54} \citation{10CFR50.54}
\@writefile{toc}{\contentsline {section}{\numberline {2}State of the Art and Limits of Current Practice}{3}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}Current Reactor Procedures and Operation}{3}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Human Factors in Nuclear Accidents}{3}{}\protected@file@percent }
\citation{Kemeny1979} \citation{Kemeny1979}
\citation{WNA2020} \citation{WNA2020}
\citation{hogberg_root_2013} \citation{hogberg_root_2013}
\citation{zhang_analysis_2025} \citation{zhang_analysis_2025}
\citation{Kiniry2024} \citation{Kiniry2024}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ This is the key insight — the hybrid nature is already there, just not formally verified.}{4}{}\protected@file@percent }
\pgfsyspdfmark {pgfid116}{29333260}{45891583}
\pgfsyspdfmark {pgfid119}{33755687}{45865847}
\pgfsyspdfmark {pgfid120}{36070152}{45626163}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Human Factors in Nuclear Accidents}{4}{}\protected@file@percent }
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Strong thesis for this subsection.}{4}{}\protected@file@percent }
\pgfsyspdfmark {pgfid121}{27354523}{35711657}
\pgfsyspdfmark {pgfid124}{33755687}{35685921}
\pgfsyspdfmark {pgfid125}{36070152}{35446237}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ ``the person responsible for reactor safety is often the root cause of failures'' — devastating summary. Very effective.}{4}{}\protected@file@percent }
\pgfsyspdfmark {pgfid126}{24580098}{26208937}
\pgfsyspdfmark {pgfid129}{33755687}{26183201}
\pgfsyspdfmark {pgfid130}{36070152}{25943517}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Strong empirical grounding. The Chinese plant data is a nice addition — shows this isn't just a Western regulatory perspective.}{4}{}\protected@file@percent }
\pgfsyspdfmark {pgfid131}{11564802}{17656489}
\pgfsyspdfmark {pgfid134}{33755687}{16604393}
\pgfsyspdfmark {pgfid135}{36070152}{16364709}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Well-stated. The ``four decades'' point drives it home.}{4}{}\protected@file@percent }
\pgfsyspdfmark {pgfid136}{24906501}{13855401}
\pgfsyspdfmark {pgfid139}{33755687}{5097685}
\pgfsyspdfmark {pgfid140}{36070152}{4858001}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.3}Formal Methods}{4}{}\protected@file@percent } \@writefile{toc}{\contentsline {subsection}{\numberline {2.3}Formal Methods}{4}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsubsection}{\numberline {2.3.1}HARDENS}{4}{}\protected@file@percent } \@writefile{toc}{\contentsline {subsubsection}{\numberline {2.3.1}HARDENS}{4}{}\protected@file@percent }
\citation{Kiniry2024} \citation{Kiniry2024}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {2.3.2}Sequent Calculus and Differential Dynamic Logic}{5}{}\protected@file@percent } \@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Good technical depth on HARDENS toolchain.}{5}{}\protected@file@percent }
\pgfsyspdfmark {pgfid141}{22013224}{31637503}
\pgfsyspdfmark {pgfid144}{33755687}{31611767}
\pgfsyspdfmark {pgfid145}{36070152}{31372083}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Clear articulation of the gap your work fills.}{5}{}\protected@file@percent }
\pgfsyspdfmark {pgfid146}{23378487}{22134783}
\pgfsyspdfmark {pgfid149}{33755687}{22109047}
\pgfsyspdfmark {pgfid150}{36070152}{21869363}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {2.3.2}Sequent Calculus and Differential Dynamic Logic}{6}{}\protected@file@percent }
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{red!40}{\textcolor {red!40}{o}}\ Typo: ``ivariant'' should be ``invariant''}{6}{}\protected@file@percent }
\pgfsyspdfmark {pgfid151}{19651738}{35711657}
\pgfsyspdfmark {pgfid154}{33755687}{35685921}
\pgfsyspdfmark {pgfid155}{36070152}{35446237}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{yellow!60}{\textcolor {yellow!60}{o}}\ 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.}{6}{}\protected@file@percent }
\pgfsyspdfmark {pgfid156}{11704839}{28109481}
\pgfsyspdfmark {pgfid159}{33755687}{28083745}
\pgfsyspdfmark {pgfid160}{36070152}{27844061}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{orange!50}{\textcolor {orange!50}{o}}\ ``but are far from a complete methodology to design systems with'' — awkward ending preposition. Try: ``but remain far from a complete design methodology'' or ``but do not yet constitute a complete design methodology.''}{6}{}\protected@file@percent }
\pgfsyspdfmark {pgfid161}{22592676}{26208937}
\pgfsyspdfmark {pgfid164}{33755687}{13903167}
\pgfsyspdfmark {pgfid165}{36070152}{13663483}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ 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.}{6}{}\protected@file@percent }
\pgfsyspdfmark {pgfid166}{17744690}{21847466}
\citation{HANDBOOK ON HYBRID SYSTEMS} \citation{HANDBOOK ON HYBRID SYSTEMS}
\@writefile{toc}{\contentsline {section}{\numberline {3}Research Approach}{7}{}\protected@file@percent } \@writefile{toc}{\contentsline {section}{\numberline {3}Research Approach}{7}{}\protected@file@percent }
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{orange!50}{\textcolor {orange!50}{o}}\ Missing space before ``Our}{7}{}\protected@file@percent }
\pgfsyspdfmark {pgfid167}{10825988}{33160126}
\pgfsyspdfmark {pgfid170}{33755687}{33134390}
\pgfsyspdfmark {pgfid171}{36070152}{32894706}
\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Simplified hybrid automaton for reactor startup. Each discrete state $q_i$ has associated continuous dynamics $f_i$. Guard conditions on transitions (e.g., $T_{avg} > T_{min}$) are predicates over continuous state. Invariant violations ($\neg Inv_i$) trigger transitions to the SCRAM state. The operational level manages discrete transitions; the tactical level executes continuous control within each mode.}}{8}{}\protected@file@percent } \@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Simplified hybrid automaton for reactor startup. Each discrete state $q_i$ has associated continuous dynamics $f_i$. Guard conditions on transitions (e.g., $T_{avg} > T_{min}$) are predicates over continuous state. Invariant violations ($\neg Inv_i$) trigger transitions to the SCRAM state. The operational level manages discrete transitions; the tactical level executes continuous control within each mode.}}{8}{}\protected@file@percent }
\newlabel{fig:hybrid_automaton}{{1}{8}{Research Approach}{figure.1}{}} \newlabel{fig:hybrid_automaton}{{1}{8}{Research Approach}{figure.1}{}}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ This is your key insight — the novelty is compositional, not component-level.}{8}{}\protected@file@percent }
\pgfsyspdfmark {pgfid172}{21716682}{23775512}
\pgfsyspdfmark {pgfid175}{33755687}{23749776}
\pgfsyspdfmark {pgfid176}{36070152}{23510092}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}System Requirements, Specifications, and Discrete Controllers}{8}{}\protected@file@percent } \@writefile{toc}{\contentsline {subsection}{\numberline {3.1}System Requirements, Specifications, and Discrete Controllers}{8}{}\protected@file@percent }
\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Control scope hierarchy in nuclear power operations. Strategic control (long-term planning) remains with human management. HAHACS addresses the operational level (discrete mode switching) and tactical level (continuous control within modes), which together form a hybrid control system.}}{9}{}\protected@file@percent } \@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Control scope hierarchy in nuclear power operations. Strategic control (long-term planning) remains with human management. HAHACS addresses the operational level (discrete mode switching) and tactical level (continuous control within modes), which together form a hybrid control system.}}{9}{}\protected@file@percent }
\newlabel{fig:strat_op_tact}{{2}{9}{System Requirements, Specifications, and Discrete Controllers}{figure.2}{}} \newlabel{fig:strat_op_tact}{{2}{9}{System Requirements, Specifications, and Discrete Controllers}{figure.2}{}}
\citation{MANYUS THESIS}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.2}Continuous Control Modes}{11}{}\protected@file@percent } \@writefile{toc}{\contentsline {subsection}{\numberline {3.2}Continuous Control Modes}{11}{}\protected@file@percent }
\citation{MANYUS THESIS}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ This three-mode taxonomy is elegant — maps verification tools to control objectives cleanly.}{12}{}\protected@file@percent }
\pgfsyspdfmark {pgfid179}{16597916}{12329325}
\pgfsyspdfmark {pgfid182}{33755687}{12303589}
\pgfsyspdfmark {pgfid183}{36070152}{12063905}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.2.1}Transitory Modes}{12}{}\protected@file@percent } \@writefile{toc}{\contentsline {subsubsection}{\numberline {3.2.1}Transitory Modes}{12}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.2.2}Stabilizing Modes}{12}{}\protected@file@percent } \@writefile{toc}{\contentsline {subsubsection}{\numberline {3.2.2}Stabilizing Modes}{13}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.2.3}Expulsory Modes}{13}{}\protected@file@percent } \@writefile{toc}{\contentsline {subsubsection}{\numberline {3.2.3}Expulsory Modes}{14}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {3.3}Industrial Implementation}{14}{}\protected@file@percent } \@writefile{toc}{\contentsline {subsection}{\numberline {3.3}Industrial Implementation}{15}{}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {4}Metrics for Success}{15}{}\protected@file@percent } \@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{red!40}{\textcolor {red!40}{o}}\ Typo: ``excess should be ``access}{15}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{TRL 3 \textit {Critical Function and Proof of Concept}}{15}{}\protected@file@percent } \pgfsyspdfmark {pgfid184}{16922734}{5204649}
\@writefile{toc}{\contentsline {paragraph}{TRL 4 \textit {Laboratory Testing of Integrated Components}}{15}{}\protected@file@percent } \pgfsyspdfmark {pgfid187}{33755687}{5178913}
\@writefile{toc}{\contentsline {paragraph}{TRL 5 \textit {Laboratory Testing in Relevant Environment}}{15}{}\protected@file@percent } \pgfsyspdfmark {pgfid188}{36070152}{4939229}
\@writefile{toc}{\contentsline {section}{\numberline {5}Risks and Contingencies}{17}{}\protected@file@percent } \@writefile{toc}{\contentsline {section}{\numberline {4}Metrics for Success}{17}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {5.1}Computational Tractability of Synthesis}{17}{}\protected@file@percent } \@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ TRL as primary metric is smart — speaks industry language.}{17}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{17}{}\protected@file@percent } \pgfsyspdfmark {pgfid189}{26292290}{42662846}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{18}{}\protected@file@percent } \pgfsyspdfmark {pgfid192}{33755687}{42637110}
\pgfsyspdfmark {pgfid193}{36070152}{42397426}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Good framing — explains why other metrics are insufficient.}{17}{}\protected@file@percent }
\pgfsyspdfmark {pgfid194}{20090191}{35060670}
\pgfsyspdfmark {pgfid197}{33755687}{35034934}
\pgfsyspdfmark {pgfid198}{36070152}{34795250}
\@writefile{toc}{\contentsline {paragraph}{TRL 3 \textit {Critical Function and Proof of Concept}}{17}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{TRL 4 \textit {Laboratory Testing of Integrated Components}}{17}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{TRL 5 \textit {Laboratory Testing in Relevant Environment}}{18}{}\protected@file@percent }
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{yellow!60}{\textcolor {yellow!60}{o}}\ Consider noting why graded responses are out of scope — is it time, complexity, or scope creep? Brief justification helps.}{18}{}\protected@file@percent }
\pgfsyspdfmark {pgfid199}{9102038}{33199444}
\pgfsyspdfmark {pgfid202}{33755687}{33173708}
\pgfsyspdfmark {pgfid203}{36070152}{32934024}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Clear success criteria. Committee will know exactly what ``done'' looks like.}{18}{}\protected@file@percent }
\pgfsyspdfmark {pgfid204}{12395286}{18945364}
\pgfsyspdfmark {pgfid207}{33755687}{18919628}
\pgfsyspdfmark {pgfid208}{36070152}{18679944}
\@writefile{toc}{\contentsline {section}{\numberline {5}Risks and Contingencies}{19}{}\protected@file@percent }
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Honest acknowledgment of risks with clear contingencies — committee will appreciate this.}{19}{}\protected@file@percent }
\pgfsyspdfmark {pgfid209}{20770641}{44563390}
\pgfsyspdfmark {pgfid212}{33755687}{44537654}
\pgfsyspdfmark {pgfid213}{36070152}{44297970}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.1}Computational Tractability of Synthesis}{19}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{19}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{21}{}\protected@file@percent }
\citation{eia_lcoe_2022} \citation{eia_lcoe_2022}
\citation{eesi_datacenter_2024} \citation{eesi_datacenter_2024}
\citation{eia_lcoe_2022} \citation{eia_lcoe_2022}
\@writefile{toc}{\contentsline {section}{\numberline {6}Broader Impacts}{20}{}\protected@file@percent } \@writefile{toc}{\contentsline {section}{\numberline {6}Broader Impacts}{23}{}\protected@file@percent }
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ ``If it works here, it works anywhere — strong closing argument.}{24}{}\protected@file@percent }
\pgfsyspdfmark {pgfid214}{24213455}{31637503}
\pgfsyspdfmark {pgfid217}{33755687}{31611767}
\pgfsyspdfmark {pgfid218}{36070152}{31372083}
\bibstyle{ieeetr} \bibstyle{ieeetr}
\bibdata{references} \bibdata{references}
\@writefile{toc}{\contentsline {section}{\numberline {7}Schedule, Milestones, and Deliverables}{22}{}\protected@file@percent } \@writefile{toc}{\contentsline {section}{\numberline {7}Schedule, Milestones, and Deliverables}{25}{}\protected@file@percent }
\gtt@chartextrasize{0}{164.1287pt} \gtt@chartextrasize{0}{164.1287pt}
\@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces Project schedule showing major research thrusts, milestones (orange row), and publications (green row). Red diamonds indicate completion points. Overlapping bars indicate parallel work where appropriate.}}{22}{}\protected@file@percent } \@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces Project schedule showing major research thrusts, milestones (orange row), and publications (green row). Red diamonds indicate completion points. Overlapping bars indicate parallel work where appropriate.}}{25}{}\protected@file@percent }
\newlabel{fig:gantt}{{3}{22}{Schedule, Milestones, and Deliverables}{figure.3}{}} \newlabel{fig:gantt}{{3}{25}{Schedule, Milestones, and Deliverables}{figure.3}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {7.1}Milestones and Deliverables}{22}{}\protected@file@percent } \@writefile{toc}{\contentsline {subsection}{\numberline {7.1}Milestones and Deliverables}{25}{}\protected@file@percent }
\bibcite{NUREG-0899}{1} \bibcite{NUREG-0899}{1}
\bibcite{10CFR50.34}{2} \bibcite{10CFR50.34}{2}
\bibcite{10CFR55.59}{3} \bibcite{10CFR55.59}{3}
@ -76,9 +236,13 @@
\bibcite{Kemeny1979}{9} \bibcite{Kemeny1979}{9}
\bibcite{WNA2020}{10} \bibcite{WNA2020}{10}
\bibcite{hogberg_root_2013}{11} \bibcite{hogberg_root_2013}{11}
\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Clear timeline with publication targets — shows you have a plan.}{26}{}\protected@file@percent }
\pgfsyspdfmark {pgfid220}{15051800}{39239679}
\pgfsyspdfmark {pgfid223}{33755687}{39213943}
\pgfsyspdfmark {pgfid224}{36070152}{38974259}
\@writefile{toc}{\contentsline {section}{References}{26}{}\protected@file@percent }
\bibcite{zhang_analysis_2025}{12} \bibcite{zhang_analysis_2025}{12}
\bibcite{Kiniry2024}{13} \bibcite{Kiniry2024}{13}
\bibcite{eia_lcoe_2022}{14} \bibcite{eia_lcoe_2022}{14}
\bibcite{eesi_datacenter_2024}{15} \bibcite{eesi_datacenter_2024}{15}
\@writefile{toc}{\contentsline {section}{References}{23}{}\protected@file@percent } \gdef \@abspage@last{31}
\gdef \@abspage@last{27}

4
main.blg
View File

@ -1,11 +1,11 @@
This is BibTeX, Version 0.99d (TeX Live 2025) This is BibTeX, Version 0.99d (TeX Live 2025)
Capacity: max_strings=200000, hash_size=200000, hash_prime=170003 Capacity: max_strings=200000, hash_size=200000, hash_prime=170003
The top-level auxiliary file: main.aux The top-level auxiliary file: main.aux
White space in argument---line 36 of file main.aux White space in argument---line 156 of file main.aux
: \citation{HANDBOOK : \citation{HANDBOOK
: ON HYBRID SYSTEMS} : ON HYBRID SYSTEMS}
I'm skipping whatever remains of this command I'm skipping whatever remains of this command
White space in argument---line 43 of file main.aux White space in argument---line 172 of file main.aux
: \citation{MANYUS : \citation{MANYUS
: THESIS} : THESIS}
I'm skipping whatever remains of this command I'm skipping whatever remains of this command

32
main.fdb_latexmk
View File

@ -1,13 +1,13 @@
# Fdb version 4 # Fdb version 4
["bibtex main"] 1773106474.93179 "main.aux" "main.bbl" "main" 1773106474.96468 2 ["bibtex main"] 1773107049.11865 "main.aux" "main.bbl" "main" 1773107049.14627 2
"./references.bib" 1770435796.31586 14069 2a4f74c587187a8a71049043171eb0fe "" "./references.bib" 1770435796.31586 14069 2a4f74c587187a8a71049043171eb0fe ""
"/Users/split/Library/TinyTeX/texmf-dist/bibtex/bst/base/ieeetr.bst" 1292289607 18361 1a00e58565e7f19bf2b3e1bfb82254ae "" "/Users/split/Library/TinyTeX/texmf-dist/bibtex/bst/base/ieeetr.bst" 1292289607 18361 1a00e58565e7f19bf2b3e1bfb82254ae ""
"main.aux" 1773106474.76109 7231 2769f5164b2ddb0c968502f2788a9df8 "pdflatex" "main.aux" 1773107048.94201 22239 5965f8733374baeb9476cb314eae6831 "pdflatex"
(generated) (generated)
"main.bbl" "main.bbl"
"main.blg" "main.blg"
(rewritten before read) (rewritten before read)
["pdflatex"] 1773106473.46494 "main.tex" "main.pdf" "main" 1773106474.96491 0 ["pdflatex"] 1773107046.68698 "main.tex" "main.pdf" "main" 1773107049.14649 0
"/Users/split/Library/TinyTeX/texmf-dist/fonts/enc/dvips/base/8r.enc" 1165713224 4850 80dc9bab7f31fb78a000ccfed0e27cab "" "/Users/split/Library/TinyTeX/texmf-dist/fonts/enc/dvips/base/8r.enc" 1165713224 4850 80dc9bab7f31fb78a000ccfed0e27cab ""
"/Users/split/Library/TinyTeX/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm" 1136768653 1408 5937f58aa508ea2cea4901c07d10f5fe "" "/Users/split/Library/TinyTeX/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm" 1136768653 1408 5937f58aa508ea2cea4901c07d10f5fe ""
"/Users/split/Library/TinyTeX/texmf-dist/fonts/tfm/adobe/times/psyro.tfm" 1136768653 1544 23a042a74981a3e4b6ce2e350e390409 "" "/Users/split/Library/TinyTeX/texmf-dist/fonts/tfm/adobe/times/psyro.tfm" 1136768653 1544 23a042a74981a3e4b6ce2e350e390409 ""
@ -239,20 +239,20 @@
"/Users/split/Library/TinyTeX/texmf-var/fonts/map/pdftex/updmap/pdftex.map" 1771879278 94137 fe53532163e1d92c794c09ef981daf8d "" "/Users/split/Library/TinyTeX/texmf-var/fonts/map/pdftex/updmap/pdftex.map" 1771879278 94137 fe53532163e1d92c794c09ef981daf8d ""
"/Users/split/Library/TinyTeX/texmf-var/web2c/pdftex/pdflatex.fmt" 1770868900 2236375 139dae50424001d43c49d2d79a9c607f "" "/Users/split/Library/TinyTeX/texmf-var/web2c/pdftex/pdflatex.fmt" 1770868900 2236375 139dae50424001d43c49d2d79a9c607f ""
"/Users/split/Library/TinyTeX/texmf.cnf" 1770868853 637 edd806fb06a89761a6034e1968af9017 "" "/Users/split/Library/TinyTeX/texmf.cnf" 1770868853 637 edd806fb06a89761a6034e1968af9017 ""
"1-goals-and-outcomes/goals.tex" 1773106456.22497 6449 2997df4b13b90c69ee012b87ddd9cd94 "" "1-goals-and-outcomes/goals.tex" 1773106867.32987 7170 36d8a6065b56159b6538c4deeec20cec ""
"1-goals-and-outcomes/research-statement.tex" 1773105333.1977 4450 070caee751214eaddffa6b3403f8ed43 "" "1-goals-and-outcomes/research-statement.tex" 1773106841.28106 5728 e199dc357f5f0fb9556e5eedcaee0f49 ""
"2-state-of-the-art/state-of-art.tex" 1773105333.19841 12622 1460f7a4c2b48a1a772d8a0f5db216af "" "2-state-of-the-art/state-of-art.tex" 1773106947.01689 14525 3b8c13d63175e6d9fd1a60995e47777f ""
"3-research-approach/approach.tex" 1773105333.19929 35753 93d4c7b608feeba783c33affa59dd220 "" "3-research-approach/approach.tex" 1773106988.29302 36035 28bfba4166bebc2d97137ab44e7cb41c ""
"4-metrics-of-success/metrics.tex" 1773105333.19967 5586 e5fb80ced00bcdc318ffe3861b0064bc "" "4-metrics-of-success/metrics.tex" 1773107008.7714 5967 9d1414599bd374b4166fcce4de6e6644 ""
"5-risks-and-contingencies/risks.tex" 1773105333.20003 10412 17e755aa8451c45198372af7afe3c500 "" "5-risks-and-contingencies/risks.tex" 1773107023.74552 10515 44f5f800e1332517ebfe61e7db38b7cc ""
"6-broader-impacts/impacts.tex" 1773105333.20065 4834 418aae223b778759691eaf9124a5360c "" "6-broader-impacts/impacts.tex" 1773107032.45472 4912 c7ccb2b7aade93b198e985e4832fd6a8 ""
"8-schedule/schedule.tex" 1773105333.20091 4473 8ad96bbf9cedf2ea09298ecbd4e01b83 "" "8-schedule/schedule.tex" 1773107042.40456 4551 57e4fef2d56e8d84227d70745141e7eb ""
"dane_proposal_format.cls" 1770435796.31147 2883 ea175794171aa0291ef71716b2190bf0 "" "dane_proposal_format.cls" 1770435796.31147 2883 ea175794171aa0291ef71716b2190bf0 ""
"main.aux" 1773106474.76109 7231 2769f5164b2ddb0c968502f2788a9df8 "pdflatex" "main.aux" 1773107048.94201 22239 5965f8733374baeb9476cb314eae6831 "pdflatex"
"main.bbl" 1773106474.96361 2919 0ea026a17b15c1ad2ed657bdbf26dfdc "bibtex main" "main.bbl" 1773107049.14524 2919 0ea026a17b15c1ad2ed657bdbf26dfdc "bibtex main"
"main.tex" 1773106452.46565 1379 944a0991d85aa6b5966f2f945e5ef1a1 "" "main.tex" 1773106811.51228 2254 8716b1483d4b9717095f17207a781e0a ""
"main.toc" 1773106474.76365 2129 eb658283ff0c872296846602d3e9dde6 "pdflatex" "main.toc" 1773107048.94477 2130 3335d961966833131187fb817e48a809 "pdflatex"
"todonotes.sty" 1773106013.90863 21404 916e19cbd009b6d289c8194b313d3895 "" "todonotes.sty" 1773106494.99347 21404 916e19cbd009b6d289c8194b313d3895 ""
(generated) (generated)
"main.aux" "main.aux"
"main.log" "main.log"

8
main.fls
View File

@ -464,6 +464,8 @@ INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/tfm/public/cm/cmr10.tfm
INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/vf/adobe/times/zptmcm7m.vf INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/vf/adobe/times/zptmcm7m.vf
INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/tfm/adobe/times/psyro.tfm INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/tfm/adobe/times/psyro.tfm
INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/tfm/public/cm/cmmi10.tfm INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/tfm/public/cm/cmmi10.tfm
INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/vf/adobe/times/ptmri7t.vf
INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/tfm/adobe/times/ptmri8r.tfm
INPUT ./3-research-approach/approach.tex INPUT ./3-research-approach/approach.tex
INPUT ./3-research-approach/approach.tex INPUT ./3-research-approach/approach.tex
INPUT ./3-research-approach/approach.tex INPUT ./3-research-approach/approach.tex
@ -502,7 +504,6 @@ INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/tfm/public/rsfs/rsfs5.tfm
INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/vf/adobe/times/zptmcm7m.vf INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/vf/adobe/times/zptmcm7m.vf
INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/tfm/adobe/times/psyro.tfm INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/tfm/adobe/times/psyro.tfm
INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/tfm/public/cm/cmmi10.tfm INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/tfm/public/cm/cmmi10.tfm
INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/tfm/adobe/times/ptmri8r.tfm
INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/vf/adobe/times/zptmcm7t.vf INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/vf/adobe/times/zptmcm7t.vf
INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm
INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm
@ -522,11 +523,10 @@ INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm
INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm
INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/tfm/public/cm/cmr10.tfm INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/tfm/public/cm/cmr10.tfm
INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/vf/adobe/times/ptmr7t.vf INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/vf/adobe/times/ptmr7t.vf
INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm
INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm
INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/vf/adobe/times/ptmb7t.vf INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/vf/adobe/times/ptmb7t.vf
INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/tfm/adobe/times/ptmb8r.tfm INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/tfm/adobe/times/ptmb8r.tfm
INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/vf/adobe/times/ptmri7t.vf INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm
INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm
INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/vf/adobe/times/zptmcm7t.vf INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/vf/adobe/times/zptmcm7t.vf
INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm
INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm INPUT /Users/split/Library/TinyTeX/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm

209
main.log
View File

@ -1,4 +1,4 @@
This is pdfTeX, Version 3.141592653-2.6-1.40.28 (TeX Live 2025) (preloaded format=pdflatex 2026.2.12) 9 MAR 2026 21:34 This is pdfTeX, Version 3.141592653-2.6-1.40.28 (TeX Live 2025) (preloaded format=pdflatex 2026.2.12) 9 MAR 2026 21:44
entering extended mode entering extended mode
restricted \write18 enabled. restricted \write18 enabled.
%&-line parsing enabled. %&-line parsing enabled.
@ -774,7 +774,7 @@ Package: todonotes 2024/01/05 v1.1.7 Todonotes source and documentation.
Package: todonotes 2024/01/05 Package: todonotes 2024/01/05
\c@@todonotes@numberoftodonotes=\count403 \c@@todonotes@numberoftodonotes=\count403
) )
LaTeX Font Info: Trying to load font information for OT1+ptm on input line 18. LaTeX Font Info: Trying to load font information for OT1+ptm on input line 43.
(/Users/split/Library/TinyTeX/texmf-dist/tex/latex/psnfss/ot1ptm.fd (/Users/split/Library/TinyTeX/texmf-dist/tex/latex/psnfss/ot1ptm.fd
File: ot1ptm.fd 2001/06/04 font definitions for OT1/ptm. File: ot1ptm.fd 2001/06/04 font definitions for OT1/ptm.
) (/Users/split/Library/TinyTeX/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def ) (/Users/split/Library/TinyTeX/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def
@ -783,20 +783,20 @@ File: l3backend-pdftex.def 2025-10-09 L3 backend support: PDF output (pdfTeX)
) (./main.aux) ) (./main.aux)
\openout1 = `main.aux'. \openout1 = `main.aux'.
LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 18. LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 43.
LaTeX Font Info: ... okay on input line 18. LaTeX Font Info: ... okay on input line 43.
LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 18. LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 43.
LaTeX Font Info: ... okay on input line 18. LaTeX Font Info: ... okay on input line 43.
LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 18. LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 43.
LaTeX Font Info: ... okay on input line 18. LaTeX Font Info: ... okay on input line 43.
LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 18. LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 43.
LaTeX Font Info: ... okay on input line 18. LaTeX Font Info: ... okay on input line 43.
LaTeX Font Info: Checking defaults for TS1/cmr/m/n on input line 18. LaTeX Font Info: Checking defaults for TS1/cmr/m/n on input line 43.
LaTeX Font Info: ... okay on input line 18. LaTeX Font Info: ... okay on input line 43.
LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 18. LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 43.
LaTeX Font Info: ... okay on input line 18. LaTeX Font Info: ... okay on input line 43.
LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 18. LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 43.
LaTeX Font Info: ... okay on input line 18. LaTeX Font Info: ... okay on input line 43.
*geometry* driver: auto-detecting *geometry* driver: auto-detecting
*geometry* detected driver: pdftex *geometry* detected driver: pdftex
@ -810,7 +810,7 @@ LaTeX Font Info: ... okay on input line 18.
* v-part:(T,H,B)=(72.26999pt, 650.43001pt, 72.26999pt) * v-part:(T,H,B)=(72.26999pt, 650.43001pt, 72.26999pt)
* \paperwidth=614.295pt * \paperwidth=614.295pt
* \paperheight=794.96999pt * \paperheight=794.96999pt
* \textwidth=469.75502pt * \textwidth=397.48499pt
* \textheight=650.43001pt * \textheight=650.43001pt
* \oddsidemargin=0.0pt * \oddsidemargin=0.0pt
* \evensidemargin=0.0pt * \evensidemargin=0.0pt
@ -846,34 +846,64 @@ Package: pdflscape-nometadata 2025-06-23 v0.14 Display of landscape pages in PDF
Package pdflscape Info: Auto-detected driver: pdftex on input line 81. Package pdflscape Info: Auto-detected driver: pdftex on input line 81.
)) ))
\c@lstlisting=\count405 \c@lstlisting=\count405
LaTeX Font Info: Trying to load font information for OT1+ztmcm on input line 21. LaTeX Font Info: Trying to load font information for OT1+ztmcm on input line 46.
(/Users/split/Library/TinyTeX/texmf-dist/tex/latex/psnfss/ot1ztmcm.fd (/Users/split/Library/TinyTeX/texmf-dist/tex/latex/psnfss/ot1ztmcm.fd
File: ot1ztmcm.fd 2000/01/03 Fontinst v1.801 font definitions for OT1/ztmcm. File: ot1ztmcm.fd 2000/01/03 Fontinst v1.801 font definitions for OT1/ztmcm.
) )
LaTeX Font Info: Trying to load font information for OML+ztmcm on input line 21. LaTeX Font Info: Trying to load font information for OML+ztmcm on input line 46.
(/Users/split/Library/TinyTeX/texmf-dist/tex/latex/psnfss/omlztmcm.fd (/Users/split/Library/TinyTeX/texmf-dist/tex/latex/psnfss/omlztmcm.fd
File: omlztmcm.fd 2000/01/03 Fontinst v1.801 font definitions for OML/ztmcm. File: omlztmcm.fd 2000/01/03 Fontinst v1.801 font definitions for OML/ztmcm.
) )
LaTeX Font Info: Trying to load font information for OMS+ztmcm on input line 21. LaTeX Font Info: Trying to load font information for OMS+ztmcm on input line 46.
(/Users/split/Library/TinyTeX/texmf-dist/tex/latex/psnfss/omsztmcm.fd (/Users/split/Library/TinyTeX/texmf-dist/tex/latex/psnfss/omsztmcm.fd
File: omsztmcm.fd 2000/01/03 Fontinst v1.801 font definitions for OMS/ztmcm. File: omsztmcm.fd 2000/01/03 Fontinst v1.801 font definitions for OMS/ztmcm.
) )
LaTeX Font Info: Trying to load font information for OMX+ztmcm on input line 21. LaTeX Font Info: Trying to load font information for OMX+ztmcm on input line 46.
(/Users/split/Library/TinyTeX/texmf-dist/tex/latex/psnfss/omxztmcm.fd (/Users/split/Library/TinyTeX/texmf-dist/tex/latex/psnfss/omxztmcm.fd
File: omxztmcm.fd 2000/01/03 Fontinst v1.801 font definitions for OMX/ztmcm. File: omxztmcm.fd 2000/01/03 Fontinst v1.801 font definitions for OMX/ztmcm.
) )
LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <14.4> not available LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <14.4> not available
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 21. (Font) Font shape `OT1/ptm/b/n' tried instead on input line 46.
LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <10.95> not available LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <10.95> not available
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 21. (Font) Font shape `OT1/ptm/b/n' tried instead on input line 46.
LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <8> not available LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <8> not available
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 21. (Font) Font shape `OT1/ptm/b/n' tried instead on input line 46.
LaTeX Font Info: Trying to load font information for U+rsfs on input line 21. LaTeX Font Info: Trying to load font information for U+rsfs on input line 46.
(/Users/split/Library/TinyTeX/texmf-dist/tex/latex/jknapltx/ursfs.fd (/Users/split/Library/TinyTeX/texmf-dist/tex/latex/jknapltx/ursfs.fd
File: ursfs.fd 1998/03/24 rsfs font definition file (jk) File: ursfs.fd 1998/03/24 rsfs font definition file (jk)
) [1 ) [1
{/Users/split/Library/TinyTeX/texmf-var/fonts/map/pdftex/updmap/pdftex.map}{/Users/split/Library/TinyTeX/texmf-dist/fonts/enc/dvips/base/8r.enc}] (./1-goals-and-outcomes/research-statement.tex) [1] (./main.toc {/Users/split/Library/TinyTeX/texmf-var/fonts/map/pdftex/updmap/pdftex.map}{/Users/split/Library/TinyTeX/texmf-dist/fonts/enc/dvips/base/8r.enc}] (./1-goals-and-outcomes/research-statement.tex
LaTeX Warning: Marginpar on page i moved.
LaTeX Warning: Marginpar on page i moved.
LaTeX Warning: Marginpar on page i moved.
LaTeX Warning: Marginpar on page i moved.
LaTeX Warning: Marginpar on page i moved.
LaTeX Warning: Marginpar on page i moved.
LaTeX Warning: Marginpar on page i moved.
Overfull \hbox (7.2216pt too wide) in paragraph at lines 67--77
\OT1/ptm/m/n/12 mode-switching con-trollers from reg-u-la-tory pro-ce-dures with lit-tle for-mal meth-
[]
LaTeX Warning: Marginpar on page i moved.
[1]) [2] (./main.toc
LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <12> not available LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <12> not available
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 4. (Font) Font shape `OT1/ptm/b/n' tried instead on input line 4.
LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <9> not available LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <9> not available
@ -884,11 +914,45 @@ LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <7> not available
\tf@toc=\write4 \tf@toc=\write4
\openout4 = `main.toc'. \openout4 = `main.toc'.
[2] (./1-goals-and-outcomes/goals.tex [3] (./1-goals-and-outcomes/goals.tex
LaTeX Warning: Marginpar on page 1 moved. LaTeX Warning: Marginpar on page 1 moved.
[1]) [2] (./2-state-of-the-art/state-of-art.tex [3] [4] [5]) [6] (./3-research-approach/approach.tex
LaTeX Warning: Marginpar on page 1 moved.
LaTeX Warning: Marginpar on page 1 moved.
LaTeX Warning: Marginpar on page 1 moved.
LaTeX Warning: Marginpar on page 1 moved.
LaTeX Warning: Marginpar on page 1 moved.
[1])
LaTeX Warning: Marginpar on page 2 moved.
[2] (./2-state-of-the-art/state-of-art.tex
LaTeX Warning: Marginpar on page 3 moved.
[3]
LaTeX Warning: Marginpar on page 4 moved.
LaTeX Warning: Marginpar on page 4 moved.
[4] [5]
LaTeX Warning: Marginpar on page 6 moved.
) [6] (./3-research-approach/approach.tex
LaTeX Warning: Citation `HANDBOOK ON HYBRID SYSTEMS' on page 7 undefined on input line 50. LaTeX Warning: Citation `HANDBOOK ON HYBRID SYSTEMS' on page 7 undefined on input line 50.
@ -900,18 +964,73 @@ LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <6> not available
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 103. (Font) Font shape `OT1/ptm/b/n' tried instead on input line 103.
LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <5> not available LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <5> not available
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 109. (Font) Font shape `OT1/ptm/b/n' tried instead on input line 109.
[8] [9] [10]
LaTeX Warning: Citation `MANYUS THESIS' on page 11 undefined on input line 383. Overfull \hbox (10.87595pt too wide) in paragraph at lines 128--134
[][]
[11] [12] [13]) [14] (./4-metrics-of-success/metrics.tex [15]) [16] (./5-risks-and-contingencies/risks.tex [17] [18]) [19] (./6-broader-impacts/impacts.tex) [20] [21] (./8-schedule/schedule.tex
Missing character: There is no , in font nullfont!
) (./main.bbl [22]
Underfull \hbox (badness 10000) in paragraph at lines 32--33
\OT1/cmtt/m/n/12 nuclear . org / information -[] library / safety -[] and -[] security / safety -[] of -[]
[] []
[23]) [24] (./main.aux) [8]
Overfull \hbox (68.04898pt too wide) in paragraph at lines 203--207
[][]
[]
[9] [10] [11]
LaTeX Warning: Citation `MANYUS THESIS' on page 12 undefined on input line 383.
[12] [13] [14] [15]) [16] (./4-metrics-of-success/metrics.tex
Overfull \hbox (22.73904pt too wide) in paragraph at lines 12--24
\OT1/ptm/m/n/12 plic-itly mea-sure the gap be-tween aca-demic proof-of-concept and prac-ti-cal deployment---
[]
[17]) [18] (./5-risks-and-contingencies/risks.tex [19]
Overfull \hbox (6.11617pt too wide) in paragraph at lines 76--90
[]\OT1/ptm/m/n/12 The pri-mary con-tin-gency for in-ter-face com-plex-ity is re-strict-ing con-tin-u-ous modes
[]
[20]) [21] [22] (./6-broader-impacts/impacts.tex
Overfull \hbox (2.22pt too wide) in paragraph at lines 3--10
\OT1/ptm/m/n/12 dat-a-cen-ters re-quir-ing hun-dreds of megawatts of con-tin-u-ous power. De-ploy-ing SMRs
[]
[23]) [24] (./8-schedule/schedule.tex
Missing character: There is no , in font nullfont!
Overfull \hbox (39.7858pt too wide) in paragraph at lines 71--72
[][]
[]
) (./main.bbl [25]
Underfull \hbox (badness 1571) in paragraph at lines 23--24
[]\OT1/ptm/m/n/12 U.S. Nu-clear Reg-u-la-tory Com-mis-sion, ``Part 55|Op-er-a-tors' Li-censes.''
[]
Underfull \hbox (badness 10000) in paragraph at lines 23--24
\OT1/cmtt/m/n/12 https : / / www . nrc . gov / reading -[] rm / doc -[] collections / cfr / part055 /
[]
Underfull \hbox (badness 10000) in paragraph at lines 26--27
\OT1/cmtt/m/n/12 https : / / www . nrc . gov / reading -[] rm / doc -[] collections / cfr / part050 /
[]
Underfull \hbox (badness 10000) in paragraph at lines 32--33
[]\OT1/ptm/m/n/12 World Nu-clear As-so-ci-a-tion, ``Safety of nu-clear power re-ac-tors.''
[]
Underfull \hbox (badness 10000) in paragraph at lines 32--33
\OT1/cmtt/m/n/12 https : / / www . world -[] nuclear . org / information -[] library / safety -[]
[]
Underfull \hbox (badness 10000) in paragraph at lines 32--33
\OT1/cmtt/m/n/12 and -[] security / safety -[] of -[] plants / safety -[] of -[] nuclear -[] power -[]
[]
[26]) [27] (./main.aux)
*********** ***********
LaTeX2e <2025-11-01> LaTeX2e <2025-11-01>
L3 programming layer <2026-01-19> L3 programming layer <2026-01-19>
@ -925,18 +1044,18 @@ LaTeX Warning: Label(s) may have changed. Rerun to get cross-references right.
) )
Here is how much of TeX's memory you used: Here is how much of TeX's memory you used:
26246 strings out of 469514 26575 strings out of 469514
552438 string characters out of 5469022 560233 string characters out of 5469022
984190 words of memory out of 5000000 1031670 words of memory out of 5000000
54290 multiletter control sequences out of 15000+600000 54619 multiletter control sequences out of 15000+600000
683164 words of font info for 159 fonts, out of 8000000 for 9000 683164 words of font info for 159 fonts, out of 8000000 for 9000
14 hyphenation exceptions out of 8191 14 hyphenation exceptions out of 8191
110i,9n,108p,1062b,960s stack positions out of 10000i,1000n,20000p,200000b,200000s 110i,9n,108p,1062b,1083s stack positions out of 10000i,1000n,20000p,200000b,200000s
</Users/split/Library/TinyTeX/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb></Users/split/Library/TinyTeX/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></Users/split/Library/TinyTeX/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb></Users/split/Library/TinyTeX/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt12.pfb></Users/split/Library/TinyTeX/texmf-dist/fonts/type1/public/amsfonts/symbols/msbm10.pfb></Users/split/Library/TinyTeX/texmf-dist/fonts/type1/public/rsfs/rsfs10.pfb></Users/split/Library/TinyTeX/texmf-dist/fonts/type1/urw/symbol/usyr.pfb></Users/split/Library/TinyTeX/texmf-dist/fonts/type1/urw/symbol/usyr.pfb></Users/split/Library/TinyTeX/texmf-dist/fonts/type1/urw/times/utmb8a.pfb></Users/split/Library/TinyTeX/texmf-dist/fonts/type1/urw/times/utmbi8a.pfb></Users/split/Library/TinyTeX/texmf-dist/fonts/type1/urw/times/utmr8a.pfb></Users/split/Library/TinyTeX/texmf-dist/fonts/type1/urw/times/utmri8a.pfb> </Users/split/Library/TinyTeX/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb></Users/split/Library/TinyTeX/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></Users/split/Library/TinyTeX/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb></Users/split/Library/TinyTeX/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt12.pfb></Users/split/Library/TinyTeX/texmf-dist/fonts/type1/public/amsfonts/symbols/msbm10.pfb></Users/split/Library/TinyTeX/texmf-dist/fonts/type1/public/rsfs/rsfs10.pfb></Users/split/Library/TinyTeX/texmf-dist/fonts/type1/urw/symbol/usyr.pfb></Users/split/Library/TinyTeX/texmf-dist/fonts/type1/urw/symbol/usyr.pfb></Users/split/Library/TinyTeX/texmf-dist/fonts/type1/urw/times/utmb8a.pfb></Users/split/Library/TinyTeX/texmf-dist/fonts/type1/urw/times/utmbi8a.pfb></Users/split/Library/TinyTeX/texmf-dist/fonts/type1/urw/times/utmr8a.pfb></Users/split/Library/TinyTeX/texmf-dist/fonts/type1/urw/times/utmri8a.pfb>
Output written on main.pdf (27 pages, 190748 bytes). Output written on main.pdf (31 pages, 206928 bytes).
PDF statistics: PDF statistics:
180 PDF objects out of 1000 (max. 8388607) 193 PDF objects out of 1000 (max. 8388607)
109 compressed objects within 2 object streams 118 compressed objects within 2 object streams
0 named destinations out of 1000 (max. 500000) 0 named destinations out of 1000 (max. 500000)
109 words of extra memory for PDF output out of 10000 (max. 10000000) 109 words of extra memory for PDF output out of 10000 (max. 10000000)

BIN
main.pdf
View File

Binary file not shown.

33
main.tex
View File

@ -8,11 +8,36 @@
\usepackage{pdfpages} % For including PDF files \usepackage{pdfpages} % For including PDF files
% === SPLIT'S EDITING COMMENTS === % === SPLIT'S EDITING COMMENTS ===
% Remove this block when done editing % Set to 1 for edit mode (wider margins, visible comments)
% Set to 0 for final mode (normal margins, comments hidden)
\newcommand{\editmode}{1}
\ifnum\editmode=1
% Edit mode: load todonotes, adjust margins
\usepackage[colorinlistoftodos,prependcaption,textsize=small]{todonotes} \usepackage[colorinlistoftodos,prependcaption,textsize=small]{todonotes}
\newcommand{\splitnote}[1]{\todo[color=green!40,author=Split]{#1}} \setlength{\marginparwidth}{2.5cm}
\newcommand{\splitinline}[1]{\todo[inline,color=green!40,author=Split]{#1}} \setlength{\oddsidemargin}{0in}
\setlength{\marginparwidth}{2.5cm} % Make room for margin notes \setlength{\textwidth}{5.5in} % Narrower text = more margin space
% Color-coded comment commands
% Green: General observations, "nice work", vibes
\newcommand{\splitnote}[1]{\todo[color=green!40]{#1}}
% Yellow: "Hey, check this out maybe?" - suggestions
\newcommand{\splitsuggest}[1]{\todo[color=yellow!60]{#1}}
% Orange: "This needs some polish" - should fix
\newcommand{\splitpolish}[1]{\todo[color=orange!50]{#1}}
% Red: "Fix this. Not acceptable." - must fix
\newcommand{\splitfix}[1]{\todo[color=red!40]{#1}}
% Inline versions
\newcommand{\splitinline}[1]{\todo[inline,color=green!40]{#1}}
\else
% Final mode: no comments, normal margins
\newcommand{\splitnote}[1]{}
\newcommand{\splitsuggest}[1]{}
\newcommand{\splitpolish}[1]{}
\newcommand{\splitfix}[1]{}
\newcommand{\splitinline}[1]{}
\fi
% ================================ % ================================
\begin{document} \begin{document}

36
main.toc
View File

@ -1,27 +1,27 @@
\contentsline {section}{Contents}{ii}{}% \contentsline {section}{Contents}{iii}{}%
\contentsline {section}{\numberline {1}Goals and Outcomes}{1}{}% \contentsline {section}{\numberline {1}Goals and Outcomes}{1}{}%
\contentsline {section}{\numberline {2}State of the Art and Limits of Current Practice}{3}{}% \contentsline {section}{\numberline {2}State of the Art and Limits of Current Practice}{3}{}%
\contentsline {subsection}{\numberline {2.1}Current Reactor Procedures and Operation}{3}{}% \contentsline {subsection}{\numberline {2.1}Current Reactor Procedures and Operation}{3}{}%
\contentsline {subsection}{\numberline {2.2}Human Factors in Nuclear Accidents}{3}{}% \contentsline {subsection}{\numberline {2.2}Human Factors in Nuclear Accidents}{4}{}%
\contentsline {subsection}{\numberline {2.3}Formal Methods}{4}{}% \contentsline {subsection}{\numberline {2.3}Formal Methods}{4}{}%
\contentsline {subsubsection}{\numberline {2.3.1}HARDENS}{4}{}% \contentsline {subsubsection}{\numberline {2.3.1}HARDENS}{4}{}%
\contentsline {subsubsection}{\numberline {2.3.2}Sequent Calculus and Differential Dynamic Logic}{5}{}% \contentsline {subsubsection}{\numberline {2.3.2}Sequent Calculus and Differential Dynamic Logic}{6}{}%
\contentsline {section}{\numberline {3}Research Approach}{7}{}% \contentsline {section}{\numberline {3}Research Approach}{7}{}%
\contentsline {subsection}{\numberline {3.1}System Requirements, Specifications, and Discrete Controllers}{8}{}% \contentsline {subsection}{\numberline {3.1}System Requirements, Specifications, and Discrete Controllers}{8}{}%
\contentsline {subsection}{\numberline {3.2}Continuous Control Modes}{11}{}% \contentsline {subsection}{\numberline {3.2}Continuous Control Modes}{11}{}%
\contentsline {subsubsection}{\numberline {3.2.1}Transitory Modes}{12}{}% \contentsline {subsubsection}{\numberline {3.2.1}Transitory Modes}{12}{}%
\contentsline {subsubsection}{\numberline {3.2.2}Stabilizing Modes}{12}{}% \contentsline {subsubsection}{\numberline {3.2.2}Stabilizing Modes}{13}{}%
\contentsline {subsubsection}{\numberline {3.2.3}Expulsory Modes}{13}{}% \contentsline {subsubsection}{\numberline {3.2.3}Expulsory Modes}{14}{}%
\contentsline {subsection}{\numberline {3.3}Industrial Implementation}{14}{}% \contentsline {subsection}{\numberline {3.3}Industrial Implementation}{15}{}%
\contentsline {section}{\numberline {4}Metrics for Success}{15}{}% \contentsline {section}{\numberline {4}Metrics for Success}{17}{}%
\contentsline {paragraph}{TRL 3 \textit {Critical Function and Proof of Concept}}{15}{}% \contentsline {paragraph}{TRL 3 \textit {Critical Function and Proof of Concept}}{17}{}%
\contentsline {paragraph}{TRL 4 \textit {Laboratory Testing of Integrated Components}}{15}{}% \contentsline {paragraph}{TRL 4 \textit {Laboratory Testing of Integrated Components}}{17}{}%
\contentsline {paragraph}{TRL 5 \textit {Laboratory Testing in Relevant Environment}}{15}{}% \contentsline {paragraph}{TRL 5 \textit {Laboratory Testing in Relevant Environment}}{18}{}%
\contentsline {section}{\numberline {5}Risks and Contingencies}{17}{}% \contentsline {section}{\numberline {5}Risks and Contingencies}{19}{}%
\contentsline {subsection}{\numberline {5.1}Computational Tractability of Synthesis}{17}{}% \contentsline {subsection}{\numberline {5.1}Computational Tractability of Synthesis}{19}{}%
\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{17}{}% \contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{19}{}%
\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{18}{}% \contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{21}{}%
\contentsline {section}{\numberline {6}Broader Impacts}{20}{}% \contentsline {section}{\numberline {6}Broader Impacts}{23}{}%
\contentsline {section}{\numberline {7}Schedule, Milestones, and Deliverables}{22}{}% \contentsline {section}{\numberline {7}Schedule, Milestones, and Deliverables}{25}{}%
\contentsline {subsection}{\numberline {7.1}Milestones and Deliverables}{22}{}% \contentsline {subsection}{\numberline {7.1}Milestones and Deliverables}{25}{}%
\contentsline {section}{References}{23}{}% \contentsline {section}{References}{26}{}%