vault backup: 2025-12-17 15:32:09

.obsidian/plugins/obsidian-git/obsidian_askpass.sh

@@ -0,0 +1,23 @@
+#!/bin/sh
+
+PROMPT="$1"
+TEMP_FILE="$OBSIDIAN_GIT_CREDENTIALS_INPUT"
+
+cleanup() {
+    rm -f "$TEMP_FILE" "$TEMP_FILE.response"
+}
+trap cleanup EXIT
+
+echo "$PROMPT" > "$TEMP_FILE"
+
+while [ ! -e "$TEMP_FILE.response" ]; do
+    if [ ! -e "$TEMP_FILE" ]; then
+        echo "Trigger file got removed: Abort" >&2
+        exit 1
+    fi
+    sleep 0.1
+done
+
+RESPONSE=$(cat "$TEMP_FILE.response")
+
+echo "$RESPONSE"

.taskrc

@@ -15,7 +15,7 @@
 # Use the command 'task show' to see all defaults and overrides
 
 # Files
-data.location=/home/danesabo/Documents/Dane's Vault/.task
+data.location=~/Documents/Dane's Vault/.task
 
 # To use the default location of the XDG directories,
 # move this configuration file from ~/.taskrc to ~/.config/task/taskrc and uncomment below
@@ -27,7 +27,7 @@ data.location=/home/danesabo/Documents/Dane's Vault/.task
 #include light-16.theme
 #include light-256.theme
 #include dark-16.theme
-include dark-256.theme
+include light-256.theme
 #include dark-red-256.theme
 #include dark-green-256.theme
 #include dark-blue-256.theme
@@ -40,4 +40,4 @@ include dark-256.theme
 #include no-color.theme
 
 urgency.user.project.zk.coefficient=1.0
-news.version=2.6.0
+news.version=3.4.2

Writing/THESIS_PROPOSAL/1-goals-and-outcomes/research_statement_v1.tex

@@ -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}

Writing/THESIS_PROPOSAL/1-goals-and-outcomes/v1.tex

@@ -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.

Writing/THESIS_PROPOSAL/2-state-of-the-art/outline.md

@@ -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)
+

Writing/THESIS_PROPOSAL/2-state-of-the-art/v1.tex

@@ -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.

Writing/THESIS_PROPOSAL/3-research-approach/outline.md

@@ -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?

Writing/THESIS_PROPOSAL/3-research-approach/v1.tex

@@ -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.

Writing/THESIS_PROPOSAL/4-metrics-of-success/v1.tex

@@ -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.

Writing/THESIS_PROPOSAL/5-risks-and-contingencies/assumptions.md

@@ -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.
+

Writing/THESIS_PROPOSAL/5-risks-and-contingencies/v1.tex

@@ -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.

Writing/THESIS_PROPOSAL/6-broader-impacts/v1.tex

@@ -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.

Writing/THESIS_PROPOSAL/8-schedule/v1.tex

@@ -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. 

Writing/THESIS_PROPOSAL/ERLM-Proposal-Review-Summary.md

@@ -0,0 +1,627 @@
+# ERLM Proposal Writing Review - Executive Summary
+
+**Date**: December 2, 2025 **Reviewer**: Claude Code
+**Framework**: Gopen's Sense of Structure
+
+---
+
+## Overview
+
+This proposal demonstrates strong technical content, clear
+methodology, and comprehensive coverage of all required
+elements. The research approach is well-conceived, and the
+progression from problem statement through solution is
+logical. The writing is generally clear and professional.
+
+**Key Strengths:**
+- Excellent technical depth and specificity
+- Strong motivation established through human factors
+statistics
+- Clear three-thrust research structure
+- Comprehensive risk analysis with concrete contingencies
+- Good use of specific examples (TMI accident, HARDENS
+project)
+
+**Priority Areas for Revision:**
+- Sentence-level: Strengthen stress positions to emphasize
+key claims
+- Paragraph-level: Sharpen point-issue structure in some
+sections
+- Section-level: Tighten organization in State of the Art
+section
+- Big picture: Strengthen "so what" connections throughout
+
+---
+
+## Priority Issues (Top 10)
+
+### 1. **SOTA Section Length and Organization**
+[SECTION-LEVEL] **Location**: State of the Art section (358
+lines) **Issue**: The SOTA section is the longest in the
+proposal and covers multiple distinct topics (current
+procedures, human factors, HARDENS). While comprehensive, it
+risks overwhelming readers and obscuring your key
+ contributions. **Impact**: HIGH - Reviewers may lose track
+ of your argument in the density **Recommendation**:
+ Consider restructuring with clearer signposting. Each
+ subsection should explicitly connect back to what gap
+ you're filling. The current "\textbf{LIMITATION:}" callouts
+ are excellent—ensure every major subsection has one.
+
+### 2. **Weak Stress Positions Throughout** [SENTENCE-LEVEL]
+**Location**: All sections, especially Goals and State of
+the Art **Issue**: Many sentences place old/known
+information in stress position (sentence-final), missing
+opportunities to emphasize new claims **Impact**:
+MEDIUM-HIGH - Reduces rhetorical impact of key claims **See
+Pattern**: "Stress Position Weakness" below for examples and
+fixes
+
+### 3. **Missing "So What" Connections** [BIG PICTURE]
+**Location**: Transitions between major sections **Issue**:
+The proposal moves from problem → approach → metrics without
+always explicitly stating "this matters because..." at
+transition points **Impact**: MEDIUM-HIGH - Reviewers may
+not fully grasp significance **Recommendation**: Add
+explicit "if successful, this enables..." statements at the
+end of Goals section and beginning of Metrics section
+
+### 4. **Passive Voice Obscuring Agency** [SENTENCE-LEVEL]
+**Location**: Research Approach, especially subsection
+introductions **Issue**: Passive constructions like "will be
+employed" and "will be used" hide who does what and reduce
+directness **Impact**: MEDIUM - Reduces clarity and makes
+writing feel less confident **See Pattern**: "Passive Voice"
+below
+
+### 5. **Point-Issue Structure in Paragraphs**
+[PARAGRAPH-LEVEL] **Location**: State of the Art, Risk
+sections **Issue**: Some paragraphs present information
+without first establishing why readers should care (the
+"issue") **Impact**: MEDIUM - Readers may wonder "why are
+you telling me this?" **See Pattern**: "Point-Issue
+Structure" below
+
+### 6. **Topic String Breaks** [PARAGRAPH-LEVEL]
+**Location**: Research Approach, subsection transitions
+**Issue**: Topic position doesn't always establish clear
+continuity from previous sentence, forcing readers to
+reconstruct connections **Impact**: MEDIUM - Increases
+cognitive load **See Pattern**: "Topic Position &
+Continuity" below
+
+### 7. **Nominalization Hiding Action** [SENTENCE-LEVEL]
+**Location**: Throughout, especially Research Approach
+**Issue**: Action buried in nouns (e.g., "implementation"
+instead of "implement", "verification" instead of "verify")
+**Impact**: MEDIUM - Makes writing feel static rather than
+dynamic **Recommendation**: Convert nominalizations to
+active verbs where possible
+
+### 8. **Long Complex Sentences** [SENTENCE-LEVEL]
+**Location**: State of the Art (lines 45-51), Risks (lines
+72-79) **Issue**: Some sentences exceed 40-50 words with
+multiple subordinate clauses, challenging comprehension
+**Impact**: MEDIUM - Reviewers may have to re-read
+**Recommendation**: Break into 2-3 shorter sentences with
+clear logical flow
+
+### 9. **Subsection Balance in Risks Section**
+[SECTION-LEVEL] **Location**: Risks and Contingencies
+section **Issue**: Four subsections of vastly different
+lengths (computational tractability gets more space than
+discrete-continuous interface, despite latter being more
+fundamental) **Impact**: LOW-MEDIUM - May suggest misaligned
+priorities **Recommendation**: Consider whether space
+allocation reflects actual risk magnitude
+
+### 10. **Broader Impacts Underutilized** [BIG PICTURE]
+**Location**: Broader Impacts section (75 lines vs 358 for
+SOTA) **Issue**: This section is relatively brief given that
+economic impact is a major motivation for SMRs **Impact**:
+LOW-MEDIUM - Missing opportunity to strengthen value
+proposition **Recommendation**: Consider expanding economic
+analysis or adding brief discussion of workforce/educational
+impacts
+
+---
+
+## Key Patterns Identified
+
+### Pattern 1: Stress Position Weakness
+
+**Principle** (Gopen): The stress position (end of sentence)
+should contain the most important new information. Readers
+expect climax at sentence-end and are disappointed when they
+find old information or weak phrases there.
+
+**Example 1** (Goals and Outcomes, lines 13-17): ```
+Current: "Currently, nuclear plant operations rely on
+extensively trained human operators who follow detailed
+written procedures and strict regulatory requirements to
+manage reactor control." ```
+- **Issue**: Sentence ends with "manage reactor control"—a
+restatement of the opening. The key claim is buried
+mid-sentence: "extensively trained...detailed
+procedures...strict requirements"
+- **Fixed**: "Currently, nuclear plant operations require
+extensively trained human operators following detailed
+written procedures under strict regulatory requirements."
+
+**Example 2** (State of the Art, lines 53-54): ``` Current:
+"Procedures lack formal verification of correctness and
+completeness." ```
+- **Issue**: Ends weakly with "completeness" which is minor
+compared to the bigger issue
+- **Fixed**: "Procedures lack formal verification, leaving
+correctness and completeness unproven."
+
+**Example 3** (Research Approach, lines 41-42): ``` Current:
+"The following sections discuss how these thrusts will be
+accomplished." ```
+- **Issue**: Pure metadiscourse in stress position, provides
+no new information
+- **Fixed**: Delete this sentence—the enumeration provides
+sufficient transition, or combine with previous sentence:
+"...through three main thrusts, each detailed below."
+
+**Similar instances**:
+- Goals lines 29-32: "...we will combine formal methods..."
+- State of the Art lines 81-85: "...no application of hybrid
+control theory exists..."
+- Research Approach lines 115-116: "...enable progression to
+the next step..."
+- Metrics lines 29-31: "...makes this metric directly
+relevant..."
+- Risks lines 12-13: "...identification of remaining
+barriers to deployment"
+
+**How to fix**: Identify the most important new claim in
+each sentence and move it to the end. Often this means
+converting from "X does Y to achieve Z" to "X achieves Z by
+doing Y."
+
+---
+
+### Pattern 2: Passive Voice Obscuring Agency
+
+**Principle** (Gopen): Passive voice obscures who does what
+and reduces directness. In proposal writing, active voice
+demonstrates confidence and control. Use passive only when
+the agent is truly unimportant or unknown.
+
+**Example 1** (Research Approach, line 118): ``` Current:
+"We will employ state-of-the-art reactive synthesis
+tools..." ```
+- **Issue**: "Employ" is weak; you're not hiring the tools,
+you're using them
+- **Better**: "We will use Strix, a state-of-the-art
+reactive synthesis tool..."
+- **Best**: "Strix will translate our temporal logic
+specifications into deterministic automata..." (Shows what
+the tool *does*, not just that you'll use it)
+
+**Example 2** (Research Approach, line 207): ``` Current:
+"Control barrier functions will be employed when..." ```
+- **Issue**: Passive—who employs them? And "employed" sounds
+formal/stuffy
+- **Fixed**: "We will use control barrier functions to
+verify..." or better "Control barrier functions verify..."
+
+**Example 3** (Metrics, line 67): ``` Current: "This
+milestone delivers an internal technical report..." ```
+- **Issue**: Milestones don't deliver, people do
+- **Fixed**: "We will deliver an internal technical report
+documenting..."
+
+**Similar instances**:
+- Research Approach lines 161, 175, 206, 220: "will be
+employed", "will be developed", "will be used"
+- Metrics lines 69, 73, 79, 84: "...delivers a [document]"
+- Risks lines 57, 109, 163: various passives
+
+**How to fix**:
+1. Identify the real agent (usually "we")
+2. Make agent the subject: "We will X" or "X will Y"
+3. Choose strong active verbs: use/apply/develop/verify (not
+employ/utilize)
+
+---
+
+### Pattern 3: Point-Issue Structure Weakness
+
+**Principle** (Gopen): Paragraphs should begin by
+establishing (1) the point/claim being made and (2) why it
+matters (the issue). Discussion then supports that point.
+Readers need context before details.
+
+**Example 1** (State of the Art, lines 88-107): ``` Current
+paragraph begins: "The persistent role of human error in
+nuclear safety incidents, despite decades of
+improvements..." ```
+- **Analysis**: This paragraph immediately dives into the
+"persistent role" without first establishing why we're
+discussing human factors at all. Reader thinks: "Wait,
+weren't we just talking about procedures?"
+- **Fixed**: Add issue statement first: "Human factors
+provide the most compelling motivation for formal automated
+control. Despite decades of improvements in training and
+procedures, human error persists in 70-80% of nuclear
+incidents—suggesting that operator-based control faces
+fundamental, not remediable, limitations."
+
+**Example 2** (Risks, first paragraph): ``` Current: "This
+research relies on several critical assumptions that, if
+invalidated, would require scope adjustment..." ```
+- **Analysis**: Good—this establishes both point (critical
+assumptions exist) and issue (invalidity requires
+adjustment) immediately. The paragraph then delivers on this
+promise. This is a good model!
+
+**Example 3** (Research Approach, lines 166-169): ```
+Current: "While discrete system components will be
+synthesized with correctness guarantees, they represent only
+half of the complete system." ```
+- **Analysis**: Good issue statement (discrete alone
+insufficient), but could be sharper about the point. What
+will this section show?
+- **Fixed**: "While discrete system components will be
+synthesized with correctness guarantees, they represent only
+half of the complete system. This section describes how we
+will develop continuous control modes, verify their
+correctness, and address the unique verification challenges
+at the discrete-continuous interface."
+
+**Similar instances**:
+- State of the Art lines 13-34: long paragraph with delayed
+point
+- Goals lines 103-119: impact paragraph could be tighter
+- Approach lines 178-208: three-mode classification needs
+clearer framing
+
+**How to fix**:
+1. First sentence should state the paragraph's point
+2. Second sentence (or same sentence) should state why this
+matters
+3. Remaining sentences provide supporting detail
+
+---
+
+### Pattern 4: Topic Position & Continuity
+
+**Principle** (Gopen): The topic position (beginning of
+sentence) should contain old/familiar information that links
+to what came before. This creates flow and coherence. Abrupt
+topic shifts disorient readers.
+
+**Example 1** (Goals, lines 18-23): ``` Sentence 1: "...this
+reliance on human operators prevents the introduction of
+autonomous control capabilities..."
+
+Sentence 2: "Emerging technologies like small modular
+reactors face significantly higher per-megawatt staffing
+costs..." ```
+- **Issue**: Topic shifts abruptly from "reliance on
+operators" to "emerging technologies". Connection exists
+(both about staffing challenges) but isn't explicit
+- **Fixed**: "...prevents autonomous control capabilities.
+This limitation creates particular challenges for emerging
+technologies like small modular reactors, which face
+significantly higher per-megawatt staffing costs..."
+
+**Example 2** (State of the Art, lines 234-243): ```
+Sentence about what HARDENS addressed: "...discrete digital
+control logic..."
+
+Next sentence: "However, the project did not address
+continuous dynamics..." ```
+- **Analysis**: Good use of "however, the project" in topic
+position—maintains focus on HARDENS while pivoting to
+limitation. This is a good model!
+
+**Example 3** (Research Approach, lines 56-58): ``` Sentence
+1: "...we may be able to translate them into logical
+formulae..."
+
+Sentence 2: "Linear Temporal Logic (LTL) provides four
+fundamental operators..." ```
+- **Issue**: Abrupt topic shift from "translating
+procedures" to "LTL provides". Missing: why LTL? Why now?
+- **Fixed**: "...translate them into logical formulae. To
+formalize these procedures, we will use Linear Temporal
+Logic (LTL), which provides four fundamental operators..."
+
+**Similar instances**:
+- Goals lines 23-27: "emerging technologies" → "what is
+needed"
+- State of the Art lines 72-74: control modes → division
+between automated/human
+- Approach lines 183-185: stabilizing mode example →
+transitory mode definition
+
+**How to fix**:
+1. Identify the topic of the previous sentence
+2. Begin next sentence with something related to that topic
+3. Use transitional phrases when shifting topics: "This
+[previous thing] leads to [new thing]"
+
+---
+
+### Pattern 5: Long Complex Sentences
+
+**Principle**: Sentences with multiple subordinate clauses
+(especially over 35-40 words) tax reader working memory.
+Breaking into multiple sentences often improves clarity
+without losing sophistication.
+
+**Example 1** (State of the Art, lines 48-51): ``` Current
+(51 words): "Procedures undergo technical evaluation,
+simulator validation testing, and biennial review as part of
+operator requalification under 10 CFR 55.59, but despite
+these rigorous development processes, procedures
+fundamentally lack formal verification of key safety
+properties." ```
+- **Issue**: Long sentence with list, subordinate clause,
+and contrast—hard to parse
+- **Fixed (2 sentences)**: "Procedures undergo technical
+evaluation, simulator validation testing, and biennial
+review as part of operator requalification under 10 CFR
+55.59. Despite these rigorous development processes,
+procedures fundamentally lack formal verification of key
+safety properties."
+
+**Example 2** (Risks, lines 72-78): ``` Current (57 words):
+"Temporal logic operates on boolean predicates, while
+continuous control requires reasoning about differential
+equations and reachable sets, and guard conditions that
+require complex nonlinear predicates may resist boolean
+abstraction, making synthesis intractable." ```
+- **Issue**: Run-on with multiple clauses strung together
+with commas
+- **Fixed (3 sentences)**: "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. This mismatch could make
+synthesis intractable."
+
+**Similar instances**:
+- State of the Art lines 44-51: procedure development
+description
+- Research Approach lines 40-45: hybrid system description
+- Risks lines 17-24: computational tractability discussion
+- Broader Impacts lines 13-23: economic analysis
+
+**How to fix**:
+1. Identify natural breakpoints (usually where you have
+"and" or "but")
+2. Create new sentences at these breaks
+3. Ensure each new sentence has clear topic position
+4. May need to repeat/reference previous sentence's subject
+for clarity
+
+---
+
+## Section-Level Issues
+
+### Goals and Outcomes Section **Strengths**: Excellent
+structure with clear goal → problem → approach → outcomes →
+impact progression. The four-paragraph opening is very
+strong.
+
+**Issues**:
+- Lines 29-53 (Approach paragraph): This is dense and tries
+to cover too much. Consider breaking into two paragraphs:
+one on the approach concept, one on the hypothesis and
+rationale.
+- Outcomes enumeration: Very clear, but could strengthen the
+transition from strategy to outcome in each item. Currently
+reads as "we'll do X. [new sentence] This enables Y."
+Consider: "We'll do X, enabling Y."
+
+### State of the Art Section **Strengths**: Comprehensive,
+well-researched, excellent use of the HARDENS case study as
+both positive example and gap identifier.
+
+**Issues**:
+- **Length**: At 358 lines, this risks losing readers. Most
+concerning: readers may forget your framing by the time they
+reach your contribution.
+- **Organization**: Four major subsections (procedures,
+human factors, HARDENS, research imperative) would benefit
+from a roadmap sentence at the beginning: "To understand the
+need for hybrid control synthesis, we first examine..."
+- **Balance**: HARDENS subsection is 89 lines—nearly 25% of
+SOTA. While impressive, consider whether this should be a
+separate section or whether some detail could move to an
+appendix.
+- **Transition to Approach**: The "Research Imperative"
+subsection is excellent but feels like it belongs at the
+start of Research Approach rather than end of SOTA.
+
+### Research Approach Section **Strengths**: Clear
+three-thrust structure, good use of equations and examples,
+strong technical detail.
+
+**Issues**:
+- **Subsection transitions**: The transitions between the
+three main subsections (Procedures→Temporal,
+Temporal→Discrete, Discrete→Continuous) could be smoother.
+Each starts somewhat abruptly.
+- **SmAHTR introduction**: The SmAHTR demonstration case is
+introduced suddenly at line 253. Consider introducing it
+earlier (perhaps in Goals section or at start of Approach)
+so readers know it's coming.
+- **Three-mode classification**: Lines 178-208 present the
+stabilizing/transitory/expulsory framework, which is
+innovative. This deserves more prominence—consider
+highlighting it as a key contribution.
+
+### Metrics of Success Section **Strengths**: TRL framework
+is well-justified, progression through levels is clear.
+
+**Issues**:
+- **Defensive tone**: Lines 11-30 spend considerable space
+justifying why TRL is appropriate. This is good but could be
+more concise. Consider: one paragraph on why TRLs (lines
+10-19) rather than two.
+- **Grading criteria**: The TRL definitions (3, 4, 5) are
+excellent. Very concrete and measurable.
+
+### Risks and Contingencies Section **Strengths**:
+Comprehensive, each risk has indicators and contingencies,
+well-organized.
+
+**Issues**:
+- **Subsection balance**: Four subsections range from 41
+lines (computational) to 65 lines (discrete-continuous).
+Ensure space reflects actual risk level.
+- **Mitigation vs. contingency**: Some subsections blur
+"mitigation" (preventing problems) and "contingency"
+(response if they occur). Consider clarifying this
+structure.
+
+### Broader Impacts Section **Strengths**: Clear economic
+motivation, good connection to SMRs and datacenter
+application.
+
+**Issues**:
+- **Brevity**: At 75 lines, this is the shortest technical
+section. Given that economic viability is a key motivation,
+consider expanding.
+- **Missed opportunities**: Could briefly mention
+workforce/educational impacts (training future engineers in
+formal methods), equity (providing reliable clean energy to
+underserved areas), broader applicability beyond nuclear.
+
+### Budget Section **Brief review**: Budget is
+comprehensive, well-justified, appropriate. Minor note:
+Consider whether the high-performance workstation (Year 1)
+might need upgrades in Year 2-3 as synthesis scales up.
+
+### Schedule Section **Brief review**: Schedule is ambitious
+but realistic. Six trimesters for dissertation research is
+reasonable. Publication strategy is smart (nuclear community
+first, then broader control theory community). Minor note:
+Line 73 has a space issue ("t ranslation").
+
+---
+
+## Big Picture Observations
+
+### Narrative and Argument Structure
+
+**Strengths**:
+- Clear problem-solution arc: operators make errors →
+procedures lack formal guarantees → hybrid control synthesis
+provides guarantees
+- Good use of motivating examples (TMI, human error
+statistics, HARDENS)
+- Technical progression is logical: discrete synthesis →
+continuous verification → integrated system
+
+**Opportunities**:
+1. **Strengthen "so what" transitions**: The proposal
+sometimes presents information without explicitly stating
+significance. Add more "This matters because..." statements.
+2. **Emphasize novelty earlier**: The three-mode
+classification and discrete-continuous interface
+verification are novel contributions. Signal this earlier
+and more explicitly.
+3. **Create more callbacks**: When describing Research
+Approach, refer back to specific limitations identified in
+State of the Art. Currently these connections are implicit.
+
+### Rhetorical Effectiveness
+
+**Credibility established through**:
+- Comprehensive literature review
+- Specific technical detail
+- Access to industry hardware (Emerson partnership)
+- Prior conference recognition (best student paper)
+
+**Value proposition**:
+- Clear economic impact (O&M cost reduction)
+- Safety improvement (mathematical guarantees vs. human
+operators)
+- Broader applicability (methodology generalizes)
+
+**Could strengthen**:
+- More explicit statements of what's novel vs. what's
+established practice
+- Stronger emphasis on the unique combination of discrete
+synthesis + continuous verification (others do one or the
+other, not both)
+
+### Content Gaps and Consistency
+
+**Terminology**:
+- Generally consistent
+- Good introduction of technical terms (hybrid automata,
+temporal logic, reachability analysis)
+- Minor: "correct by construction" vs. "provably
+correct"—used interchangeably, which is fine, but could note
+they're synonymous
+
+**Scope consistency**:
+- Excellent—stays focused on startup procedures for SmAHTR
+- Appropriately acknowledges limitations (TRL 5, not
+deployment-ready)
+- Risk section addresses what happens if scope must narrow
+
+**Potential gaps**:
+1. **Cybersecurity**: Not mentioned. For autonomous nuclear
+control, shouldn't there be at least a paragraph on security
+verification?
+2. **Regulatory path**: You mention "regulatory
+requirements" but don't detail what NRC approval process
+would look like. Even a paragraph would strengthen
+credibility.
+3. **Comparison with alternatives**: What about machine
+learning approaches to autonomous control? Worth a paragraph
+explaining why formal methods are superior for
+safety-critical systems.
+
+---
+
+## Gopen Framework Quick Reference
+
+**Stress Position**: End of sentence should contain most
+important new information. Readers expect climax there.
+
+**Topic Position**: Beginning of sentence should contain
+familiar information that links to previous sentence.
+Creates flow.
+
+**Point-Issue Structure**: Paragraphs should open by stating
+(1) the point/claim and (2) why it matters, before providing
+supporting detail.
+
+**Topic String**: The chain of topics across sentences in a
+paragraph. Strong topic strings create coherence; broken
+ones confuse readers.
+
+**Old→New Information Flow**: Information should flow from
+familiar (old) to unfamiliar (new) within sentences and
+paragraphs.
+
+---
+
+## Next Steps
+
+1. **Start with Priority Issues 1-3**: These have the
+highest impact
+2. **Apply Patterns**: Use the pattern examples to fix
+similar instances throughout
+3. **Consult Detailed Document**: For comprehensive
+checkbox-by-checkbox revisions
+4. **Section-by-section revision**: Work through one section
+at a time, applying patterns
+5. **Final pass for consistency**: Ensure changes maintain
+consistent terminology and tone
+
+This proposal has strong technical content and a solid
+structure. The revisions suggested here will strengthen
+clarity, emphasize key contributions, and make the argument
+even more compelling for reviewers. Good luck with your
+revisions!

Writing/THESIS_PROPOSAL/dane_proposal_format.cls

@@ -0,0 +1,109 @@
+\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}
+
+% 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:}}
+
+% 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}

Writing/THESIS_PROPOSAL/main.aux

@@ -0,0 +1,99 @@
+\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}
+\@writefile{toc}{\contentsline {section}{\numberline {2}State of the Art and Limits of Current Practice}{2}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}Current Reactor Procedures and Operation}{2}{}\protected@file@percent }
+\citation{WRPS.Description,gentillon_westinghouse_1999}
+\citation{operator_statistics}
+\citation{10CFR55}
+\citation{10CFR50.54}
+\citation{Kemeny1979}
+\citation{WNA2020}
+\citation{hogberg_root_2013}
+\citation{zhang_analysis_2025}
+\citation{Kiniry2024}
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Human Factors in Nuclear Accidents}{3}{}\protected@file@percent }
+\citation{Kiniry2024}
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.3}HARDENS and Formal Methods}{4}{}\protected@file@percent }
+\citation{katis_capture_2022}
+\@writefile{toc}{\contentsline {section}{\numberline {3}Research Approach}{5}{}\protected@file@percent }
+\citation{baier_principles_2008}
+\citation{meyer_strix_2018,jacobs_reactive_2024}
+\citation{branicky_multiple_1998}
+\citation{branicky_multiple_1998}
+\citation{bansal_hamilton-jacobi_2017,guernic_reachability_2009}
+\citation{frehse_spaceex_2011,mitchell_time-dependent_2005}
+\citation{prajna_safety_2004}
+\@writefile{toc}{\contentsline {section}{\numberline {4}Metrics for Success}{9}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {paragraph}{TRL 3 \textit  {Critical Function and Proof of Concept}}{10}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {paragraph}{TRL 4 \textit  {Laboratory Testing of Integrated Components}}{10}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {paragraph}{TRL 5 \textit  {Laboratory Testing in Relevant Environment}}{10}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {section}{\numberline {5}Risks and Contingencies}{11}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsection}{\numberline {5.1}Computational Tractability of Synthesis}{11}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{11}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{12}{}\protected@file@percent }
+\citation{eia_lcoe_2022}
+\citation{eesi_datacenter_2024}
+\citation{eia_lcoe_2022}
+\@writefile{toc}{\contentsline {section}{\numberline {6}Broader Impacts}{13}{}\protected@file@percent }
+\@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.}}{15}{}\protected@file@percent }
+\newlabel{fig:gantt}{{1}{15}{Schedule, Milestones, and Deliverables}{}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {7.1}Milestones and Deliverables}{15}{}\protected@file@percent }
+\bibstyle{ieeetr}
+\bibdata{references}
+\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{katis_capture_2022}{14}
+\bibcite{baier_principles_2008}{15}
+\bibcite{meyer_strix_2018}{16}
+\bibcite{jacobs_reactive_2024}{17}
+\@writefile{toc}{\contentsline {section}{References}{16}{}\protected@file@percent }
+\bibcite{branicky_multiple_1998}{18}
+\bibcite{bansal_hamilton-jacobi_2017}{19}
+\bibcite{guernic_reachability_2009}{20}
+\bibcite{frehse_spaceex_2011}{21}
+\bibcite{mitchell_time-dependent_2005}{22}
+\bibcite{prajna_safety_2004}{23}
+\bibcite{eia_lcoe_2022}{24}
+\bibcite{eesi_datacenter_2024}{25}
+\@writefile{toc}{\contentsline {section}{\numberline {8}Budget and Budget Justification}{I}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsection}{\numberline {8.1}Budget Summary}{I}{}\protected@file@percent }
+\@writefile{lot}{\contentsline {table}{\numberline {1}{\ignorespaces Proposed Budget by Year and Category}}{I}{}\protected@file@percent }
+\newlabel{tab:budget}{{1}{I}{Budget Summary}{}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {8.2}Budget Justification}{II}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsubsection}{\numberline {8.2.1}Senior Personnel}{II}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {paragraph}{Faculty Advisor}{II}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsubsection}{\numberline {8.2.2}Other Personnel}{II}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {paragraph}{Graduate Research Assistant (Principal Investigator)}{II}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsubsection}{\numberline {8.2.3}Fringe Benefits}{II}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {paragraph}{Faculty Fringe Benefits}{II}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {paragraph}{Graduate Research Assistant Fringe Benefits}{II}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsubsection}{\numberline {8.2.4}Travel}{II}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {paragraph}{Conference Travel (\$4,000 per year)}{II}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {paragraph}{Industry Collaboration Visits (\$1,500 per year)}{II}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsubsection}{\numberline {8.2.5}Other Direct Costs}{II}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {paragraph}{Materials and Supplies}{II}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {paragraph}{Publication Costs}{II}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {paragraph}{Computing and Cloud Services}{III}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsubsection}{\numberline {8.2.6}H. Indirect Costs (Facilities \& Administrative)}{III}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {section}{\numberline {9}Supplemental Sections}{III}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsection}{\numberline {9.1}Biosketch}{III}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsection}{\numberline {9.2}Data Management Plan}{VI}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsection}{\numberline {9.3}Facilities}{X}{}\protected@file@percent }
+\gdef \@abspage@last{31}

Writing/THESIS_PROPOSAL/main.bbl

@@ -0,0 +1,83 @@
+\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{katis_capture_2022}
+A.~Katis, A.~Mavridou, D.~Giannakopoulou, T.~Pressburger, and J.~Schumann, ``Capture, analyze, diagnose: Realizability checking of requirements in {FRET},'' in {\em Computer Aided Verification} (S.~Shoham and Y.~Vizel, eds.), pp.~490--504, Springer International Publishing.
+
+\bibitem{baier_principles_2008}
+C.~Baier and J.-P. Katoen, {\em Principles of Model Checking}.
+\newblock {MIT} Press.
+
+\bibitem{meyer_strix_2018}
+P.~J. Meyer, S.~Sickert, and M.~Luttenberger, ``Strix: Explicit reactive synthesis strikes back!,'' in {\em Computer Aided Verification} (H.~Chockler and G.~Weissenbacher, eds.), pp.~578--586, Springer International Publishing.
+
+\bibitem{jacobs_reactive_2024}
+S.~Jacobs {\em et~al.}, ``The reactive synthesis competition ({SYNTCOMP}): 2018-2021.''
+
+\bibitem{branicky_multiple_1998}
+M.~Branicky, ``Multiple lyapunov functions and other analysis tools for switched and hybrid systems,'' vol.~43, no.~4, pp.~475--482.
+
+\bibitem{bansal_hamilton-jacobi_2017}
+S.~Bansal, M.~Chen, S.~Herbert, and C.~J. Tomlin, ``Hamilton-jacobi reachability: A brief overview and recent advances,'' in {\em 2017 {IEEE} 56th Annual Conference on Decision and Control ({CDC})}, pp.~2242--2253.
+
+\bibitem{guernic_reachability_2009}
+C.~L. Guernic, ``Reachability analysis of hybrid systems with linear continuous dynamics.''
+
+\bibitem{frehse_spaceex_2011}
+G.~Frehse, C.~Le~Guernic, A.~Donzé, S.~Cotton, R.~Ray, O.~Lebeltel, R.~Ripado, A.~Girard, T.~Dang, and O.~Maler, ``{SpaceEx}: Scalable verification of hybrid systems,'' in {\em Computer Aided Verification} (G.~Gopalakrishnan and S.~Qadeer, eds.), pp.~379--395, Springer.
+
+\bibitem{mitchell_time-dependent_2005}
+I.~Mitchell, A.~Bayen, and C.~Tomlin, ``A time-dependent hamilton-jacobi formulation of reachable sets for continuous dynamic games,'' vol.~50, no.~7, pp.~947--957.
+
+\bibitem{prajna_safety_2004}
+S.~Prajna and A.~Jadbabaie, ``Safety verification of hybrid systems using barrier certificates,'' in {\em Hybrid Systems: Computation and Control} (R.~Alur and G.~J. Pappas, eds.), pp.~477--492, Springer.
+
+\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}

Writing/THESIS_PROPOSAL/main.blg

@@ -0,0 +1,71 @@
+This is BibTeX, Version 0.99d (TeX Live 2023/Debian)
+Capacity: max_strings=200000, hash_size=200000, hash_prime=170003
+The top-level auxiliary file: main.aux
+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--entry type for "guernic_reachability_2009" isn't style-file defined
+--line 221 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
+Warning--empty year in katis_capture_2022
+Warning--empty year in baier_principles_2008
+Warning--empty year in meyer_strix_2018
+Warning--empty journal in branicky_multiple_1998
+Warning--empty year in branicky_multiple_1998
+Warning--empty year in bansal_hamilton-jacobi_2017
+Warning--empty year in frehse_spaceex_2011
+Warning--empty journal in mitchell_time-dependent_2005
+Warning--empty year in mitchell_time-dependent_2005
+Warning--empty year in prajna_safety_2004
+You've used 25 entries,
+            1876 wiz_defined-function locations,
+            608 strings with 7728 characters,
+and the built_in function-call counts, 5612 in all, are:
+= -- 511
+> -- 249
+< -- 2
++ -- 93
+- -- 68
+* -- 382
+:= -- 798
+add.period$ -- 27
+call.type$ -- 25
+change.case$ -- 27
+chr.to.int$ -- 0
+cite$ -- 41
+duplicate$ -- 260
+empty$ -- 567
+format.name$ -- 68
+if$ -- 1343
+int.to.chr$ -- 0
+int.to.str$ -- 25
+missing$ -- 11
+newline$ -- 83
+num.names$ -- 32
+pop$ -- 125
+preamble$ -- 1
+purify$ -- 0
+quote$ -- 0
+skip$ -- 204
+stack$ -- 0
+substring$ -- 276
+swap$ -- 86
+text.length$ -- 2
+text.prefix$ -- 0
+top$ -- 0
+type$ -- 0
+warning$ -- 16
+while$ -- 53
+width$ -- 27
+write$ -- 210
+(There were 20 warnings)

Writing/THESIS_PROPOSAL/main.fdb_latexmk

@@ -0,0 +1,267 @@
+# Fdb version 4
+["bibtex main"] 1764990267.80751 "main.aux" "main.bbl" "main" 1764990468.02866 0
+  "./references.bib" 1764980611.90841 14069 2a4f74c587187a8a71049043171eb0fe ""
+  "/usr/share/texlive/texmf-dist/bibtex/bst/base/ieeetr.bst" 1292289607 18361 1a00e58565e7f19bf2b3e1bfb82254ae ""
+  "main.aux" 1764990467.86727 6961 b67c1d53687261878883c1352f4b1410 "pdflatex"
+  (generated)
+  "main.bbl"
+  "main.blg"
+  (rewritten before read)
+["pdflatex"] 1764990467.13431 "main.tex" "main.pdf" "main" 1764990468.02883 0
+  "/etc/texmf/web2c/texmf.cnf" 1726065852.27662 475 c0e671620eb5563b2130f56340a5fde8 ""
+  "/usr/share/texlive/texmf-dist/fonts/enc/dvips/base/8r.enc" 1165713224 4850 80dc9bab7f31fb78a000ccfed0e27cab ""
+  "/usr/share/texlive/texmf-dist/fonts/map/fontname/texfonts.map" 1577235249 3524 cb3e574dea2d1052e39280babc910dc8 ""
+  "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm" 1136768653 1408 5937f58aa508ea2cea4901c07d10f5fe ""
+  "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/psyro.tfm" 1136768653 1544 23a042a74981a3e4b6ce2e350e390409 ""
+  "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm" 1136768653 2172 fd0c924230362ff848a33632ed45dc23 ""
+  "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb8c.tfm" 1136768653 1340 d2f6275bc4fa3f07e3bc50aae2c71eab ""
+  "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb8r.tfm" 1136768653 4524 6bce29db5bc272ba5f332261583fee9c ""
+  "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmbi7t.tfm" 1136768653 2228 e564491c42a4540b5ebb710a75ff306c ""
+  "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmbi8r.tfm" 1136768653 4480 10409ed8bab5aea9ec9a78028b763919 ""
+  "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm" 1136768653 2124 2601a75482e9426d33db523edf23570a ""
+  "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr8c.tfm" 1136768653 1352 fa28a7e6d323c65ce7d13d5342ff6be2 ""
+  "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm" 1136768653 4408 25b74d011a4c66b7f212c0cc3c90061b ""
+  "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm" 1136768653 2288 f478fc8fed18759effb59f3dad7f3084 ""
+  "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri8c.tfm" 1136768653 1428 3f135d3346fb7bfe71989ef2e19a9f01 ""
+  "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri8r.tfm" 1136768653 4640 532ca3305aad10cc01d769f3f91f1029 ""
+  "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm" 1136768653 2232 db256afffc8202da192b4641df14d602 ""
+  "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7t.tfm" 1136768653 2172 1d00c2a0d10f23031be62329457a870c ""
+  "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm" 1136768653 1032 20febbd0f0c9a48eb78616f897008286 ""
+  "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm" 1136768653 1520 ad7b3c1a480a03b3e41b5fbb13d938f2 ""
+  "/usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm" 1246382020 916 f87d7c45f9c908e672703b83b72241a3 ""
+  "/usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm" 1246382020 908 2921f8a10601f252058503cc6570e581 ""
+  "/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmmi10.tfm" 1136768653 1528 abec98dbc43e172678c11b3b9031252a ""
+  "/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmr10.tfm" 1136768653 1296 45809c5a464d5f32c8f98ba97c1bb47f ""
+  "/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmr12.tfm" 1136768653 1288 655e228510b4c2a1abe905c368440826 ""
+  "/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmsy10.tfm" 1136768653 1124 6c73e740cf17375f03eec0ee63599741 ""
+  "/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmtt12.tfm" 1136768653 772 9a936b7f5e2ff0557fce0f62822f0bbf ""
+  "/usr/share/texlive/texmf-dist/fonts/tfm/public/rsfs/rsfs10.tfm" 1229303445 688 37338d6ab346c2f1466b29e195316aa4 ""
+  "/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb" 1248133631 36299 5f9df58c2139e7edcf37c8fca4bd384d ""
+  "/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb" 1248133631 35752 024fb6c41858982481f6968b5fc26508 ""
+  "/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb" 1248133631 32569 5e5ddc8df908dea60932f3c484a54c0d ""
+  "/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt12.pfb" 1248133631 24252 1e4e051947e12dfb50fee0b7f4e26e3a ""
+  "/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/symbols/msam10.pfb" 1248133631 31764 459c573c03a4949a528c2cc7f557e217 ""
+  "/usr/share/texlive/texmf-dist/fonts/type1/urw/symbol/usyr.pfb" 1136849748 33709 b09d2e140b7e807d3a97058263ab6693 ""
+  "/usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmb8a.pfb" 1136849748 44729 811d6c62865936705a31c797a1d5dada ""
+  "/usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmbi8a.pfb" 1136849748 44656 0cbca70e0534538582128f6b54593cca ""
+  "/usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmr8a.pfb" 1136849748 46026 6dab18b61c907687b520c72847215a68 ""
+  "/usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmri8a.pfb" 1136849748 45458 a3faba884469519614ca56ba5f6b1de1 ""
+  "/usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmb7t.vf" 1136768653 1372 788387fea833ef5963f4c5bffe33eb89 ""
+  "/usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmb8c.vf" 1136768653 3556 f148a8ed6ef01fed553027171e4f9b22 ""
+  "/usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmbi7t.vf" 1136768653 1384 6ac0f8b839230f5d9389287365b243c0 ""
+  "/usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmr7t.vf" 1136768653 1380 0ea3a3370054be6da6acd929ec569f06 ""
+  "/usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmr8c.vf" 1136768653 3556 8a9a6dcbcd146ef985683f677f4758a6 ""
+  "/usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmri7t.vf" 1136768653 1384 a9d8adaf491ce34e5fba99dc7bbe5f39 ""
+  "/usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmri8c.vf" 1136768653 3564 2068501a2226e54ce367edd5b047e424 ""
+  "/usr/share/texlive/texmf-dist/fonts/vf/adobe/times/zptmcm7m.vf" 1136768653 1132 27520247d3fe18d4266a226b461885c2 ""
+  "/usr/share/texlive/texmf-dist/fonts/vf/adobe/times/zptmcm7t.vf" 1136768653 1108 d271d6f9de4122c3f8d3b65666167fac ""
+  "/usr/share/texlive/texmf-dist/fonts/vf/adobe/times/zptmcm7y.vf" 1136768653 964 5673178ff30617b900214de28ab32b38 ""
+  "/usr/share/texlive/texmf-dist/tex/context/base/mkii/supp-pdf.mkii" 1461363279 71627 94eb9990bed73c364d7f53f960cc8c5b ""
+  "/usr/share/texlive/texmf-dist/tex/generic/iftex/iftex.sty" 1644112042 7237 bdd120a32c8fdb4b433cf9ca2e7cd98a ""
+  "/usr/share/texlive/texmf-dist/tex/generic/iftex/ifvtex.sty" 1572645307 1057 525c2192b5febbd8c1f662c9468335bb ""
+  "/usr/share/texlive/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty" 1701727651 17865 1a9bd36b4f98178fa551aca822290953 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcore.code.tex" 1673816307 1016 1c2b89187d12a2768764b83b4945667c ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorearrows.code.tex" 1601326656 43820 1fef971b75380574ab35a0d37fd92608 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreexternal.code.tex" 1601326656 19324 f4e4c6403dd0f1605fd20ed22fa79dea ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcoregraphicstate.code.tex" 1601326656 6038 ccb406740cc3f03bbfb58ad504fe8c27 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreimage.code.tex" 1673816307 6911 f6d4cf5a3fef5cc879d668b810e82868 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorelayers.code.tex" 1601326656 4883 42daaf41e27c3735286e23e48d2d7af9 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreobjects.code.tex" 1601326656 2544 8c06d2a7f0f469616ac9e13db6d2f842 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathconstruct.code.tex" 1601326656 44195 5e390c414de027626ca5e2df888fa68d ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathprocessing.code.tex" 1601326656 17311 2ef6b2e29e2fc6a2fc8d6d652176e257 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathusage.code.tex" 1601326656 21302 788a79944eb22192a4929e46963a3067 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepatterns.code.tex" 1673816307 9691 3d42d89522f4650c2f3dc616ca2b925e ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepoints.code.tex" 1601326656 33335 dd1fa4814d4e51f18be97d88bf0da60c ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorequick.code.tex" 1601326656 2965 4c2b1f4e0826925746439038172e5d6f ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorerdf.code.tex" 1601326656 5196 2cc249e0ee7e03da5f5f6589257b1e5b ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorescopes.code.tex" 1673816307 20821 7579108c1e9363e61a0b1584778804aa ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreshade.code.tex" 1601326656 35249 abd4adf948f960299a4b3d27c5dddf46 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcoretransformations.code.tex" 1673816307 22012 81b34a0aa8fa1a6158cc6220b00e4f10 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcoretransparency.code.tex" 1601326656 8893 e851de2175338fdf7c17f3e091d94618 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/graphs/tikzlibrarygraphs.code.tex" 1673816307 86723 0209bbf0dbb55cd8213ecb06ebea3349 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryarrows.code.tex" 1601326656 319 225dfe354ba678ff3c194968db39d447 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarybackgrounds.code.tex" 1601326656 4572 4a19637ef65ce88ad2f2d5064b69541d ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarycalc.code.tex" 1601326656 15929 463535aa2c4268fead6674a75c0e8266 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarychains.code.tex" 1673816307 6816 d02c83dff7646998a96988d92df7f6f4 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarydecorations.code.tex" 1673816307 5628 dc0ee4ba7f3e40acae5600067ce833de ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarydecorations.markings.code.tex" 1601326656 788 fb28645a91ec7448ebe79bee60965a88 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryfadings.code.tex" 1601326656 1179 5483d86c1582c569e665c74efab6281f ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarypatterns.code.tex" 1601326656 770 82e332cc9cc48e06b8070d74393a185a ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarypositioning.code.tex" 1601326656 3937 3f208572dd82c71103831da976d74f1a ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshadows.code.tex" 1601326656 2889 d698e3a959304efa342d47e3bb86da5b ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.arrows.code.tex" 1601326656 410 048d1174dabde96757a5387b8f23d968 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.callouts.code.tex" 1601326656 1201 8bd51e254d3ecf0cd2f21edd9ab6f1bb ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.code.tex" 1601326656 494 8de62576191924285b021f4fc4292e16 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.geometric.code.tex" 1601326656 339 be0fe46d92a80e3385dd6a83511a46f2 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.misc.code.tex" 1601326656 329 ba6d5440f8c16779c2384e0614158266 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.multipart.code.tex" 1673816307 923 c7a223b32ffdeb1c839d97935eee61ff ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshapes.symbols.code.tex" 1601326656 475 4b4056fe07caa0603fede9a162fe666d ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarytopaths.code.tex" 1608933718 11518 738408f795261b70ce8dd47459171309 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/tikz.code.tex" 1673816307 186782 af500404a9edec4d362912fe762ded92 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/decorations/pgflibrarydecorations.markings.code.tex" 1601326656 5220 c70346acb7ff99702098460fd6c18993 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/pgflibraryarrows.code.tex" 1601326656 31874 89148c383c49d4c72114a76fd0062299 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/pgflibraryarrows.meta.code.tex" 1601326656 58801 1e750fb0692eb99aaac45698bbec96b1 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/pgflibraryfadings.code.tex" 1601326656 2563 d5b174eb7709fd6bdcc2f70953dbdf8e ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/pgflibrarypatterns.code.tex" 1601326656 7936 49e55444d57eb69a380c6baa35094828 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/pgflibraryplothandlers.code.tex" 1601326656 32995 ac577023e12c0e4bd8aa420b2e852d1a ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.arrows.code.tex" 1673816307 91587 d9b31a3e308b08833e4528a7b4484b4a ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.callouts.code.tex" 1601326656 33336 427c354e28a4802ffd781da22ae9f383 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.geometric.code.tex" 1673816307 161011 76ab54df0aa1a9d3b27a94864771d38d ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.misc.code.tex" 1673816307 46249 d1f322c52d26cf506b4988f31902cd5d ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.multipart.code.tex" 1601326656 62281 aff261ef10ba6cbe8e3c872a38c05a61 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshapes.symbols.code.tex" 1673816307 90521 9d46d4504c2ffed28ff5ef3c43d15f21 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfint.code.tex" 1557692582 3063 8c415c68a0f3394e45cfeca0b65f6ee6 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex" 1673816307 949 cea70942e7b7eddabfb3186befada2e6 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathcalc.code.tex" 1673816307 13270 2e54f2ce7622437bf37e013d399743e3 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfloat.code.tex" 1673816307 104717 9b2393fbf004a0ce7fa688dbce423848 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.base.code.tex" 1601326656 10165 cec5fa73d49da442e56efc2d605ef154 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.basic.code.tex" 1601326656 28178 41c17713108e0795aac6fef3d275fbca ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.code.tex" 1673816307 9649 85779d3d8d573bfd2cd4137ba8202e60 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.comparison.code.tex" 1601326656 3865 ac538ab80c5cf82b345016e474786549 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.integerarithmetics.code.tex" 1557692582 3177 27d85c44fbfe09ff3b2cf2879e3ea434 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.misc.code.tex" 1621110968 11024 0179538121bc2dba172013a3ef89519f ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.random.code.tex" 1673816307 7890 0a86dbf4edfd88d022e0d889ec78cc03 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.round.code.tex" 1601326656 3379 781797a101f647bab82741a99944a229 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.trigonometric.code.tex" 1601326656 92405 f515f31275db273f97b9d8f52e1b0736 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathparser.code.tex" 1673816307 37466 97b0a1ba732e306a1a2034f5a73e239f ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathutil.code.tex" 1601326656 8471 c2883569d03f69e8e1cabfef4999cfd7 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/modules/pgfmoduledecorations.code.tex" 1673816307 71742 3da44a8be6626eef1c400c68776c7a0f ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/modules/pgfmodulematrix.code.tex" 1673816307 21211 1e73ec76bd73964d84197cc3d2685b01 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/modules/pgfmoduleplot.code.tex" 1601326656 16121 346f9013d34804439f7436ff6786cef7 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/modules/pgfmoduleshapes.code.tex" 1673816307 44792 271e2e1934f34c759f4dedb1e14a5015 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/pgf.revision.tex" 1673816307 114 e6d443369d0673933b38834bf99e422d ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/systemlayer/pgf.cfg" 1601326656 926 2963ea0dcf6cc6c0a770b69ec46a477b ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-common-pdf.def" 1673816307 5542 32f75a31ea6c3a7e1148cd6d5e93dbb7 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-pdftex.def" 1673816307 12612 7774ba67bfd72e593c4436c2de6201e3 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/systemlayer/pgfsys.code.tex" 1673816307 61351 bc5f86e0355834391e736e97a61abced ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/systemlayer/pgfsysprotocol.code.tex" 1601326656 1896 b8e0ca0ac371d74c0ca05583f6313c91 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/systemlayer/pgfsyssoftpath.code.tex" 1601326656 7778 53c8b5623d80238f6a20aa1df1868e63 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfcalendar.code.tex" 1673816307 24149 056c3eb5ebac53bc396649bc52434c12 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgffor.code.tex" 1673816307 24033 d8893a1ec4d1bfa101b172754743d340 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfkeys.code.tex" 1673816307 39784 414c54e866ebab4b801e2ad81d9b21d8 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfkeyslibraryfiltered.code.tex" 1673816307 37433 940bc6d409f1ffd298adfdcaf125dd86 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfrcs.code.tex" 1673816307 4385 510565c2f07998c8a0e14f0ec07ff23c ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfutil-common.tex" 1673816307 29239 22e8c7516012992a49873eff0d868fed ""
+  "/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfutil-latex.def" 1673816307 6950 8524a062d82b7afdc4a88a57cb377784 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/xkeyval/xkeyval.tex" 1655411236 19231 27205ee17aaa2902aea3e0c07a3cfc65 ""
+  "/usr/share/texlive/texmf-dist/tex/generic/xkeyval/xkvutils.tex" 1655411236 7677 9cb1a74d945bc9331f2181c0a59ff34a ""
+  "/usr/share/texlive/texmf-dist/tex/latex/adjustbox/adjcalc.sty" 1666037967 5598 c49b91713cbe5e50a1fabefb733eda0d ""
+  "/usr/share/texlive/texmf-dist/tex/latex/adjustbox/adjustbox.sty" 1666037967 56907 e3e515e490dbc35309a010b5bbe1bef5 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/adjustbox/tc-pdftex.def" 1666037967 4070 1677cfee6374067b93f61cf57ecd7144 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/adjustbox/trimclip.sty" 1666037967 7244 36558f478da08e083d7316a63ba4bcd6 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty" 1359763108 5949 3f3fd50a8cc94c3d4cbf4fc66cd3df1c ""
+  "/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty" 1359763108 13829 94730e64147574077f8ecfea9bb69af4 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty" 1686341992 2222 499d61426192c39efd8f410ee1a52b9c ""
+  "/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty" 1686341992 4173 82ac04dfb1256038fad068287fbb4fe6 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty" 1686341992 88371 d84032c0f422c3d1e282266c01bef237 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty" 1686341992 4474 b811654f4bf125f11506d13d13647efb ""
+  "/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty" 1686341992 2444 0d0c1ee65478277e8015d65b86983da2 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/base/article.cls" 1705352648 20144 147463a6a579f4597269ef9565205cfe ""
+  "/usr/share/texlive/texmf-dist/tex/latex/base/ifthen.sty" 1705352648 5319 2b738d02ce36ada6dcdd9534940db0ee ""
+  "/usr/share/texlive/texmf-dist/tex/latex/base/inputenc.sty" 1705352648 5048 425739d70251273bf93e3d51f3c40048 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/base/size12.clo" 1705352648 8449 f07039d8e4e89f21078d9b5137579bfc ""
+  "/usr/share/texlive/texmf-dist/tex/latex/booktabs/booktabs.sty" 1579038678 6078 f1cb470c9199e7110a27851508ed7a5c ""
+  "/usr/share/texlive/texmf-dist/tex/latex/cite/cite.sty" 1425427964 26218 19edeff8cdc2bcb704e8051dc55eb5a7 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/collectbox/collectbox.sty" 1666037909 9124 59c3b56f1a073de66e3eea35f9c173c8 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/colortbl/colortbl.sty" 1659300143 12441 3b2a708337608012a865c7d9b7f05d28 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/currfile/currfile.sty" 1665433346 10709 a0fbaa73a4497077eef19db56dca76fd ""
+  "/usr/share/texlive/texmf-dist/tex/latex/datetime/datetime-defaults.sty" 1427500626 4105 4c80eaed8cd4f9a80cc6244c0adeb81f ""
+  "/usr/share/texlive/texmf-dist/tex/latex/datetime/datetime.sty" 1427500626 27587 b023ffe1328fa89e7f133201d87029de ""
+  "/usr/share/texlive/texmf-dist/tex/latex/enumitem/enumitem.sty" 1561238569 51697 f8f08183cd2080d9d18a41432d651dfb ""
+  "/usr/share/texlive/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty" 1579991033 13886 d1306dcf79a944f6988e688c1785f9ce ""
+  "/usr/share/texlive/texmf-dist/tex/latex/eso-pic/eso-pic.sty" 1683144721 11876 6ef493863ae0d7a984706973240c2237 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/etoolbox/etoolbox.sty" 1601931149 46845 3b58f70c6e861a13d927bff09d35ecbc ""
+  "/usr/share/texlive/texmf-dist/tex/latex/filehook/filehook-2020.sty" 1666814490 9005 c47d9138e4a690658bcefab0dd0af8d7 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/filehook/filehook.sty" 1666814490 1210 95c2d0abf75beadf7e7547b73b345c24 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/filemod/filemod-expmin.sty" 1316560476 2845 2b7393c472a738889b77cb266b9ef35d ""
+  "/usr/share/texlive/texmf-dist/tex/latex/fmtcount/fc-english.def" 1580337424 14353 f66b7dd28616119c2519cd5cc4dcae14 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/fmtcount/fcnumparser.sty" 1580337424 12389 43a81443714469abac77ce09f44ad2e2 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/fmtcount/fcprefix.sty" 1580337424 12098 5c732241af77b5f0e56e640b7d538395 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/fmtcount/fmtcount.sty" 1582668197 30872 ed70d543c537f19c96fc753321f1c3cc ""
+  "/usr/share/texlive/texmf-dist/tex/latex/geometry/geometry.sty" 1578002852 41601 9cf6c5257b1bc7af01a58859749dd37a ""
+  "/usr/share/texlive/texmf-dist/tex/latex/gincltex/gincltex.sty" 1315265409 3594 7c105130ddd1211e8275b3c1288d84c8 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/graphics-cfg/color.cfg" 1459978653 1213 620bba36b25224fa9b7e1ccb4ecb76fd ""
+  "/usr/share/texlive/texmf-dist/tex/latex/graphics-cfg/graphics.cfg" 1465944070 1224 978390e9c2234eab29404bc21b268d1e ""
+  "/usr/share/texlive/texmf-dist/tex/latex/graphics-def/pdftex.def" 1663965824 19448 1e988b341dda20961a6b931bcde55519 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/graphics/color.sty" 1654720880 7233 e46ce9241d2b2ca2a78155475fdd557a ""
+  "/usr/share/texlive/texmf-dist/tex/latex/graphics/graphics.sty" 1654720880 18387 8f900a490197ebaf93c02ae9476d4b09 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/graphics/graphicx.sty" 1654720880 8010 a8d949cbdbc5c983593827c9eec252e1 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty" 1654720880 2671 7e67d78d9b88c845599a85b2d41f2e39 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/graphics/lscape.sty" 1654720880 1822 5e4f855a9ecb640f34881e4b457fa9aa ""
+  "/usr/share/texlive/texmf-dist/tex/latex/graphics/mathcolor.ltx" 1667332637 2885 9c645d672ae17285bba324998918efd8 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/graphics/rotating.sty" 1654720880 7060 497c495d7b832441a479571bbce898ae ""
+  "/usr/share/texlive/texmf-dist/tex/latex/graphics/trig.sty" 1654720880 4023 293ea1c16429fc0c4cf605f4da1791a9 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/ifoddpage/ifoddpage.sty" 1666126449 2142 eae42205b97b7a3ad0e58db5fe99e3e6 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/kvoptions/kvoptions.sty" 1655478651 22555 6d8e155cfef6d82c3d5c742fea7c992e ""
+  "/usr/share/texlive/texmf-dist/tex/latex/kvsetkeys/kvsetkeys.sty" 1665067230 13815 760b0c02f691ea230f5359c4e1de23a7 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def" 1704491087 30006 57b07afb710ee2f649c65cfbafda39c1 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg" 1279039959 678 4792914a8f45be57bb98413425e4c7af ""
+  "/usr/share/texlive/texmf-dist/tex/latex/listings/listings.cfg" 1677530001 1829 d8258b7d94f5f955e70c623e525f9f45 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/listings/listings.sty" 1677530001 80947 75a96bb4c9f40ae31d54a01d924df2ff ""
+  "/usr/share/texlive/texmf-dist/tex/latex/listings/lstmisc.sty" 1677530001 77021 d05e9115c67855816136d82929db8892 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/makecell/makecell.sty" 1249334690 15773 2dd7dde1ec1c2a3d0c85bc3b273e04d8 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/multirow/multirow.sty" 1615845910 6149 2398eec4faa1ee24ff761581e580ecf1 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/pdflscape/pdflscape-nometadata.sty" 1667072951 6572 ea530fbbe537629fd97736d33babc07d ""
+  "/usr/share/texlive/texmf-dist/tex/latex/pdflscape/pdflscape.sty" 1667072951 2224 1230ab76aa62221ccbd90bca8c8c015e ""
+  "/usr/share/texlive/texmf-dist/tex/latex/pdfpages/pdfpages.sty" 1705871773 54914 ea9713532d0d0ae802ca2446650f9ded ""
+  "/usr/share/texlive/texmf-dist/tex/latex/pdfpages/pppdftex.def" 1705871773 6591 249ecc067cc3246c4ed39a577ded77e3 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/pgf/basiclayer/pgf.sty" 1601326656 1090 bae35ef70b3168089ef166db3e66f5b2 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/pgf/basiclayer/pgfcore.sty" 1673816307 373 00b204b1d7d095b892ad31a7494b0373 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/pgf/compatibility/pgfcomp-version-0-65.sty" 1601326656 21013 f4ff83d25bb56552493b030f27c075ae ""
+  "/usr/share/texlive/texmf-dist/tex/latex/pgf/compatibility/pgfcomp-version-1-18.sty" 1601326656 989 c49c8ae06d96f8b15869da7428047b1e ""
+  "/usr/share/texlive/texmf-dist/tex/latex/pgf/frontendlayer/tikz.sty" 1601326656 339 c2e180022e3afdb99c7d0ea5ce469b7d ""
+  "/usr/share/texlive/texmf-dist/tex/latex/pgf/math/pgfmath.sty" 1601326656 306 c56a323ca5bf9242f54474ced10fca71 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/pgf/systemlayer/pgfsys.sty" 1601326656 443 8c872229db56122037e86bcda49e14f3 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/pgf/utilities/pgfcalendar.sty" 1601326656 328 7411531f2e9e5c6aa139c84fbe10702e ""
+  "/usr/share/texlive/texmf-dist/tex/latex/pgf/utilities/pgffor.sty" 1601326656 348 ee405e64380c11319f0e249fed57e6c5 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/pgf/utilities/pgfkeys.sty" 1601326656 274 5ae372b7df79135d240456a1c6f2cf9a ""
+  "/usr/share/texlive/texmf-dist/tex/latex/pgf/utilities/pgfrcs.sty" 1601326656 325 f9f16d12354225b7dd52a3321f085955 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/pgfgantt/pgfgantt.sty" 1515620707 47785 88c861f46c2f86a25c7b7d0c7b0072ed ""
+  "/usr/share/texlive/texmf-dist/tex/latex/psnfss/mathptmx.sty" 1586716065 4631 6e41de2b7a83dfa5d2c4b0a2fe01f046 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/psnfss/omlztmcm.fd" 1137110629 411 12564a37a279e4e0b533cdf5e03eeb7c ""
+  "/usr/share/texlive/texmf-dist/tex/latex/psnfss/omsztmcm.fd" 1137110629 348 f4ce75d394e7d9ac12ca7aac4045ed77 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/psnfss/omxztmcm.fd" 1137110629 329 c8cddcc90b6f567b28408eb374773c9c ""
+  "/usr/share/texlive/texmf-dist/tex/latex/psnfss/ot1ptm.fd" 1137110629 961 15056f4a61917ceed3a44e4ac11fcc52 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/psnfss/ot1ztmcm.fd" 1137110629 329 aee7226812ba4138ac67a018466b488d ""
+  "/usr/share/texlive/texmf-dist/tex/latex/psnfss/ts1ptm.fd" 1137110629 619 96f56dc5d1ef1fe1121f1cfeec70ee0c ""
+  "/usr/share/texlive/texmf-dist/tex/latex/setspace/setspace.sty" 1670275497 22490 8cac309b79a4c53a4ffce4b1b07aead0 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/standalone/standalone.sty" 1665433651 34855 01a6d48b146a4c824944925004b07205 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/svn-prov/svn-prov.sty" 1272330018 6852 44ea8d7e58290cde708a34ebf3953571 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/titlesec/titlesec.sty" 1698436711 48766 0b93839be28e9744a24c45075c75b2e2 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/tocbibind/tocbibind.sty" 1287012853 8927 46f54e33fc9cef24f78ab3bc811cb63f ""
+  "/usr/share/texlive/texmf-dist/tex/latex/tools/array.sty" 1698869629 12667 e4b5eb11e4b7239e6c8a52bbe074a6c6 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/tools/calc.sty" 1698869629 10214 547fd4d29642cb7c80bf54b49d447f01 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/tools/dcolumn.sty" 1698869629 2758 6d8c3b2be328b1495f570893443a8736 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/tools/shellesc.sty" 1698869629 4121 f96144e646260251ded7f19bcb6f4e71 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/tools/tabularx.sty" 1698869629 7147 d45559f8a31b8c53ada0640516660003 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/url/url.sty" 1388531844 12796 8edb7d69a20b857904dd0ea757c14ec9 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/varwidth/varwidth.sty" 1238697683 10894 d359a13923460b2a73d4312d613554c8 ""
+  "/usr/share/texlive/texmf-dist/tex/latex/xcolor/xcolor.sty" 1700082560 55487 80a65caedd3722f4c20a14a69e785d8f ""
+  "/usr/share/texlive/texmf-dist/tex/latex/xkeyval/xkeyval.sty" 1655411236 4937 4ce600ce9bd4ec84d0250eb6892fcf4f ""
+  "/usr/share/texlive/texmf-dist/web2c/texmf.cnf" 1707919699 40399 f2c302f7d2af602abb742093540a5834 ""
+  "/usr/share/texmf/web2c/texmf.cnf" 1707919699 40399 f2c302f7d2af602abb742093540a5834 ""
+  "/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map" 1760105440.02229 5312232 f3296911be9cc021788f3f879cf0a47d ""
+  "/var/lib/texmf/web2c/pdftex/pdflatex.fmt" 1726065868 6800790 607442c924ed54405961d2b8ac2a25ae ""
+  "1-goals-and-outcomes/research_statement_v2.tex" 1764988975.93677 4450 070caee751214eaddffa6b3403f8ed43 ""
+  "1-goals-and-outcomes/v8.tex" 1764987710.74095 5825 07f6fba24cfa050a3b2b00c416f0f45f ""
+  "2-state-of-the-art/v7.tex" 1764987725.29096 10609 44863eb08e23052a1623ef3ebcb1e3ae ""
+  "3-research-approach/v5.tex" 1764987711.02695 17228 76776c8f57e50cca2efc146c8bbe301e ""
+  "4-metrics-of-success/v3.tex" 1764987211.44054 5586 e5fb80ced00bcdc318ffe3861b0064bc ""
+  "5-risks-and-contingencies/v3.tex" 1764987320.59343 10412 17e755aa8451c45198372af7afe3c500 ""
+  "6-broader-impacts/v3.tex" 1764987383.35954 4834 418aae223b778759691eaf9124a5360c ""
+  "7-budget/v2.tex" 1764989376.54455 7317 5cdea8ea5ec67b0fc00884e406429935 ""
+  "8-schedule/v2.tex" 1764989806.19871 4473 8ad96bbf9cedf2ea09298ecbd4e01b83 ""
+  "9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf" 1764192995.54731 76839 d12cfa78304f51e96ce0e12460ece1e3 ""
+  "9-supplemental-sections/cv-1786798.pdf" 1764192995.54731 31602 224112b9f507ae1e989c0341a7eb3f42 ""
+  "9-supplemental-sections/v1.tex" 1764975820.90587 2306 2e5bf084cf72f93d80cf9138d1569d6f ""
+  "dane_proposal_format.cls" 1764990266.03918 2581 ff22f600587ffbc4d06e6b2a42f70c6e ""
+  "main.aux" 1764990467.86727 6961 b67c1d53687261878883c1352f4b1410 "pdflatex"
+  "main.bbl" 1764990267.84655 5012 668a266823d48f68a9ac1ddb0c83466e "bibtex main"
+  "main.tex" 1764990070.94187 979 6111485af35d67a2918f2bc5ac1beeb0 ""
+  "main.toc" 1764990467.86827 3034 1f2c010ba6afb7a4edffb1989ad7b820 "pdflatex"
+  (generated)
+  "main.aux"
+  "main.log"
+  "main.pdf"
+  "main.toc"
+  (rewritten before read)

Writing/THESIS_PROPOSAL/main.fls

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

Writing/THESIS_PROPOSAL/main.tex

@@ -0,0 +1,33 @@
+\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}
+\input{2-state-of-the-art/v1}
+\input{3-research-approach/v1}
+\input{4-metrics-of-success/v1}
+\input{5-risks-and-contingencies/v1}
+\input{6-broader-impacts/v1}
+\input{8-schedule/v1}
+\newpage
+\bibliographystyle{ieeetr}
+\bibliography{references}
+
+% White Paper (optional)
+% \input{whitepaper/v1}
+
+\end{document}

Writing/THESIS_PROPOSAL/main.toc

@@ -0,0 +1,41 @@
+\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}{2}{}%
+\contentsline {subsection}{\numberline {2.1}Current Reactor Procedures and Operation}{2}{}%
+\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}{5}{}%
+\contentsline {section}{\numberline {4}Metrics for Success}{9}{}%
+\contentsline {paragraph}{TRL 3 \textit {Critical Function and Proof of Concept}}{10}{}%
+\contentsline {paragraph}{TRL 4 \textit {Laboratory Testing of Integrated Components}}{10}{}%
+\contentsline {paragraph}{TRL 5 \textit {Laboratory Testing in Relevant Environment}}{10}{}%
+\contentsline {section}{\numberline {5}Risks and Contingencies}{11}{}%
+\contentsline {subsection}{\numberline {5.1}Computational Tractability of Synthesis}{11}{}%
+\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{11}{}%
+\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{12}{}%
+\contentsline {section}{\numberline {6}Broader Impacts}{13}{}%
+\contentsline {section}{\numberline {7}Schedule, Milestones, and Deliverables}{14}{}%
+\contentsline {subsection}{\numberline {7.1}Milestones and Deliverables}{15}{}%
+\contentsline {section}{References}{16}{}%
+\contentsline {section}{\numberline {8}Budget and Budget Justification}{I}{}%
+\contentsline {subsection}{\numberline {8.1}Budget Summary}{I}{}%
+\contentsline {subsection}{\numberline {8.2}Budget Justification}{II}{}%
+\contentsline {subsubsection}{\numberline {8.2.1}Senior Personnel}{II}{}%
+\contentsline {paragraph}{Faculty Advisor}{II}{}%
+\contentsline {subsubsection}{\numberline {8.2.2}Other Personnel}{II}{}%
+\contentsline {paragraph}{Graduate Research Assistant (Principal Investigator)}{II}{}%
+\contentsline {subsubsection}{\numberline {8.2.3}Fringe Benefits}{II}{}%
+\contentsline {paragraph}{Faculty Fringe Benefits}{II}{}%
+\contentsline {paragraph}{Graduate Research Assistant Fringe Benefits}{II}{}%
+\contentsline {subsubsection}{\numberline {8.2.4}Travel}{II}{}%
+\contentsline {paragraph}{Conference Travel (\$4,000 per year)}{II}{}%
+\contentsline {paragraph}{Industry Collaboration Visits (\$1,500 per year)}{II}{}%
+\contentsline {subsubsection}{\numberline {8.2.5}Other Direct Costs}{II}{}%
+\contentsline {paragraph}{Materials and Supplies}{II}{}%
+\contentsline {paragraph}{Publication Costs}{II}{}%
+\contentsline {paragraph}{Computing and Cloud Services}{III}{}%
+\contentsline {subsubsection}{\numberline {8.2.6}H. Indirect Costs (Facilities \& Administrative)}{III}{}%
+\contentsline {section}{\numberline {9}Supplemental Sections}{III}{}%
+\contentsline {subsection}{\numberline {9.1}Biosketch}{III}{}%
+\contentsline {subsection}{\numberline {9.2}Data Management Plan}{VI}{}%
+\contentsline {subsection}{\numberline {9.3}Facilities}{X}{}%

Writing/THESIS_PROPOSAL/references.bib

@@ -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},
+}

Writing/THESIS_PROPOSAL/references_old.bib

@@ -0,0 +1,547 @@
+% Foundational Papers
+
+@article{alur1995algorithmic,
+  title={The algorithmic analysis of hybrid systems},
+  author={Alur, Rajeev and Courcoubetis, Costas and Halbwachs, Nicolas and Henzinger, Thomas A and Ho, Pei-Hsin and Nicollin, Xavier and Olivero, Alfredo and Sifakis, Joseph and Yovine, Sergio},
+  journal={Theoretical Computer Science},
+  volume={138},
+  number={1},
+  pages={3--34},
+  year={1995},
+  publisher={Elsevier}
+}
+
+@inproceedings{alur1993hybrid,
+  title={Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems},
+  author={Alur, Rajeev and Courcoubetis, Costas and Henzinger, Thomas A and Ho, Pei-Hsin},
+  booktitle={Hybrid Systems},
+  pages={209--229},
+  year={1993},
+  publisher={Springer}
+}
+
+@article{mitchell2005time,
+  title={A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games},
+  author={Mitchell, Ian M and Bayen, Alexandre M and Tomlin, Claire J},
+  journal={IEEE Transactions on Automatic Control},
+  volume={50},
+  number={7},
+  pages={947--957},
+  year={2005},
+  publisher={IEEE}
+}
+
+@article{platzer2008differential,
+  title={Differential dynamic logic for hybrid systems},
+  author={Platzer, Andr{\'e}},
+  journal={Journal of Automated Reasoning},
+  volume={41},
+  number={2},
+  pages={143--189},
+  year={2008},
+  publisher={Springer}
+}
+
+@article{platzer2017complete,
+  title={A complete uniform substitution calculus for differential dynamic logic},
+  author={Platzer, Andr{\'e}},
+  journal={Journal of Automated Reasoning},
+  volume={59},
+  number={2},
+  pages={219--265},
+  year={2017},
+  publisher={Springer}
+}
+
+@inproceedings{donze2010robust,
+  title={Robust satisfaction of temporal logic over real-valued signals},
+  author={Donz{\'e}, Alexandre and Maler, Oded},
+  booktitle={International Conference on Formal Modeling and Analysis of Timed Systems},
+  pages={92--106},
+  year={2010},
+  publisher={Springer}
+}
+
+% Control Theory and Stability
+
+@article{geromel2006stability,
+  title={Stability and stabilization of continuous-time switched linear systems},
+  author={Geromel, Jos{\'e} C and Colaneri, Patrizio},
+  journal={SIAM Journal on Control and Optimization},
+  volume={45},
+  number={5},
+  pages={1915--1930},
+  year={2006},
+  publisher={SIAM}
+}
+
+@book{liberzon2003switching,
+  title={Switching in systems and control},
+  author={Liberzon, Daniel},
+  year={2003},
+  publisher={Birkh{\"a}user Boston}
+}
+
+@article{branicky1998multiple,
+  title={Multiple Lyapunov functions and other analysis tools for switched and hybrid systems},
+  author={Branicky, Michael S},
+  journal={IEEE Transactions on Automatic Control},
+  volume={43},
+  number={4},
+  pages={475--482},
+  year={1998},
+  publisher={IEEE}
+}
+
+% Recent Advances (2020-2025)
+
+@article{yang2024learning,
+  title={Learning Local Control Barrier Functions for Hybrid Systems},
+  author={Yang, Shuo and Chen, Yiwei and Yin, Xiang and Mangharam, Rahul},
+  journal={arXiv preprint arXiv:2401.14907},
+  year={2024}
+}
+
+@inproceedings{su2024switching,
+  title={Switching Controller Synthesis for Hybrid Systems Against STL Formulas},
+  author={Su, Mingyu and Vizel, Yakir and Vardi, Moshe Y},
+  booktitle={International Symposium on Formal Methods},
+  pages={231--248},
+  year={2024},
+  publisher={Springer}
+}
+
+@article{yao2024model,
+  title={Model predictive control of stochastic hybrid systems with signal temporal logic constraints},
+  author={Yao, Li and Wang, Yiming and Chen, Xiang},
+  journal={Automatica},
+  volume={159},
+  pages={111037},
+  year={2024},
+  publisher={Elsevier}
+}
+
+@article{yu2024online,
+  title={Online control synthesis for uncertain systems under signal temporal logic specifications},
+  author={Yu, Pian and Gao, Yulong and Jiang, Frank J and Johansson, Karl H and Dimarogonas, Dimos V},
+  journal={The International Journal of Robotics Research},
+  volume={43},
+  number={3},
+  pages={284--307},
+  year={2024},
+  publisher={SAGE}
+}
+
+% Tools and Frameworks
+
+@inproceedings{meyer2018strix,
+  title={Strix: Explicit reactive synthesis strikes back!},
+  author={Meyer, Philipp J and Luttenberger, Michael},
+  booktitle={International Conference on Computer Aided Verification},
+  pages={578--586},
+  year={2018},
+  publisher={Springer}
+}
+
+@techreport{giannakopoulou2022fret,
+  title={Capturing and Analyzing Requirements with FRET},
+  author={Giannakopoulou, Dimitra and Mavridou, Anastasia and Rhein, Julian and Pressburger, Thomas and Schumann, Johann and Shi, Nija},
+  institution={NASA Ames Research Center},
+  year={2022},
+  number={NASA/TM-20220007610}
+}
+
+@inproceedings{fulton2015keymaera,
+  title={KeYmaera X: An axiomatic tactical theorem prover for hybrid systems},
+  author={Fulton, Nathan and Mitsch, Stefan and Quesel, Jan-David and V{\"o}lp, Marcus and Platzer, Andr{\'e}},
+  booktitle={International Conference on Automated Deduction},
+  pages={527--538},
+  year={2015},
+  publisher={Springer}
+}
+
+@inproceedings{frehse2011spaceex,
+  title={SpaceEx: Scalable verification of hybrid systems},
+  author={Frehse, Goran and Le Guernic, Colas and Donz{\'e}, Alexandre and Cotton, Scott and Ray, Rajarshi and Lebeltel, Olivier and Ripado, Rodolfo and Girard, Antoine and Dang, Thao and Maler, Oded},
+  booktitle={International Conference on Computer Aided Verification},
+  pages={379--395},
+  year={2011},
+  publisher={Springer}
+}
+
+@inproceedings{chen2013flow,
+  title={Flow*: An analyzer for non-linear hybrid systems},
+  author={Chen, Xin and {\'A}brah{\'a}m, Erika and Sankaranarayanan, Sriram},
+  booktitle={International Conference on Computer Aided Verification},
+  pages={258--263},
+  year={2013},
+  publisher={Springer}
+}
+
+@inproceedings{larsen1997uppaal,
+  title={UPPAAL in a nutshell},
+  author={Larsen, Kim G and Pettersson, Paul and Yi, Wang},
+  journal={International Journal on Software Tools for Technology Transfer},
+  volume={1},
+  number={1-2},
+  pages={134--152},
+  year={1997},
+  publisher={Springer}
+}
+
+% Reachability and Verification
+
+
+@INPROCEEDINGS{bansal2017hamilton,
+  author={Bansal, Somil and Chen, Mo and Herbert, Sylvia and Tomlin, Claire J.},
+  booktitle={2017 IEEE 56th Annual Conference on Decision and Control (CDC)}, 
+  title={Hamilton-Jacobi reachability: A brief overview and recent advances}, 
+  year={2017},
+  volume={},
+  pages={2242-2253},
+  keywords={Games;Safety;Tools;Trajectory;Tutorials;Level set;Aircraft},
+  doi={10.1109/CDC.2017.8263977}
+}
+
+@article{althoff2021set,
+  title={Set propagation techniques for reachability analysis},
+  author={Althoff, Matthias and Frehse, Goran and Girard, Antoine},
+  journal={Annual Review of Control, Robotics, and Autonomous Systems},
+  volume={4},
+  pages={369--395},
+  year={2021},
+  publisher={Annual Reviews}
+}
+
+@inproceedings{tabuada2004compositional,
+  title={Compositional abstractions of hybrid control systems},
+  author={Tabuada, Paulo and Pappas, George J and Lima, Pedro},
+  journal={Discrete Event Dynamic Systems},
+  volume={14},
+  number={2},
+  pages={203--238},
+  year={2004},
+  publisher={Springer}
+}
+
+% Applications
+
+@article{varaiya1993smart,
+  title={Smart cars on smart roads: Problems of control},
+  author={Varaiya, Pravin},
+  journal={IEEE Transactions on Automatic Control},
+  volume={38},
+  number={2},
+  pages={195--207},
+  year={1993},
+  publisher={IEEE}
+}
+
+@article{verlinden2024hybrid,
+  title={Hybrid reliability modeling of nuclear safety systems: A case study on the reactor protection system of a research reactor},
+  author={Verlinden, S and Deridder, F and Wagemans, P},
+  journal={Nuclear Engineering and Design},
+  volume={417},
+  pages={112868},
+  year={2024},
+  publisher={Elsevier}
+}
+
+% Competitions and Benchmarks
+
+@inproceedings{hscc2024proceedings,
+  title={Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control},
+  booktitle={HSCC '24},
+  year={2024},
+  publisher={ACM},
+  address={New York, NY, USA}
+}
+
+@inproceedings{jacobs2017syntcomp,
+  title={The 4th reactive synthesis competition (SYNTCOMP 2017): Benchmarks, participants \& results},
+  author={Jacobs, Swen and Bloem, Roderick and Brenguier, Romain and others},
+  booktitle={6th Workshop on Synthesis},
+  year={2017},
+  series={EPTCS},
+  volume={260}
+}
+
+% Supporting Papers
+
+@article{wabersich2018linear,
+  title={Linear model predictive safety certification for learning-based control},
+  author={Wabersich, Kim P and Zeilinger, Melanie N},
+  journal={Automatica},
+  volume={97},
+  pages={48--59},
+  year={2018},
+  publisher={Elsevier}
+}
+
+@inproceedings{prajna2004safety,
+  title={Safety verification of hybrid systems using barrier certificates},
+  author={Prajna, Stephen and Jadbabaie, Ali},
+  booktitle={International Workshop on Hybrid Systems: Computation and Control},
+  pages={477--492},
+  year={2004},
+  publisher={Springer}
+}
+
+@article{ames2017control,
+  title={Control barrier function based quadratic programs for safety critical systems},
+  author={Ames, Aaron D and Xu, Xiangru and Grizzle, Jessy W and Tabuada, Paulo},
+  journal={IEEE Transactions on Automatic Control},
+  volume={62},
+  number={8},
+  pages={3861--3876},
+  year={2017},
+  publisher={IEEE}
+}
+
+@article{srinivasan2018control,
+  title={Control of mobile robots using barrier functions under temporal logic specifications},
+  author={Srinivasan, Mohit and Coogan, Samuel},
+  journal={IEEE Transactions on Robotics},
+  volume={37},
+  number={2},
+  pages={363--374},
+  year={2021},
+  publisher={IEEE}
+}
+
+%broader impacts
+@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}
+}
+@techreport{DOE-HDBK-1028-2009,
+  title        = {Human Performance Handbook},
+  author       = {{U.S. Department of Energy}},
+  institution  = {U.S. Department of Energy},
+  year         = {2009},
+  number       = {DOE-HDBK-1028-2009},
+  type         = {Handbook}
+}
+
+@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{Wang2025,
+  title   = {Analysis of Human Error in Nuclear Power Plant Operations: A Systematic Review of Events from 2007--2020},
+  author  = {Wang, Y. and others},
+  journal = {Journal of Nuclear Safety},
+  year    = {2025},
+  note    = {Analysis of 190 events at Chinese nuclear power plants}
+}
+
+@misc{10CFR55,
+  title        = {Operators' Licenses},
+  author       = {{U.S. Nuclear Regulatory Commission}},
+  howpublished = {10 CFR Part 55},
+  note         = {Code of Federal Regulations}
+}
+
+@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{10CFR50,
+  title        = {Domestic Licensing of Production and Utilization Facilities},
+  author       = {{U.S. Nuclear Regulatory Commission}},
+  howpublished = {10 CFR Part 50},
+  note         = {Code of Federal Regulations}
+}
+
+@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}
+}
+
+@techreport{IAEA-TECDOC-1580,
+  title       = {Good Practices for Cost Effective Maintenance of Nuclear Power Plants},
+  author      = {{International Atomic Energy Agency}},
+  institution = {International Atomic Energy Agency},
+  year        = {2007},
+  number      = {TECDOC-1580}
+}
+
+@techreport{NUREG-2114,
+  title       = {Cognitive Basis for Human Reliability Analysis},
+  author      = {{U.S. Nuclear Regulatory Commission}},
+  institution = {U.S. Nuclear Regulatory Commission},
+  year        = {2016},
+  number      = {NUREG-2114}
+}
+
+@article{Zerovnik2023,
+  title   = {Knowledge Transfer Challenges in Nuclear Operations},
+  author  = {\v{Z}erovnik, Gašper and others},
+  journal = {Nuclear Engineering and Design},
+  year    = {2023},
+  note    = {Analysis of knowledge transfer from experienced operators}
+}
+
+@article{Jo2021,
+  title   = {Automation Paradox in Nuclear Power Plant Control: Effects on Operator Situation Awareness},
+  author  = {Jo, Y. and others},
+  journal = {Nuclear Engineering and Technology},
+  year    = {2021},
+  note    = {Empirical study of automation effects on operator performance}
+}
+
+@techreport{IAEA2008,
+  title       = {Modern Instrumentation and Control for Nuclear Power Plants: A Guidebook},
+  author      = {{International Atomic Energy Agency}},
+  institution = {International Atomic Energy Agency},
+  year        = {2008},
+  number      = {Technical Reports Series No. 387}
+}
+
+@article{Lee2019,
+  title   = {Autonomous Control of Nuclear Reactors Using Long Short-Term Memory Networks},
+  author  = {Lee, D. and others},
+  journal = {Nuclear Engineering and Technology},
+  year    = {2019},
+  note    = {Demonstration of LSTM-based autonomous control in LOC and SGTR scenarios}
+}
+
+@inproceedings{IEEE2019,
+  title     = {Formal Verification Challenges for Nuclear I\&C Systems},
+  author    = {{IEEE Working Group}},
+  booktitle = {IEEE Conference on Nuclear Power Instrumentation, Control and Human-Machine Interface Technologies},
+  year      = {2019},
+  note      = {Discussion of state space explosion in formal verification}
+}
+
+@misc{IAEA-severe-accidents,
+  title        = {Human Error as Root Cause in Severe Nuclear Accidents},
+  author       = {{International Atomic Energy Agency}},
+  howpublished = {IAEA Safety Report},
+  note         = {Analysis of TMI, Chernobyl, and Fukushima accidents}
+}
+
+@article{Dumas1999,
+  title   = {Worker Error and Safety in Nuclear Facilities},
+  author  = {Dumas, Lloyd},
+  journal = {Journal of Nuclear Safety},
+  year    = {1999},
+  note    = {Study of incidents at 10 nuclear centers}
+}
+
+@techreport{IAEA-INSAG-1,
+  title       = {Summary Report on the Post-Accident Review Meeting on the Chernobyl Accident},
+  author      = {{International Nuclear Safety Advisory Group}},
+  institution = {International Atomic Energy Agency},
+  year        = {1986},
+  number      = {INSAG-1}
+}
+
+@techreport{IAEA-INSAG-7,
+  title       = {The Chernobyl Accident: Updating of INSAG-1},
+  author      = {{International Nuclear Safety Advisory Group}},
+  institution = {International Atomic Energy Agency},
+  year        = {1992},
+  number      = {INSAG-7}
+}
+
+@techreport{NUREG-CR-1278,
+  title       = {Handbook of Human Reliability Analysis with Emphasis on Nuclear Power Plant Applications (THERP)},
+  author      = {Swain, A. D. and Guttmann, H. E.},
+  institution = {U.S. Nuclear Regulatory Commission},
+  year        = {1983},
+  number      = {NUREG/CR-1278}
+}
+
+@techreport{NUREG-CR-6883,
+  title       = {The SPAR-H Human Reliability Analysis Method},
+  author      = {Gertman, D. and others},
+  institution = {U.S. Nuclear Regulatory Commission},
+  year        = {2005},
+  number      = {NUREG/CR-6883}
+}
+
+@techreport{NUREG-2127,
+  title       = {International HRA Empirical Study: Phase 1 Report},
+  author      = {{U.S. Nuclear Regulatory Commission}},
+  institution = {U.S. Nuclear Regulatory Commission},
+  year        = {2013},
+  number      = {NUREG-2127}
+}
+
+@article{Rasmussen1983,
+  title   = {Skills, Rules, and Knowledge; Signals, Signs, and Symbols, and Other Distinctions in Human Performance Models},
+  author  = {Rasmussen, J.},
+  journal = {IEEE Transactions on Systems, Man, and Cybernetics},
+  year    = {1983},
+  volume  = {SMC-13},
+  number  = {3},
+  pages   = {257--266}
+}
+
+@article{Miller1956,
+  title   = {The Magical Number Seven, Plus or Minus Two: Some Limits on Our Capacity for Processing Information},
+  author  = {Miller, George A.},
+  journal = {Psychological Review},
+  year    = {1956},
+  volume  = {63},
+  number  = {2},
+  pages   = {81--97}
+}
+
+@techreport{NUREG-2256,
+  title       = {Integrated Human Event Analysis System for Emergency Crew Actions (IDHEAS-ECA)},
+  author      = {{U.S. Nuclear Regulatory Commission}},
+  institution = {U.S. Nuclear Regulatory Commission},
+  year        = {2022},
+  number      = {NUREG-2256}
+}
+
+@book{Reason1990,
+  title     = {Human Error},
+  author    = {Reason, James},
+  publisher = {Cambridge University Press},
+  year      = {1990}
+}
+
+@article{Lee2018,
+  title   = {Deep Reinforcement Learning for Autonomous Nuclear Reactor Control},
+  author  = {Lee, D. and others},
+  journal = {Nuclear Engineering and Design},
+  year    = {2018},
+  note    = {Demonstration of autonomous control superior to human-plus-automation}
+}
+
+@techreport{Kiniry2022,
+  title       = {High Assurance Rigorous Digital Engineering for Nuclear Safety (HARDENS) Final Technical Report},
+  author      = {Kiniry, Joseph and Bakst, Alexander and Podhradsky, Michal and Hansen, Simon and Bivin, Andrew},
+  institution = {Galois, Inc. / U.S. Nuclear Regulatory Commission},
+  year        = {2022},
+  number      = {ML22326A307},
+  note        = {NRC Contract 31310021C0014}
+}

Writing/THESIS_PROPOSAL/whitepaper/v1.tex

@@ -0,0 +1,421 @@
+% PROJECT SUMMARY
+\section*{Project Summary}
+
+\subsection*{Overview}
+
+This research will develop a methodology for creating autonomous hybrid control
+systems with mathematical guarantees of safe and correct behavior. Nuclear power
+plants require the highest levels of control system reliability, where failures
+can result in significant economic losses or radiological release. Currently,
+nuclear operations rely on extensively trained human operators who follow
+detailed written procedures to manage reactor control. However, reliance on
+human operators prevents introduction of autonomous control capabilities and
+creates fundamental economic challenges for next-generation reactor designs.
+Without introducing automation, emerging technologies like small modular
+reactors face significantly higher per-megawatt staffing costs than conventional
+plants, threatening their economic viability.
+
+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. Hybrid systems use discrete logic to switch between continuous 
+control modes, similar to 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. 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.
+
+\subsection*{Intellectual Merit}
+
+The intellectual merit lies in unifying discrete synthesis and continuous 
+verification to enable end-to-end correctness guarantees for hybrid systems. 
+This research will advance knowledge by developing a systematic, 
+tool-supported methodology for translating written procedures into temporal 
+logic, synthesizing provably correct discrete switching logic, and developing 
+verified continuous controllers. The approach addresses a fundamental gap in 
+hybrid system design by bridging formal methods from computer science and 
+control theory.
+
+\subsection*{Broader Impacts}
+
+This research directly addresses the multi-billion dollar operations and 
+maintenance cost challenge facing nuclear power deployment. By synthesizing 
+provably correct hybrid controllers, we can automate routine operational 
+sequences that currently require constant human oversight, enabling a shift 
+from direct operator control to supervisory monitoring. Beyond nuclear 
+applications, this research will establish a generalizable framework for 
+autonomous control of safety-critical systems including chemical process 
+control, aerospace systems, and autonomous transportation.
+
+\newpage
+
+% RESEARCH DESCRIPTION
+\section*{Research Description}
+
+\section{Objectives}
+% 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
+While human operators have maintained the nuclear industry's exceptional safety
+record, 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, threatening their
+economic viability. 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 from these specifications using reactive synthesis
+tools such as Strix, which generates deterministic automata that are provably
+correct by construction. Third, we will develop and verify 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 methodology by developing an
+autonomous startup controller for a Small Modular Advanced High Temperature
+Reactor (SmAHTR) and implementing it on an Emerson Ovation control system using
+the ARCADE hardware-in-the-loop platform. 
+% Pay-off
+This approach will demonstrate autonomous control can be used for complex
+nuclear power operations while maintaining safety guarantees.
+
+\vspace{11pt}
+
+% 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. This process uses
+    structured intermediate representations to bridge natural language and
+    mathematical logic. 
+    % 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. This trial will include multiple
+    coordinated control modes from cold shutdown through criticality to power
+    operation on a SmAHTR reactor simulation in a hardware-in-the-loop
+    experiment. 
+    % 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}
+\section{State of the Art and Limits of Current Practice}
+
+Automation of some nuclear power operations is already performed today. Highly
+automated systems handle reactor protection and emergency core cooling, while
+human operators retain strategic decision-making. Autonomous systems are trusted
+to handle emergency situations that are considered terminal operations, but
+otherwise introduce too much risk to reactor operations. Contrary to this notion
+is the fact that 70--80\% of all nuclear power plant events are attributed to
+human error rather than equipment failures. The persistence of this ratio despite
+four decades of improvements to procedures and control rooms suggests
+fundamental cognitive limitations rather than remediable deficiencies.
+
+The Nuclear Regulatory Commission has recognized that introducing automation
+into the control room is the only way forward. Recent efforts to apply formal
+methods to nuclear control have shown both promise and remaining gaps. The High
+Assurance Rigorous Digital Engineering for Nuclear Safety (HARDENS) project
+represents the most advanced application to date. HARDENS produced a complete
+Reactor Trip System with full traceability from NRC requirements through formal
+specifications to verified binaries of a controller implementation. The project
+employed formal methods along the control design stack. This comprehensive
+approach demonstrated that formal methods may be technically feasible and
+economically viable for nuclear protection systems.
+
+But despite these accomplishments, HARDENS has a fundamental limitation directly
+relevant to our work. The project addressed only discrete digital control logic
+without modeling or verifying continuous reactor dynamics. Real reactor safety
+depends on interaction between continuous processes and discrete control
+decisions. HARDENS verified the discrete controller in isolation but not the
+closed-loop hybrid system behavior. 
+
+\section{Research Approach}
+
+This research will overcome the identified limitations by combining formal 
+methods from computer science with control theory to build hybrid control 
+systems that are correct by construction. We accomplish this through three 
+main thrusts:
+
+\begin{enumerate} 
+
+  \item We will translate natural language procedures and
+  requirements into temporal logic specifications using the Formal Requirements
+  Elicitation Tool (FRET). 
+
+  \item We will synthesize these temporal logic
+  specifications into the discrete component of the hybrid controller using
+  reactive synthesis. 
+
+  \item We will build continuous control modes that satisfy discrete controller
+  transition requirements.
+
+\end{enumerate}
+
+Commercial nuclear power operations remain manually controlled despite
+significant advances in control systems. The key insight is that procedures
+performed by human operators are highly prescriptive and well-documented. To
+formalize these procedures, we will use temporal logic, which captures system
+behaviors through temporal relations. Linear Temporal Logic provides four
+fundamental operators: next ($X$), eventually ($F$), globally ($G$), and until
+($U$). These operators enable precise specification of time-dependent
+requirements. The most efficient path to accomplish this translation is through
+NASA's Formal Requirements Elicitation Tool (FRET). FRET employs FRETish, a
+specialized requirements language that restricts requirements to easily
+understood components while eliminating ambiguity. FRET enforces structure by
+requiring all requirements to contain six components: Scope, Condition,
+Component, Shall, Timing, and Response.
+
+FRET provides functionality to check realizability of a system. 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 
+contain behavioral inconsistencies that represent the physical equivalent of 
+software bugs. Using FRET during autonomous controller development allows us 
+to identify and resolve these errors systematically. FRET exports requirements 
+in temporal logic format compatible with reactive synthesis tools, enabling 
+the second thrust of our approach.
+
+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 in size, where each node represents a 
+unique discrete state. The connections between nodes, called state 
+transitions, specify the conditions under which the discrete controller moves 
+from state to state. This complete mapping constitutes a discrete automaton.
+
+We will employ reactive synthesis tools which translate linear temporal logic
+specifications into deterministic automata automatically while maximizing
+generated automata quality. Once constructed, the automaton can be
+straightforwardly implemented using standard programming control flow
+constructs. The discrete automata representation yields an important theoretical 
+guarantee. Because the discrete automaton is synthesized entirely through 
+automated tools from design requirements and operating procedures, we can 
+prove that the automaton---and therefore our hybrid switching behavior---is 
+correct by construction. 
+
+This correctness guarantee 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. Autonomous control lacks this adaptive advantage. By
+synthesizing controllers from logical specifications with guaranteed
+correctness, we eliminate the possibility of switching errors.
+
+While discrete system components will be synthesized with correctness 
+guarantees, they represent only half of the complete system. The continuous 
+modes will be developed after discrete automaton construction, leveraging the 
+automaton structure and transitions to design multiple smaller, specialized 
+continuous controllers. 
+
+The discrete automaton 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: 
+Stabilizing modes maintain the hybrid system within its current discrete mode, 
+corresponding to steady-state normal operating modes like full-power 
+load-following control. Transitory modes have the primary goal of 
+transitioning the hybrid system from one discrete state to another, such as 
+controlled warm-up procedures. Expulsory modes are specialized transitory 
+modes with additional safety constraints that ensure the system is directed to 
+a safe stabilizing mode during failure conditions, such as reactor SCRAM.
+
+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. Current techniques struggle with this problem because dynamic 
+discontinuities complicate verification. This work alleviates these problems 
+by designing continuous controllers specifically with transitions in mind. By 
+decomposing continuous modes according to their required behavior at 
+transition points, we avoid solving trajectories through the entire hybrid 
+system.
+
+To ensure continuous modes satisfy their requirements, we will employ three 
+complementary techniques. Reachability analysis computes the reachable set of 
+states for a given input set. We will use reachability when continuous 
+state ranges at discrete transition boundaries are defined and verify that 
+continuous modes only can reach such defined ranges. Otherwise, assume-guarantee contracts will be 
+employed 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. 
+Finally, barrier certificates will prove that mode transitions are satisfied. Control 
+barrier functions provide a method to certify safety by establishing 
+differential inequality conditions that guarantee forward invariance of safe 
+sets.
+
+Combining these three techniques will enable us to prove that continuous 
+components satisfy discrete requirements and thus complete system behavior. To 
+demonstrate this methodology, we will develop an autonomous startup controller 
+for a Small Modular Advanced High Temperature Reactor (SmAHTR). SmAHTR 
+represents an ideal test case with well-documented startup procedures that 
+must transition through multiple distinct operational modes: initial cold 
+conditions, controlled heating to operating temperature, approach to 
+criticality, low-power physics testing, and power ascension to full operating 
+capacity. We have access to an already developed high-fidelity SmAHTR model in Simulink that 
+captures the thermal-hydraulic and neutron kinetics behavior. 
+
+The synthesized hybrid controller will be implemented on an Emerson Ovation
+control system platform, which is representative of industry-standard control
+hardware. This control system will be used in a hardware-in-the-loop simulation,
+where the Advanced Reactor Cyber Analysis and Development Environment
+(ARCADE) suite will serve as the integration layer. This
+hardware-in-the-loop configuration enables validation of the controller
+implementation on actual industrial control equipment.
+
+\section{Metrics of Success}
+
+This research will be measured by advancement through Technology Readiness
+Levels, progressing from fundamental concepts to validated prototype
+demonstration. The work begins at TRL 2--3 and aims to reach TRL 5, where system
+components operate successfully in a relevant laboratory environment. TRLs
+provide the ideal success metric because they explicitly measure the gap between
+academic proof-of-concept and practical deployment. This gap is precisely what
+our work aims to bridge. TRLs capture both theoretical rigor and practical
+feasibility simultaneously. The nuclear industry already uses TRLs for
+technology assessment, making this metric directly relevant to potential
+adopters.
+
+Moving from current state (TRL 2--3) to target (TRL 5) requires progressing
+through component isolation, system integration, and hardware validation. By
+reaching TRL 5, we will have demonstrated a complete autonomous hybrid
+controller operating on industrial control hardware through hardware-in-the-loop
+testing. Achieving TRL 5 establishes both theoretical validity and practical
+feasibility, proving that the methodology produces verified controllers
+implementable with current technology and providing a clear pathway for nuclear
+industry adoption and broader application to safety-critical autonomous systems.
+
+\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 for hyperscale 
+datacenters. According to the U.S. Energy Information Administration, advanced 
+nuclear power entering service in 2027 is projected to cost \$88.24 per 
+megawatt-hour. With datacenter electricity demand projected to reach 1,050 
+terawatt-hours annually by 2030, operations and maintenance costs represent 
+approximately 23--30\% of total levelized cost, translating to \$21--28 
+billion annually for projected datacenter demand.
+
+This research directly addresses the multi-billion dollar O\&M cost challenge.
+Current nuclear operations require full control room staffing for each reactor.
+These staffing requirements drive high O\&M costs, particularly for smaller
+reactor designs where the same overhead must be spread across lower power
+output. The economic burden threatens the viability of next-generation nuclear
+technologies. But, by synthesizing provably correct hybrid controllers, we can
+automate routine operational sequences that currently require constant human
+oversight. This enables a change from direct operator control to
+supervisory monitoring where operators oversee multiple autonomous reactors
+rather than manually controlling individual units. The transition fundamentally
+changes the economics of nuclear operations.
+
+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. By formally verifying both 
+discrete mode-switching logic and continuous control behavior, this research 
+will produce controllers with mathematical proofs of correctness. These 
+guarantees enable automation to safely handle routine operations that 
+currently require human operators to follow written procedures.
+
+Beyond nuclear applications, 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. These domains share similar economic and safety considerations
+that favor increased autonomy with provable correctness guarantees. By
+demonstrating this approach in nuclear power this research will establish both
+technical feasibility and regulatory pathways for broader adoption across
+critical infrastructure.
+
+\newpage
+
+% REFERENCES CITED
+
+\begin{thebibliography}{99}
+
+\bibitem{10CFR55}
+U.S. Nuclear Regulatory Commission. ``10 CFR Part 55 - Operators' Licenses.''
+\textit{Code of Federal Regulations}, 2024.
+
+\bibitem{Kemeny1979}
+J. G. Kemeny et al. ``Report of the President's Commission on the Accident
+at Three Mile Island.'' U.S. Government Printing Office, October 1979.
+
+\bibitem{NUREG-0899}
+U.S. Nuclear Regulatory Commission. ``Guidelines for the Preparation of
+Emergency Operating Procedures.'' NUREG-0899, August 1982.
+
+\bibitem{DOE-HDBK-1028-2009}
+U.S. Department of Energy. ``Human Performance Improvement Handbook.''
+DOE-HDBK-1028-2009, June 2009.
+
+\bibitem{WNA2020}
+World Nuclear Association. ``Safety of Nuclear Power Reactors.''
+\textit{World Nuclear Association Information Library}, 2020.
+
+\bibitem{Kiniry2022}
+J. Kiniry et al. ``High Assurance Rigorous Digital Engineering for Nuclear
+Safety (HARDENS).'' NRC Final Technical Report ML22326A307, October 2022.
+
+\bibitem{eia_lcoe_2022}
+U.S. Energy Information Administration. ``Levelized Costs of New Generation
+Resources in the Annual Energy Outlook 2022.'' Report, March 2022.
+
+\bibitem{eesi_datacenter_2024}
+Environmental and Energy Study Institute. ``Data Center Energy Needs are
+Upending Power Grids and Threatening the Climate.'' Web article, 2024.
+
+\end{thebibliography}
+