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

first commit

Browse Source
This commit is contained in:
Dane Sabo 2026-02-06 20:23:52 -05:00
commit c5e7784810
30 changed files with 4408 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

BIN
.DS_Store vendored Normal file
View File

Binary file not shown.

82
1-goals-and-outcomes/research_statement_v1.tex Normal file
View File

@ -0,0 +1,82 @@
% GOAL PARAGRAPH
The goal of this research is to develop a methodology for creating autonomous
control systems with event-driven control laws that have guarantees of safe and
correct behavior.
% INTRODUCTORY PARAGRAPH Hook
Nuclear power relies on extensively trained operators who follow detailed
written procedures to manage reactor control. Based on these procedures and
operators' interpretation of plant conditions, operators make critical decisions
about when to switch between control objectives.
% Gap
But, reliance on human operators has created an economic challenge for
next-generation nuclear power plants. Small modular reactors face significantly
higher per-megawatt staffing costs than conventional plants. Autonomous control
systems are needed that can safely manage complex operational sequences with the
same assurance as human-operated systems, but without constant supervision.
% APPROACH PARAGRAPH Solution
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.
% Rationale
Hybrid systems use discrete logic to switch between continuous control modes,
similar to how operators change control strategies. Existing formal methods
generate provably correct switching logic but cannot handle continuous dynamics
during transitions, while traditional control theory verifies continuous
behavior but lacks tools for proving discrete switching correctness.
% Hypothesis and Technical Approach
We will bridge this gap through a three-stage methodology. First, we will
translate written operating procedures into temporal logic specifications using
NASA's Formal Requirements Elicitation Tool (FRET), which structures
requirements into scope, condition, component, timing, and response elements.
This structured approach enables realizability checking to identify conflicts
and ambiguities in procedures before implementation. Second, we will synthesize
discrete mode switching logic using reactive synthesis
to generate deterministic automata that are provably
correct by construction. Third, we will develop continuous
controllers for each discrete mode using standard control theory and
reachability analysis. We will classify continuous modes based on their
transition objectives, and then employ assume-guarantee contracts and barrier
certificates to prove that mode transitions occur safely and as defined by the
deterministic automata. This compositional approach enables local verification
of continuous modes without requiring global trajectory analysis across the
entire hybrid system. We will demonstrate this on an Emerson Ovation control system.
% Pay-off
This approach will demonstrate autonomous control can be used for complex
nuclear power operations while maintaining safety guarantees.
% OUTCOMES PARAGRAPHS
If this research is successful, we will be able to do the following:
\begin{enumerate}
% OUTCOME 1 Title
\item \textit{Synthesize written procedures into verified control logic.}
% Strategy
We will develop a methodology for converting written operating procedures
into formal specifications. These specifications will be synthesized into
discrete control logic using reactive synthesis tools.
% Outcome
Control engineers will be able to generate mode-switching controllers from
regulatory procedures with little formal methods expertise, reducing
barriers to high-assurance control systems.
% OUTCOME 2 Title
\item \textit{Verify continuous control behavior across mode transitions. }
% Strategy
We will develop methods using reachability analysis to ensure continuous control modes
satisfy discrete transition requirements.
% Outcome
Engineers will be able to design continuous controllers using standard
practices while ensuring system correctness and proving mode transitions
occur safely at the right times.
% OUTCOME 3 Title
\item \textit{Demonstrate autonomous reactor startup control with safety
guarantees. }
% Strategy
We will implement this methodology on a small modular reactor simulation
using industry-standard control hardware. % Outcome
Control engineers will be able to implement high-assurance autonomous
controls on industrial platforms they already use, enabling users to
achieve autonomy without retraining costs or developing new equipment.
\end{enumerate}

114
1-goals-and-outcomes/v1.tex Normal file
View File

@ -0,0 +1,114 @@
\section{Goals and Outcomes}
% GOAL PARAGRAPH
The goal of this research is to develop a methodology for creating autonomous
hybrid control systems with mathematical guarantees of safe and correct
behavior.
% INTRODUCTORY PARAGRAPH Hook
Nuclear power plants require the highest levels of control system reliability,
where failures can result in significant economic losses, service interruptions,
or radiological release.
% Known information
Currently, nuclear plant operations rely on extensively trained human operators
who follow detailed written procedures and strict regulatory requirements to
manage reactor control. These operators make critical decisions about when to
switch between different control modes based on their interpretation of plant
conditions and procedural guidance.
% Gap
This reliance on human operators prevents autonomous control capabilities and
creates a fundamental economic challenge for next-generation reactor designs.
Small modular reactors, in particular, face per-megawatt staffing costs far
exceeding those of conventional plants and threaten their economic viability.
% Critical Need
What is needed is a method to create autonomous control systems that safely
manage complex operational sequences with the same assurance as human-operated
systems, but without constant human supervision.
% APPROACH PARAGRAPH Solution
To address this need, we will combine formal methods with control theory to
build hybrid control systems that are correct by construction.
% Rationale
Hybrid systems use discrete logic to switch between continuous control modes,
mirroring how operators change control strategies. Existing formal methods can
generate provably correct switching logic from written requirements, but they
cannot handle the continuous dynamics that occur during transitions between
modes. Meanwhile, traditional control theory can verify continuous behavior but
lacks tools for proving correctness of discrete switching decisions.
% Hypothesis
By synthesizing discrete mode transitions directly from written operating
procedures and verifying continuous behavior between transitions, we can create
hybrid control systems with end-to-end correctness guarantees. If existing
procedures can be formalized into logical specifications and continuous dynamics
verified against transition requirements, then autonomous controllers can be
built that are provably free from design defects.
% Pay-off
This approach will enable autonomous control in nuclear power plants while
maintaining the high safety standards required by the industry.
% Qualifications
This work is conducted within the University of Pittsburgh Cyber Energy Center,
which provides access to industry collaboration and Emerson control hardware,
ensuring that developed solutions align with practical implementation
requirements.
% OUTCOMES PARAGRAPHS
If this research is successful, we will be able to do the following:
\begin{enumerate}
% OUTCOME 1 Title
\item \textbf{Translate written procedures into verified control logic.}
% Strategy
We will develop a methodology for converting existing written operating
procedures into formal specifications that can be automatically synthesized
into discrete control logic. This process will use structured intermediate
representations to bridge natural language procedures and mathematical
logic.
% Outcome
Control system engineers will generate verified mode-switching controllers
directly from regulatory procedures without formal methods expertise,
lowering the barrier to high-assurance control systems.
% OUTCOME 2 Title
\item \textbf{Verify continuous control behavior across mode transitions.}
% Strategy
We will establish methods for analyzing continuous control modes to ensure
they satisfy discrete transition requirements. Using classical control
theory for linear systems and reachability analysis for nonlinear dynamics,
we will verify that each continuous mode safely reaches its intended
transitions.
Engineers will design continuous controllers using standard practices while
iterating to ensure broader system correctness, proving that mode
transitions occur safely and at the correct times.
% OUTCOME 3 Title
\item \textbf{Demonstrate autonomous reactor startup control with safety
guarantees.}
% Strategy
We will apply this methodology to develop an autonomous controller for
nuclear reactor startup procedures, implementing it on a small modular
reactor simulation using industry-standard control hardware. This
demonstration will prove correctness across multiple coordinated control
modes from cold shutdown through criticality to power operation.
% Outcome
We will demonstrate that autonomous hybrid control can be realized in the
nuclear industry with current equipment, establishing a path toward reduced
operator staffing while maintaining safety.
\end{enumerate}
% IMPACT PARAGRAPH Innovation
The innovation in this work is unifying discrete synthesis with continuous
verification to enable end-to-end correctness guarantees for hybrid systems.
% Outcome Impact
If successful, control engineers will create autonomous controllers from
existing procedures with mathematical proof of correct behavior. High-assurance
autonomous control will become practical for safety-critical applications.
% Impact/Pay-off
This capability is essential for the economic viability of next-generation
nuclear power. Small modular reactors offer a promising solution to growing
energy demands, but their success depends on reducing per-megawatt operating
costs through increased autonomy. This research will provide the tools to
achieve that autonomy while maintaining the exceptional safety record the
nuclear industry requires.

138
2-state-of-the-art/outline.md Normal file
View File

@ -0,0 +1,138 @@
# Outline of State of the Art
## Writing is thinking, and this is like journaling
This research is really about using techniques that we
already have to make hybrid systems that from the jump are
provably adherent to requirements and in general that we can
say what they're gonna do fo sho. Does that make any sense?
The critical technologies to do this are as follows, in no
particular order: discrete system theory and reactive
synthesis, temporal logics, reachability for hybrid systems.
Things that are adjacent to what I'm doing but aren't what
I'm doing include stuff by Platzer and all the differential
dynamic logic stuff. His stuff looks like another way of
conquering this problem but adds a whole lot of complexity
and makes synthesis ambiguous. Great at checking, but what
does that mean for designing?
I feel like I should get more sources on designing hybrid
systems. I think there are some books out there about this
maybe.
----
**Outline**
----
## 1. Hybrid Control Systems Foundations
- **Classical hybrid systems theory** (Branicky, Liberzon,
Morse - switching systems)
- **Hybrid automata and modeling** (Henzinger, Alur, Dill)
- **Stability analysis for switching systems** (Shorten,
Narendra, Lin & Antsaklis)
**Key points to include:**
- Definition of hybrid systems and why they're needed for
complex control
- Challenges in stability analysis when switching between
controllers
- Gap between individual mode stability and overall system
stability
- Motivate why traditional control theory alone is
insufficient
## 2. Discrete Controller Synthesis
- **Reactive synthesis from temporal logic** (Pnueli, Bloem,
Ehlers)
- **Tools like Strix, TuLiP, SLUGS** - emphasize their
discrete-only assumptions
- **LTL/GR(1) synthesis** and why these assume instantaneous
transitions
**Key points to include:**
- Power of temporal logic for specifying complex behaviors
- Success of reactive synthesis in discrete domains
- Correctness-by-construction guarantees from synthesis
tools
- Critical limitation: assumption of instantaneous state
changes
- Why this breaks down for physical systems with continuous
dynamics
## 3. Continuous System Verification
- **Reachability analysis** (Girard, Le Guernic, Althoff -
especially for nonlinear systems)
- **Linear system verification** (Boyd, Dullerud - classical
control meets verification)
- **Set-based methods** (Mitchell, Tomlin for
Hamilton-Jacobi reachability)
**Key points to include:**
- Mature tools for analyzing continuous dynamics
- Reachability as the fundamental verification problem
- Computational challenges for nonlinear systems
- Gap: these are analysis tools, not synthesis tools
- They tell you if a controller works, but don't help design
it
## 4. Existing Hybrid Verification Approaches
- **Platzer's differential dynamic logic** (as you noted -
good for verification, unclear for synthesis)
- **SpaceEx, Flow*, dReach** - model checking tools that
don't synthesize
- **Contract-based design** (Benveniste,
Sangiovanni-Vincentelli)
**Key points to include:**
- Current approaches focus on verification after design
- Platzer's dL: powerful for proving correctness, but
synthesis unclear
- Model checking tools require pre-designed controllers
- Contract-based approaches: compositional but still
verification-focused
- Missing: unified synthesis framework that handles both
discrete and continuous
## 5. The Gap You're Filling
- **Why discrete synthesis + continuous verification hasn't
been unified**
- **Challenges with non-instantaneous transitions**
- **The synthesis vs. verification divide**
**Key points to include:**
- Fundamental mismatch: discrete synthesis assumes instant
transitions
- Physical reality: transitions take time and follow
continuous trajectories
- Current workflow: synthesize discrete, design continuous,
then verify
- Your contribution: unified framework for
correct-by-construction hybrid synthesis
- Nuclear startup as ideal testbed: well-defined continuous
dynamics + explicit procedural requirements
## Key Sources to Hunt Down
**Foundational hybrid systems:**
- Branicky's "Multiple Lyapunov functions and other analysis
tools"
- Liberzon's "Switching in Systems and Control"
- Antsaklis & Koutsoukos survey papers
**Reactive synthesis:**
- Ehlers & Topcu on GR(1) synthesis
- Recent Strix papers (Meyer, Sickert, Luttenberger)
- Wongpiromsarn's work on TuLiP
**Hybrid verification:**
- Althoff's reachability analysis work
- Girard's papers on abstraction-based verification
- Any recent survey on hybrid system verification tools
**Nuclear/critical systems control:**
- Look for papers on autonomous nuclear plant operation
- Regulatory papers on control system requirements (might be
more engineering sources)

165
2-state-of-the-art/v1.tex Normal file
View File

@ -0,0 +1,165 @@
\section{State of the Art and Limits of Current Practice}
The principal aim of this research is to create autonomous reactor control
systems that are tractably safe. To understand what is being automated, we must
first understand how nuclear reactors are operated today. This section examines
reactor operators and the operating procedures we aim to leverage, then
investigates limitations of human-based operation, and concludes with current
formal methods approaches to reactor control systems.
\subsection{Current Reactor Procedures and Operation}
Nuclear plant procedures exist in a hierarchy: normal operating procedures for
routine operations, abnormal operating procedures for off-normal conditions,
Emergency Operating Procedures (EOPs) for design-basis accidents, Severe
Accident Management Guidelines (SAMGs) for beyond-design-basis events, and
Extensive Damage Mitigation Guidelines (EDMGs) for catastrophic damage
scenarios. These procedures must comply with 10 CFR 50.34(b)(6)(ii) and are
developed using guidance from NUREG-0900~\cite{NUREG-0899, 10CFR50.34}, but their
development relies fundamentally on expert judgment and simulator validation
rather than formal verification. Procedures undergo technical evaluation,
simulator validation testing, and biennial review as part of operator
requalification under 10 CFR 55.59~\cite{10CFR55.59}. Despite this rigor,
procedures fundamentally lack formal verification of key safety properties. No
mathematical proof exists that procedures cover all possible plant states, that
required actions can be completed within available timeframes, or that
transitions between procedure sets maintain safety invariants.
\textbf{LIMITATION:} \textit{Procedures lack formal verification of correctness
and completeness.} Current procedure development relies on expert judgment and
simulator validation. No mathematical proof exists that procedures cover all
possible plant states, that required actions can be completed within available
timeframes, or that transitions between procedure sets maintain safety
invariants. Paper-based procedures cannot ensure correct application, and even
computer-based procedure systems lack the formal guarantees that automated
reasoning could provide.
Nuclear plants operate with multiple control modes: automatic control, where the
reactor control system maintains target parameters through continuous reactivity
adjustment; manual control, where operators directly manipulate the reactor; and
various intermediate modes. In typical pressurized water reactor operation, the
reactor control system automatically maintains a floating average temperature
and compensates for power demand changes through reactivity feedback loops
alone. Safety systems, by contrast, operate with implemented automation. Reactor
Protection Systems trip automatically on safety signals with millisecond
response times, and engineered safety features actuate automatically on accident
signals without operator action required.
The division between automated and human-controlled functions reveals the
fundamental challenge of hybrid control. Highly automated systems handle reactor
protection---automatic trips on safety parameters, emergency core cooling
actuation, containment isolation, and basic process
control~\cite{WRPS.Description, gentillon_westinghouse_1999}. Human operators,
however, retain control of strategic decision-making: power level changes,
startup/shutdown sequences, mode transitions, and procedure implementation.
\subsection{Human Factors in Nuclear Accidents}
Current-generation nuclear power plants employ over 3,600 active NRC-licensed
reactor operators in the United States~\cite{operator_statistics}. These
operators divide into Reactor Operators (ROs), who manipulate reactor controls,
and Senior Reactor Operators (SROs), who direct plant operations and serve as
shift supervisors~\cite{10CFR55}. Staffing typically requires at least two ROs
and one SRO for current-generation units~\cite{10CFR50.54}. Becoming a reactor
operator requires several years of training.
The persistent role of human error in nuclear safety incidents---despite decades
of improvements in training and procedures---provides the most compelling
motivation for formal automated control with mathematical safety guarantees.
Operators hold legal authority under 10 CFR Part 55 to make critical decisions,
including departing from normal regulations during emergencies. The Three Mile
Island (TMI) accident demonstrated how a combination of personnel error, design
deficiencies, and component failures led to partial meltdown when operators
misread confusing and contradictory readings and shut off the emergency water
system~\cite{Kemeny1979}. The President's Commission on TMI identified a
fundamental ambiguity: placing responsibility for safe power plant operations on
the licensee without formal verification that operators can fulfill this
responsibility does not guarantee safety. This tension between operational
flexibility and safety assurance remains unresolved: the person responsible for
reactor safety is often the root cause of failures.
Multiple independent analyses converge on a striking statistic: 70--80\% of
nuclear power plant events are attributed to human error, versus approximately
20\% to equipment failures~\cite{WNA2020}. More significantly, the root cause of
all severe accidents at nuclear power plants---Three Mile Island, Chernobyl, and
Fukushima Daiichi---has been identified as poor safety management and safety
culture: primarily human factors~\cite{hogberg_root_2013}. A detailed analysis
of 190 events at Chinese nuclear power plants from
2007--2020~\cite{zhang_analysis_2025} found that 53\% of events involved active
errors, while 92\% were associated with latent errors---organizational and
systemic weaknesses that create conditions for failure.
\textbf{LIMITATION:} \textit{Human factors impose fundamental reliability limits
that cannot be overcome through training alone.} The persistent human
error contribution despite four decades of improvements demonstrates that these
limitations are fundamental rather than a remediable part of human-driven control.
\subsection{HARDENS and Formal Methods}
The High Assurance Rigorous Digital Engineering for Nuclear Safety (HARDENS)
project represents the most advanced application of formal methods to nuclear
reactor control systems to date~\cite{Kiniry2024}.
HARDENS aimed to address a fundamental dilemma: existing U.S. nuclear control
rooms rely on analog technologies from the 1950s--60s. This technology is
obsolete compared to modern control systems and incurs significant risk and
cost. The NRC contracted Galois, a formal methods firm, to demonstrate that
Model-Based Systems Engineering and formal methods could design, verify, and
implement a complex protection system meeting regulatory criteria at a fraction
of typical cost. The project delivered a Reactor Trip System (RTS)
implementation with full traceability from NRC Request for Proposals and IEEE
standards through formal architecture specifications to verified software.
HARDENS employed formal methods tools and techniques across the verification
hierarchy. High-level specifications used Lando, SysMLv2, and FRET (NASA Formal
Requirements Elicitation Tool) to capture stakeholder requirements, domain
engineering, certification requirements, and safety requirements. Requirements
were analyzed for consistency, completeness, and realizability using SAT and SMT
solvers. Executable formal models used Cryptol to create a behavioral model of
the entire RTS, including all subsystems, components, and limited digital twin
models of sensors, actuators, and compute infrastructure. Automatic code
synthesis generated verifiable C implementations and SystemVerilog hardware
implementations directly from Cryptol models---eliminating the traditional gap
between specification and implementation where errors commonly arise.
Despite its accomplishments, HARDENS has a fundamental limitation directly
relevant to hybrid control synthesis: the project addressed only discrete
digital control logic without modeling or verifying continuous reactor dynamics.
The Reactor Trip System specification and verification covered discrete state
transitions (trip/no-trip decisions), digital sensor input processing through
discrete logic, and discrete actuation outputs (reactor trip commands). The
project did not address continuous dynamics of nuclear reactor physics. Real
reactor safety depends on the interaction between continuous
processes---temperature, pressure, neutron flux---evolving in response to
discrete control decisions. HARDENS verified the discrete controller in
isolation but not the closed-loop hybrid system behavior.
\textbf{LIMITATION:} \textit{HARDENS addressed discrete control logic without
continuous dynamics or hybrid system verification.} Verifying discrete control
logic alone provides no guarantee that the closed-loop system exhibits desired
continuous behavior such as stability, convergence to setpoints, or maintained
safety margins.
HARDENS produced a demonstrator system at Technology Readiness Level 2--3
(analytical proof of concept with laboratory breadboard validation) rather than
a deployment-ready system validated through extended operational testing. The
NRC Final Report explicitly notes~\cite{Kiniry2024} that all material is
considered in development, not a finalized product, and that ``The demonstration
of its technical soundness was to be at a level consistent with satisfaction of
the current regulatory criteria, although with no explicit demonstration of how
regulatory requirements are met.'' The project did not include deployment in
actual nuclear facilities, testing with real reactor systems under operational
conditions, side-by-side validation with operational analog RTS systems,
systematic failure mode testing (radiation effects, electromagnetic
interference, temperature extremes), NRC licensing review, or human factors
validation with licensed operators in realistic control room scenarios.
\textbf{LIMITATION:} \textit{HARDENS achieved TRL 2--3 without experimental
validation.} While formal verification provides mathematical correctness
guarantees for the implemented discrete logic, the gap between formal
verification and actual system deployment involves myriad practical
considerations: integration with legacy systems, long-term reliability
under harsh environments, human-system interaction in realistic
operational contexts, and regulatory acceptance of formal methods as
primary assurance evidence.

53
3-research-approach/Untitled.canvas Normal file
View File

@ -0,0 +1,53 @@
{
"nodes":[
{"id":"aed191c3719f280b","x":-500,"y":520,"width":250,"height":60,"type":"text","text":"Discrete automata"},
{"id":"5ca8709465aa1eb8","x":-945,"y":550,"width":400,"height":375,"color":"4","type":"file","file":"Zettelkasten/Permanent Notes/20250821123741-syntcomp.md"},
{"id":"e9c5745032b1dd06","x":-1360,"y":470,"width":340,"height":400,"color":"4","type":"file","file":"Zettelkasten/Permanent Notes/20250819103208-strix.md"},
{"id":"a54ef0f53d23c989","x":-995,"y":-620,"width":675,"height":80,"type":"text","text":"# WHAT BELONGS IN THE RESEARCH APPROACH?"},
{"id":"0124a70ed7d9dde1","x":-995,"y":-500,"width":250,"height":60,"type":"text","text":"What is the problem?"},
{"id":"94ace1bf38c73a00","x":-670,"y":-500,"width":230,"height":60,"type":"text","text":"We want to automote complex systems"},
{"id":"482ca00bb17abaf7","x":-364,"y":-500,"width":250,"height":60,"color":"1","type":"text","text":"Ultimately we're replacing human tasks"},
{"id":"af23f539c0d2c8a8","x":-995,"y":-400,"width":250,"height":60,"type":"text","text":"We can leverage prescriptive procedures for this"},
{"id":"3d90877135704e66","x":-995,"y":-270,"width":250,"height":60,"type":"text","text":"translation of procedures"},
{"id":"89aac0a009838655","x":-50,"y":-500,"width":250,"height":60,"color":"1","type":"text","text":"We're doing this needing guarantees of behavior"},
{"id":"5467e220d316b68e","x":-50,"y":-340,"width":250,"height":60,"color":"5","type":"text","text":"Formal Methods"},
{"id":"47816cf87b1f4d37","x":-489,"y":330,"width":250,"height":60,"type":"text","text":"Reactive Synthesis"},
{"id":"1f085c02451b41bf","x":-100,"y":640,"width":250,"height":60,"type":"text","text":"Continuous systems as transitions"},
{"id":"7e9c528ccdb4a1d3","x":-100,"y":500,"width":250,"height":60,"type":"text","text":"Guard conditions between switching"},
{"id":"cb089746088729eb","x":200,"y":-110,"width":250,"height":60,"color":"3","type":"text","text":"Automated translation?"},
{"id":"80d6b5c2f79c7f50","x":-632,"y":-270,"width":250,"height":60,"type":"text","text":"FRET"},
{"id":"a5e0333a1fd97c8e","x":-670,"y":-140,"width":325,"height":270,"type":"file","file":"Zettelkasten/Permanent Notes/20250818132022-temporal-logic.md"},
{"id":"04df937be9ee9d65","x":280,"y":460,"width":250,"height":60,"type":"text","text":"Reachability / Barrier certificates"},
{"id":"d10e5739a9b02d59","x":500,"y":738,"width":250,"height":60,"color":"3","type":"text","text":"Can this checking be done automatically?"},
{"id":"92b9577c4ad80dfb","x":375,"y":603,"width":250,"height":67,"type":"text","text":"Stabilizing, Transitory, and Expulsory Modes"},
{"id":"40c1a6ca6bb2a079","x":530,"y":160,"width":250,"height":60,"color":"2","type":"text","text":"Emerson Ovation buildout"}
],
"edges":[
{"id":"f0c616247ef362b8","fromNode":"47816cf87b1f4d37","fromSide":"bottom","toNode":"aed191c3719f280b","toSide":"top"},
{"id":"68c2c4285845f3f5","fromNode":"aed191c3719f280b","fromSide":"right","toNode":"7e9c528ccdb4a1d3","toSide":"left"},
{"id":"3071e0f7125058a4","fromNode":"47816cf87b1f4d37","fromSide":"right","toNode":"7e9c528ccdb4a1d3","toSide":"top"},
{"id":"909f7eb2167c285a","fromNode":"7e9c528ccdb4a1d3","fromSide":"bottom","toNode":"1f085c02451b41bf","toSide":"top"},
{"id":"00f7c15f8f153793","fromNode":"aed191c3719f280b","fromSide":"right","toNode":"1f085c02451b41bf","toSide":"left"},
{"id":"6dabdb83917f1676","fromNode":"47816cf87b1f4d37","fromSide":"right","toNode":"cb089746088729eb","toSide":"left"},
{"id":"7a14b61146a640dd","fromNode":"cb089746088729eb","fromSide":"right","toNode":"40c1a6ca6bb2a079","toSide":"top"},
{"id":"373a8bc63b77ed85","fromNode":"1f085c02451b41bf","fromSide":"right","toNode":"04df937be9ee9d65","toSide":"left"},
{"id":"6e9387d64739205d","fromNode":"5467e220d316b68e","fromSide":"bottom","toNode":"47816cf87b1f4d37","toSide":"top"},
{"id":"c5d073eba30e1a37","fromNode":"5467e220d316b68e","fromSide":"bottom","toNode":"04df937be9ee9d65","toSide":"top"},
{"id":"e4acffa12fc95726","fromNode":"47816cf87b1f4d37","fromSide":"bottom","toNode":"e9c5745032b1dd06","toSide":"top"},
{"id":"5d0ea7af94f651a9","fromNode":"47816cf87b1f4d37","fromSide":"bottom","toNode":"5ca8709465aa1eb8","toSide":"top"},
{"id":"0b6dace9fb98e600","fromNode":"e9c5745032b1dd06","fromSide":"right","toNode":"5ca8709465aa1eb8","toSide":"left"},
{"id":"850b211b8ecde5ac","fromNode":"5ca8709465aa1eb8","fromSide":"left","toNode":"e9c5745032b1dd06","toSide":"right"},
{"id":"d9ae9a8976519272","fromNode":"a5e0333a1fd97c8e","fromSide":"bottom","toNode":"47816cf87b1f4d37","toSide":"top"},
{"id":"03a9e226f2d2aa09","fromNode":"3d90877135704e66","fromSide":"right","toNode":"80d6b5c2f79c7f50","toSide":"left"},
{"id":"87fc0d0886d181eb","fromNode":"80d6b5c2f79c7f50","fromSide":"bottom","toNode":"a5e0333a1fd97c8e","toSide":"top"},
{"id":"66a86ae15f229f63","fromNode":"0124a70ed7d9dde1","fromSide":"right","toNode":"94ace1bf38c73a00","toSide":"left"},
{"id":"2f42c8e21d248d8f","fromNode":"af23f539c0d2c8a8","fromSide":"bottom","toNode":"3d90877135704e66","toSide":"top"},
{"id":"6cdfe28f96ff5711","fromNode":"482ca00bb17abaf7","fromSide":"bottom","toNode":"af23f539c0d2c8a8","toSide":"right"},
{"id":"ee4864d5b86a989b","fromNode":"94ace1bf38c73a00","fromSide":"right","toNode":"482ca00bb17abaf7","toSide":"left"},
{"id":"1ae35a126fc91ed2","fromNode":"482ca00bb17abaf7","fromSide":"right","toNode":"89aac0a009838655","toSide":"left"},
{"id":"ffc24ca21b2b87be","fromNode":"89aac0a009838655","fromSide":"bottom","toNode":"5467e220d316b68e","toSide":"top"},
{"id":"af0ec4d18e1c7771","fromNode":"04df937be9ee9d65","fromSide":"top","toNode":"40c1a6ca6bb2a079","toSide":"bottom"},
{"id":"d3dc6a0f7afb009e","fromNode":"04df937be9ee9d65","fromSide":"bottom","toNode":"92b9577c4ad80dfb","toSide":"top"},
{"id":"e93c36e60eba4a8b","fromNode":"92b9577c4ad80dfb","fromSide":"bottom","toNode":"d10e5739a9b02d59","toSide":"top"}
]
}

35
3-research-approach/outline.md Normal file
View File

@ -0,0 +1,35 @@
Okay so here's how things will go:
Integrate V design into the workings here
1. Requirement identification and translation
1. Point towards hardens lando thing
2. we're going to do a nuclear start up sequence
2. Synthesize requirements into a discrete automata
1. this makes up our mode switching behavior
2. There's probably going to be a serious amount of
refinement required here
3. Figure out by the structure of the nodes what the
purpose of the mode is
1. Do all traces leave? Do any traces leave? What
does this mean for the FUNCTION of the node?
3. Build controllers that satisfy each mode requirement
1. Reachability to ensure valid input and output sets?
2. We can ensure zeno behavior won't happen by looking
at the interface between modes
3. We should also see based on reachability that a well
built controller ONLY can enter the modes as
specified by the discrete automata
4. Contract based methods?
4. Fuck it man, that's like your provability or whatever
man.
What are the critical needs?
1. We need a way to build some operating procedures into
controllers for autonomy
2. How the hell do we know what the goals of each mode are?
3. How do we know for sure the continuous dynamics will
actually get us there?

285
3-research-approach/v1.tex Normal file
View File

@ -0,0 +1,285 @@
\section{Research Approach}
This research will overcome the limitations of current practice to build
high-assurance hybrid control systems for critical infrastructure. Building
these systems with formal correctness guarantees requires three main thrusts:
\begin{enumerate}
\item Translate operating procedures and requirements into temporal logic
formulae
\item Create the discrete half of a hybrid controller using reactive synthesis
\item Develop continuous controllers to operate between modes, and verify
their correctness
\end{enumerate}
Commercial nuclear power operations remain manually controlled by human
operators, yet the procedures they follow are highly prescriptive and
well-documented. This suggests that human operators may not be entirely
necessary given current technology. Written procedures and requirements are
sufficiently detailed that they may be translatable into logical formulae with
minimal effort. If successful, this approach enables automation of existing
procedures without system reengineering. To formalize these procedures, we will
use temporal logic, which captures system behaviors through temporal relations.
The most efficient path for this translation is NASA's Formal Requirements
Elicitation Tool (FRET). FRET employs a specialized requirements language called
FRETish that restricts requirements to easily understood components while
eliminating ambiguity~\cite{katis_capture_2022}. FRETish bridges natural language
and mathematical specifications through a structured English-like syntax
automatically translatable to temporal logic.
FRET enforces this structure by requiring all requirements to contain six
components: %CITE FRET MANUAL
\begin{enumerate}
\item Scope: \textit{What modes does this requirement apply to?}
\item Condition: \textit{Scope plus additional specificity}
\item Component: \textit{What system element does this requirement affect?}
\item Shall
\item Timing: \textit{When does the response occur?}
\item Response: \textit{What action should be taken?}
\end{enumerate}
FRET provides functionality to check system \textit{realizability}. Realizability
analysis determines whether written requirements are complete by examining the
six structural components. Complete requirements neither conflict with one
another nor leave any behavior undefined. Systems that are not realizable from
their procedure definitions and design requirements present problems beyond
autonomous control implementation. Such systems contain behavioral
inconsistencies---the physical equivalent of software bugs. Using FRET during
autonomous controller development allows systematic identification and
resolution of these errors.
The second category of realizability issues involves undefined behaviors
typically left to human judgment during operations. This ambiguity is
undesirable for high-assurance systems, since even well-trained humans remain
prone to errors. Addressing these specification gaps in FRET during development
yields controllers free from these vulnerabilities.
FRET exports requirements in temporal logic format compatible with reactive
synthesis tools. Linear Temporal Logic (LTL) builds upon modal logic's
foundational operators for necessity ($\Box$, ``box'') and possibility
($\Diamond$, ``diamond''), extending them to reason about temporal
behavior~\cite{baier_principles_2008}. The box operator $\Box$ expresses that a
property holds at all future times (necessarily always), while the diamond
operator $\Diamond$ expresses that a property holds at some future time
(possibly eventually). These are complemented by the next operator ($X$) for the
immediate successor state and the until operator ($U$) for expressing
persistence conditions.
Consider a nuclear reactor SCRAM requirement expressed in natural language:
\textit{``If a high temperature alarm triggers, control rods must immediately
insert and remain inserted until operator reset.''} This plain language
requirement can be translated into a rigorous logical specification:
\begin{equation}
\Box(HighTemp \rightarrow X(RodsInserted \wedge (\neg
RodsWithdrawn\ U\ OperatorReset)))
\end{equation}
This specification precisely captures the temporal relationship between the
alarm condition, the required response, and the persistence requirement. The
necessity operator $\Box$ ensures this safety property holds throughout all
possible future system executions, while the next operator $X$ enforces
immediate response. The until operator $U$ maintains the state constraint until
the reset condition occurs. No ambiguity exists in this scenario because all
decisions are represented by discrete variables. Formulating operating rules in
this logic enforces finite, correct operation.
Reactive synthesis is an active research field focused on generating discrete
controllers from temporal logic specifications. The term ``reactive'' indicates
that the system responds to environmental inputs to produce control outputs.
These synthesized systems are finite, with each node representing a unique
discrete state. The connections between nodes, called \textit{state
transitions}, specify the conditions under which the discrete controller moves
from state to state. This complete mapping of possible states and transitions
constitutes a \textit{discrete automaton}. Discrete automata can be represented
graphically as nodes (discrete states) with edges indicating transitions between
them. From the automaton graph, one can fully describe discrete system dynamics
and develop intuitive understanding of system behavior. Hybrid systems naturally
exhibit discrete behavior amenable to formal analysis through these finite state
representations.
We will employ state-of-the-art reactive synthesis tools, particularly Strix,
which has demonstrated superior performance in the Reactive Synthesis
Competition (SYNTCOMP) through efficient parity game solving
algorithms~\cite{meyer_strix_2018,jacobs_reactive_2024}. Strix translates linear
temporal logic specifications into deterministic automata automatically while
maximizing generated automata quality. Once constructed, the automaton can be
implemented using standard programming control flow constructs. The graphical
representation enables inspection and facilitates communication with controls
programmers who lack formal methods expertise.
We will use discrete automata to represent the switching behavior of our hybrid
system. This approach yields an important theoretical guarantee: because the
discrete automaton is synthesized entirely through automated tools from design
requirements and operating procedures, the automaton---and therefore our hybrid
switching behavior---is \textit{correct by construction}. Correctness of the
switching controller is paramount. Mode switching represents the primary
responsibility of human operators in control rooms today. Human operators
possess the advantage of real-time judgment: when mistakes occur, they can
correct them dynamically with capabilities extending beyond written procedures.
Autonomous control lacks this adaptive advantage. Instead, autonomous
controllers replacing human operators must not make switching errors between
continuous modes. Synthesizing controllers from logical specifications with
guaranteed correctness eliminates the possibility of switching errors.
While discrete system components will be synthesized with correctness
guarantees, they represent only half of the complete system. Autonomous
controllers like those we are developing exhibit continuous dynamics within
discrete states. These systems, called hybrid systems, combine continuous
dynamics (flows) with discrete transitions (jumps). These dynamics can be
formally expressed as~\cite{branicky_multiple_1998}:
\begin{equation}
\dot{x}(t) = f(x(t),q(t),u(t))
\end{equation}
\begin{equation}
q(k+1) = \nu(x(k),q(k),u(k))
\end{equation}
Here, $f(\cdot)$ defines the continuous dynamics while $\nu(\cdot)$ governs
discrete transitions. The continuous states $x$, discrete state $q$, and
control input $u$ interact to produce hybrid behavior. The discrete state $q$
defines which continuous dynamics mode is currently active. Our focus centers
on continuous autonomous hybrid systems, where continuous states remain
unchanged during jumps---a property naturally exhibited by physical systems. For
example, a nuclear reactor switching from warm-up to load-following control
cannot instantaneously change its temperature or control rod position, but can
instantaneously change control laws.
The approach described for producing discrete automata yields physics-agnostic
specifications representing only half of a complete hybrid autonomous
controller. These automata alone cannot define the full behavior of the control
systems we aim to construct. The continuous modes will be developed after
discrete automaton construction, leveraging the automaton structure and
transitions to design multiple smaller, specialized continuous controllers.
Notably, translation into linear temporal logic creates barriers between
different control modes. Switching from one mode to another becomes a discrete
boolean variable. \(RodsInserted\) or \(HighTemp\) in the temporal
specifications are booleans, but in the real system they represent physical
features in the state space. These features mark where continuous control modes
end and begin; their definition is critical for determining which control mode
is active at any given time. Information about where in the state space these
conditions exist will be preserved from the original requirements and included
in continuous control mode development, but will not appear as numeric values in
discrete mode switching synthesis.
The discrete automaton transitions are key to the supervisory behavior of the
autonomous controller. These transitions mark decision points for switching
between continuous control modes and define their strategic objectives. We
will classify three types of high-level continuous controller objectives based
on discrete mode transitions:
\begin{enumerate}
\item \textbf{Stabilizing:} A stabilizing control mode has one primary
objective: maintaining the hybrid system within its current discrete mode.
This corresponds to steady-state normal operating modes, such as a
full-power load-following controller in a nuclear power plant. Stabilizing
modes can be identified from discrete automata as nodes with only incoming
transitions.
\item \textbf{Transitory:} A transitory control mode has the primary goal of
transitioning the hybrid system from one discrete state to another. In
nuclear applications, this might represent a controlled warm-up procedure.
Transitory modes ultimately drive the system toward a stabilizing
steady-state mode. These modes may have secondary objectives within a
discrete state, such as maintaining specific temperature ramp rates before
reaching full-power operation.
\item \textbf{Expulsory:} An expulsory mode is a specialized transitory mode
with additional safety constraints. Expulsory modes ensure the system is
directed to a safe stabilizing mode during failure conditions. For example,
if a transitory mode fails to achieve its intended transition, the
expulsory mode activates to immediately and irreversibly guide the system
toward a globally safe state. A reactor SCRAM exemplifies an expulsory
continuous mode: when initiated, it must reliably terminate the nuclear
reaction and direct the reactor toward stabilizing decay heat removal.
\end{enumerate}
Building continuous modes after constructing discrete automata enables local
controller design focused on satisfying discrete transitions. The primary
challenge in hybrid system verification is ensuring global stability across
transitions~\cite{branicky_multiple_1998}. Current techniques struggle with this
problem because dynamic discontinuities complicate
verification~\cite{bansal_hamilton-jacobi_2017,guernic_reachability_2009}. This
work alleviates these problems by designing continuous controllers specifically
with transitions in mind. Decomposing continuous modes according to their
required behavior at transition points avoids solving trajectories through the
entire hybrid system. Instead, local behavior information at transition
boundaries suffices. To ensure continuous modes satisfy their requirements, we
employ three main techniques: reachability analysis, assume-guarantee contracts,
and barrier certificates.
Reachability analysis computes the reachable set of states for a given input
set. While trivial for linear continuous systems, recent advances have extended
reachability to complex nonlinear
systems~\cite{frehse_spaceex_2011,mitchell_time-dependent_2005}. We use
reachability to define continuous state ranges at discrete transition boundaries
and verify that requirements are satisfied within continuous modes.
Assume-guarantee contracts apply when continuous state boundaries are not
explicitly defined. For any given mode, the input range for reachability
analysis is defined by the output ranges of discrete modes that transition to
it. This compositional approach ensures each continuous controller is prepared
for its possible input range, enabling reachability analysis without global
system analysis. Finally, barrier certificates prove that mode transitions are
satisfied. Barrier certificates ensure that continuous modes on either side of a
transition behave appropriately by preventing system trajectories from crossing
a given barrier. Control barrier functions certify safety by establishing
differential inequality conditions that guarantee forward invariance of safe
sets~\cite{prajna_safety_2004}. For example, a barrier certificate can guarantee
that a transitory mode transferring control to a stabilizing mode will always
move away from the transition boundary, rather than destabilizing the target
stabilizing mode.
This compositional approach has several advantages. First, this approach breaks
down autonomous controller design into smaller pieces. For designers of future
autonomous control systems, the barrier to entry is low, and design milestones
are clear due to the procedural nature of this research plan. Second, measurable
design progress also enables measurement of regulatory adherence. Each step in
this development procedure generates an artifact that can be independently
evaluated as proof of safety and performance. Finally, the compositional nature
of this development plan enables incremental refinement between control system
layers. For example, difficulty developing a continuous mode may reflect a
discrete automaton that is too restrictive, prompting refinement of system
design requirements. This synthesis between levels promotes broader
understanding of the autonomous controller.
To demonstrate this methodology, we will develop an autonomous startup
controller for a Small Modular Advanced High Temperature Reactor (SmAHTR). We
have already developed a high-fidelity SmAHTR model in Simulink that captures
the thermal-hydraulic and neutron kinetics behavior essential for verifying
continuous controller performance under realistic plant dynamics. The
synthesized hybrid controller will be implemented on an Emerson Ovation control
system platform, representative of industry-standard control hardware deployed
in modern nuclear facilities. The Advanced Reactor Cyber Analysis and
Development Environment (ARCADE) suite will serve as the integration layer,
managing real-time communication between the Simulink simulation and the Ovation
controller. This hardware-in-the-loop configuration enables validation of the
controller implementation on actual industrial control equipment interfacing
with a realistic reactor simulation, assessing computational performance,
real-time execution constraints, and communication latency effects.
Demonstrating autonomous startup control on this representative platform will
establish both the theoretical validity and practical feasibility of the
synthesis methodology for deployment in actual small modular reactor systems.
This unified approach addresses a fundamental gap in hybrid system design by
bridging formal methods and control theory through a systematic, tool-supported
methodology. Translating existing nuclear procedures into temporal logic,
synthesizing provably correct discrete switching logic, and developing verified
continuous controllers creates a complete framework for autonomous hybrid
control with mathematical guarantees. The result is an autonomous controller
that not only replicates human operator decision-making but does so with formal
assurance that switching logic is correct by construction and continuous
behavior satisfies safety requirements. This methodology transforms nuclear
reactor control from a manually intensive operation requiring constant human
oversight into a fully autonomous system with higher reliability than
human-operated alternatives. More broadly, this approach establishes a
replicable framework for developing high-assurance autonomous controllers in any
domain where operating procedures are well-documented and safety is paramount.

429
3-research-approach/v2.tex Normal file
View File

@ -0,0 +1,429 @@
\section{Research Approach}
\iffalse
HACS: hybrid autonomous control system
HAHACS: High-Assurance Hybrid AUtonomous Control System
The research approach here needs to clearly outline the solution the the problem
and identify the actions taken that will advance knowledge and solve the
problem.
First, what is the problem?
\textit{
Inhibition to adopt hybrid autonomous control in critical infrastructure is
rooted in safety concerns of system stability. Without a human in the loop
with general intelligence, HACS have not been trusted where failure modes can
be unique and novel.
}
So, what's the solution?
\textit{
This research approach develops a methodology to build HACS that are provably
safe. This methodology builds on existing technologies, and unifies different
research thrusts to build a complete hybrid control system. To do this, the
problem of a HAHCS is broken into three distinct pieces:
\begin{enumerate}
\item System specification: properties of the HAHaCS such as transition
between control modes and system invariants are specified using a formal
methods tool.
- This provides exact behavior
- allows realizabillity checking of controller specs. Can a controller
actually be built from these specs?
- ?
- ?
\item Discrete Behavior Synthesis: The discrete component of the controller
is synthesized directly from system specifications using reactive
synthesis.
- This ELIMINATES wholesale the possibility of introducing logical bugs
in the creation of the strategic part of the HAHCS. Critical decisions
that are normally made by a human are automated directly from the
formal specifications.
- This does two critical things:
- It makes the creation of the controller tractable. The reasons the
controller changes between modes acn be traced back to the
specification (and thus any requirements), which is a trace for
liability and justification of system behavior
- Discrete control decisions made by humans are reliant on the human
operator operating correctly. Humans are intrinsically probabalistic
creatures who cannot eliminate human error. By defining the behavior
of this system using temporal logics and synthesizing the controller
using deterministic algorithims, we are assured that strategic
decisions will always be made as according to operating procedures.
\item Continuous Behavior Synthesis and Verification: The continuous
components of the controller are built using existing dynamics and control
theory but then verified using reachability and barrier certificats.
- It's very challenging (nigh impossible) to say for certain how to
build any continuous control mode. That is honestly going to be have to
left to the specific control system and its objectives. It's not really
the point of this PhD to say how to do that. For that reason, I'm going
to assume that controllers between modes are generally possible to
build. That is to say that there exists a controller that can transition
between modes, but it is a human hunt to find it.
- To check if a candidate controller does transition between discrete
modes, we do two things:
- Check invariants using reachability. Specifications will require
that control modes transiiton from one mode to the next, where
appropriate. When this is the case, these invariants are extracted to
be checked using reachability. The control mode is given the possible
entry conditions of the 'entry' mode, and the possible 'exit' states
are analyzed. A cont. controller passes this reachability test if
there is no reachable state that is not at the exit condition of the
state transition.
--- This needs flushed out more. I think this can really be clarified
using entry and exit conditions of Mealy machines. The continuous
system IS the transition, and the reachabililty test is saying whether
or not the physical system actually satisfies the entry and exit
conditions.
- Then, for systems that need to STAY within one mode, we will use
barrier certificates. These can let us define a continuous state
boundary, and define for a discrete controller state, the total
controller will NOT leave the continuous boundary.
- One thing that must be considered is the idea that this analysis is
predicated on the physical system being correct to the model. If this
isn't true, we must define continuous modes that catch failure states.
If transition invariants are violated, we must shut down the system, and
build safety oriented control modes that we can be sure with a much
broader set of entry conditions will safely shut down the plant.
-- Q for dan: is it critical to really have software to namedrop or is it
better to stay amorphous on the technology? Iirc Manyu did a little bit of
both.
\end{enumerate}
What's the intellectual merit?
\textit{
There is no outstanding way to build HAHACS. This methodology provides a
basis for systems engineers to think about the components of a HAHACS as
interlocking pieces whos verification interlinks into a broader system.
This will also motivate the adoption of temporal logic to define autonomous
control systems, by allowing a close connection and tracability between
requirements from regulations to system specifications.
}
}
Some thoughts on invariants, and how they fit here: There are several types of
safety invariants that HAHACS might have.
1. Conditions that initiate a switch between control modes (reactiive synthesis
relevant)
2. Invariants about the stability of discrete states (barrier certificates)
3. Invariants ensuring the transition between discrete states (reachability)
4. Invariants about the timeliness of discrete transitions (??? Reachability?)
How do we reason about all of these invariants. Well, fundamentally they can
all be reasoned about with temporal logic statements. Using next and eventually
operators, we can get to the fundamental behavior of all of these modes. What's
challenging is the fact that we ensure that all of these specifications are
validated differs between the type of invariant. This is really the beauty of
this approach, and the intellectual merit. This proposal provides a way for
hybrid control systems to be verified for autonomous control systems by
diversifying the way that the invariants are checked.
Reactive synthesis helps us build discrete controllers using specifications
that have conditons that don't depend on time. These invariants generally are
strategic decisions, such as changing between operating modes, initiating power
level changes, or perhaps doing a refueling or shutdown routine. These
specifications are able to be nearly directly drawn from operating procedures,
and should be closely tied to instructions that would be used for human
operators. They have checkpoints for the continuous system in between different
control implements. An example is, raise power at a certain rate while ensure
temperature remains between certain bounds. These conditions are physical
states, but they are a binary result. The condition is really binary, desipite
perhaps having units of celsius or %power. When we build discrete controllers
from these specifications, we get the validation of the controller of these
specs for free by nature of reactive synthesis tools. We get direct
traceability from the operating procedure to the discrete controller
implementation with minimal human effort.
That being said, there are no free lunches here. Ultimately, we're controlling
physical systems, and while we can automate the controller building between
stratgic objectives, it is not trivial to do so for the controller of the
physical process. These controllers are going to have to be built manually,
with the continuous dynamics of the system in mind. Helpfully, if
specifications are complete first, one can obtain discrete controller before
building physical controllers. The result of this is a simplification of
controller design, becuase the operational goals of each continuous controller
is clearly outlined by the invariants that define the goal of each discrete
mode. While for reactive synthesis purposes conditions such as a certain
temperature being reached or power level attained are binary variables, the
continuous physical meaning becomes important in the design and analysis of the
physical controllers. The continuous value of these conditions becomes the goal
of the continuous controller design, while also providing a basis to check
controller performance.
To check continuous controllers are valid, we can split continuous controller
objectives into two types. First, we have continuous controllers that are
designed to move the plant between two different discrete modes. These will be
called 'transitory' controllers, because their entire purpose is to transition
the plant betweeen between discrete control modes. Because of the specification
of the hybrid control system a priori, we will have defined what the invariants
of these transitions are in continuous state space. Then, once a continuosu
controller design is developed, it can be validated using reachability
analysis. The input set for the analysis is the possible states that enter this
transitory mode, while the reachable states must be entirely contained within
the exit invariant for the controller to pass. At the time of writing this
proposal, it is not clear what the most efficient way to obetain this
continuous controller is, but is generally beyond the scope of this work. It is
assumed that they generally won't be so difficult to find for most systems, as
the refinement of the discrete controller should simplify the control
objectives of the physical controllers significantly.
The second type of continuous controller that may be utilized in a HAHAHCS is a
controller that tries to maintaine a continuous steady state, such that no
discrete transitions are triggered. Reachability on these systems may not prove
a prudent approach to validating this behavior for a candidate continuous
controller, and instead, barrier certificates must be used. Barrier
certificates analyze the dynamics of the system to say whether or not flux
across a given boudnary exists. That is to say that they evaluate whether or
not there is a trajectory or not that leaves a given boundary. This definition
is exactly what defines the validity of a stabilizing continuous control mode.
Once again, because the design of the discrete controller defines careful
boundaries in continuous state space, the barrier is known a priori of which we
must satisfy this condition. This will eliminate the search for such a barrier,
and minimze complicatoin in validating stabilizing continuous control modes.
Finally, consideration must be paid for when errors occur. The validation of
these continuous control modes hinges upon having an assumption ofcorrect
model, which in the case of a mechanical failure will almsot certainly be
invalidated. Special continuous controllers for these conditions must be
created, called 'explusory' control modes. These controllers will be
responsible for ensuring safety in case of failure, and will be designed with
reachability, but in this case, additional allocation for the allowing of
physical parameters will be allowed in the analysis. Traditional safety
analysis will also be used to identify potential failure modes, and the
modelling of their worst case dynamics. The HAHCS will be able to idenfity why
such a fault occors because an discrte boundary condition will be violated by
the continuous physical controller. That is to say, since we will have
validated the continuous control modes using reachability and barrier
certificates a priori, we will know with certainty that the only room for
dynamics to change is a shift in the plant dynamics, not that of the proven
controller.
\fi
%%%%%%%%%% TABLESETTING
% what is a hybrid system really for this proposal
% Define: A hybrid system with continuous state space X ⊆ ℝⁿ and discrete modes Q = {q₁, q₂, ..., qₘ}
% Each discrete mode qᵢ has an associated continuous state region Xᵢ ⊆ X
% The discrete controller manages transitions between modes based on continuous state thresholds
% what are requirements, anyways?
% why do we care about defining the whole hybrid system into requirements?
% How do different requirements line up into different parts of the system?
% (operational vs strategic requirements and their relevance to different parts
% of our system)
Autonomous control systems are fundamentally different from automatic control
systems. The difference between these systems is the level at which
they operate. Automatic control systems are purely operational systems,
To build a high-assurance hybrid autonomous control system (HAHACS), a
mathematical description of the system must be established. This work will make
use of automata theory while including logical statements and control theory.
The nomenclature and lexicon between these fields is far from homogenous, and
the reviewer of this proposal is not expected to be an expert in all fields
simultaneously. To present the research ideas as clearly as possible in this
section, the following syntax is explained.
A hybrid system is a dynamical system that has both continuous and discrete
states. The specific type of system discussed in this proposal are continuous
autonomous hybrid systems. This means that these systems a) do not have
external input \footnote{This is not strictly true in our case because we allow
strategic inputs. For example, a remote powerplant may receive a start-up or
shutdown command from a different location, but only this binary high level
input is a strategic input.} and b) continuous states do not change
instantaneously when discrete states change. For our systems of interest, the
continuous states are physical, and are always Lipschitz continuous. This
nomenclature is heavily borrowed from \cite{HANDBOOK ON HYBRID SYSTEMS CONTROL},
but is redefined here for convenience:
\begin{equation}
H = (\mathcal{Q}, \mathcal{X}, \mathbf{f}, Init, \mathcal{G}, \mathcal{R}, Inv)
\end{equation}
where:
\begin{itemize}
\item \( \mathcal{Q}\): is the discrete states of the system
\item \( \mathcal{X}\): is the continuous states of the system
\item \(\mathbf{f}: \mathcal{Q} \times \mathbb{R} \rightarrow \mathbb{R} \), where
\(\mathbf{f}_i\) is a
vector field that defines the continuous dynamics for each \(q_i\)
\item \(Init\): the initial states of \(q\) and \(x\)
\item \( G\): guard
conditions that define when discrete state transitions occur
\item \(\delta: \mathcal{Q} \times G \rightarrow \mathcal{Q}\), are the
discrete state transition functions
\item \mathcal{R}: Reset maps that define state 'jumps'
\item \(Inv\): Safety invariants on the continuous dynamics
\end{itemize}
The creation of a HAHACS essentially boils down to the creation of such a tuple
where there are proof artifacts that the intended behavior of the control system
are satisfied by the actual implementation of the control systems. But to create
such a HAHACS, we must first completely describe its behavior.
%% Brief discussion on what each part of this tuple means for us
\subsection{System Requirement and Specifications}
Temporal logic is a powerful set of semantics to build systems that can have
complex but deterministic behavior.
%%%%%%%%%%% Building discrete controllers
% Buildout of requirements from written procedures (this is easy for critical
% systems - we already have the requirements)
% What happens to the invariants that specify a continuous space? Save em for
% later. Here they become binary for our purposes
% KEY POINT: We don't IMPOSE discrete abstraction - we FORMALIZE existing practice
% Operating procedures (esp. nuclear) already define go/no-go conditions as discrete predicates
% e.g., "WHEN coolant temp >315°C AND pressurizer level 30-60% THEN MAY initiate load following"
% These thresholds come from design-basis safety analysis, validated over decades
% Our methodology assumes this domain knowledge exists and provides formalization framework
% The discrete predicates p₁, p₂, ... are Boolean functions over continuous state: pᵢ: X → {true, false}
% Q: How do we rigorously set thresholds for continuous→discrete abstraction?
% Q: How do we handle hysteresis to prevent mode chattering near boundaries?
% Q: How do we account for sensor noise and measurement uncertainty?
% Q: How do we handle numerical precision issues when creating discrete automata? (relates to task 36)
% Discrete controller implementation can be realized with reactive synthesis.
% LTL specs to automata
% talk a bit about tools here like FRET. Talk about previous attempts.
%%%%%%%%%%%% Building continuous controllers
% The whole point of a hybrid system is that there are continuous components
% underneath the digital system. We built the discrete like the physical doesn't
% exist, but it really does. So how do we capture the physical system too?
% SCOPE FRAMING: This methodology VERIFIES continuous controllers, not SYNTHESIZES them
% Compare to model checking: doesn't tell you HOW to design software, verifies if it satisfies specs
% We assume controllers can be designed using standard control theory techniques
% Our contribution: verification that candidate controllers compose correctly with discrete layer
% What are the main different kinds of continuous modes we may see?
% Mathematical structure: Each discrete mode qᵢ provides three key pieces of information:
% 1. Entry conditions: X_entry,i ⊆ X (initial state set)
% 2. Exit conditions: X_exit,i ⊆ X (target state set)
% 3. Invariants: X_safe,i ⊆ X (safety envelope during operation)
% These come from the discrete controller synthesis and define objectives for continuous control
% Q: Who designs the continuous controllers and how? This methodology verifies
% them, but doesn't synthesize them. Is this a scope problem?
%%%%%% Transitory modes
% entry and exit conditions
% the goal is getting from one physical state to another
% MATHEMATICAL FORMULATION:
% Control objective: reach(X_entry,i) → reach(X_exit,i) while maintaining x(t) ∈ X_safe,i
% Standard control techniques (LQR, MPC, trajectory optimization) applied with these constraints
%
% VERIFICATION: Reachability analysis confirms ALL trajectories starting in X_entry,i
% reach X_exit,i without violating X_safe,i
% Formally: Reach(X_entry,i, f(x,u), T) ⊆ X_exit,i ∪ X_safe,i
% where f(x,u) is the closed-loop continuous dynamics
%
% we have the physical requirements from earlier specifications. Here we use
% them in a reachability analysis. This time, we use the actual physical values
% instead of the binary yes/no we used for discrete
% Q: How do we verify timing constraints? If a transitory controller eventually
% reaches the exit condition but takes too long, that violates safety. Timed
% automata? Timed reachability?
% Q: Should formalize the Mealy machine perspective - continuous system IS the
% transition, and entry/exit conditions are the discrete states. This could be
% a unifying conceptual framework.
%%%%%% stabilizing modes
% these are control modes with an objective of KEEPING a certain discrete state
% stable
%
% MATHEMATICAL FORMULATION:
% Control objective: remain(X_target,i) where X_target,i ⊂ X_safe,i
% Standard feedback control (PID, state feedback, LQG) applied to maintain equilibrium
%
% VERIFICATION: Barrier certificates prove closed-loop dynamics cannot escape X_safe,i
% Formally: Find B(x) s.t. ∇B(x)·f(x,u) ≤ 0 for all x ∈ ∂X_safe,i
% This proves no trajectory can cross the boundary (no flux out of safety region)
%
% we also have the physical requirements for this. These can be used for barrier
% certificates. We can prove that our model won't leave a given area without
% some disturbance.
%%%%%% expulsory modes
% I've made an implicit assumption when talking about transitory and stabilizing
% modes. That our model is correct. This might not be true
% In the case of a failure, our model will almost certainly be incorrect. For
% this, we have to build safe shutdown modes too, since a human won't be in the
% loop to shut things down.
%
% MATHEMATICAL FORMULATION:
% Control objective: reach(X_current) → reach(X_safe_shutdown) under parameter uncertainty
% where X_current may be anywhere in X (worst-case entry conditions)
% Dynamics have parametric uncertainty: f(x,u,θ) where θ ∈ Θ_failure
%
% VERIFICATION: Parametric reachability analysis with robustness margins
% Reach(X_current, f(x,u,θ), T) ⊆ X_safe_shutdown for all θ ∈ Θ_failure
% Conservative bounds on Θ_failure come from FMEA/traditional safety analysis
% WE can detect physical failures exist because our physical controllers have
% previously been proven as correct by reachability and barrier certificates. We
% KNOW our controller cannot be incorrect for the plant, so if an invariant is
% violated, we KNOW it's the plant that has changed.
% Q: What about sensor failures (wrong readings vs actual plant failure)?
% Q: What about unmodeled disturbances that aren't failures?
% Q: What if model uncertainty was too optimistic to begin with?
% Need to be more precise about what "model failure" means and detect-ability.
% We do this using continuous modes that shutdown the system, and using
% reachability analysis with parametric uncertainty, we can prove for a range of
% error conditions we can maintain safe shutdown.
% Q: How much parametric uncertainty is enough? How do we determine bounds for
% worst-case failure dynamics? Need methodology for this.
%%%%%%%%%%%% Implementation with industrial partnerships
%%%%%%% Emerson
%talk about this
% ovation system
% scenic? Is that what they call it?
% ripe partnership with Westinghouse
% Likely build a model with a ccng plant. They already have sophisticated models
% of them
% build controller with simplified model, then test with high fidelity digital
% twin
%
%%%%%%%%%%

88
4-metrics-of-success/v1.tex Normal file
View File

@ -0,0 +1,88 @@
\section{Metrics for Success}
This research will be measured by advancement through Technology Readiness
Levels, progressing from fundamental concepts to validated prototype
demonstration. This work begins at TRL 2--3 and aims to reach TRL 5, where
system components operate successfully in a relevant laboratory environment.
This section explains why TRL advancement provides the most appropriate success
metric and defines the specific criteria required to achieve TRL 5.
Technology Readiness Levels provide the ideal success metric because they
explicitly measure the gap between academic proof-of-concept and practical
deployment---precisely what this work aims to bridge. Academic metrics like
papers published or theorems proved cannot capture practical feasibility.
Empirical metrics like simulation accuracy or computational speed cannot
demonstrate theoretical rigor. TRLs measure both dimensions simultaneously.
Advancing from TRL 3 to TRL 5 requires maintaining theoretical rigor while
progressively demonstrating practical feasibility. Formal verification must
remain valid as the system moves from individual components to integrated
hardware testing.
The nuclear industry requires extremely high assurance before deploying new
control technologies. Demonstrating theoretical correctness alone is
insufficient for adoption; conversely, showing empirical performance without
formal guarantees fails to meet regulatory requirements. TRLs capture this dual
requirement naturally. Each level represents both increased practical maturity
and sustained theoretical validity. Furthermore, TRL assessment forces explicit
identification of remaining barriers to deployment. The nuclear industry already
uses TRLs for technology assessment, making this metric directly relevant to
potential adopters. Reaching TRL 5 provides a clear answer to industry questions
about feasibility and maturity that academic publications alone cannot.
Moving from current state to target requires achieving three intermediate
levels, each representing a distinct validation milestone:
\paragraph{TRL 3 \textit{Critical Function and Proof of Concept}}
For this research, TRL 3 means demonstrating that each component of the
methodology works in isolation. Startup procedures must be translated into
temporal logic specifications that pass realizability analysis. A discrete
automaton must be synthesized with interpretable structure. At least one
continuous controller must be designed with reachability analysis proving
transition requirements are satisfied. Independent review must confirm that
specifications match intended procedural behavior. This proves the fundamental
approach on a simplified startup sequence.
\paragraph{TRL 4 \textit{Laboratory Testing of Integrated Components}}
For this research, TRL 4 means demonstrating a complete integrated hybrid
controller in simulation. All startup procedures must be formalized with a
synthesized automaton covering all operational modes. Continuous controllers
must exist for all discrete modes. Verification must be complete for all mode
transitions using reachability analysis, barrier certificates, and
assume-guarantee contracts. The integrated controller must execute complete
startup sequences in software simulation with zero safety violations across
multiple consecutive runs. This proves that formal correctness guarantees can be
maintained throughout system integration.
\paragraph{TRL 5 \textit{Laboratory Testing in Relevant Environment}}
For this research, TRL 5 means demonstrating the verified controller on
industrial control hardware through hardware-in-the-loop testing. The discrete
automaton must be implemented on the Emerson Ovation control system and verified
to match synthesized specifications exactly. Continuous controllers must execute
at required rates. The ARCADE interface must establish stable real-time
communication between the Emerson Ovation hardware and SmAHTR simulation.
Complete autonomous startup sequences must execute via hardware-in-the-loop
across the full operational envelope. The controller must handle off-nominal
scenarios to validate that expulsory modes function correctly. For example,
simulated sensor failures must trigger appropriate fault detection and mode
transitions, and loss-of-cooling scenarios must activate SCRAM procedures as
specified. Graded responses to minor disturbances are outside this work's scope.
Formal verification results must remain valid, with discrete behavior matching
specifications and continuous trajectories remaining within verified bounds.
This proves that the methodology produces verified controllers implementable on
industrial hardware.
Progress will be assessed quarterly through collection of specific data
comparing actual results against TRL advancement criteria. Specification
development status indicates progress toward TRL 3. Synthesis results and
verification coverage indicate progress toward TRL 4. Simulation performance
metrics and hardware integration milestones indicate progress toward TRL 5. The
research plan will be revised only when new data invalidates fundamental
assumptions. This research succeeds if it achieves TRL 5 by demonstrating a
complete autonomous hybrid controller with formal correctness guarantees
operating on industrial control hardware through hardware-in-the-loop testing in
a relevant laboratory environment. This establishes both theoretical validity
and practical feasibility, proving that the methodology produces verified
controllers and that implementation is achievable with current technology.

67
5-risks-and-contingencies/assumptions.md Normal file
View File

@ -0,0 +1,67 @@
# Risk and Contingencies Assumptions Exercise
**The outcome I want to achieve is?**
- Turn written reqs into discrete controller
- Build continuous modes that ensure hybrid stability
- Implement on industrial controller with HIL simulation
**What can't anyone solve this today?**
- Nobody has tried to build system like this with stability
in mind from the ground up. NUCE is a specific domain this
is useful. Reliance on human operators for safety.
**The research approach I am using is?**
- Formal Methods + Control Theory
- FRET - Reachability
- Reactive Synthesis
**This research approach relies on these fundamental
principles?**
- Temporal logic precision
- automata
- differential and difference equations
- procedure writing
**The experiment that I will perform is?**
- trying to make an autonomous start up procedure for a
SmAHTR reactor
**The equipment I will use is?**
1. FRET
2. STRIX
3. Simulink
4. Reachability tools
5. Ovation
**I will analyze the results using?**
1. Prose. How hard was this to do, what MacGuyvering needed
done? What TRL?
**The expected outcome of this experiment is?**
1. A working autonomous start up controller can take a
simulation from cold to critical without needing a human
operator to intervene.
**What happens if this experiment does not work?**
1. We'll shift to a smaller, simpler problem where we can
overcome the limits.
**What happens if the hypothesis or prediction is false?**
1. We'll show the gap between current procedure writing and
where we need to be to actually do synthesis.
**What assumptions do I have that, if proven wrong, would
derail this project?**
1. Temporal logic from FRET is easy to synthesize with STRIX
2. I'm not going to have state-space explosion happen
3. Writing a start-up procedure for SmAHTR isn't that hard
4. People give a crap about molten salt reactors
5. This whole discrete boundary thing is not going to be
really hard to implement. The idea is conditions for the
transitions between modes to be boolean variables for
the temporal lgoic, but that they correspond to some surface
in the continuous state space. How am I going to keep track
of that?
6. Computational cost. Center for Research Computing is the
answer.

158
5-risks-and-contingencies/v1.tex Normal file
View File

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

71
6-broader-impacts/v1.tex Normal file
View File

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

96
8-schedule/v1.tex Normal file
View File

@ -0,0 +1,96 @@
\section{Schedule, Milestones, and Deliverables}
This research will be conducted over six trimesters (24 months) of full-time
effort following the proposal defense in Spring 2026. The work progresses
sequentially through three main research thrusts before culminating in
integrated demonstration and validation.
The first semester (Spring 2026) focuses on Thrust 1, translating startup
procedures into formal temporal logic specifications using FRET. This
establishes the foundation for automated synthesis by converting natural
language procedures into machine-readable requirements. The second semester
(Summer 2026) addresses Thrust 2, using Strix to synthesize the discrete
automaton that defines mode-switching behavior. With the discrete structure
established, the third semester (Fall 2026) develops the continuous controllers
for each operational mode through Thrust 3, employing reachability analysis and
barrier certificates to verify that each mode satisfies its transition
requirements. Integration and validation occupy the remaining three semesters.
Figure \ref{fig:gantt} shows the complete project schedule including research thrusts, major milestones, and planned publications.
\begin{figure}[htbp]
\centering
\begin{ganttchart}[
hgrid,
vgrid={*{4}{draw=none}, dotted},
x unit=0.4cm,
y unit title=0.6cm,
y unit chart=0.4cm,
title/.append style={fill=gray!30},
title height=1,
bar/.append style={fill=blue!50},
bar height=0.5,
bar label font=\small,
milestone/.append style={fill=red, shape=diamond},
milestone height=0.5
]{1}{24}
% Timeline headers
\gantttitle{2026}{12}
\gantttitle{2027}{12} \\
\gantttitle{Spring}{4}
\gantttitle{Summer}{4}
\gantttitle{Fall}{4}
\gantttitle{Spring}{4}
\gantttitle{Summer}{4}
\gantttitle{Fall}{4} \\
% Major thrusts
\ganttbar{Thrust 1: Procedure Translation}{1}{5} \\
\ganttbar{Thrust 2: Discrete Synthesis}{4}{10} \\
\ganttbar{Thrust 3: Continuous Control}{9}{15} \\
\ganttbar{Integration \& Simulation (TRL 4)}{13}{17} \\
\ganttbar{Hardware-in-Loop Testing (TRL 5)}{16}{21} \\
\ganttbar{Dissertation Writing}{18}{24} \\[grid]
% Milestones row
\ganttbar[bar/.append style={fill=orange!50}]{Milestones}{1}{24}
\ganttmilestone{}{4}
\ganttmilestone{}{8}
\ganttmilestone{}{12}
\ganttmilestone{}{16}
\ganttmilestone{}{20}
\ganttmilestone{}{24} \\
% Publications row
\ganttbar[bar/.append style={fill=green!50}]{Publications}{1}{24}
\ganttmilestone{}{8}
\ganttmilestone{}{16}
\ganttmilestone{}{20}
\end{ganttchart}
\caption{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.}
\label{fig:gantt}
\end{figure}
\subsection{Milestones and Deliverables}
Six major milestones mark critical validation points throughout the research. M1
(Month 4) confirms that startup procedures have been successfully translated to
temporal logic using FRET with realizability analysis demonstrating consistent
and complete specifications. M2 (Month 8) validates computational tractability
by demonstrating that Strix can synthesize a complete discrete automaton from
the formalized specifications. This milestone delivers a conference paper
submission to NPIC\&HMIT documenting the procedure-to-specification translation
methodology. M3 (Month 12) achieves TRL 3 by proving that continuous controllers
can be designed and verified to satisfy discrete transition requirements. This
milestone delivers an internal technical report demonstrating component-level
verification. M4 (Month 16) achieves TRL 4 through integrated simulation
demonstrating that component-level correctness composes to system-level
correctness. This milestone delivers a journal paper submission to IEEE
Transactions on Automatic Control presenting the complete hybrid synthesis
methodology. M5 (Month 20) achieves TRL 5 by demonstrating practical
implementability on industrial hardware. This milestone delivers a conference
paper submission to NPIC\&HMIT or CDC documenting hardware implementation and
experimental validation. M6 (Month 24) completes the dissertation documenting
the entire methodology, experimental results, and research contributions.

133
CLAUDE.md Normal file
View File

@ -0,0 +1,133 @@
# CLAUDE.md
This file provides guidance to Claude Code (claude.ai/code) when working with code in this repository.
## Project Overview
This is a PhD thesis proposal for developing a methodology to build High-Assurance Hybrid Autonomous Control Systems (HAHACS) for critical infrastructure. The proposal is titled "From Cold Start to Critical: Formal Synthesis of Autonomous Hybrid Controllers."
**Intellectual Merit**: The contribution is architectural unification rather than algorithmic novelty. The methodology provides a systematic decomposition mapping verification techniques to control mode types, composing existing formal methods into a complete framework where none existed.
**Key Insight**: The methodology formalizes EXISTING discrete abstractions from operating procedures (especially nuclear) rather than imposing arbitrary ones. Operating procedures already define go/no-go conditions as discrete predicates - this work provides the formalization and verification framework.
## Document Structure
The proposal uses a modular LaTeX structure with numbered section directories:
- `main.tex` - Root document that inputs all sections
- `1-goals-and-outcomes/` - Research statement and goals
- `2-state-of-the-art/` - Literature review
- `3-research-approach/` - Core methodology (CURRENTLY ACTIVE WORK)
- `4-metrics-of-success/` - Success criteria
- `5-risks-and-contingencies/` - Risk analysis
- `6-broader-impacts/` - Broader impacts
- `8-schedule/` - Timeline
Each section directory contains:
- `v1.tex` (or `v2.tex` for actively revised sections) - Main content
- `outline.md` (optional) - Planning notes and structure
**IMPORTANT**: Section 3 (research-approach) is currently being revised. `main.tex` inputs `v2.tex` for this section, which contains extensive inline comments and questions prefixed with `%` and `% Q:`.
## Building the Document
```bash
# Full build with bibliography
pdflatex main.tex
bibtex main
pdflatex main.tex
pdflatex main.tex
# Quick build (no bibliography updates)
pdflatex main.tex
# Use latexmk for automated builds
latexmk -pdf main.tex
# Clean auxiliary files
latexmk -c
```
The output is `main.pdf`.
## Key Technical Concepts
### Mathematical Notation
- **Continuous state space**: X ⊆ ℝⁿ
- **Discrete modes**: Q = {q₁, q₂, ...}
- **Per-mode continuous regions**: X_entry,i, X_exit,i, X_safe,i
- **Discrete predicates**: pᵢ: X → {true, false} (Boolean functions over continuous state)
### Three Control Mode Types
Each mode type has distinct control objectives and verification methods:
1. **Transitory modes**: Transition between discrete states
- Objective: reach(X_entry) → reach(X_exit) while maintaining x(t) ∈ X_safe
- Verification: Reachability analysis
- Formal: Reach(X_entry, f(x,u), T) ⊆ X_exit ∪ X_safe
2. **Stabilizing modes**: Maintain steady state
- Objective: remain(X_target) where X_target ⊂ X_safe
- Verification: Barrier certificates
- Formal: ∇B(x)·f(x,u) ≤ 0 on boundary ∂X_safe
3. **Expulsory modes**: Safe shutdown under failures
- Objective: reach(X_current) → reach(X_safe_shutdown) under parametric uncertainty
- Verification: Parametric robust reachability
- Formal: Reach(X_current, f(x,u,θ), T) ⊆ X_safe_shutdown for all θ ∈ Θ_failure
### Scope Boundaries
- **Verify** continuous controllers, not **synthesize** them (analogous to model checking)
- Assume controllers can be designed using standard control theory
- Contribution is verification that candidate controllers compose correctly with discrete layer
## Active Development Context
### Current Focus (as of 2026-01-26)
Editing the research approach section (`3-research-approach/v2.tex`) with a Wednesday (2026-01-28) draft deadline.
### Open Technical Questions
Questions are embedded in `v2.tex` comments. Key unresolved issues:
**Easier to address:**
- Hysteresis and sensor noise handling (standard control theory)
- Mealy machine formalization (presentation issue)
- Failure detection scope boundaries (precision in claims)
**More challenging:**
- Timing constraint verification (timed automata integration)
- Parametric uncertainty bounds methodology
- Numerical precision in discrete abstraction (task 36 in taskwarrior)
- Controller design gap (scope vulnerability)
### Taskwarrior Integration
The user tracks tasks in taskwarrior. The Thesis project has ~45 tasks including:
- 9 writing tasks for research approach sections (due 2026-01-28)
- Multiple reading tasks on hybrid systems, reachability, formal methods
- Outstanding question (task 36): "How do we handle numerical barriers when creating discrete automata?"
Use `task list project:Thesis` to see current tasks.
## Bibliography
References are in `references.bib` using IEEE transaction format. The bibliography includes:
- Hybrid systems theory and verification
- Formal methods (reactive synthesis, temporal logic)
- Control theory (reachability, barrier certificates)
- Nuclear regulatory documents (NUREG, 10 CFR)
- Industrial control systems
## Custom LaTeX Class
`dane_proposal_format.cls` provides:
- NSF-compliant formatting (Times New Roman, 1" margins)
- Custom `\task{title}{description}` command for numbered tasks
- TikZ libraries for diagrams
- Table and figure formatting
- Default metadata (title, author, advisor)
## Writing Style Notes
- Inline comments in `.tex` files starting with `%` are working notes
- Comments with `% Q:` indicate open questions requiring research/decisions
- Sections marked with `\iffalse ... \fi` are draft text, not compiled
- Text after `\iffalse` blocks are outlines/notes for future writing

BIN
ERLM_Request_for_Proposals.pdf Normal file
View File

Binary file not shown.

0
README.md Normal file
View File

0
biblatex.sty Normal file
View File

116
dane_proposal_format.cls Normal file
View File

@ -0,0 +1,116 @@
\NeedsTeXFormat{LaTeX2e}
\ProvidesClass{prayer_circle}[2025/09/02 Custom class for academic documents]
% Pass options and load base class
\PassOptionsToClass{12pt,titlepage}{article}
\LoadClass{article}
% Core packages
\RequirePackage[utf8]{inputenc}
\RequirePackage[margin=1.0in]{geometry}
\RequirePackage[hyphens]{url}
% Font selection (NSF compliant)
% Uncomment ONE of the following font options:
\RequirePackage{mathptmx} % Times New Roman (11pt minimum)
% \RequirePackage{mathpazo} % Palatino (10pt minimum)
% \RequirePackage{helvet}\renewcommand{\familydefault}{\sfdefault} % Arial (10pt minimum)
% Default: Computer Modern (11pt minimum) - current 12pt is compliant
% Document formatting
\RequirePackage[small,compact]{titlesec}
\RequirePackage{setspace}
\RequirePackage{datetime}
\RequirePackage{cite}
\RequirePackage{tocbibind}
% Set spacing and numbering
\singlespacing
\setcounter{secnumdepth}{3}
\setcounter{tocdepth}{5}
% Graphics and figures
\RequirePackage{graphicx}
\RequirePackage{pdfpages}
\RequirePackage{rotating}
% \RequirePackage[nolists,nomarkers]{endfloat} % Commented out - uncomment if needed
% TikZ libraries
\RequirePackage{tikz}
\usetikzlibrary{%
positioning,%
shapes,%
arrows,%
graphs,%
calc,%
chains,%
decorations.markings,%
shadows,%
shapes.arrows,%
arrows.meta%
}
% Standalone documents
\RequirePackage{standalone}
% Tables
\RequirePackage{booktabs}
\RequirePackage{tabularx}
\RequirePackage{makecell}
\RequirePackage{dcolumn}
\RequirePackage{multirow}
\RequirePackage{lscape}
\setlength{\belowcaptionskip}{\abovecaptionskip}
% Mathematics
\RequirePackage{amsmath}
\RequirePackage{amssymb}
\RequirePackage{mathrsfs}
% Lists and code
\RequirePackage[inline]{enumitem}
\RequirePackage{listings}
\setlist{noitemsep,listparindent=24pt}
% Specialized packages
\RequirePackage{pgfgantt}
% Custom lengths
\newlength{\figurewidth}
\setlength{\figurewidth}{0.9\textwidth}
\newlength{\figureheight}
\setlength{\figureheight}{0.75\textheight}
% Custom commands and counters
\newcounter{task}
\setcounter{task}{0}
\newcommand{\task}[2]{%
\stepcounter{task}%
\subsubsection{Task \arabic{task}: #1}%
\begin{quote}%
\textit{#2}%
\end{quote}%
}
\newcommand{\emphitem}[1]{\item \emph{#1:}}
% Mathematical notation shortcuts
\newcommand{\mc}[1]{\mathcal{#1}} % calligraphic (Q, X, etc.)
\newcommand{\ms}[1]{\mathscr{#1}} % script
\newcommand{\mf}[1]{\mathfrak{#1}} % Fraktur/Gothic
\newcommand{\bb}[1]{\mathbb{#1}} % blackboard bold (ℝ, ℚ, etc.)
% Default document metadata (can be overridden)
\title{From Cold Start to Critical:\\ Formal Synthesis of Autonomous Hybrid Controllers}
\author{%
PI: Dane A. Sabo\\
dane.sabo@pitt.edu\\
\\
Advisor: Dr. Daniel G. Cole\\
dgcole@pitt.edu\\
\\
Track: PhD Mechanical Engineering
}
\date{\today}

59
main.aux Normal file
View File

@ -0,0 +1,59 @@
\relax
\providecommand \oddpage@label [2]{}
\@writefile{toc}{\contentsline {section}{Contents}{ii}{}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {1}Goals and Outcomes}{1}{}\protected@file@percent }
\citation{NUREG-0899,10CFR50.34}
\citation{10CFR55.59}
\citation{WRPS.Description,gentillon_westinghouse_1999}
\citation{operator_statistics}
\citation{10CFR55}
\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{WNA2020}
\citation{hogberg_root_2013}
\citation{zhang_analysis_2025}
\citation{Kiniry2024}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.3}HARDENS and Formal Methods}{4}{}\protected@file@percent }
\citation{Kiniry2024}
\citation{HANDBOOK ON HYBRID SYSTEMS CONTROL}
\@writefile{toc}{\contentsline {section}{\numberline {3}Research Approach}{6}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}System Requirement and Specifications}{6}{}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {4}Metrics for Success}{7}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{TRL 3 \textit {Critical Function and Proof of Concept}}{7}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{TRL 4 \textit {Laboratory Testing of Integrated Components}}{7}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{TRL 5 \textit {Laboratory Testing in Relevant Environment}}{7}{}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {5}Risks and Contingencies}{9}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {5.1}Computational Tractability of Synthesis}{9}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{9}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{10}{}\protected@file@percent }
\citation{eia_lcoe_2022}
\citation{eesi_datacenter_2024}
\citation{eia_lcoe_2022}
\@writefile{toc}{\contentsline {section}{\numberline {6}Broader Impacts}{12}{}\protected@file@percent }
\bibstyle{ieeetr}
\bibdata{references}
\@writefile{toc}{\contentsline {section}{\numberline {7}Schedule, Milestones, and Deliverables}{14}{}\protected@file@percent }
\gtt@chartextrasize{0}{164.1287pt}
\@writefile{lof}{\contentsline {figure}{\numberline {1}{\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.}}{14}{}\protected@file@percent }
\newlabel{fig:gantt}{{1}{14}{Schedule, Milestones, and Deliverables}{figure.1}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {7.1}Milestones and Deliverables}{14}{}\protected@file@percent }
\bibcite{NUREG-0899}{1}
\bibcite{10CFR50.34}{2}
\bibcite{10CFR55.59}{3}
\bibcite{WRPS.Description}{4}
\bibcite{gentillon_westinghouse_1999}{5}
\bibcite{operator_statistics}{6}
\bibcite{10CFR55}{7}
\bibcite{10CFR50.54}{8}
\bibcite{Kemeny1979}{9}
\bibcite{WNA2020}{10}
\bibcite{hogberg_root_2013}{11}
\bibcite{zhang_analysis_2025}{12}
\bibcite{Kiniry2024}{13}
\bibcite{eia_lcoe_2022}{14}
\bibcite{eesi_datacenter_2024}{15}
\@writefile{toc}{\contentsline {section}{References}{15}{}\protected@file@percent }
\gdef \@abspage@last{19}

52
main.bbl Normal file
View File

@ -0,0 +1,52 @@
\begin{thebibliography}{10}
\bibitem{NUREG-0899}
{U.S. Nuclear Regulatory Commission}, ``Guidelines for the preparation of emergency operating procedures,'' Tech. Rep. NUREG-0899, U.S. Nuclear Regulatory Commission, 1982.
\bibitem{10CFR50.34}
{U.S. Nuclear Regulatory Commission}, ``{10 CFR Part 50.34}.'' Code of Federal Regulations.
\bibitem{10CFR55.59}
{U.S. Nuclear Regulatory Commission}, ``{10 CFR Part 55.59}.'' Code of Federal Regulations.
\bibitem{WRPS.Description}
``{Westinghouse RPS System Description},'' tech. rep., Westinghouse Electric Corporation.
\bibitem{gentillon_westinghouse_1999}
C.~D. Gentillon, D.~Marksberry, D.~Rasmuson, M.~B. Calley, S.~A. Eide, and T.~Wierman, ``Westinghouse reactor protection system unavailability, 1984-1995.''
\newblock Number: {INEEL}/{CON}-99-00374 Publisher: Idaho National Engineering and Environmental Laboratory.
\bibitem{operator_statistics}
{U.S. Nuclear Regulatory Commission}, ``{Operator Licensing}.'' \url{https://www.nrc.gov/reactors/operator-licensing}.
\bibitem{10CFR55}
{U.S. Nuclear Regulatory Commission}, ``{Part 55—Operators' Licenses}.'' \url{https://www.nrc.gov/reading-rm/doc-collections/cfr/part055/full-text}.
\bibitem{10CFR50.54}
{U.S. Nuclear Regulatory Commission}, ``{§ 50.54 Conditions of Licenses}.'' \url{https://www.nrc.gov/reading-rm/doc-collections/cfr/part050/part050-0054}.
\bibitem{Kemeny1979}
J.~G. Kemeny {\em et~al.}, ``Report of the president's commission on the accident at three mile island,'' tech. rep., President's Commission on the Accident at Three Mile Island, October 1979.
\bibitem{WNA2020}
{World Nuclear Association}, ``Safety of nuclear power reactors.'' \url{https://www.world-nuclear.org/information-library/safety-and-security/safety-of-plants/safety-of-nuclear-power-reactors.aspx}, 2020.
\bibitem{hogberg_root_2013}
L.~Högberg, ``Root causes and impacts of severe accidents at large nuclear power plants,'' vol.~42, no.~3, pp.~267--284.
\bibitem{zhang_analysis_2025}
M.~Zhang, L.~Dai, W.~Chen, and E.~Pang, ``Analysis of human errors in nuclear power plant event reports,'' vol.~57, no.~10, p.~103687.
\bibitem{Kiniry2024}
J.~Kiniry, A.~Bakst, S.~Hansen, M.~Podhradsky, and A.~Bivin, ``High assurance rigorous digital engineering for nuclear safety (hardens) final technical report,'' Tech. Rep. TLR-RES-RES/DE-2024-005, Galois, Inc. / U.S. Nuclear Regulatory Commission, 2024.
\newblock NRC Contract 31310021C0014.
\bibitem{eia_lcoe_2022}
{U.S. Energy Information Administration}, ``Levelized costs of new generation resources in the annual energy outlook 2022,'' report, U.S. Energy Information Administration, March 2022.
\newblock See Table 1b, page 9.
\bibitem{eesi_datacenter_2024}
{Environmental and Energy Study Institute}, ``Data center energy needs are upending power grids and threatening the climate.'' Web article, 2024.
\newblock Accessed: 2025-09-29.
\end{thebibliography}

63
main.blg Normal file
View File

@ -0,0 +1,63 @@
This is BibTeX, Version 0.99d (TeX Live 2025)
Capacity: max_strings=200000, hash_size=200000, hash_prime=170003
The top-level auxiliary file: main.aux
White space in argument---line 21 of file main.aux
: \citation{HANDBOOK
: ON HYBRID SYSTEMS CONTROL}
I'm skipping whatever remains of this command
The style file: ieeetr.bst
Database file #1: references.bib
Warning--entry type for "gentillon_westinghouse_1999" isn't style-file defined
--line 32 of file references.bib
Warning--entry type for "operator_statistics" isn't style-file defined
--line 45 of file references.bib
Warning--entry type for "10CFR50.54" isn't style-file defined
--line 59 of file references.bib
Warning--empty author in WRPS.Description
Warning--empty year in WRPS.Description
Warning--empty journal in hogberg_root_2013
Warning--empty year in hogberg_root_2013
Warning--empty journal in zhang_analysis_2025
Warning--empty year in zhang_analysis_2025
You've used 15 entries,
1876 wiz_defined-function locations,
555 strings with 5820 characters,
and the built_in function-call counts, 2404 in all, are:
= -- 221
> -- 100
< -- 2
+ -- 42
- -- 27
* -- 143
:= -- 371
add.period$ -- 18
call.type$ -- 15
change.case$ -- 18
chr.to.int$ -- 0
cite$ -- 21
duplicate$ -- 102
empty$ -- 259
format.name$ -- 27
if$ -- 575
int.to.chr$ -- 0
int.to.str$ -- 15
missing$ -- 2
newline$ -- 52
num.names$ -- 14
pop$ -- 64
preamble$ -- 1
purify$ -- 0
quote$ -- 0
skip$ -- 78
stack$ -- 0
substring$ -- 44
swap$ -- 22
text.length$ -- 2
text.prefix$ -- 0
top$ -- 0
type$ -- 0
warning$ -- 6
while$ -- 18
width$ -- 17
write$ -- 128
(There was 1 error message)

264
main.fdb_latexmk Normal file
View File

@ -0,0 +1,264 @@
# Fdb version 4
["bibtex main"] 1769715964.87129 "main.aux" "main.bbl" "main" 1770062339.7998 2
"./references.bib" 1765591319.20023 14069 2a4f74c587187a8a71049043171eb0fe ""
"/usr/local/texlive/2025/texmf-dist/bibtex/bst/base/ieeetr.bst" 1292289607 18361 1a00e58565e7f19bf2b3e1bfb82254ae ""
"main.aux" 1770062339.59974 3798 3e4f846d5a63c369ad994a87de4a30be "pdflatex"
(generated)
"main.bbl"
"main.blg"
(rewritten before read)
["pdflatex"] 1770062338.22246 "main.tex" "main.pdf" "main" 1770062339.79991 2
"/usr/local/texlive/2025/texmf-dist/fonts/enc/dvips/base/8r.enc" 1165713224 4850 80dc9bab7f31fb78a000ccfed0e27cab ""
"/usr/local/texlive/2025/texmf-dist/fonts/map/fontname/texfonts.map" 1577235249 3524 cb3e574dea2d1052e39280babc910dc8 ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm" 1136768653 1408 5937f58aa508ea2cea4901c07d10f5fe ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/psyro.tfm" 1136768653 1544 23a042a74981a3e4b6ce2e350e390409 ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm" 1136768653 2172 fd0c924230362ff848a33632ed45dc23 ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmb8r.tfm" 1136768653 4524 6bce29db5bc272ba5f332261583fee9c ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmbi7t.tfm" 1136768653 2228 e564491c42a4540b5ebb710a75ff306c ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmbi8r.tfm" 1136768653 4480 10409ed8bab5aea9ec9a78028b763919 ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm" 1136768653 2124 2601a75482e9426d33db523edf23570a ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr8c.tfm" 1136768653 1352 fa28a7e6d323c65ce7d13d5342ff6be2 ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm" 1136768653 4408 25b74d011a4c66b7f212c0cc3c90061b ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm" 1136768653 2288 f478fc8fed18759effb59f3dad7f3084 ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmri8r.tfm" 1136768653 4640 532ca3305aad10cc01d769f3f91f1029 ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm" 1136768653 2232 db256afffc8202da192b4641df14d602 ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7t.tfm" 1136768653 2172 1d00c2a0d10f23031be62329457a870c ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm" 1136768653 1032 20febbd0f0c9a48eb78616f897008286 ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm" 1136768653 1520 ad7b3c1a480a03b3e41b5fbb13d938f2 ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm" 1246382020 916 f87d7c45f9c908e672703b83b72241a3 ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm" 1246382020 908 2921f8a10601f252058503cc6570e581 ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/public/cm/cmmi10.tfm" 1136768653 1528 abec98dbc43e172678c11b3b9031252a ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/public/cm/cmr10.tfm" 1136768653 1296 45809c5a464d5f32c8f98ba97c1bb47f ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/public/cm/cmr12.tfm" 1136768653 1288 655e228510b4c2a1abe905c368440826 ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/public/cm/cmsy10.tfm" 1136768653 1124 6c73e740cf17375f03eec0ee63599741 ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/public/cm/cmtt12.tfm" 1136768653 772 9a936b7f5e2ff0557fce0f62822f0bbf ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/public/rsfs/rsfs10.tfm" 1229303445 688 37338d6ab346c2f1466b29e195316aa4 ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/public/rsfs/rsfs5.tfm" 1229303445 684 3a51bd4fd9600428d5264cf25f04bb9a ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/public/rsfs/rsfs7.tfm" 1229303445 692 1b6510779f0f05e9cbf03e0f6c8361e6 ""
"/usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb" 1248133631 36299 5f9df58c2139e7edcf37c8fca4bd384d ""
"/usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb" 1248133631 35752 024fb6c41858982481f6968b5fc26508 ""
"/usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb" 1248133631 32569 5e5ddc8df908dea60932f3c484a54c0d ""
"/usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt12.pfb" 1248133631 24252 1e4e051947e12dfb50fee0b7f4e26e3a ""
"/usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/symbols/msbm10.pfb" 1248133631 34694 ad62b13721ee8eda1dcc8993c8bd7041 ""
"/usr/local/texlive/2025/texmf-dist/fonts/type1/public/rsfs/rsfs10.pfb" 1229303445 16077 4737ac34f0fb5608550f3780a0202c22 ""
"/usr/local/texlive/2025/texmf-dist/fonts/type1/urw/symbol/usyr.pfb" 1136849748 33709 b09d2e140b7e807d3a97058263ab6693 ""
"/usr/local/texlive/2025/texmf-dist/fonts/type1/urw/times/utmb8a.pfb" 1136849748 44729 811d6c62865936705a31c797a1d5dada ""
"/usr/local/texlive/2025/texmf-dist/fonts/type1/urw/times/utmbi8a.pfb" 1136849748 44656 0cbca70e0534538582128f6b54593cca ""
"/usr/local/texlive/2025/texmf-dist/fonts/type1/urw/times/utmr8a.pfb" 1136849748 46026 6dab18b61c907687b520c72847215a68 ""
"/usr/local/texlive/2025/texmf-dist/fonts/type1/urw/times/utmri8a.pfb" 1136849748 45458 a3faba884469519614ca56ba5f6b1de1 ""
"/usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmb7t.vf" 1136768653 1372 788387fea833ef5963f4c5bffe33eb89 ""
"/usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmbi7t.vf" 1136768653 1384 6ac0f8b839230f5d9389287365b243c0 ""
"/usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmr7t.vf" 1136768653 1380 0ea3a3370054be6da6acd929ec569f06 ""
"/usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmr8c.vf" 1136768653 3556 8a9a6dcbcd146ef985683f677f4758a6 ""
"/usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmri7t.vf" 1136768653 1384 a9d8adaf491ce34e5fba99dc7bbe5f39 ""
"/usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/zptmcm7m.vf" 1136768653 1132 27520247d3fe18d4266a226b461885c2 ""
"/usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/zptmcm7t.vf" 1136768653 1108 d271d6f9de4122c3f8d3b65666167fac ""
"/usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/zptmcm7y.vf" 1136768653 964 5673178ff30617b900214de28ab32b38 ""
"/usr/local/texlive/2025/texmf-dist/tex/context/base/mkii/supp-pdf.mkii" 1461363279 71627 94eb9990bed73c364d7f53f960cc8c5b ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/iftex/iftex.sty" 1734129479 7984 7dbb9280f03c0a315425f1b4f35d43ee ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/iftex/ifvtex.sty" 1572645307 1057 525c2192b5febbd8c1f662c9468335bb ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty" 1701727651 17865 1a9bd36b4f98178fa551aca822290953 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcore.code.tex" 1673816307 1016 1c2b89187d12a2768764b83b4945667c ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorearrows.code.tex" 1601326656 43820 1fef971b75380574ab35a0d37fd92608 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreexternal.code.tex" 1601326656 19324 f4e4c6403dd0f1605fd20ed22fa79dea ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcoregraphicstate.code.tex" 1601326656 6038 ccb406740cc3f03bbfb58ad504fe8c27 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreimage.code.tex" 1673816307 6911 f6d4cf5a3fef5cc879d668b810e82868 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorelayers.code.tex" 1601326656 4883 42daaf41e27c3735286e23e48d2d7af9 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreobjects.code.tex" 1601326656 2544 8c06d2a7f0f469616ac9e13db6d2f842 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathconstruct.code.tex" 1601326656 44195 5e390c414de027626ca5e2df888fa68d ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathprocessing.code.tex" 1601326656 17311 2ef6b2e29e2fc6a2fc8d6d652176e257 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathusage.code.tex" 1601326656 21302 788a79944eb22192a4929e46963a3067 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepatterns.code.tex" 1673816307 9691 3d42d89522f4650c2f3dc616ca2b925e ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepoints.code.tex" 1601326656 33335 dd1fa4814d4e51f18be97d88bf0da60c ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorequick.code.tex" 1601326656 2965 4c2b1f4e0826925746439038172e5d6f ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorerdf.code.tex" 1601326656 5196 2cc249e0ee7e03da5f5f6589257b1e5b ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorescopes.code.tex" 1673816307 20821 7579108c1e9363e61a0b1584778804aa ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreshade.code.tex" 1601326656 35249 abd4adf948f960299a4b3d27c5dddf46 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcoretransformations.code.tex" 1673816307 22012 81b34a0aa8fa1a6158cc6220b00e4f10 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcoretransparency.code.tex" 1601326656 8893 e851de2175338fdf7c17f3e091d94618 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/graphs/tikzlibrarygraphs.code.tex" 1673816307 86723 0209bbf0dbb55cd8213ecb06ebea3349 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryarrows.code.tex" 1601326656 319 225dfe354ba678ff3c194968db39d447 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarybackgrounds.code.tex" 1601326656 4572 4a19637ef65ce88ad2f2d5064b69541d ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarycalc.code.tex" 1601326656 15929 463535aa2c4268fead6674a75c0e8266 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarychains.code.tex" 1673816307 6816 d02c83dff7646998a96988d92df7f6f4 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarydecorations.code.tex" 1673816307 5628 dc0ee4ba7f3e40acae5600067ce833de ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarydecorations.markings.code.tex" 1601326656 788 fb28645a91ec7448ebe79bee60965a88 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryfadings.code.tex" 1601326656 1179 5483d86c1582c569e665c74efab6281f ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarypatterns.code.tex" 1601326656 770 82e332cc9cc48e06b8070d74393a185a ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarypositioning.code.tex" 1601326656 3937 3f208572dd82c71103831da976d74f1a ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshadows.code.tex" 1601326656 2889 d698e3a959304efa342d47e3bb86da5b ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.arrows.code.tex" 1601326656 410 048d1174dabde96757a5387b8f23d968 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.callouts.code.tex" 1601326656 1201 8bd51e254d3ecf0cd2f21edd9ab6f1bb ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.code.tex" 1601326656 494 8de62576191924285b021f4fc4292e16 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.geometric.code.tex" 1601326656 339 be0fe46d92a80e3385dd6a83511a46f2 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.misc.code.tex" 1601326656 329 ba6d5440f8c16779c2384e0614158266 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.multipart.code.tex" 1673816307 923 c7a223b32ffdeb1c839d97935eee61ff ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.symbols.code.tex" 1601326656 475 4b4056fe07caa0603fede9a162fe666d ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarytopaths.code.tex" 1608933718 11518 738408f795261b70ce8dd47459171309 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/tikz.code.tex" 1673816307 186782 af500404a9edec4d362912fe762ded92 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/decorations/pgflibrarydecorations.markings.code.tex" 1601326656 5220 c70346acb7ff99702098460fd6c18993 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/pgflibraryarrows.code.tex" 1601326656 31874 89148c383c49d4c72114a76fd0062299 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/pgflibraryarrows.meta.code.tex" 1601326656 58801 1e750fb0692eb99aaac45698bbec96b1 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/pgflibraryfadings.code.tex" 1601326656 2563 d5b174eb7709fd6bdcc2f70953dbdf8e ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/pgflibrarypatterns.code.tex" 1601326656 7936 49e55444d57eb69a380c6baa35094828 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/pgflibraryplothandlers.code.tex" 1601326656 32995 ac577023e12c0e4bd8aa420b2e852d1a ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.arrows.code.tex" 1673816307 91587 d9b31a3e308b08833e4528a7b4484b4a ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.callouts.code.tex" 1601326656 33336 427c354e28a4802ffd781da22ae9f383 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.geometric.code.tex" 1673816307 161011 76ab54df0aa1a9d3b27a94864771d38d ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.misc.code.tex" 1673816307 46249 d1f322c52d26cf506b4988f31902cd5d ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.multipart.code.tex" 1601326656 62281 aff261ef10ba6cbe8e3c872a38c05a61 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.symbols.code.tex" 1673816307 90521 9d46d4504c2ffed28ff5ef3c43d15f21 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfint.code.tex" 1557692582 3063 8c415c68a0f3394e45cfeca0b65f6ee6 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex" 1673816307 949 cea70942e7b7eddabfb3186befada2e6 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathcalc.code.tex" 1673816307 13270 2e54f2ce7622437bf37e013d399743e3 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfloat.code.tex" 1673816307 104717 9b2393fbf004a0ce7fa688dbce423848 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.base.code.tex" 1601326656 10165 cec5fa73d49da442e56efc2d605ef154 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.basic.code.tex" 1601326656 28178 41c17713108e0795aac6fef3d275fbca ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.code.tex" 1673816307 9649 85779d3d8d573bfd2cd4137ba8202e60 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.comparison.code.tex" 1601326656 3865 ac538ab80c5cf82b345016e474786549 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.integerarithmetics.code.tex" 1557692582 3177 27d85c44fbfe09ff3b2cf2879e3ea434 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.misc.code.tex" 1621110968 11024 0179538121bc2dba172013a3ef89519f ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.random.code.tex" 1673816307 7890 0a86dbf4edfd88d022e0d889ec78cc03 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.round.code.tex" 1601326656 3379 781797a101f647bab82741a99944a229 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.trigonometric.code.tex" 1601326656 92405 f515f31275db273f97b9d8f52e1b0736 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathparser.code.tex" 1673816307 37466 97b0a1ba732e306a1a2034f5a73e239f ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathutil.code.tex" 1601326656 8471 c2883569d03f69e8e1cabfef4999cfd7 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/modules/pgfmoduledecorations.code.tex" 1673816307 71742 3da44a8be6626eef1c400c68776c7a0f ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/modules/pgfmodulematrix.code.tex" 1673816307 21211 1e73ec76bd73964d84197cc3d2685b01 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/modules/pgfmoduleplot.code.tex" 1601326656 16121 346f9013d34804439f7436ff6786cef7 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/modules/pgfmoduleshapes.code.tex" 1673816307 44792 271e2e1934f34c759f4dedb1e14a5015 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/pgf.revision.tex" 1673816307 114 e6d443369d0673933b38834bf99e422d ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgf.cfg" 1601326656 926 2963ea0dcf6cc6c0a770b69ec46a477b ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-common-pdf.def" 1673816307 5542 32f75a31ea6c3a7e1148cd6d5e93dbb7 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-pdftex.def" 1673816307 12612 7774ba67bfd72e593c4436c2de6201e3 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgfsys.code.tex" 1673816307 61351 bc5f86e0355834391e736e97a61abced ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgfsysprotocol.code.tex" 1601326656 1896 b8e0ca0ac371d74c0ca05583f6313c91 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgfsyssoftpath.code.tex" 1601326656 7778 53c8b5623d80238f6a20aa1df1868e63 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfcalendar.code.tex" 1673816307 24149 056c3eb5ebac53bc396649bc52434c12 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgffor.code.tex" 1673816307 24033 d8893a1ec4d1bfa101b172754743d340 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfkeys.code.tex" 1673816307 39784 414c54e866ebab4b801e2ad81d9b21d8 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfkeyslibraryfiltered.code.tex" 1673816307 37433 940bc6d409f1ffd298adfdcaf125dd86 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfrcs.code.tex" 1673816307 4385 510565c2f07998c8a0e14f0ec07ff23c ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfutil-common.tex" 1673816307 29239 22e8c7516012992a49873eff0d868fed ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfutil-latex.def" 1673816307 6950 8524a062d82b7afdc4a88a57cb377784 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/xkeyval/xkeyval.tex" 1655411236 19231 27205ee17aaa2902aea3e0c07a3cfc65 ""
"/usr/local/texlive/2025/texmf-dist/tex/generic/xkeyval/xkvutils.tex" 1655411236 7677 9cb1a74d945bc9331f2181c0a59ff34a ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/adjustbox/adjcalc.sty" 1666037967 5598 c49b91713cbe5e50a1fabefb733eda0d ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/adjustbox/adjustbox.sty" 1740604409 56907 b74d2bd6fed8dc761953edb2fbea781b ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/adjustbox/tc-pdftex.def" 1740604409 4304 461724faa0dfbdec2d80de16c11f407c ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/adjustbox/trimclip.sty" 1740176375 7245 2bf1779563af51e666da8f26ea1f8455 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/amsfonts.sty" 1359763108 5949 3f3fd50a8cc94c3d4cbf4fc66cd3df1c ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/amssymb.sty" 1359763108 13829 94730e64147574077f8ecfea9bb69af4 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsbsy.sty" 1717359999 2222 2166a1f7827be30ddc30434e5efcee1b ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsgen.sty" 1717359999 4173 d22509bc0c91281d991b2de7c88720dd ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsmath.sty" 1730928152 88370 c780f23aea0ece6add91e09b44dca2cd ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsopn.sty" 1717359999 4474 23ca1d3a79a57b405388059456d0a8df ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amstext.sty" 1717359999 2444 71618ea5f2377e33b04fb97afdd0eac2 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/base/article.cls" 1738182759 20144 63d8bacaf52e5abf4db3bc322373e1d4 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/base/ifthen.sty" 1738182759 5525 9dced5929f36b19fa837947f5175b331 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/base/inputenc.sty" 1738182759 5048 0270515b828149155424600fd2d58ac5 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/base/size12.clo" 1738182759 8449 ffe4ba2166a344827c3a832d1d5e0a91 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/booktabs/booktabs.sty" 1579038678 6078 f1cb470c9199e7110a27851508ed7a5c ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/cite/cite.sty" 1425427964 26218 19edeff8cdc2bcb704e8051dc55eb5a7 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/collectbox/collectbox.sty" 1666037909 9124 59c3b56f1a073de66e3eea35f9c173c8 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/colortbl/colortbl.sty" 1720383029 12726 67708fc852a887b2ba598148f60c3756 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/currfile/currfile.sty" 1710537833 11079 d0660dd7678e4c3c56d9890bce94a3e5 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/datetime/datetime-defaults.sty" 1427500626 4105 4c80eaed8cd4f9a80cc6244c0adeb81f ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/datetime/datetime.sty" 1427500626 27587 b023ffe1328fa89e7f133201d87029de ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/enumitem/enumitem.sty" 1738874546 52272 63d293bc0d496619edb57585740861a2 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty" 1579991033 13886 d1306dcf79a944f6988e688c1785f9ce ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/eso-pic/eso-pic.sty" 1683144721 11876 6ef493863ae0d7a984706973240c2237 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/etoolbox/etoolbox.sty" 1739306980 46850 d87daedc2abdc653769a6f1067849fe0 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/filehook/filehook-2020.sty" 1666814490 9005 c47d9138e4a690658bcefab0dd0af8d7 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/filehook/filehook.sty" 1666814490 1210 95c2d0abf75beadf7e7547b73b345c24 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/filemod/filemod-expmin.sty" 1316560476 2845 2b7393c472a738889b77cb266b9ef35d ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/fmtcount/fc-english.def" 1739135561 13002 b14af1bcf50fb2c1b95ba5f32e7fc962 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/fmtcount/fcnumparser.sty" 1739135561 11038 6f51846fb936ca8566fb2a1c957c6dab ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/fmtcount/fcprefix.sty" 1739135561 10747 3648e4fffb9f130ffceebed92b30d963 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/fmtcount/fmtcount.sty" 1739135561 29567 3875eaa69e0aae20dbf9ea7da73cb26a ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/geometry/geometry.sty" 1578002852 41601 9cf6c5257b1bc7af01a58859749dd37a ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/gincltex/gincltex.sty" 1315265409 3594 7c105130ddd1211e8275b3c1288d84c8 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/graphics-cfg/color.cfg" 1459978653 1213 620bba36b25224fa9b7e1ccb4ecb76fd ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/graphics-cfg/graphics.cfg" 1465944070 1224 978390e9c2234eab29404bc21b268d1e ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/graphics-def/pdftex.def" 1713382759 19440 9da9dcbb27470349a580fca7372d454b ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/graphics/color.sty" 1730496337 7245 57f7defed4fb41562dc4b6ca13958ca9 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/graphics/graphics.sty" 1730496337 18363 dee506cb8d56825d8a4d020f5d5f8704 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/graphics/graphicx.sty" 1717359999 8010 6f2ad8c2b2ffbd607af6475441c7b5e4 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/graphics/keyval.sty" 1717359999 2671 70891d50dac933918b827d326687c6e8 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/graphics/lscape.sty" 1717359999 1822 ce7e39e35ea3027d24b527bd5c5034d5 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/graphics/mathcolor.ltx" 1667332637 2885 9c645d672ae17285bba324998918efd8 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/graphics/rotating.sty" 1717359999 7060 c21bdf2a03ef9298ad94a39d4110f07c ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/graphics/trig.sty" 1717359999 4023 2c9f39712cf7b43d3eb93a8bbd5c8f67 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/ifoddpage/ifoddpage.sty" 1666126449 2142 eae42205b97b7a3ad0e58db5fe99e3e6 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/jknapltx/mathrsfs.sty" 1137110241 300 12fa6f636b617656f2810ee82cb05015 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/jknapltx/ursfs.fd" 1137110241 548 cc4e3557704bfed27c7002773fad6c90 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/kvoptions/kvoptions.sty" 1655478651 22555 6d8e155cfef6d82c3d5c742fea7c992e ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/kvsetkeys/kvsetkeys.sty" 1665067230 13815 760b0c02f691ea230f5359c4e1de23a7 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def" 1716410060 29785 9f93ab201fe5dd053afcc6c1bcf7d266 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg" 1279039959 678 4792914a8f45be57bb98413425e4c7af ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/listings/listings.cfg" 1727126400 1865 301ae3c26fb8c0243307b619a6aa2dd3 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/listings/listings.sty" 1727126400 81640 997090b6c021dc4af9ee00a97b85c5b4 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/listings/lstmisc.sty" 1727126400 77051 be68720e5402397a830abb9eed5a2cb4 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/listings/lstpatch.sty" 1710360531 353 9024412f43e92cd5b21fe9ded82d0610 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/makecell/makecell.sty" 1249334690 15773 2dd7dde1ec1c2a3d0c85bc3b273e04d8 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/multirow/multirow.sty" 1731446765 6696 886c9f3087d0b973ed2c19aa79cb3023 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/pdflscape/pdflscape-nometadata.sty" 1667072951 6572 ea530fbbe537629fd97736d33babc07d ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/pdflscape/pdflscape.sty" 1667072951 2224 1230ab76aa62221ccbd90bca8c8c015e ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/pdfpages/pdfpages.sty" 1738442568 56557 52caee30c1fe86973ee17a572171abb0 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/pdfpages/pppdftex.def" 1738442568 6446 d89a65b3f6b4b32146b499348640e1cf ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/pgf/basiclayer/pgf.sty" 1601326656 1090 bae35ef70b3168089ef166db3e66f5b2 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/pgf/basiclayer/pgfcore.sty" 1673816307 373 00b204b1d7d095b892ad31a7494b0373 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/pgf/compatibility/pgfcomp-version-0-65.sty" 1601326656 21013 f4ff83d25bb56552493b030f27c075ae ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/pgf/compatibility/pgfcomp-version-1-18.sty" 1601326656 989 c49c8ae06d96f8b15869da7428047b1e ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/pgf/frontendlayer/tikz.sty" 1601326656 339 c2e180022e3afdb99c7d0ea5ce469b7d ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/pgf/math/pgfmath.sty" 1601326656 306 c56a323ca5bf9242f54474ced10fca71 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/pgf/systemlayer/pgfsys.sty" 1601326656 443 8c872229db56122037e86bcda49e14f3 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/pgf/utilities/pgfcalendar.sty" 1601326656 328 7411531f2e9e5c6aa139c84fbe10702e ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/pgf/utilities/pgffor.sty" 1601326656 348 ee405e64380c11319f0e249fed57e6c5 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/pgf/utilities/pgfkeys.sty" 1601326656 274 5ae372b7df79135d240456a1c6f2cf9a ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/pgf/utilities/pgfrcs.sty" 1601326656 325 f9f16d12354225b7dd52a3321f085955 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/pgfgantt/pgfgantt.sty" 1718825887 47792 a7e008294ecd88e823d949404eb72b1c ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/mathptmx.sty" 1586716065 4631 6e41de2b7a83dfa5d2c4b0a2fe01f046 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/omlztmcm.fd" 1137110629 411 12564a37a279e4e0b533cdf5e03eeb7c ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/omsztmcm.fd" 1137110629 348 f4ce75d394e7d9ac12ca7aac4045ed77 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/omxztmcm.fd" 1137110629 329 c8cddcc90b6f567b28408eb374773c9c ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/ot1ptm.fd" 1137110629 961 15056f4a61917ceed3a44e4ac11fcc52 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/ot1ztmcm.fd" 1137110629 329 aee7226812ba4138ac67a018466b488d ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/ts1ptm.fd" 1137110629 619 96f56dc5d1ef1fe1121f1cfeec70ee0c ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/setspace/setspace.sty" 1670275497 22490 8cac309b79a4c53a4ffce4b1b07aead0 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/standalone/standalone.sty" 1740345147 34855 da6c70080898b3166f2c1d8f28ed2602 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/svn-prov/svn-prov.sty" 1272330018 6852 44ea8d7e58290cde708a34ebf3953571 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/titlesec/titlesec.sty" 1736023606 48766 87a17a4ef312a39cd43896e34a679a56 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/tocbibind/tocbibind.sty" 1287012853 8927 46f54e33fc9cef24f78ab3bc811cb63f ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/tools/array.sty" 1730496337 14552 27664839421e418b87f56fa4c6f66b1a ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/tools/calc.sty" 1717359999 10214 61188260d324e94bc2f66825d7d3fdf4 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/tools/dcolumn.sty" 1717359999 2758 86fa9d68b26327d0f1d7a6c34674f4f8 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/tools/shellesc.sty" 1717359999 4121 6039ae6d0916154d7ba5f20a77b9ab2c ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/tools/tabularx.sty" 1717359999 7243 e5dac1240636811edb77568b81818372 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/url/url.sty" 1388531844 12796 8edb7d69a20b857904dd0ea757c14ec9 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/varwidth/varwidth.sty" 1238697683 10894 d359a13923460b2a73d4312d613554c8 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/xcolor/xcolor.sty" 1727642399 55384 b454dec21c2d9f45ec0b793f0995b992 ""
"/usr/local/texlive/2025/texmf-dist/tex/latex/xkeyval/xkeyval.sty" 1655411236 4937 4ce600ce9bd4ec84d0250eb6892fcf4f ""
"/usr/local/texlive/2025/texmf-dist/web2c/texmf.cnf" 1739380943 42148 61becc7c670cd061bb319c643c27fdd4 ""
"/usr/local/texlive/2025/texmf-var/fonts/map/pdftex/updmap/pdftex.map" 1765668892 5467155 19efa205003f9ecad95fbbaa6ff24da1 ""
"/usr/local/texlive/2025/texmf-var/web2c/pdftex/pdflatex.fmt" 1741450574 3345740 46b66fdb0378f7bf5921b5eabf1762b8 ""
"/usr/local/texlive/2025/texmf.cnf" 1741450484 577 418a7058ec8e006d8704f60ecd22c938 ""
"1-goals-and-outcomes/research_statement_v1.tex" 1765591319.18896 4450 070caee751214eaddffa6b3403f8ed43 ""
"1-goals-and-outcomes/v1.tex" 1765591319.1893 5825 07f6fba24cfa050a3b2b00c416f0f45f ""
"2-state-of-the-art/v1.tex" 1765591319.1898 10609 44863eb08e23052a1623ef3ebcb1e3ae ""
"3-research-approach/v2.tex" 1770062336.52686 22203 b3b90c4fbb94cd85cdcce085ec1b2a8a ""
"4-metrics-of-success/v1.tex" 1765591319.19036 5586 e5fb80ced00bcdc318ffe3861b0064bc ""
"5-risks-and-contingencies/v1.tex" 1765591319.19058 10412 17e755aa8451c45198372af7afe3c500 ""
"6-broader-impacts/v1.tex" 1765591319.19072 4834 418aae223b778759691eaf9124a5360c ""
"8-schedule/v1.tex" 1765591319.19095 4473 8ad96bbf9cedf2ea09298ecbd4e01b83 ""
"dane_proposal_format.cls" 1769715785.9835 2883 ea175794171aa0291ef71716b2190bf0 ""
"main.aux" 1770062339.59974 3798 3e4f846d5a63c369ad994a87de4a30be "pdflatex"
"main.bbl" 1769715964.93568 2919 0ea026a17b15c1ad2ed657bdbf26dfdc "bibtex main"
"main.tex" 1769453692.01808 954 ea089365572626745e262fed177e4fa3 ""
"main.toc" 1770062339.60048 1565 b9f0d6ea3d8646810f16fc895e4d44da "pdflatex"
(generated)
"main.aux"
"main.log"
"main.pdf"
"main.toc"
(rewritten before read)

564
main.fls Normal file
View File

@ -0,0 +1,564 @@
PWD /Users/danesabo/Documents/Dane's Vault/Writing/THESIS_PROPOSAL
INPUT /usr/local/texlive/2025/texmf.cnf
INPUT /usr/local/texlive/2025/texmf-dist/web2c/texmf.cnf
INPUT /usr/local/texlive/2025/texmf-var/web2c/pdftex/pdflatex.fmt
INPUT main.tex
OUTPUT main.log
INPUT ./dane_proposal_format.cls
INPUT dane_proposal_format.cls
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/base/article.cls
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/base/article.cls
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/base/size12.clo
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/base/size12.clo
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/base/size12.clo
INPUT /usr/local/texlive/2025/texmf-dist/fonts/map/fontname/texfonts.map
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/cm/cmr12.tfm
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/base/inputenc.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/base/inputenc.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/geometry/geometry.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/geometry/geometry.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics/keyval.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics/keyval.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/iftex/ifvtex.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/iftex/ifvtex.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/iftex/iftex.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/iftex/iftex.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/url/url.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/url/url.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/mathptmx.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/mathptmx.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/titlesec/titlesec.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/titlesec/titlesec.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/setspace/setspace.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/setspace/setspace.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/datetime/datetime.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/datetime/datetime.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/etoolbox/etoolbox.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/etoolbox/etoolbox.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/fmtcount/fmtcount.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/fmtcount/fmtcount.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/base/ifthen.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/base/ifthen.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/xkeyval/xkeyval.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/xkeyval/xkeyval.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/xkeyval/xkeyval.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/xkeyval/xkvutils.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/fmtcount/fcprefix.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/fmtcount/fcprefix.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/fmtcount/fcnumparser.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/fmtcount/fcnumparser.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsgen.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsgen.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/datetime/datetime-defaults.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/datetime/datetime-defaults.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/cite/cite.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/cite/cite.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/tocbibind/tocbibind.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/tocbibind/tocbibind.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics/graphicx.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics/graphicx.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics/graphics.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics/graphics.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics/trig.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics/trig.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics-cfg/graphics.cfg
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics-cfg/graphics.cfg
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics-cfg/graphics.cfg
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics-def/pdftex.def
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics-def/pdftex.def
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics-def/pdftex.def
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pdfpages/pdfpages.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pdfpages/pdfpages.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/tools/calc.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/tools/calc.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/eso-pic/eso-pic.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/eso-pic/eso-pic.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/xcolor/xcolor.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/xcolor/xcolor.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/xcolor/xcolor.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics-cfg/color.cfg
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics-cfg/color.cfg
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics-cfg/color.cfg
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics/mathcolor.ltx
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics/mathcolor.ltx
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics/mathcolor.ltx
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pdfpages/pppdftex.def
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pdfpages/pppdftex.def
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pdfpages/pppdftex.def
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics/rotating.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics/rotating.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/frontendlayer/tikz.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/frontendlayer/tikz.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/basiclayer/pgf.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/basiclayer/pgf.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/utilities/pgfrcs.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/utilities/pgfrcs.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfutil-common.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfutil-latex.def
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfrcs.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfrcs.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfrcs.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/pgf.revision.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/pgf.revision.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/basiclayer/pgfcore.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/basiclayer/pgfcore.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/systemlayer/pgfsys.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/systemlayer/pgfsys.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgfsys.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgfsys.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgfsys.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfkeys.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfkeyslibraryfiltered.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgf.cfg
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-pdftex.def
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-pdftex.def
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-common-pdf.def
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgfsyssoftpath.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgfsyssoftpath.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgfsyssoftpath.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgfsysprotocol.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgfsysprotocol.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/systemlayer/pgfsysprotocol.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcore.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcore.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcore.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathutil.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathparser.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.basic.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.trigonometric.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.random.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.comparison.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.base.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.round.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.misc.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.integerarithmetics.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathcalc.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmathfloat.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfint.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepoints.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathconstruct.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathusage.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorescopes.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcoregraphicstate.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcoretransformations.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorequick.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreobjects.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathprocessing.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorearrows.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreshade.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreimage.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreexternal.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorelayers.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcoretransparency.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepatterns.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/basiclayer/pgfcorerdf.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/modules/pgfmoduleshapes.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/modules/pgfmoduleplot.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/compatibility/pgfcomp-version-0-65.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/compatibility/pgfcomp-version-0-65.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/compatibility/pgfcomp-version-1-18.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/compatibility/pgfcomp-version-1-18.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/utilities/pgffor.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/utilities/pgffor.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/utilities/pgfkeys.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/utilities/pgfkeys.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfkeys.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfkeys.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfkeys.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/math/pgfmath.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/math/pgfmath.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgffor.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgffor.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgffor.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/tikz.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/tikz.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/tikz.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/pgflibraryplothandlers.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/pgflibraryplothandlers.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/modules/pgfmodulematrix.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarytopaths.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarytopaths.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarypositioning.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarypositioning.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.geometric.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.geometric.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.geometric.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.geometric.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.misc.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.misc.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.misc.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.misc.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.symbols.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.symbols.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.symbols.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.symbols.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.arrows.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.arrows.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.arrows.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.arrows.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.callouts.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.callouts.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.callouts.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.callouts.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.multipart.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.multipart.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.multipart.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.multipart.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryarrows.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryarrows.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/pgflibraryarrows.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/pgflibraryarrows.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/graphs/tikzlibrarygraphs.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/graphs/tikzlibrarygraphs.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarycalc.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarycalc.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarychains.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarychains.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarydecorations.markings.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarydecorations.markings.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarydecorations.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarydecorations.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/modules/pgfmoduledecorations.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/decorations/pgflibrarydecorations.markings.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/decorations/pgflibrarydecorations.markings.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshadows.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshadows.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryfadings.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryfadings.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/pgflibraryfadings.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/pgflibraryfadings.code.tex
OUTPUT main.pdf
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/pgflibraryarrows.meta.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/pgflibraryarrows.meta.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/pgflibraryarrows.meta.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/standalone/standalone.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/standalone/standalone.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/tools/shellesc.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/tools/shellesc.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/tools/shellesc.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/currfile/currfile.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/currfile/currfile.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/kvoptions/kvoptions.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/kvoptions/kvoptions.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/kvsetkeys/kvsetkeys.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/kvsetkeys/kvsetkeys.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/filehook/filehook.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/filehook/filehook.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/filehook/filehook-2020.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/filehook/filehook-2020.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/gincltex/gincltex.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/gincltex/gincltex.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/gincltex/gincltex.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/svn-prov/svn-prov.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/svn-prov/svn-prov.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/adjustbox/adjustbox.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/adjustbox/adjustbox.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/adjustbox/adjcalc.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/adjustbox/adjcalc.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/adjustbox/trimclip.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/adjustbox/trimclip.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/collectbox/collectbox.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/collectbox/collectbox.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/adjustbox/tc-pdftex.def
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/adjustbox/tc-pdftex.def
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/adjustbox/tc-pdftex.def
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/ifoddpage/ifoddpage.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/ifoddpage/ifoddpage.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/ifoddpage/ifoddpage.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/varwidth/varwidth.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/varwidth/varwidth.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/varwidth/varwidth.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/filemod/filemod-expmin.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/filemod/filemod-expmin.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/booktabs/booktabs.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/booktabs/booktabs.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/tools/tabularx.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/tools/tabularx.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/tools/array.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/tools/array.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/makecell/makecell.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/makecell/makecell.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/tools/dcolumn.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/tools/dcolumn.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/multirow/multirow.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/multirow/multirow.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics/lscape.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics/lscape.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsmath.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsmath.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsopn.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amstext.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amstext.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsbsy.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsbsy.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsopn.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/amssymb.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/amssymb.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/amsfonts.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/amsfonts.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/jknapltx/mathrsfs.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/jknapltx/mathrsfs.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/enumitem/enumitem.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/enumitem/enumitem.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/listings/listings.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/listings/listings.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/listings/lstpatch.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/listings/lstpatch.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/listings/lstpatch.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/listings/lstmisc.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/listings/lstmisc.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/listings/lstmisc.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/listings/listings.cfg
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/listings/listings.cfg
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/listings/listings.cfg
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgfgantt/pgfgantt.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgfgantt/pgfgantt.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarybackgrounds.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarybackgrounds.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarypatterns.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarypatterns.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/pgflibrarypatterns.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/libraries/pgflibrarypatterns.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/utilities/pgfcalendar.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pgf/utilities/pgfcalendar.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfcalendar.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfcalendar.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfcalendar.code.tex
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/colortbl/colortbl.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/colortbl/colortbl.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics/color.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/ot1ptm.fd
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/ot1ptm.fd
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/ot1ptm.fd
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def
INPUT ./main.aux
INPUT ./main.aux
INPUT main.aux
OUTPUT main.aux
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/fmtcount/fc-english.def
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/fmtcount/fc-english.def
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/fmtcount/fc-english.def
INPUT /usr/local/texlive/2025/texmf-dist/tex/context/base/mkii/supp-pdf.mkii
INPUT /usr/local/texlive/2025/texmf-dist/tex/context/base/mkii/supp-pdf.mkii
INPUT /usr/local/texlive/2025/texmf-dist/tex/context/base/mkii/supp-pdf.mkii
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pdflscape/pdflscape.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pdflscape/pdflscape.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pdflscape/pdflscape-nometadata.sty
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/pdflscape/pdflscape-nometadata.sty
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/ot1ztmcm.fd
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/ot1ztmcm.fd
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/ot1ztmcm.fd
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7t.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7t.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7t.tfm
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/omlztmcm.fd
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/omlztmcm.fd
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/omlztmcm.fd
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/omsztmcm.fd
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/omsztmcm.fd
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/omsztmcm.fd
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/omxztmcm.fd
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/omxztmcm.fd
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/omxztmcm.fd
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/jknapltx/ursfs.fd
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/jknapltx/ursfs.fd
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/jknapltx/ursfs.fd
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/rsfs/rsfs10.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/rsfs/rsfs10.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/rsfs/rsfs10.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmr7t.vf
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm
INPUT /usr/local/texlive/2025/texmf-var/fonts/map/pdftex/updmap/pdftex.map
INPUT /usr/local/texlive/2025/texmf-dist/fonts/enc/dvips/base/8r.enc
INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmr7t.vf
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmr7t.vf
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm
INPUT ./1-goals-and-outcomes/research_statement_v1.tex
INPUT ./1-goals-and-outcomes/research_statement_v1.tex
INPUT 1-goals-and-outcomes/research_statement_v1.tex
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmr7t.vf
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmri7t.vf
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmri8r.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm
INPUT ./main.toc
INPUT ./main.toc
INPUT main.toc
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7t.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7t.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7t.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/rsfs/rsfs10.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/rsfs/rsfs10.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/rsfs/rsfs7.tfm
OUTPUT main.toc
INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmb7t.vf
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmb8r.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmb7t.vf
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmb8r.tfm
INPUT ./1-goals-and-outcomes/v1.tex
INPUT ./1-goals-and-outcomes/v1.tex
INPUT ./1-goals-and-outcomes/v1.tex
INPUT ./1-goals-and-outcomes/v1.tex
INPUT 1-goals-and-outcomes/v1.tex
INPUT ./2-state-of-the-art/v1.tex
INPUT ./2-state-of-the-art/v1.tex
INPUT ./2-state-of-the-art/v1.tex
INPUT ./2-state-of-the-art/v1.tex
INPUT 2-state-of-the-art/v1.tex
INPUT ./3-research-approach/v2.tex
INPUT ./3-research-approach/v2.tex
INPUT ./3-research-approach/v2.tex
INPUT ./3-research-approach/v2.tex
INPUT 3-research-approach/v2.tex
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7t.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7t.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7t.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/rsfs/rsfs10.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/rsfs/rsfs5.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/ts1ptm.fd
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/ts1ptm.fd
INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/ts1ptm.fd
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr8c.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmr7t.vf
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/zptmcm7m.vf
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/psyro.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/cm/cmmi10.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/zptmcm7t.vf
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/cm/cmr10.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/zptmcm7y.vf
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/cm/cmsy10.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmr8c.vf
INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/zptmcm7m.vf
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/psyro.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/cm/cmmi10.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmri8r.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmr7t.vf
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmr7t.vf
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm
INPUT ./4-metrics-of-success/v1.tex
INPUT ./4-metrics-of-success/v1.tex
INPUT ./4-metrics-of-success/v1.tex
INPUT ./4-metrics-of-success/v1.tex
INPUT 4-metrics-of-success/v1.tex
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmbi7t.tfm
INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmbi7t.vf
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmbi8r.tfm
INPUT ./5-risks-and-contingencies/v1.tex
INPUT ./5-risks-and-contingencies/v1.tex
INPUT ./5-risks-and-contingencies/v1.tex
INPUT ./5-risks-and-contingencies/v1.tex
INPUT 5-risks-and-contingencies/v1.tex
INPUT ./6-broader-impacts/v1.tex
INPUT ./6-broader-impacts/v1.tex
INPUT ./6-broader-impacts/v1.tex
INPUT ./6-broader-impacts/v1.tex
INPUT 6-broader-impacts/v1.tex
INPUT ./8-schedule/v1.tex
INPUT ./8-schedule/v1.tex
INPUT ./8-schedule/v1.tex
INPUT ./8-schedule/v1.tex
INPUT 8-schedule/v1.tex
INPUT ./main.bbl
INPUT ./main.bbl
INPUT main.bbl
INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/cm/cmtt12.tfm
INPUT main.aux
INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb
INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb
INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb
INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt12.pfb
INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/symbols/msbm10.pfb
INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/rsfs/rsfs10.pfb
INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/urw/symbol/usyr.pfb
INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/urw/times/utmb8a.pfb
INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/urw/times/utmbi8a.pfb
INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/urw/times/utmr8a.pfb
INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/urw/times/utmri8a.pfb

1000
main.log Normal file
View File

File diff suppressed because it is too large Load Diff

BIN
main.pdf Normal file
View File

Binary file not shown.

BIN
main.synctex.gz Normal file
View File

Binary file not shown.

45
main.tex Normal file
View File

@ -0,0 +1,45 @@
\documentclass{dane_proposal_format}
\usepackage{booktabs} % For professional tables
\usepackage{tabularx} % For flexible table columns
\usepackage{multirow} % For multi-row cells
\usepackage{array} % Enhanced table formatting
\usepackage[table]{xcolor} % For colored tables (optional)
\usepackage{pgfgantt}
\usepackage{pdfpages} % For including PDF files
\begin{document}
\pagenumbering{roman}
\maketitle
\input{1-goals-and-outcomes/research_statement_v1.tex}
\newpage
\tableofcontents
\newpage
\pagenumbering{arabic}
\input{1-goals-and-outcomes/v1}
\newpage
\input{2-state-of-the-art/v1}
\newpage
\input{3-research-approach/v2}
\newpage
\input{4-metrics-of-success/v1}
\newpage
\input{5-risks-and-contingencies/v1}
\newpage
\input{6-broader-impacts/v1}
\newpage
\input{8-schedule/v1}
\bibliographystyle{ieeetr}
\bibliography{references}
% White Paper (optional)
% \input{whitepaper/v1}
\end{document}

20
main.toc Normal file
View File

@ -0,0 +1,20 @@
\contentsline {section}{Contents}{ii}{}%
\contentsline {section}{\numberline {1}Goals and Outcomes}{1}{}%
\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.2}Human Factors in Nuclear Accidents}{3}{}%
\contentsline {subsection}{\numberline {2.3}HARDENS and Formal Methods}{4}{}%
\contentsline {section}{\numberline {3}Research Approach}{6}{}%
\contentsline {subsection}{\numberline {3.1}System Requirement and Specifications}{6}{}%
\contentsline {section}{\numberline {4}Metrics for Success}{7}{}%
\contentsline {paragraph}{TRL 3 \textit {Critical Function and Proof of Concept}}{7}{}%
\contentsline {paragraph}{TRL 4 \textit {Laboratory Testing of Integrated Components}}{7}{}%
\contentsline {paragraph}{TRL 5 \textit {Laboratory Testing in Relevant Environment}}{7}{}%
\contentsline {section}{\numberline {5}Risks and Contingencies}{9}{}%
\contentsline {subsection}{\numberline {5.1}Computational Tractability of Synthesis}{9}{}%
\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{9}{}%
\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{10}{}%
\contentsline {section}{\numberline {6}Broader Impacts}{12}{}%
\contentsline {section}{\numberline {7}Schedule, Milestones, and Deliverables}{14}{}%
\contentsline {subsection}{\numberline {7.1}Milestones and Deliverables}{14}{}%
\contentsline {section}{References}{15}{}%

311
references.bib Normal file
View File

@ -0,0 +1,311 @@
@techreport{NUREG-0899,
title = {Guidelines for the Preparation of Emergency Operating Procedures},
author = {{U.S. Nuclear Regulatory Commission}},
institution = {U.S. Nuclear Regulatory Commission},
year = {1982},
number = {NUREG-0899}
}
@misc{10CFR50.34,
title = {{10 CFR Part 50.34}},
author = {{U.S. Nuclear Regulatory Commission}},
howpublished = {Code of Federal Regulations},
urldate = {2025-12-05},
url = {https://www.nrc.gov/reading-rm/doc-collections/cfr/part050/part050-0034}
}
@misc{10CFR55.59,
title = {{10 CFR Part 55.59}},
author = {{U.S. Nuclear Regulatory Commission}},
howpublished = {Code of Federal Regulations},
urldate = {2025-12-05},
url = {https://www.nrc.gov/reading-rm/doc-collections/cfr/part055/part055-0059}
}
@techreport{WRPS.Description,
title = {{Westinghouse RPS System Description}},
institution = {Westinghouse Electric Corporation},
url = {https://nrcoe.inl.gov/publicdocs/SystemStudies/rps-w-description.pdf},
urldate = {2025-12-05}
}
@online{gentillon_westinghouse_1999,
title = {Westinghouse Reactor Protection System Unavailability, 1984-1995},
url = {https://digital.library.unt.edu/ark:/67531/metadc620476/},
titleaddon = {{PSA} '99, Washington, {DC} ({US}), 08/22/1999--08/25/1999},
type = {Article},
author = {Gentillon, C. D. and Marksberry, D. and Rasmuson, D. and Calley, M. B. and Eide, S. A. and Wierman, T.},
urldate = {2025-12-05},
date = {1999-08-01},
note = {Number: {INEEL}/{CON}-99-00374
Publisher: Idaho National Engineering and Environmental Laboratory},
file = {Full Text PDF:/home/danesabo/Zotero/storage/7QKWQ8NI/Gentillon et al. - 1999 - Westinghouse Reactor Protection System Unavailability, 1984-1995.pdf:application/pdf},
}
@online{operator_statistics,
title = {{Operator Licensing}},
author = {{U.S. Nuclear Regulatory Commission}},
howpublished = {\url{https://www.nrc.gov/reactors/operator-licensing}},
urldate = {2025-11-28},
file = {Operator Licensing | Nuclear Regulatory Commission:/home/danesabo/Zotero/storage/KUP9B5GH/operator-licensing.html:text/html},
}
@misc{10CFR55,
title = {{Part 55—Operators' Licenses}},
author = {{U.S. Nuclear Regulatory Commission}},
howpublished = {\url{https://www.nrc.gov/reading-rm/doc-collections/cfr/part055/full-text}},
}
@online{10CFR50.54,
title = {{§ 50.54 Conditions of Licenses}},
author = {{U.S. Nuclear Regulatory Commission}},
howpublished = {\url{https://www.nrc.gov/reading-rm/doc-collections/cfr/part050/part050-0054}},
urldate = {2025-11-28},
file = {§ 50.54 Conditions of licenses. | Nuclear Regulatory Commission:/home/danesabo/Zotero/storage/THTZUD3T/part050-0054.html:text/html},
}
@techreport{Kemeny1979,
title = {Report of the President's Commission on the Accident at Three Mile Island},
author = {Kemeny, John G. and others},
institution = {President's Commission on the Accident at Three Mile Island},
year = {1979},
month = {October}
}
@misc{WNA2020,
title = {Safety of Nuclear Power Reactors},
author = {{World Nuclear Association}},
year = {2020},
howpublished = {\url{https://www.world-nuclear.org/information-library/safety-and-security/safety-of-plants/safety-of-nuclear-power-reactors.aspx}}
}
@article{hogberg_root_2013,
title = {Root Causes and Impacts of Severe Accidents at Large Nuclear Power Plants},
volume = {42},
issn = {0044-7447},
url = {https://pmc.ncbi.nlm.nih.gov/articles/PMC3606704/},
doi = {10.1007/s13280-013-0382-x},
pages = {267--284},
number = {3},
journaltitle = {Ambio},
shortjournal = {Ambio},
author = {Högberg, Lars},
urldate = {2025-12-05},
date = {2013-04},
pmid = {23423737},
pmcid = {PMC3606704},
file = {Full Text:/home/danesabo/Zotero/storage/E8F2QZGR/Högberg - 2013 - Root Causes and Impacts of Severe Accidents at Large Nuclear Power Plants.pdf:application/pdf},
}
@article{zhang_analysis_2025,
title = {Analysis of human errors in nuclear power plant event reports},
volume = {57},
issn = {1738-5733},
url = {https://www.sciencedirect.com/science/article/pii/S1738573325002554},
doi = {10.1016/j.net.2025.103687},
pages = {103687},
number = {10},
journaltitle = {Nuclear Engineering and Technology},
shortjournal = {Nuclear Engineering and Technology},
author = {Zhang, Meihui and Dai, Licao and Chen, Wenming and Pang, Ensheng},
urldate = {2025-12-05},
date = {2025-10-01},
keywords = {Active errors, {HFACS} model, Latent errors, Licensee event reports},
file = {ScienceDirect Snapshot:/home/danesabo/Zotero/storage/N5R2Z3GL/S1738573325002554.html:text/html},
}
@techreport{Kiniry2024,
title = {High Assurance Rigorous Digital Engineering for Nuclear Safety (HARDENS) Final Technical Report},
author = {Kiniry, Joseph and Bakst, Alexander and Hansen, Simon and Podhradsky, Michal and Bivin, Andrew},
institution = {Galois, Inc. / U.S. Nuclear Regulatory Commission},
year = {2024},
number = {TLR-RES-RES/DE-2024-005},
note = {NRC Contract 31310021C0014}
}
@techreport{eia_lcoe_2022,
author = {{U.S. Energy Information Administration}},
title = {Levelized Costs of New Generation Resources in the Annual Energy Outlook 2022},
institution = {U.S. Energy Information Administration},
year = {2022},
month = {March},
type = {Report},
url = {https://www.eia.gov/outlooks/aeo/pdf/electricity_generation.pdf},
note = {See Table 1b, page 9}
}
@misc{eesi_datacenter_2024,
author = {{Environmental and Energy Study Institute}},
title = {Data Center Energy Needs Are Upending Power Grids and Threatening the Climate},
howpublished = {Web article},
year = {2024},
url = {https://www.eesi.org/articles/view/data-center-energy-needs-are-upending-power-grids-and-threatening-the-climate},
note = {Accessed: 2025-09-29}
}
@book{baier_principles_2008,
location = {Cambridge, {MA}, {USA}},
title = {Principles of Model Checking},
isbn = {978-0-262-02649-9},
abstract = {A comprehensive introduction to the foundations of model checking, a fully automated technique for finding flaws in hardware and software; with extensive examples and both practical and theoretical exercises.},
pagetotal = {984},
publisher = {{MIT} Press},
author = {Baier, Christel and Katoen, Joost-Pieter},
date = {2008-04-25},
langid = {english},
}
@inproceedings{katis_capture_2022,
location = {Cham},
title = {Capture, Analyze, Diagnose: Realizability Checking Of Requirements in {FRET}},
isbn = {978-3-031-13188-2},
doi = {10.1007/978-3-031-13188-2_24},
shorttitle = {Capture, Analyze, Diagnose},
pages = {490--504},
booktitle = {Computer Aided Verification},
publisher = {Springer International Publishing},
author = {Katis, Andreas and Mavridou, Anastasia and Giannakopoulou, Dimitra and Pressburger, Thomas and Schumann, Johann},
editor = {Shoham, Sharon and Vizel, Yakir},
date = {2022},
langid = {english},
file = {Full Text PDF:/home/danesabo/Zotero/storage/3JPVH8U2/Katis et al. - 2022 - Capture, Analyze, Diagnose Realizability Checking Of Requirements in FRET.pdf:application/pdf},
}
@inproceedings{meyer_strix_2018,
location = {Cham},
title = {Strix: Explicit Reactive Synthesis Strikes Back!},
isbn = {978-3-319-96145-3},
doi = {10.1007/978-3-319-96145-3_31},
shorttitle = {Strix},
pages = {578--586},
booktitle = {Computer Aided Verification},
publisher = {Springer International Publishing},
author = {Meyer, Philipp J. and Sickert, Salomon and Luttenberger, Michael},
editor = {Chockler, Hana and Weissenbacher, Georg},
date = {2018},
langid = {english},
}
@misc{jacobs_reactive_2024,
title = {The Reactive Synthesis Competition ({SYNTCOMP}): 2018-2021},
url = {http://arxiv.org/abs/2206.00251},
doi = {10.48550/arXiv.2206.00251},
shorttitle = {The Reactive Synthesis Competition ({SYNTCOMP})},
number = {{arXiv}:2206.00251},
publisher = {{arXiv}},
author = {Jacobs, Swen and others},
urldate = {2025-12-06},
date = {2024-05-06},
eprinttype = {arxiv},
eprint = {2206.00251 [cs]},
keywords = {Computer Science - Logic in Computer Science},
file = {Preprint PDF:/home/danesabo/Zotero/storage/GU6W5UH4/Jacobs et al. - 2024 - The Reactive Synthesis Competition (SYNTCOMP) 2018-2021.pdf:application/pdf;Snapshot:/home/danesabo/Zotero/storage/57UPK6A5/2206.html:text/html},
}
@article{branicky_multiple_1998,
title = {Multiple Lyapunov functions and other analysis tools for switched and hybrid systems},
volume = {43},
issn = {1558-2523},
url = {https://ieeexplore.ieee.org/document/664150},
doi = {10.1109/9.664150},
pages = {475--482},
number = {4},
journaltitle = {{IEEE} Transactions on Automatic Control},
author = {Branicky, M.S.},
urldate = {2025-09-10},
date = {1998-04},
keywords = {Automata, Control systems, Difference equations, Differential equations, Lagrangian functions, Limit-cycles, Lyapunov method, Stability analysis, Switched systems, Switches},
file = {PDF:/home/danesabo/Zotero/storage/5AQWDPAA/Branicky - 1998 - Multiple Lyapunov functions and other analysis tools for switched and hybrid systems.pdf:application/pdf},
}
@thesis{guernic_reachability_2009,
title = {Reachability Analysis of Hybrid Systems with Linear Continuous Dynamics},
url = {https://theses.hal.science/tel-00422569},
institution = {Université Joseph-Fourier - Grenoble I},
type = {phdthesis},
author = {Guernic, Colas Le},
urldate = {2025-09-14},
date = {2009-10-28},
langid = {english},
file = {Full Text PDF:/home/danesabo/Zotero/storage/A5XNTDZ9/Guernic - 2009 - Reachability Analysis of Hybrid Systems with Linear Continuous Dynamics.pdf:application/pdf},
}
@inproceedings{alur_hybrid_1993,
location = {Berlin, Heidelberg},
title = {Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems},
isbn = {978-3-540-48060-0},
doi = {10.1007/3-540-57318-6_30},
shorttitle = {Hybrid automata},
pages = {209--229},
booktitle = {Hybrid Systems},
publisher = {Springer},
author = {Alur, Rajeev and Courcoubetis, Costas and Henzinger, Thomas A. and Ho, Pei -Hsin},
editor = {Grossman, Robert L. and Nerode, Anil and Ravn, Anders P. and Rischel, Hans},
date = {1993},
langid = {english},
keywords = {Acceptance Condition, Hybrid Automaton, Hybrid System, Mutual Exclusion, Reachability Problem},
file = {Full Text PDF:/home/danesabo/Zotero/storage/WBXYUC86/Alur et al. - 1993 - Hybrid automata An algorithmic approach to the specification and verification of hybrid systems.pdf:application/pdf},
}
@article{mitchell_time-dependent_2005,
title = {A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games},
volume = {50},
issn = {1558-2523},
url = {https://ieeexplore.ieee.org/abstract/document/1463302},
doi = {10.1109/TAC.2005.851439},
pages = {947--957},
number = {7},
journaltitle = {{IEEE} Transactions on Automatic Control},
author = {Mitchell, I.M. and Bayen, A.M. and Tomlin, C.J.},
urldate = {2025-09-15},
date = {2005-07},
keywords = {Aircraft, Collaborative software, Collision avoidance, Computational modeling, Differential games, Hamilton–Jacobi equations, Nonlinear equations, Nonlinear systems, Partial differential equations, reachability, Trajectory, Vehicle dynamics, verification, Viscosity},
file = {Snapshot:/home/danesabo/Zotero/storage/SLKV9PEI/1463302.html:text/html;Submitted Version:/home/danesabo/Zotero/storage/9YWL2UDH/Mitchell et al. - 2005 - A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games.pdf:application/pdf},
}
@inproceedings{frehse_spaceex_2011,
location = {Berlin, Heidelberg},
title = {{SpaceEx}: Scalable Verification of Hybrid Systems},
isbn = {978-3-642-22110-1},
doi = {10.1007/978-3-642-22110-1_30},
shorttitle = {{SpaceEx}},
pages = {379--395},
booktitle = {Computer Aided Verification},
publisher = {Springer},
author = {Frehse, Goran and Le Guernic, Colas and Donzé, Alexandre and Cotton, Scott and Ray, Rajarshi and Lebeltel, Olivier and Ripado, Rodolfo and Girard, Antoine and Dang, Thao and Maler, Oded},
editor = {Gopalakrishnan, Ganesh and Qadeer, Shaz},
date = {2011},
langid = {english},
keywords = {Hybrid Automaton, Hybrid System, Reachability Analysis, Reachable State, Support Function},
file = {Full Text PDF:/home/danesabo/Zotero/storage/LPQK8GY2/Frehse et al. - 2011 - SpaceEx Scalable Verification of Hybrid Systems.pdf:application/pdf},
}
@inproceedings{bansal_hamilton-jacobi_2017,
title = {Hamilton-Jacobi reachability: A brief overview and recent advances},
url = {https://ieeexplore.ieee.org/abstract/document/8263977},
doi = {10.1109/CDC.2017.8263977},
shorttitle = {Hamilton-Jacobi reachability},
eventtitle = {2017 {IEEE} 56th Annual Conference on Decision and Control ({CDC})},
pages = {2242--2253},
booktitle = {2017 {IEEE} 56th Annual Conference on Decision and Control ({CDC})},
author = {Bansal, Somil and Chen, Mo and Herbert, Sylvia and Tomlin, Claire J.},
urldate = {2025-09-15},
date = {2017-12},
keywords = {Aircraft, Games, Level set, Safety, Tools, Trajectory, Tutorials},
file = {Snapshot:/home/danesabo/Zotero/storage/EEK5IE93/8263977.html:text/html;Submitted Version:/home/danesabo/Zotero/storage/BMNLZ9DW/Bansal et al. - 2017 - Hamilton-Jacobi reachability A brief overview and recent advances.pdf:application/pdf},
}
@inproceedings{prajna_safety_2004,
location = {Berlin, Heidelberg},
title = {Safety Verification of Hybrid Systems Using Barrier Certificates},
isbn = {978-3-540-24743-2},
doi = {10.1007/978-3-540-24743-2_32},
pages = {477--492},
booktitle = {Hybrid Systems: Computation and Control},
publisher = {Springer},
author = {Prajna, Stephen and Jadbabaie, Ali},
editor = {Alur, Rajeev and Pappas, George J.},
date = {2004},
langid = {english},
keywords = {Continuous State, Discrete Transition, Hybrid System, Integral Constraint, Reachability Analysis},
}