Merge branch 'editing-demo'

1-goals-and-outcomes/goals.tex

@@ -16,15 +16,16 @@ 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
+This reliance on human operators not only prevents autonomous control
-creates a fundamental economic challenge for next-generation reactor designs.
+capabilities but creates a fundamental economic challenge for next-generation
-Small modular reactors, in particular, face per-megawatt staffing costs far
+reactor designs. Small modular reactors, in particular, face per-megawatt
-exceeding those of conventional plants and threaten their economic viability.
+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
+Autonomous control systems must safely manage complex operational sequences with
-manage complex operational sequences with the same assurance as human-operated
+the same assurance as human-operated systems, but without constant human
-systems, but without constant human supervision.
+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.
@@ -34,7 +35,11 @@ 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.
+lacks tools for proving correctness of discrete switching
+decisions. 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.
 % Hypothesis
 By synthesizing discrete mode transitions directly from written operating
 procedures and verifying continuous behavior between transitions, we can create
@@ -46,12 +51,6 @@ built that are provably free from design defects.
 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:
 
@@ -90,7 +89,8 @@ If this research is successful, we will be able to do the following:
     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.
+    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
@@ -100,7 +100,8 @@ If this research is successful, we will be able to do the following:
 
 % 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.
+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

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

@@ -1,29 +1,37 @@
 % 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.
+correct behavior.\splitnote{Strong, direct opening. Sets scope immediately.}
 
 % 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. 
+about when to switch between control objectives.\splitsuggest{Consider: 
+``operators'' appears 3x in two sentences. Maybe: ``Based on these procedures 
+and their interpretation of plant conditions, they make critical decisions...''}
 % Gap
 But, reliance on human operators has created an economic challenge for
-next-generation nuclear power plants. Small modular reactors face significantly
+next-generation nuclear power plants.\splitpolish{``But, reliance'' — the comma 
-higher per-megawatt staffing costs than conventional plants. Autonomous control
+after ``But'' is unusual. Either drop it or restructure: ``However, this 
-systems are needed that can safely manage complex operational sequences with the
+reliance...'' or ``This reliance, however, has created...''} Small modular 
-same assurance as human-operated systems, but without constant supervision.
+reactors face significantly higher per-megawatt staffing costs than conventional 
+plants. Autonomous control systems are needed that can safely manage complex 
+operational sequences with the same assurance as human-operated systems, but 
+without constant supervision.\splitsuggest{``are needed that can'' — passive. 
+Try: ``Autonomous control systems must safely manage...''}
 
 % APPROACH PARAGRAPH Solution
 To address this need, we will combine formal methods from computer science with
-control theory to build hybrid control systems that are correct by construction. 
+control theory to build hybrid control systems that are correct by 
+construction.\splitnote{Clear statement of approach.}
 % Rationale
 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. 
+behavior but lacks tools for proving discrete switching 
+correctness.\splitnote{Nice parallel structure showing the gap.}
 % Hypothesis and Technical Approach
 We will bridge this gap through a three-stage methodology. First, we will
 translate written operating procedures into temporal logic specifications using
@@ -40,10 +48,17 @@ transition objectives, and then employ assume-guarantee contracts and barrier
 certificates to prove that mode transitions occur safely and as defined by the
 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. 
+entire hybrid system. We will demonstrate this on an Emerson Ovation control 
+system.\splitsuggest{This paragraph is dense. Consider breaking after the 
+three stages, then a new paragraph for the compositional verification point 
+and Emerson demo.}
 % Pay-off
 This approach will demonstrate autonomous control can be used for complex
-nuclear power operations while maintaining safety guarantees.
+nuclear power operations while maintaining safety 
+guarantees.\splitpolish{``can be used for'' — weak. Try: ``...will demonstrate 
+that autonomous control can manage complex nuclear power operations while 
+maintaining safety guarantees.'' Or even stronger: ``...enables autonomous 
+management of complex nuclear power operations with safety guarantees.''}
 
 % OUTCOMES PARAGRAPHS
 If this research is successful, we will be able to do the following:
@@ -57,13 +72,14 @@ If this research is successful, we will be able to do the following:
     % Outcome
     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.
+    barriers to high-assurance control 
+    systems.\splitnote{Good practical framing — emphasizes accessibility.}
 
     % 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 
+    We will develop methods using reachability analysis to ensure continuous 
-    satisfy discrete transition requirements. 
+    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
@@ -77,6 +93,8 @@ If this research is successful, we will be able to do the following:
     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.
+    achieve autonomy without retraining costs or developing new 
+    equipment.\splitnote{Strong industrial grounding — the ``platforms they 
+    already use'' point is compelling for adoption.}
 
 \end{enumerate}

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

@@ -5,7 +5,8 @@ systems that are tractably safe. To understand what is being automated, we must
 first understand how nuclear reactors are operated today. This section examines
 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.
+formal methods approaches to reactor control 
+systems.
 
 \subsection{Current Reactor Procedures and Operation}
 
@@ -19,11 +20,7 @@ developed using guidance from NUREG-0899~\cite{NUREG-0899, 10CFR50.34}, but thei
 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,
+requalification under 10 CFR 55.59~\cite{10CFR55.59}. 
-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
@@ -51,7 +48,8 @@ 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.
+startup/shutdown sequences, mode transitions, and procedure 
+implementation.
 
 \subsection{Human Factors in Nuclear Accidents}
 
@@ -65,8 +63,8 @@ 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.
+motivation for formal automated control with mathematical safety 
-Operators hold legal authority under 10 CFR Part 55 to make critical decisions,
+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
@@ -76,7 +74,8 @@ 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.
+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
@@ -87,13 +86,15 @@ 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.
+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.
+limitations are fundamental rather than a remediable part of human-driven 
+control.
 
 \subsection{Formal Methods}
 \subsubsection{HARDENS}
@@ -122,7 +123,8 @@ 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.
+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
@@ -134,7 +136,8 @@ 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.
+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
@@ -172,25 +175,27 @@ dynamic logic (dL). dL introduces two additional operators
 into temporal logic: the box operator and the diamond operator. The box operator
 \([\alpha]\phi\) states that for some region \(\phi\), the hybrid system
 \(\alpha\) always remains within that region. In this way, it is a safety
-ivariant being enforced for the system. The second operator, the diamond
+invariant being enforced for the system. The second operator, the diamond
 operator \(<\alpha>\phi\) says that for the region \(\phi\), there is at least
 one trajectory of \(\alpha\) that enters that region. This is a declaration of a
-liveness property. 
+liveness property\cite{platzer2018}. 
 
-%source: https://symbolaris.com/logic/dL.html
 
 While dL allows for the specification of these liveness and safety properties,
 actually proving them for a given hybrid system is quite difficult. Automated
 proof assistants such as KeYmaera X exist to help develop proofs of systems
 using dL, but so far have been insufficient for reasonably complex hybrid
 systems. The main issue behind creating system proofs using dL is state space
-explosion and non-terminating solutions. 
+explosion and non-terminating 
+solutions.\splitsuggest{Consider adding a concrete example here — ``For 
+instance, a system with N modes and M continuous state variables...'' to give 
+readers a sense of the scaling problem.}
 %Source: that one satellite tracking paper that has the problem with the
 %gyroscopes overloding and needing to dump speed all the time
 Approaches have been made to alleviate
 these issues for nuclear power contexts using contract and decomposition based
-methods, but are far from a complete methodology to design systems with.
+methods, but do not yet constitute a complete design
-%source: Manyu's thesis. 
+methodology\cite{kapuria2025}.%source: Manyu's thesis. 
 Instead, these approaches have been used on systems that have been designed a
 priori, and require expert knowledge to create the system proofs. 
 
@@ -198,3 +203,9 @@ priori, and require expert knowledge to create the system proofs.
 %very much, so the limitation is that logic based hybrid system approaches have
 %not been used in the DESIGN of autonomous controllers, only in the analysis of
 %systems that already exist.
+\textbf{LIMITATION:} \textit{Differential dynamic logic has been used for
+post-hoc analysis of existing systems, not for the constructive design of
+autonomous controllers.} Current formal methods based approaches can in theory
+completely describe the behavior of a hybrid autonomous control system, but in
+practice remain difficult to implement, and have no straightforward application
+to the design of a hybrid autonomous control system.

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

@@ -1,165 +0,0 @@
-\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.

3-research-approach/approach.tex

@@ -47,7 +47,7 @@ This means that the system does not have external input and that continuous
 states do not change instantaneously when discrete states change. For our
 systems of interest, the continuous states are physical quantities that are
 always Lipschitz continuous. This nomenclature is borrowed from the Handbook on
-Hybrid Systems Control \cite{HANDBOOK ON HYBRID SYSTEMS}, but is redefined here
+Hybrid Systems Control \cite{lunze2009}, but is redefined here
 for convenience:
 
 \begin{equation}
@@ -75,12 +75,13 @@ The creation of a HAHACS amounts to the construction of such a tuple together
 with proof artifacts demonstrating that the intended behavior of the control
 system is satisfied by its actual implementation. This approach is tractable now
 because the infrastructure for each component has matured. The novelty is not in
-the individual pieces, but in the architecture that connects them. By defining
+the individual pieces, but in the architecture that connects them. 
-entry, exit, and safety conditions at the discrete level first, we transform the
+
-intractable problem of global hybrid verification into a collection of local
+By defining entry, exit, and safety conditions at the discrete level first, we
-verification problems with clear interfaces. Verification is performed per mode
+transform the intractable problem of global hybrid verification into a
-rather than on the full hybrid system, keeping the analysis tractable even for
+collection of local verification problems with clear interfaces. Verification is
-complex reactor operations.
+performed per mode rather than on the full hybrid system, keeping the analysis
+tractable even for complex reactor operations.
 
 \begin{figure} 
   \centering
@@ -293,16 +294,8 @@ implementation. Second, it clearly demonstrates where natural language documents
 are insufficient. These procedures may still be used by human operators, so any
 room for interpretation is a weakness that must be addressed.
 
-(Some examples of where FRET has been used and why it will be successful here)
+\splitinline{Some examples of where FRET has been used and why it will be successful
-%%% NOTES (Section 2):
+here}
-% - Add concrete FRET example showing requirement → FRETish → LTL
-% - Discuss hysteresis and how to prevent mode chattering near boundaries
-% - Address sensor noise and measurement uncertainty in threshold definitions
-% - Consider numerical precision issues when creating discrete automata
-
-% ----------------------------------------------------------------------------
-% 3. DISCRETE CONTROLLER SYNTHESIS
-% ----------------------------------------------------------------------------
 
 Once system requirements are defined as temporal logic specifications, we use
 them to build the discrete control system. To do this, reactive synthesis tools
@@ -339,19 +332,10 @@ system using temporal logics and synthesizing the controller using deterministic
 algorithms, we are assured that strategic decisions will always be made
 according to operating procedures.
 
-(Talk about how one would go from a discrete automaton to actual code)
+\splitinline{Talk about how one would go from a discrete automaton to actual
+code}
 
-(Examples of reactive synthesis in the wild)
+\splitinline{Examples of reactive synthesis in the wild}
-
-%%% NOTES (Section 3):
-% - Mention computational complexity of synthesis (doubly exponential worst case)
-% - Discuss how specification structure affects synthesis tractability
-% - Reference GR(1) fragment as a tractable subset commonly used in practice
-% - May want to include an example automaton figure
-
-% ----------------------------------------------------------------------------
-% 4. CONTINUOUS CONTROLLERS
-% ----------------------------------------------------------------------------
 
 \subsection{Continuous Control Modes}
 
@@ -380,7 +364,7 @@ continuous state space among several discrete vector fields has traditionally
 been a difficult problem for validation and verification. The discontinuity of
 the vector fields at discrete state interfaces makes reachability analysis
 computationally expensive, and analytic solutions often become intractable
-\cite{MANYUS THESIS}.
+\cite{kapuria2025, lang2021}.
 
 We circumvent these issues by designing our hybrid system from the bottom up
 with verification in mind. Each continuous control mode has an input set and
@@ -407,15 +391,6 @@ We classify continuous controllers into three types based on their objectives:
 transitory, stabilizing, and expulsory. Each type has distinct verification
 requirements that determine which formal methods tools are appropriate.
 
-%%% NOTES (Section 4):
-% - Add figure showing the relationship between entry/exit/safety sets
-% - Discuss how standard control techniques (LQR, MPC, PID) fit into this framework
-% - Mention assume-guarantee reasoning for compositional verification
-
-% ----------------------------------------------------------------------------
-% 4.1 TRANSITORY MODES
-% ----------------------------------------------------------------------------
-
 \subsubsection{Transitory Modes}
 
 Transitory modes are continuous controllers designed to move
@@ -466,16 +441,6 @@ systems require more conservative over-approximations using techniques such as
 Taylor models or polynomial zonotopes. For this work, we will select tools
 appropriate to the fidelity of the reactor models available.
 
-%%% NOTES (Section 4.1):
-% - Add timing constraints discussion: what if the transition takes too long?
-% - Consider timed reachability for systems with deadline requirements
-% - Mention that the Mealy machine perspective unifies this: continuous system
-%   IS the transition, entry/exit conditions are the discrete states
-
-% ----------------------------------------------------------------------------
-% 4.2 STABILIZING MODES
-% ----------------------------------------------------------------------------
-
 \subsubsection{Stabilizing Modes}
 
 Stabilizing modes are continuous controllers with an objective of maintaining a
@@ -523,16 +488,6 @@ For example, a lower fidelity model can be used for controller design, but a
 higher fidelity model can be used for the actual validation of that stabilizing
 controller.
 
-%%% NOTES (Section 4.2):
-% - Clarify relationship between barrier certificates and Lyapunov stability
-% - Discuss what happens at mode boundaries: barrier for this mode vs guard
-%   for transition
-% - Mention tools: SOSTOOLS, dReal, barrier function synthesis methods
-
-% ----------------------------------------------------------------------------
-% 4.3 EXPULSORY MODES
-% ----------------------------------------------------------------------------
-
 \subsubsection{Expulsory Modes}
 
 Expulsory modes are continuous controllers responsible for
@@ -582,16 +537,6 @@ plant dynamics. The expulsory mode must handle the worst-case dynamics within
 this envelope. This is where conservative controller design is appropriate as
 safety margins will matter more than performance during emergency shutdown.
 
-%%% NOTES (Section 4.3):
-% - Discuss sensor failures vs actual plant failures
-% - Address unmodeled disturbances that aren't failures
-% - How much parametric uncertainty is enough? Need methodology for bounds
-% - Mention graceful degradation: graded responses vs immediate SCRAM
-
-% ----------------------------------------------------------------------------
-% 5. INDUSTRIAL IMPLEMENTATION
-% ----------------------------------------------------------------------------
-
 \subsection{Industrial Implementation}
 
 The methodology described above must be validated on realistic
@@ -619,17 +564,9 @@ the success and impact of this work. We will directly address the gap of
 verification and validation methods for these systems and industry adoption by
 forming a two-way exchange of knowledge between the laboratory and commercial
 environments. This work stands to be successful with Emerson implementation
-because we will have excess to system experts at Emerson to help with the fine
+because we will have access to system experts at Emerson to help with the fine
 details of using the Ovation system. At the same time, we will have the benefit
 of transferring technology directly to industry with a direct collaboration in
 this research, while getting an excellent perspective of how our research
 outcomes can align best with customer needs.
 
-%%% NOTES (Section 5):
-% - Get specific details on ARCADE interface from Emerson collaboration
-% - Mention what startup sequence will be demonstrated (cold shutdown →
-%   criticality → low power?)
-% - Discuss how off-nominal scenarios will be tested (sensor failures,
-%   simulated component degradation)
-% - Reference Westinghouse relationship if relevant
-

3-research-approach/v1.tex

@@ -1,285 +0,0 @@
-\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.

3-research-approach/v2.tex

@@ -1,578 +0,0 @@
-\section{Research Approach}
-\iffalse
-
-  HACS: hybrid autonomous control system
-  HAHACS: High-Assurance Hybrid AUtonomous Control System
-
-
-The research approach here needs to clearly outline the solution the the problem
-and identify the actions taken that will advance knowledge and solve the
-problem.
-
-First, what is the problem? 
-
-\textit{ 
-
-  Inhibition to adopt hybrid autonomous control in critical infrastructure is
-  rooted in safety concerns of system stability. Without a human in the loop
-  with general intelligence, HACS have not been trusted where failure modes can
-  be unique and novel.
-
-}
-
-So, what's the solution?
-
-\textit{
-
-  This research approach develops a methodology to build HACS that are provably
-  safe. This methodology builds on existing technologies, and unifies different
-  research thrusts to build a complete hybrid control system. To do this, the
-  problem of a HAHCS is broken into three distinct pieces:
-
-  \begin{enumerate}
-
-    \item System specification: properties of the HAHaCS such as transition
-      between control modes and system invariants are specified using a formal
-      methods tool. 
-        - This provides exact behavior
-        - allows realizabillity checking of controller specs. Can a controller
-        actually be built from these specs?
-        - ?
-        - ?
-
-    \item Discrete Behavior Synthesis: The discrete component of the controller
-      is synthesized directly from system specifications using reactive
-      synthesis.
-        - This ELIMINATES wholesale the possibility of introducing logical bugs
-        in the creation of the strategic part of the HAHCS. Critical decisions
-        that are normally made by a human are automated directly from the
-        formal specifications.
-        - This does two critical things:
-          - It makes the creation of the controller tractable. The reasons the
-          controller changes between modes acn be traced back to the
-          specification (and thus any requirements), which is a trace for
-          liability and justification of system behavior
-          - Discrete control decisions made by humans are reliant on the human
-          operator operating correctly. Humans are intrinsically probabalistic
-          creatures who cannot eliminate human error. By defining the behavior
-          of this system using temporal logics and synthesizing the controller
-          using deterministic algorithims, we are assured that strategic
-          decisions will always be made as according to operating procedures.
-
-    \item Continuous Behavior Synthesis and Verification: The continuous
-      components of the controller are built using existing dynamics and control
-      theory but then verified using reachability and barrier certificats.
-        - It's very challenging (nigh impossible) to say for certain how to
-        build any continuous control mode. That is honestly going to be have to
-        left to the specific control system and its objectives. It's not really
-        the point of this PhD to say how to do that. For that reason, I'm going
-        to assume that controllers between modes are generally possible to
-        build. That is to say that there exists a controller that can transition
-        between modes, but it is a human hunt to find it.
-        - To check if a candidate controller does transition between discrete
-        modes, we do two things:
-          - Check invariants using reachability. Specifications will require
-          that control modes transiiton from one mode to the next, where
-          appropriate. When this is the case, these invariants are extracted to
-          be checked using reachability. The control mode is given the possible
-          entry conditions of the 'entry' mode, and the possible 'exit' states
-          are analyzed. A cont. controller passes this reachability test if
-          there is no reachable state that is not at the exit condition of the
-          state transition. 
-
-          --- This needs flushed out more. I think this can really be clarified
-          using entry and exit conditions of Mealy machines. The continuous
-          system IS the transition, and the reachabililty test is saying whether
-          or not the physical system actually satisfies the entry and exit
-          conditions. 
-
-          - Then, for systems that need to STAY within one mode, we will use
-          barrier certificates. These can let us define a continuous state
-          boundary, and define for a discrete controller state, the total
-          controller will NOT leave the continuous boundary.
-
-        - One thing that must be considered is the idea that this analysis is
-        predicated on the physical system being correct to the model. If this
-        isn't true, we must define continuous modes that catch failure states.
-        If transition invariants are violated, we must shut down the system, and
-        build safety oriented control modes that we can be sure with a much
-        broader set of entry conditions will safely shut down the plant.
-
-      -- Q for dan: is it critical to really have software to namedrop or is it
-      better to stay amorphous on the technology? Iirc Manyu did a little bit of
-      both.
-
-  \end{enumerate}
-
-
-  What's the intellectual merit?
-
-  \textit{
-
-    There is no outstanding way to build HAHACS. This methodology provides a
-    basis for systems engineers to think about the components of a HAHACS as
-    interlocking pieces whos verification interlinks into a broader system.
-    This will also motivate the adoption of temporal logic to define autonomous
-    control systems, by allowing a close connection and tracability between
-    requirements from regulations to system specifications.
-
-  }
-
-}
-
-Some thoughts on invariants, and how they fit here: There are several types of
-safety invariants that HAHACS might have. 
-
-1. Conditions that initiate a switch between control modes (reactiive synthesis
-relevant) 
-
-2. Invariants about the stability of discrete states (barrier certificates) 
-
-3. Invariants ensuring the transition between discrete states (reachability) 
-
-4. Invariants about the timeliness of discrete transitions (??? Reachability?)
-
-How do we reason about all of these invariants. Well, fundamentally they can
-all be reasoned about with temporal logic statements. Using next and eventually
-operators, we can get to the fundamental behavior of all of these modes. What's
-challenging is the fact that we ensure that all of these specifications are
-validated differs between the type of invariant. This is really the beauty of
-this approach, and the intellectual merit. This proposal provides a way for
-hybrid control systems to be verified for autonomous control systems by
-diversifying the way that the invariants are checked. 
-
-Reactive synthesis helps us build discrete controllers using specifications
-that have conditons that don't depend on time. These invariants generally are
-strategic decisions, such as changing between operating modes, initiating power
-level changes, or perhaps doing a refueling or shutdown routine. These
-specifications are able to be nearly directly drawn from operating procedures,
-and should be closely tied to instructions that would be used for human
-operators. They have checkpoints for the continuous system in between different
-control implements. An example is, raise power at a certain rate while ensure
-temperature remains between certain bounds. These conditions are physical
-states, but they are a binary result. The condition is really binary, desipite
-perhaps having units of celsius or %power. When we build discrete controllers
-from these specifications, we get the validation of the controller of these
-specs for free by nature of reactive synthesis tools. We get direct
-traceability from the operating procedure to the discrete controller
-implementation with minimal human effort.
-
-That being said, there are no free lunches here. Ultimately, we're controlling
-physical systems, and while we can automate the controller building between
-stratgic objectives, it is not trivial to do so for the controller of the
-physical process. These controllers are going to have to be built manually,
-with the continuous dynamics of the system in mind. Helpfully, if
-specifications are complete first, one can obtain discrete controller before
-building physical controllers. The result of this is a simplification of
-controller design, becuase the operational goals of each continuous controller
-is clearly outlined by the invariants that define the goal of each discrete
-mode. While for reactive synthesis purposes conditions such as a certain
-temperature being reached or power level attained are binary variables, the
-continuous physical meaning becomes important in the design and analysis of the
-physical controllers. The continuous value of these conditions becomes the goal
-of the continuous controller design, while also providing a basis to check
-controller performance.
-
-To check continuous controllers are valid, we can split continuous controller
-objectives into two types. First, we have continuous controllers that are
-designed to move the plant between two different discrete modes. These will be
-called 'transitory' controllers, because their entire purpose is to transition
-the plant betweeen between discrete control modes. Because of the specification
-of the hybrid control system a priori, we will have defined what the invariants
-of these transitions are in continuous state space. Then, once a continuosu
-controller design is developed, it can be validated using reachability
-analysis. The input set for the analysis is the possible states that enter this
-transitory mode, while the reachable states must be entirely contained within
-the exit invariant for the controller to pass. At the time of writing this
-proposal, it is not clear what the most efficient way to obetain this
-continuous controller is, but is generally beyond the scope of this work. It is
-assumed that they generally won't be so difficult to find for most systems, as
-the refinement of the discrete controller should simplify the control
-objectives of the physical controllers significantly.
-
-The second type of continuous controller that may be utilized in a HAHAHCS is a
-controller that tries to maintaine a continuous steady state, such that no
-discrete transitions are triggered. Reachability on these systems may not prove
-a prudent approach to validating this behavior for a candidate continuous
-controller, and instead, barrier certificates must be used. Barrier
-certificates analyze the dynamics of the system to say whether or not flux
-across a given boudnary exists. That is to say that they evaluate whether or
-not there is a trajectory or not that leaves a given boundary. This definition
-is exactly what defines the validity of a stabilizing continuous control mode.
-Once again, because the design of the discrete controller defines careful
-boundaries in continuous state space, the barrier is known a priori of which we
-must satisfy this condition. This will eliminate the search for such a barrier,
-and minimze complicatoin in validating stabilizing continuous control modes.
-
-Finally, consideration must be paid for when errors occur. The validation of
-these continuous control modes hinges upon having an assumption ofcorrect
-model, which in the case of a mechanical failure will almsot certainly be
-invalidated. Special continuous controllers for these conditions must be
-created, called 'explusory' control modes. These controllers will be
-responsible for ensuring safety in case of failure, and will be designed with
-reachability, but in this case, additional allocation for the allowing of
-physical parameters will be allowed in the analysis. Traditional safety
-analysis will also be used to identify potential failure modes, and the
-modelling of their worst case dynamics. The HAHCS will be able to idenfity why
-such a fault occors because an discrte boundary condition will be violated by
-the continuous physical controller. That is to say, since we will have
-validated the continuous control modes using reachability and barrier
-certificates a priori, we will know with certainty that the only room for
-dynamics to change is a shift in the plant dynamics, not that of the proven
-controller.
-
-\fi
-
-%%%%%%%%%% TABLESETTING
-
-% what is a hybrid system really for this proposal
-% Define: A hybrid system with continuous state space X ⊆ ℝⁿ and discrete modes Q = {q₁, q₂, ..., qₘ}
-% Each discrete mode qᵢ has an associated continuous state region Xᵢ ⊆ X
-% The discrete controller manages transitions between modes based on continuous state thresholds
-
-% what are requirements, anyways?
-
-% why do we care about defining the whole hybrid system into requirements?
-
-% How do different requirements line up into different parts of the system?
-% (operational vs strategic requirements and their relevance to different parts
-% of our system)
-
-Autonomous control systems are fundamentally different from automatic control
-systems. The difference between these systems is the level at which
-they operate. Automatic control systems are purely operational systems, 
-
-To build a high-assurance hybrid autonomous control system (HAHACS), a
-mathematical description of the system must be established. This work will make
-use of automata theory while including logical statements and control theory.
-The nomenclature and lexicon between these fields is far from homogenous, and
-the reviewer of this proposal is not expected to be an expert in all fields
-simultaneously. To present the research ideas as clearly as possible in this
-section, the following syntax is explained.
-
-A hybrid system is a dynamical system that has both continuous and discrete
-states. The specific type of system discussed in this proposal are continuous
-autonomous hybrid  systems. This means that these systems a) do not have
-external input \footnote{This is not strictly true in our case because we allow
-strategic inputs. For example, a remote powerplant may receive a start-up or
-shutdown command from a different location, but only this binary high level
-input is a strategic input.} and b) continuous states do not change
-instantaneously when discrete states change. For our systems of interest, the
-continuous states are physical, and are always Lipschitz continuous. This
-nomenclature is heavily borrowed from \cite{HANDBOOK ON HYBRID SYSTEMS CONTROL},
-but is redefined here for convenience:
-
-\begin{equation}
-  H = (\mathcal{Q}, \mathcal{X}, \mathbf{f}, Init, \mathcal{G}, \mathcal{R}, Inv)
-\end{equation}
-
-where:
-
-\begin{itemize}
-  \item \( \mathcal{Q}\): is the discrete states of the system
-  \item \( \mathcal{X}\): is the continuous states of the system
-  \item \(\mathbf{f}: \mathcal{Q} \times \mathbb{R} \rightarrow \mathbb{R} \), where
-    \(\mathbf{f}_i\) is a
-    vector field that defines the continuous dynamics for each \(q_i\)
-  \item \(Init\): the initial states of \(q\) and \(x\)
-  \item \( G\): guard
-    conditions that define when discrete state transitions occur
-  \item \(\delta: \mathcal{Q} \times G \rightarrow \mathcal{Q}\), are the
-    discrete state transition functions
-  \item \mathcal{R}: Reset maps that define state 'jumps'
-  \item \(Inv\): Safety invariants on the continuous dynamics
-\end{itemize}
-
-The creation of a HAHACS essentially boils down to the creation of such a tuple
-where there are proof artifacts that the intended behavior of the control system
-are satisfied by the actual implementation of the control systems. But to create
-such a HAHACS, we must first completely describe its behavior.
-
-%% Brief discussion on what each part of this tuple means for us
-
-\subsection{System Requirement and Specifications}
-
-Temporal logic is a powerful set of semantics to build systems that can have
-complex but deterministic behavior. 
-
-
-%%%%%%%%%%% Building discrete controllers
-
-% Buildout of requirements from written procedures (this is easy for critical
-% systems - we already have the requirements)
-
-% What happens to the invariants that specify a continuous space? Save em for
-% later. Here they become binary for our purposes
-% KEY POINT: We don't IMPOSE discrete abstraction - we FORMALIZE existing practice
-% Operating procedures (esp. nuclear) already define go/no-go conditions as discrete predicates
-% e.g., "WHEN coolant temp >315°C AND pressurizer level 30-60% THEN MAY initiate load following"
-% These thresholds come from design-basis safety analysis, validated over decades
-% Our methodology assumes this domain knowledge exists and provides formalization framework
-% The discrete predicates p₁, p₂, ... are Boolean functions over continuous state: pᵢ: X → {true, false}
-% Q: How do we rigorously set thresholds for continuous→discrete abstraction?
-% Q: How do we handle hysteresis to prevent mode chattering near boundaries?
-% Q: How do we account for sensor noise and measurement uncertainty?
-% Q: How do we handle numerical precision issues when creating discrete automata? (relates to task 36)
-
-% Discrete controller implementation can be realized with reactive synthesis. 
-% LTL specs to automata
-
-% talk a bit about tools here like FRET. Talk about previous attempts.
-
-\begin{figure}[htbp]
-  \centering
-  \framebox[0.8\textwidth]{\rule{0pt}{3cm}\textit{Strategic, operational,
-tactical placeholder}}
-  \caption{Breakdown of control scope}
-  \label{fig:strat_op_tact}
-\end{figure}
-
-
-Human control of nuclear power can be divided into three different scopes:
-strategic, operational, and tactical. Strategic control is the high-level and
-long term decision making for the plant. This level has objectives that are
-complex and economic in scale, such as managing labor needs and supply chains to
-optimize sheduled maintenence and downtime. The time scale on this level of
-control is long, often over months or years. The lowest level of control is the
-tactical level. This is the individual control of pumps, turbines, and
-chemistry of the plant. This level of control has already been somewhat
-automated today in nuclear power, and is generally considered 'automatic
-control' when autonomous. These controls are almost always continuous systems,
-and have a direct impact on the physical state of the plant. Tactical control
-objectives are things like maintaining a pressurizer level, maintaining a
-certain core temperature, or adjusting reactivity with a chemical shim. The level of
-control linking these two levels, then, is the operational control scope.
-Operational control is the primary responsibility of human operators today.
-Operational control takes the current strategic objective, and implements
-tactical control objectives to drive the plant towards strategic goals. In this
-way, it is the bridge between high and low level goals. A strategic goal may be
-to perform refueling at a certain time, while the tactical level of the plant
-currently is focused on mainting a certain core temperature. The operational
-level is what issues the shutdown procedure of the plant, using several smaller
-tactical goals along the way to achieve this objective. Thus, the combination of
-the operational and tactical level of the plant fundamentally forms a hybrid
-controller. The tactical level is the continuous evolution of the plant
-according to the control input and control law, while the operational level is a
-discrete state evolution which determines the tactical control law to reach
-different operational states.
-
-This operational control level is the main reason for the requirement of human
-opeartors in nuclear control today. The hybrid nature of this control system
-makes it difficult to prove that a controller will perform according to the
-strategic requirements, as the infrastructure to build hybrid systems today
-dooes not exist. Humans have been used for this layer because the general
-intelleigence of humans has be relied upon as a safe way to manage the hybrid
-nature of this system. But, these operators are using prescriptive operating
-manuals to perform their control with strict procedures on what control to
-implement at a given time. These procedures are the key to the operational
-control scope.
-
-The method of constructing a HAHACS in this proposal leverages two key points of
-the way this control scope is done today: first, the operational scope control
-is effectively discrete control. Second, the rules of implementing this control
-are described a priori to their implementation in operating procedures. We can
-make great use of these facts by formalizing the rules for transitioning between
-discrete states. To do this, we will use temporal logic to formalize discrete
-switching behavior. 
-
-Temporal logic is a rich syntax that allows for the definition of logical
-calculations including time related bounds. For this reason, we can make
-statements relating discrete control modes to one another. Using temporal logic,
-we can effectively describe all of the requirements of a HAHACS. The guard
-conditions \(G\) are easily defined by determining boundary conditions between
-discrete states and defining their behavior, while continuous mode invariants
-can be defined using temporal logic statements as well. These form the basis of
-any proofs about a HAHACS, and are the fundamental 'truth' statements about what
-the behavior of the system is designed to be.
-
-To build these temporal logic statements, an intermediary tool called FRET is
-planned to be used. FRET stands for Formal Requirements Elicitation Tool, and
-was designed by NASA to build high assurance timed systems. FRET is an
-intermediarly language between temporal logic and natural language that allows
-for rigid definitions of temporal behvarior while using a logic-novice friendly
-syntax. This benefit is crucial for the feasibility of this methodology for
-industry, as minimizing the barrier to formal methods is a critical component of
-their scucess. By reducing the expert knowledge required to use these tools,
-their adoption with current workforce becomes easier. 
-
-A key feature of FRET is the ability to start with logically imprecise
-statements and consecutively refine them into a well-posited specification. We
-can use this to our advantage by directly dumping in operating procedures and
-design requirements into FRET in natural language, and iteratively refining them
-into the specifications for a HAHACS. This has two distinct but important
-benefits. First, it allows us to draw a direct link from the design
-documentation to the digital system implementation. Second, it clearly
-demonstrates where the natural language documents are insufficient. These
-procedures may still be used by human operators, so any wiggle room for
-interpretation is a weakness that must be addressed.
-
-%Talk about how we go from temp logic to reactive synth. Metnion fret can
-%export, or naturlly support reactive synth solver ltlsynt, a sota react synth
-%solver
-
-Once system requirements we defined as temporal logic specifications we will use
-the specifications to build the discrete control system. To do this, reactive
-synthesis tools will be utilized. Reactive synthesis is a field in computer
-science that deals with the automated creation of reactive programs from
-temporal logic specifications. A reactive program is one that for a given state
-takes an input, and produces an output. Our systems, such as the discrete
-portion of the controller, fit exactly this this mold. The current discrete
-state, and status of guard conditions are the input to the system, while the
-output is the next discrete state. The output of a reactive synthesis algorithim
-is a discrete automata.
-
-Reactive synthesis' main advantage is the fact that at no point in the
-production of a discrete automata of the program is human engineering required.
-The resultant automata is correct by construction. This method of construction
-eliminates the possibility of human error outright at the implementation state.
-Instead, the effort on the human designer is directed at the specification of
-the system behavior itself. 
-
-% talk about what the benefits of reactive synth are. Proof chain, machine
-% checkable, blah blah blah
-
-%%%%% I NEED TO WRITE ABOUT HOW REQUIREMENTS ARE EXTRACTED AND WHAT BECOME
-CONTINUOUS CONTROLLER TRANSITIONS VS DISCRETE GUARD CONDITIONS
-
-%%%%%%%%%%%% Building continuous controllers
-\subsection{Continuous Controllers}
-
-% The whole point of a hybrid system is that there are continuous components
-% underneath the digital system. We built the discrete like the physical doesn't
-% exist, but it really does. So how do we capture the physical system too?
-
-% SCOPE FRAMING: This methodology VERIFIES continuous controllers, not SYNTHESIZES them
-% Compare to model checking: doesn't tell you HOW to design software, verifies if it satisfies specs
-% We assume controllers can be designed using standard control theory techniques
-% Our contribution: verification that candidate controllers compose correctly with discrete layer
-
-% What are the main different kinds of continuous modes we may see?
-% Mathematical structure: Each discrete mode qᵢ provides three key pieces of information:
-% 1. Entry conditions: X_entry,i ⊆ X (initial state set)
-% 2. Exit conditions: X_exit,i ⊆ X (target state set)
-% 3. Invariants: X_safe,i ⊆ X (safety envelope during operation)
-% These come from the discrete controller synthesis and define objectives for continuous control
-% Q: Who designs the continuous controllers and how? This methodology verifies
-% them, but doesn't synthesize them. Is this a scope problem?
-
-The synthesis of the discrete operational controller is only half of an
-autonomous controller. These control systems are hybrid, with both discrete and
-continuous components. In this section, we will talk about the continuous
-control modes that are the transitions between discrete modes, how they may be
-synthesized, and how we plan to verify them. 
-
-The operational control scope defines go/no-go decisions that themselves are
-deciding what kind of continuous control to implement. To this end, the entry or
-exit of a discrete state triggers are themselves the guard conditions \(G\) that
-define the barriers of the continuous controller. These continuous controllers
-all share a large state space, but each individual continuous control mode
-operates within it's own partition defined by the discrete state \(q_i\) and
-guard conditions \(G\). This partitioning of the continuous state space amongst
-several discrete vector fields controlled by the given \(q_i\) has traditionally
-been a difficult problem for validation and verification of systems properties.
-Typically, the discontinuity of the vector fields at discrete state interfaces
-make things like reachability analysis computationally expensive, and analytic
-solutions become intractable. 
-
-We circumnavigate these issues by designing our hybrid system from the bottom up
-with this verification in mind. Each continuous control mode has an input and
-output set clearly defined by our discrete transitions \textit{a priori}.
-Consider that we define the continuous state space as \(X\). Whenever we create
-guard functions from our design requirements for a given system, we are
-effectively creating subsets \(X_{entry,i}\) and \(X_{exit,i}\) for each
-discrete mode \(q_i\). These subsets define when the state transitions occur
-between discrete modes, but more importantly when building continuous control
-modes, they become control objectives.
-
-% Start talking about what it means to build controlelrs to the objectives
-% rahter than the other why around. ALso why it makes things much easier to
-% verify and validate
-
-%%%%%% Transitory modes
-
-% entry and exit conditions
-% the goal is getting from one physical state to another
-% MATHEMATICAL FORMULATION:
-% Control objective: reach(X_entry,i) → reach(X_exit,i) while maintaining x(t) ∈ X_safe,i
-% Standard control techniques (LQR, MPC, trajectory optimization) applied with these constraints
-%
-% VERIFICATION: Reachability analysis confirms ALL trajectories starting in X_entry,i
-% reach X_exit,i without violating X_safe,i
-% Formally: Reach(X_entry,i, f(x,u), T) ⊆ X_exit,i ∪ X_safe,i
-% where f(x,u) is the closed-loop continuous dynamics
-%
-% we have the physical requirements from earlier specifications. Here we use
-% them in a reachability analysis. This time, we use the actual physical values
-% instead of the binary yes/no we used for discrete
-% Q: How do we verify timing constraints? If a transitory controller eventually
-% reaches the exit condition but takes too long, that violates safety. Timed
-% automata? Timed reachability?
-% Q: Should formalize the Mealy machine perspective - continuous system IS the
-% transition, and entry/exit conditions are the discrete states. This could be
-% a unifying conceptual framework.
-
-%%%%%% stabilizing modes
-
-% these are control modes with an objective of KEEPING a certain discrete state
-% stable
-%
-% MATHEMATICAL FORMULATION:
-% Control objective: remain(X_target,i) where X_target,i ⊂ X_safe,i
-% Standard feedback control (PID, state feedback, LQG) applied to maintain equilibrium
-%
-% VERIFICATION: Barrier certificates prove closed-loop dynamics cannot escape X_safe,i
-% Formally: Find B(x) s.t. ∇B(x)·f(x,u) ≤ 0 for all x ∈ ∂X_safe,i
-% This proves no trajectory can cross the boundary (no flux out of safety region)
-%
-% we also have the physical requirements for this. These can be used for barrier
-% certificates. We can prove that our model won't leave a given area without
-% some disturbance. 
-
-%%%%%% expulsory modes
-% I've made an implicit assumption when talking about transitory and stabilizing
-% modes. That our model is correct. This might not be true
-
-% In the case of a failure, our model will almost certainly be incorrect. For
-% this, we have to build safe shutdown modes too, since a human won't be in the
-% loop to shut things down.
-%
-% MATHEMATICAL FORMULATION:
-% Control objective: reach(X_current) → reach(X_safe_shutdown) under parameter uncertainty
-% where X_current may be anywhere in X (worst-case entry conditions)
-% Dynamics have parametric uncertainty: f(x,u,θ) where θ ∈ Θ_failure
-%
-% VERIFICATION: Parametric reachability analysis with robustness margins
-% Reach(X_current, f(x,u,θ), T) ⊆ X_safe_shutdown for all θ ∈ Θ_failure
-% Conservative bounds on Θ_failure come from FMEA/traditional safety analysis
-
-% WE can detect physical failures exist because our physical controllers have
-% previously been proven as correct by reachability and barrier certificates. We
-% KNOW our controller cannot be incorrect for the plant, so if an invariant is
-% violated, we KNOW it's the plant that has changed.
-% Q: What about sensor failures (wrong readings vs actual plant failure)?
-% Q: What about unmodeled disturbances that aren't failures?
-% Q: What if model uncertainty was too optimistic to begin with?
-% Need to be more precise about what "model failure" means and detect-ability. 
-
-% We do this using continuous modes that shutdown the system, and using
-% reachability analysis with parametric uncertainty, we can prove for a range of
-% error conditions we can maintain safe shutdown.
-% Q: How much parametric uncertainty is enough? How do we determine bounds for
-% worst-case failure dynamics? Need methodology for this.
-
-%%%%%%%%%%%% Implementation with industrial partnerships
-%%%%%%% Emerson
-%talk about this
-% ovation system
-% scenic? Is that what they call it?
-% ripe partnership with Westinghouse
-% Likely build a model with a ccng plant. They already have sophisticated models
-% of them
-% build controller with simplified model, then test with high fidelity digital
-% twin
-
-
-
-
-%
-%%%%%%%%%% 

4-metrics-of-success/metrics.tex

@@ -3,8 +3,8 @@
 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.
+system components operate successfully in a relevant laboratory 
-This section explains why TRL advancement provides the most appropriate success
+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
@@ -12,8 +12,8 @@ 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.
+demonstrate theoretical rigor. TRLs measure both dimensions 
-Advancing from TRL 3 to TRL 5 requires maintaining theoretical rigor while
+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.
@@ -69,6 +69,9 @@ 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.
+If this work is successful, graded responses are an extension that requires
+additional labor, but not new capability as the mechanics of a graded response
+are an addition of special discrete modes and continuous controllers to match.
 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
@@ -85,4 +88,5 @@ 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.
+controllers and that implementation is achievable with current 
+technology.

5-risks-and-contingencies/risks.tex

@@ -49,10 +49,8 @@ rather than a failure.
 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
+systems: relating discrete switching logic to continuous dynamics. Guard conditions
-logic operates on boolean predicates, while continuous control requires
+requiring complex predicates may resist boolean abstraction, making
-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
@@ -88,18 +86,6 @@ 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
@@ -143,16 +129,3 @@ 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.

main.aux

@@ -1,57 +1,151 @@
 \relax 
 \providecommand \oddpage@label [2]{}
-\@writefile{toc}{\contentsline {section}{Contents}{ii}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {section}{Contents}{1}{}\protected@file@percent }
 \@writefile{toc}{\contentsline {section}{\numberline {1}Goals and Outcomes}{1}{}\protected@file@percent }
 \citation{NUREG-0899,10CFR50.34}
 \citation{10CFR55.59}
 \citation{WRPS.Description,gentillon_westinghouse_1999}
+\@writefile{toc}{\contentsline {section}{\numberline {2}State of the Art and Limits of Current Practice}{3}{}\protected@file@percent }
+\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Good roadmap — tells reader exactly what's coming.}{3}{}\protected@file@percent }
+\pgfsyspdfmark {pgfid1}{21980756}{40762302}
+\pgfsyspdfmark {pgfid4}{31254300}{40736566}
+\pgfsyspdfmark {pgfid5}{35899615}{40496882}
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}Current Reactor Procedures and Operation}{3}{}\protected@file@percent }
+\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{yellow!60}{\textcolor {yellow!60}{o}}\ This paragraph is doing a lot. Consider splitting: first paragraph on the hierarchy and compliance, second on the lack of formal verification. The ``No mathematical proof exists...'' sentence is powerful and deserves emphasis.}{3}{}\protected@file@percent }
+\pgfsyspdfmark {pgfid6}{20423612}{24880744}
+\pgfsyspdfmark {pgfid9}{31254300}{24855008}
+\pgfsyspdfmark {pgfid10}{35899615}{24615324}
+\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{orange!50}{\textcolor {orange!50}{o}}\ This repeats the ``No mathematical proof exists...'' sentence almost verbatim from the paragraph above. Either cut it from the paragraph or from the LIMITATION box.}{3}{}\protected@file@percent }
+\pgfsyspdfmark {pgfid11}{13626615}{17278568}
+\pgfsyspdfmark {pgfid14}{31254300}{16022170}
+\pgfsyspdfmark {pgfid15}{35899615}{15782486}
 \citation{operator_statistics}
 \citation{10CFR55}
 \citation{10CFR50.54}
-\@writefile{toc}{\contentsline {section}{\numberline {2}State of the Art and Limits of Current Practice}{3}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}Current Reactor Procedures and Operation}{3}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Human Factors in Nuclear Accidents}{3}{}\protected@file@percent }
 \citation{Kemeny1979}
 \citation{WNA2020}
 \citation{hogberg_root_2013}
 \citation{zhang_analysis_2025}
 \citation{Kiniry2024}
-\@writefile{toc}{\contentsline {subsection}{\numberline {2.3}Formal Methods}{4}{}\protected@file@percent }
+\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ This is the key insight — the hybrid nature is already there, just not formally verified.}{4}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsubsection}{\numberline {2.3.1}HARDENS}{4}{}\protected@file@percent }
+\pgfsyspdfmark {pgfid16}{14097656}{42090495}
+\pgfsyspdfmark {pgfid19}{31254300}{42064759}
+\pgfsyspdfmark {pgfid20}{35899615}{41825075}
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Human Factors in Nuclear Accidents}{4}{}\protected@file@percent }
+\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Strong thesis for this subsection.}{4}{}\protected@file@percent }
+\pgfsyspdfmark {pgfid21}{5927496}{30010025}
+\pgfsyspdfmark {pgfid24}{31254300}{29984289}
+\pgfsyspdfmark {pgfid25}{35899615}{29744605}
+\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ ``the person responsible for reactor safety is often the root cause of failures'' — devastating summary. Very effective.}{4}{}\protected@file@percent }
+\pgfsyspdfmark {pgfid26}{4915358}{19557033}
+\pgfsyspdfmark {pgfid29}{31254300}{19531297}
+\pgfsyspdfmark {pgfid30}{35899615}{19291613}
+\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Strong empirical grounding. The Chinese plant data is a nice addition — shows this isn't just a Western regulatory perspective.}{4}{}\protected@file@percent }
+\pgfsyspdfmark {pgfid31}{4609444}{10054313}
+\pgfsyspdfmark {pgfid34}{31254300}{10028577}
+\pgfsyspdfmark {pgfid35}{35899615}{9788893}
+\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Well-stated. The ``four decades'' point drives it home.}{4}{}\protected@file@percent }
+\pgfsyspdfmark {pgfid36}{4792689}{5302953}
+\pgfsyspdfmark {pgfid39}{31254300}{4760899}
+\pgfsyspdfmark {pgfid40}{35899615}{4521215}
 \citation{Kiniry2024}
-\@writefile{toc}{\contentsline {subsubsection}{\numberline {2.3.2}Sequent Calculus and Differential Dynamic Logic}{5}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.3}Formal Methods}{5}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsubsection}{\numberline {2.3.1}HARDENS}{5}{}\protected@file@percent }
+\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Good technical depth on HARDENS toolchain.}{5}{}\protected@file@percent }
+\pgfsyspdfmark {pgfid41}{20999294}{21457577}
+\pgfsyspdfmark {pgfid44}{31254300}{21431841}
+\pgfsyspdfmark {pgfid45}{35899615}{21192157}
+\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Clear articulation of the gap your work fills.}{5}{}\protected@file@percent }
+\pgfsyspdfmark {pgfid46}{23128957}{11004585}
+\pgfsyspdfmark {pgfid49}{31254300}{10978849}
+\pgfsyspdfmark {pgfid50}{35899615}{10739165}
+\@writefile{toc}{\contentsline {subsubsection}{\numberline {2.3.2}Sequent Calculus and Differential Dynamic Logic}{6}{}\protected@file@percent }
+\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{red!40}{\textcolor {red!40}{o}}\ Typo: ``ivariant'' should be ``invariant''}{6}{}\protected@file@percent }
+\pgfsyspdfmark {pgfid51}{4749422}{20507305}
+\pgfsyspdfmark {pgfid54}{31254300}{20481569}
+\pgfsyspdfmark {pgfid55}{35899615}{20241885}
+\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{yellow!60}{\textcolor {yellow!60}{o}}\ Consider adding a concrete example here — ``For instance, a system with N modes and M continuous state variables...'' to give readers a sense of the scaling problem.}{6}{}\protected@file@percent }
+\pgfsyspdfmark {pgfid56}{18750152}{12905129}
+\pgfsyspdfmark {pgfid59}{31254300}{12879393}
+\pgfsyspdfmark {pgfid60}{35899615}{12639709}
+\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{orange!50}{\textcolor {orange!50}{o}}\ ``but are far from a complete methodology to design systems with'' — awkward ending preposition. Try: ``but remain far from a complete design methodology'' or ``but do not yet constitute a complete design methodology.''}{6}{}\protected@file@percent }
+\pgfsyspdfmark {pgfid61}{8940582}{10054313}
+\pgfsyspdfmark {pgfid64}{31254300}{5829135}
+\pgfsyspdfmark {pgfid65}{35899615}{5589451}
+\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Your comment here is spot-on. You should add a LIMITATION box: \textit  {Differential dynamic logic has been used for post-hoc analysis of existing systems, not for the constructive design of autonomous controllers.} This is exactly the gap you're filling — you're doing synthesis, not just verification.}{6}{}\protected@file@percent }
+\pgfsyspdfmark {pgfid66}{14192475}{45403152}
 \citation{HANDBOOK ON HYBRID SYSTEMS}
-\@writefile{toc}{\contentsline {section}{\numberline {3}Research Approach}{7}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {section}{\numberline {3}Research Approach}{8}{}\protected@file@percent }
-\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Simplified hybrid automaton for reactor startup. Each discrete state $q_i$ has associated continuous dynamics $f_i$. Guard conditions on transitions (e.g., $T_{avg} > T_{min}$) are predicates over continuous state. Invariant violations ($\neg Inv_i$) trigger transitions to the SCRAM state. The operational level manages discrete transitions; the tactical level executes continuous control within each mode.}}{8}{}\protected@file@percent }
+\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{orange!50}{\textcolor {orange!50}{o}}\ Missing space before ``Our}{8}{}\protected@file@percent }
-\newlabel{fig:hybrid_automaton}{{1}{8}{Research Approach}{figure.1}{}}
+\pgfsyspdfmark {pgfid67}{21351522}{32209854}
-\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}System Requirements, Specifications, and Discrete Controllers}{8}{}\protected@file@percent }
+\pgfsyspdfmark {pgfid70}{31254300}{32184118}
-\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Control scope hierarchy in nuclear power operations. Strategic control (long-term planning) remains with human management. HAHACS addresses the operational level (discrete mode switching) and tactical level (continuous control within modes), which together form a hybrid control system.}}{9}{}\protected@file@percent }
+\pgfsyspdfmark {pgfid71}{35899615}{31944434}
-\newlabel{fig:strat_op_tact}{{2}{9}{System Requirements, Specifications, and Discrete Controllers}{figure.2}{}}
+\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Simplified hybrid automaton for reactor startup. Each discrete state $q_i$ has associated continuous dynamics $f_i$. Guard conditions on transitions (e.g., $T_{avg} > T_{min}$) are predicates over continuous state. Invariant violations ($\neg Inv_i$) trigger transitions to the SCRAM state. The operational level manages discrete transitions; the tactical level executes continuous control within each mode.}}{9}{}\protected@file@percent }
+\newlabel{fig:hybrid_automaton}{{1}{9}{Research Approach}{figure.1}{}}
+\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ This is your key insight — the novelty is compositional, not component-level.}{9}{}\protected@file@percent }
+\pgfsyspdfmark {pgfid72}{5905037}{17221912}
+\pgfsyspdfmark {pgfid75}{31254300}{17196176}
+\pgfsyspdfmark {pgfid76}{35899615}{16956492}
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}System Requirements, Specifications, and Discrete Controllers}{9}{}\protected@file@percent }
+\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Control scope hierarchy in nuclear power operations. Strategic control (long-term planning) remains with human management. HAHACS addresses the operational level (discrete mode switching) and tactical level (continuous control within modes), which together form a hybrid control system.}}{10}{}\protected@file@percent }
+\newlabel{fig:strat_op_tact}{{2}{10}{System Requirements, Specifications, and Discrete Controllers}{figure.2}{}}
 \citation{MANYUS THESIS}
-\@writefile{toc}{\contentsline {subsection}{\numberline {3.2}Continuous Control Modes}{11}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.2}Continuous Control Modes}{13}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.2.1}Transitory Modes}{12}{}\protected@file@percent }
+\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ This three-mode taxonomy is elegant — maps verification tools to control objectives cleanly.}{14}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.2.2}Stabilizing Modes}{12}{}\protected@file@percent }
+\pgfsyspdfmark {pgfid79}{15985073}{33177599}
-\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.2.3}Expulsory Modes}{13}{}\protected@file@percent }
+\pgfsyspdfmark {pgfid82}{31254300}{33151863}
-\@writefile{toc}{\contentsline {subsection}{\numberline {3.3}Industrial Implementation}{14}{}\protected@file@percent }
+\pgfsyspdfmark {pgfid83}{35899615}{32912179}
-\@writefile{toc}{\contentsline {section}{\numberline {4}Metrics for Success}{15}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.2.1}Transitory Modes}{14}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {paragraph}{TRL 3 \textit  {Critical Function and Proof of Concept}}{15}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.2.2}Stabilizing Modes}{15}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {paragraph}{TRL 4 \textit  {Laboratory Testing of Integrated Components}}{15}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.2.3}Expulsory Modes}{16}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {paragraph}{TRL 5 \textit  {Laboratory Testing in Relevant Environment}}{15}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.3}Industrial Implementation}{17}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {section}{\numberline {5}Risks and Contingencies}{17}{}\protected@file@percent }
+\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{red!40}{\textcolor {red!40}{o}}\ Typo: ``excess should be ``access}{17}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsection}{\numberline {5.1}Computational Tractability of Synthesis}{17}{}\protected@file@percent }
+\pgfsyspdfmark {pgfid84}{25258844}{17656489}
-\@writefile{toc}{\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{17}{}\protected@file@percent }
+\pgfsyspdfmark {pgfid87}{31254300}{17630753}
-\@writefile{toc}{\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{18}{}\protected@file@percent }
+\pgfsyspdfmark {pgfid88}{35899615}{17391069}
+\@writefile{toc}{\contentsline {section}{\numberline {4}Metrics for Success}{18}{}\protected@file@percent }
+\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ TRL as primary metric is smart — speaks industry language.}{18}{}\protected@file@percent }
+\pgfsyspdfmark {pgfid89}{6508678}{41712574}
+\pgfsyspdfmark {pgfid92}{31254300}{41686838}
+\pgfsyspdfmark {pgfid93}{35899615}{41447154}
+\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Good framing — explains why other metrics are insufficient.}{18}{}\protected@file@percent }
+\pgfsyspdfmark {pgfid94}{7276206}{33160126}
+\pgfsyspdfmark {pgfid97}{31254300}{33134390}
+\pgfsyspdfmark {pgfid98}{35899615}{32894706}
+\@writefile{toc}{\contentsline {paragraph}{TRL 3 \textit  {Critical Function and Proof of Concept}}{18}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {paragraph}{TRL 4 \textit  {Laboratory Testing of Integrated Components}}{18}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {paragraph}{TRL 5 \textit  {Laboratory Testing in Relevant Environment}}{19}{}\protected@file@percent }
+\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{yellow!60}{\textcolor {yellow!60}{o}}\ Consider noting why graded responses are out of scope — is it time, complexity, or scope creep? Brief justification helps.}{19}{}\protected@file@percent }
+\pgfsyspdfmark {pgfid99}{15785403}{27497812}
+\pgfsyspdfmark {pgfid102}{31254300}{27472076}
+\pgfsyspdfmark {pgfid103}{35899615}{27232392}
+\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Clear success criteria. Committee will know exactly what ``done'' looks like.}{19}{}\protected@file@percent }
+\pgfsyspdfmark {pgfid104}{13547172}{12293460}
+\pgfsyspdfmark {pgfid107}{31254300}{12267724}
+\pgfsyspdfmark {pgfid108}{35899615}{12028040}
+\@writefile{toc}{\contentsline {section}{\numberline {5}Risks and Contingencies}{20}{}\protected@file@percent }
+\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Honest acknowledgment of risks with clear contingencies — committee will appreciate this.}{20}{}\protected@file@percent }
+\pgfsyspdfmark {pgfid109}{19227927}{44563390}
+\pgfsyspdfmark {pgfid112}{31254300}{44537654}
+\pgfsyspdfmark {pgfid113}{35899615}{44297970}
+\@writefile{toc}{\contentsline {subsection}{\numberline {5.1}Computational Tractability of Synthesis}{20}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{20}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{22}{}\protected@file@percent }
 \citation{eia_lcoe_2022}
 \citation{eesi_datacenter_2024}
 \citation{eia_lcoe_2022}
-\@writefile{toc}{\contentsline {section}{\numberline {6}Broader Impacts}{20}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {section}{\numberline {6}Broader Impacts}{24}{}\protected@file@percent }
+\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ ``If it works here, it works anywhere — strong closing argument.}{25}{}\protected@file@percent }
+\pgfsyspdfmark {pgfid114}{19399794}{25935871}
+\pgfsyspdfmark {pgfid117}{31254300}{25910135}
+\pgfsyspdfmark {pgfid118}{35899615}{25670451}
 \bibstyle{ieeetr}
 \bibdata{references}
-\@writefile{toc}{\contentsline {section}{\numberline {7}Schedule, Milestones, and Deliverables}{22}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {section}{\numberline {7}Schedule, Milestones, and Deliverables}{26}{}\protected@file@percent }
 \gtt@chartextrasize{0}{164.1287pt}
-\@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces Project schedule showing major research thrusts, milestones (orange row), and publications (green row). Red diamonds indicate completion points. Overlapping bars indicate parallel work where appropriate.}}{22}{}\protected@file@percent }
+\@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces Project schedule showing major research thrusts, milestones (orange row), and publications (green row). Red diamonds indicate completion points. Overlapping bars indicate parallel work where appropriate.}}{26}{}\protected@file@percent }
-\newlabel{fig:gantt}{{3}{22}{Schedule, Milestones, and Deliverables}{figure.3}{}}
+\newlabel{fig:gantt}{{3}{26}{Schedule, Milestones, and Deliverables}{figure.3}{}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {7.1}Milestones and Deliverables}{22}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsection}{\numberline {7.1}Milestones and Deliverables}{26}{}\protected@file@percent }
 \bibcite{NUREG-0899}{1}
 \bibcite{10CFR50.34}{2}
 \bibcite{10CFR55.59}{3}
@@ -62,10 +156,14 @@
 \bibcite{10CFR50.54}{8}
 \bibcite{Kemeny1979}{9}
 \bibcite{WNA2020}{10}
+\@writefile{tdo}{\contentsline {todo}{\fcolorbox {black}{green!40}{\textcolor {green!40}{o}}\ Clear timeline with publication targets — shows you have a plan.}{27}{}\protected@file@percent }
+\pgfsyspdfmark {pgfid120}{4865044}{36388863}
+\pgfsyspdfmark {pgfid123}{31254300}{36363127}
+\pgfsyspdfmark {pgfid124}{35899615}{36123443}
+\@writefile{toc}{\contentsline {section}{References}{27}{}\protected@file@percent }
 \bibcite{hogberg_root_2013}{11}
 \bibcite{zhang_analysis_2025}{12}
 \bibcite{Kiniry2024}{13}
 \bibcite{eia_lcoe_2022}{14}
 \bibcite{eesi_datacenter_2024}{15}
-\@writefile{toc}{\contentsline {section}{References}{23}{}\protected@file@percent }
+\gdef \@abspage@last{30}
-\gdef \@abspage@last{27}

main.blg

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

main.fdb_latexmk

@@ -1,13 +1,13 @@
 # Fdb version 4
-["bibtex main"] 1772657516.80216 "main.aux" "main.bbl" "main" 1772909692.49481 2
+["bibtex main"] 1773173597.9699 "main.aux" "main.bbl" "main" 1773173598.03253 2
   "./references.bib" 1765591319.20023 14069 2a4f74c587187a8a71049043171eb0fe ""
   "/usr/local/texlive/2025/texmf-dist/bibtex/bst/base/ieeetr.bst" 1292289607 18361 1a00e58565e7f19bf2b3e1bfb82254ae ""
-  "main.aux" 1772909692.27813 5748 38dc212531f318e67f49d597c2908f59 "pdflatex"
+  "main.aux" 1773173597.75702 14664 f3280fe42bd32be7039c7ddcbc5aad8b "pdflatex"
   (generated)
   "main.bbl"
   "main.blg"
   (rewritten before read)
-["pdflatex"] 1772909690.76715 "main.tex" "main.pdf" "main" 1772909692.4949 0
+["pdflatex"] 1773173595.85606 "main.tex" "main.pdf" "main" 1773173598.03262 0
   "/usr/local/texlive/2025/texmf-dist/fonts/enc/dvips/base/8r.enc" 1165713224 4850 80dc9bab7f31fb78a000ccfed0e27cab ""
   "/usr/local/texlive/2025/texmf-dist/fonts/map/fontname/texfonts.map" 1577235249 3524 cb3e574dea2d1052e39280babc910dc8 ""
   "/usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm" 1136768653 1408 5937f58aa508ea2cea4901c07d10f5fe ""
@@ -243,19 +243,19 @@
   "/usr/local/texlive/2025/texmf-var/fonts/map/pdftex/updmap/pdftex.map" 1765668892 5467155 19efa205003f9ecad95fbbaa6ff24da1 ""
   "/usr/local/texlive/2025/texmf-var/web2c/pdftex/pdflatex.fmt" 1741450574 3345740 46b66fdb0378f7bf5921b5eabf1762b8 ""
   "/usr/local/texlive/2025/texmf.cnf" 1741450484 577 418a7058ec8e006d8704f60ecd22c938 ""
-  "1-goals-and-outcomes/research_statement_v1.tex" 1765591319.18896 4450 070caee751214eaddffa6b3403f8ed43 ""
+  "1-goals-and-outcomes/goals.tex" 1773173595.19694 5785 7b5e137b620440854e7e220d58ca9872 ""
-  "1-goals-and-outcomes/v1.tex" 1765591319.1893 5825 07f6fba24cfa050a3b2b00c416f0f45f ""
+  "2-state-of-the-art/state-of-art.tex" 1773107148.30113 14525 3b8c13d63175e6d9fd1a60995e47777f ""
-  "2-state-of-the-art/v2.tex" 1772909690.23793 12622 1460f7a4c2b48a1a772d8a0f5db216af ""
+  "3-research-approach/approach.tex" 1773107148.30209 36035 28bfba4166bebc2d97137ab44e7cb41c ""
-  "3-research-approach/v3.tex" 1772743152.76875 35753 93d4c7b608feeba783c33affa59dd220 ""
+  "4-metrics-of-success/metrics.tex" 1773107148.30251 5967 9d1414599bd374b4166fcce4de6e6644 ""
-  "4-metrics-of-success/v1.tex" 1765591319.19036 5586 e5fb80ced00bcdc318ffe3861b0064bc ""
+  "5-risks-and-contingencies/risks.tex" 1773107148.30287 10515 44f5f800e1332517ebfe61e7db38b7cc ""
-  "5-risks-and-contingencies/v1.tex" 1765591319.19058 10412 17e755aa8451c45198372af7afe3c500 ""
+  "6-broader-impacts/impacts.tex" 1773107148.30317 4912 c7ccb2b7aade93b198e985e4832fd6a8 ""
-  "6-broader-impacts/v1.tex" 1765591319.19072 4834 418aae223b778759691eaf9124a5360c ""
+  "8-schedule/schedule.tex" 1773107148.30345 4551 57e4fef2d56e8d84227d70745141e7eb ""
-  "8-schedule/v1.tex" 1765591319.19095 4473 8ad96bbf9cedf2ea09298ecbd4e01b83 ""
   "dane_proposal_format.cls" 1769715785.9835 2883 ea175794171aa0291ef71716b2190bf0 ""
-  "main.aux" 1772909692.27813 5748 38dc212531f318e67f49d597c2908f59 "pdflatex"
+  "main.aux" 1773173597.75702 14664 f3280fe42bd32be7039c7ddcbc5aad8b "pdflatex"
-  "main.bbl" 1772657516.86263 2919 0ea026a17b15c1ad2ed657bdbf26dfdc "bibtex main"
+  "main.bbl" 1773173598.03178 2919 0ea026a17b15c1ad2ed657bdbf26dfdc "bibtex main"
-  "main.tex" 1772218582.98667 954 b43a8fa32e5ebbd5cc6319a366737c39 ""
+  "main.tex" 1773173556.09967 2437 582e7a1c0b549a31e0ee40a98d020260 ""
-  "main.toc" 1772909692.28232 2129 eb658283ff0c872296846602d3e9dde6 "pdflatex"
+  "main.toc" 1773173597.76091 2128 2d6213c87e5e84ae87ae7dcb05dc4ca7 "pdflatex"
+  "todonotes.sty" 1773106207.6557 21404 916e19cbd009b6d289c8194b313d3895 ""
   (generated)
   "main.aux"
   "main.log"

main.fls

@@ -336,6 +336,8 @@ INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pgf/utilities/pgfcalendar.c
 INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/colortbl/colortbl.sty
 INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/colortbl/colortbl.sty
 INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics/color.sty
+INPUT ./todonotes.sty
+INPUT todonotes.sty
 INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/ot1ptm.fd
 INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/ot1ptm.fd
 INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/ot1ptm.fd
@@ -414,14 +416,6 @@ INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmr7t.vf
 INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm
 INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmr7t.vf
 INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm
-INPUT ./1-goals-and-outcomes/research_statement_v1.tex
-INPUT ./1-goals-and-outcomes/research_statement_v1.tex
-INPUT 1-goals-and-outcomes/research_statement_v1.tex
-INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm
-INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmr7t.vf
-INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm
-INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmri7t.vf
-INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmri8r.tfm
 INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm
 INPUT ./main.toc
 INPUT ./main.toc
@@ -442,6 +436,7 @@ INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm
 INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm
 INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm
 INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm
+INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm
 INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm
 INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm
 INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm
@@ -456,27 +451,31 @@ INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmb7t.vf
 INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmb8r.tfm
 INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmb7t.vf
 INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmb8r.tfm
-INPUT ./1-goals-and-outcomes/v1.tex
+INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmr7t.vf
-INPUT ./1-goals-and-outcomes/v1.tex
+INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm
-INPUT ./1-goals-and-outcomes/v1.tex
+INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmri7t.vf
-INPUT ./1-goals-and-outcomes/v1.tex
+INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmri8r.tfm
-INPUT 1-goals-and-outcomes/v1.tex
+INPUT ./1-goals-and-outcomes/goals.tex
-INPUT ./2-state-of-the-art/v2.tex
+INPUT ./1-goals-and-outcomes/goals.tex
-INPUT ./2-state-of-the-art/v2.tex
+INPUT 1-goals-and-outcomes/goals.tex
-INPUT ./2-state-of-the-art/v2.tex
+INPUT ./2-state-of-the-art/state-of-art.tex
-INPUT ./2-state-of-the-art/v2.tex
+INPUT ./2-state-of-the-art/state-of-art.tex
-INPUT 2-state-of-the-art/v2.tex
+INPUT ./2-state-of-the-art/state-of-art.tex
+INPUT ./2-state-of-the-art/state-of-art.tex
+INPUT 2-state-of-the-art/state-of-art.tex
 INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/zptmcm7t.vf
 INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm
 INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/cm/cmr10.tfm
 INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/zptmcm7m.vf
 INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/psyro.tfm
 INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/cm/cmmi10.tfm
-INPUT ./3-research-approach/v3.tex
+INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmri7t.vf
-INPUT ./3-research-approach/v3.tex
+INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmri8r.tfm
-INPUT ./3-research-approach/v3.tex
+INPUT ./3-research-approach/approach.tex
-INPUT ./3-research-approach/v3.tex
+INPUT ./3-research-approach/approach.tex
-INPUT 3-research-approach/v3.tex
+INPUT ./3-research-approach/approach.tex
+INPUT ./3-research-approach/approach.tex
+INPUT 3-research-approach/approach.tex
 INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/ts1ptm.fd
 INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/ts1ptm.fd
 INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/ts1ptm.fd
@@ -510,7 +509,6 @@ INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/rsfs/rsfs5.tfm
 INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/zptmcm7m.vf
 INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/psyro.tfm
 INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/cm/cmmi10.tfm
-INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmri8r.tfm
 INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/zptmcm7t.vf
 INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm
 INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm
@@ -530,38 +528,37 @@ INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm
 INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm
 INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/cm/cmr10.tfm
 INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmr7t.vf
-INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm
-INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm
 INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmb7t.vf
 INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmb8r.tfm
-INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmri7t.vf
+INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm
+INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm
 INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/zptmcm7t.vf
 INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm
 INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm
 INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/cm/cmr10.tfm
-INPUT ./4-metrics-of-success/v1.tex
+INPUT ./4-metrics-of-success/metrics.tex
-INPUT ./4-metrics-of-success/v1.tex
+INPUT ./4-metrics-of-success/metrics.tex
-INPUT ./4-metrics-of-success/v1.tex
+INPUT ./4-metrics-of-success/metrics.tex
-INPUT ./4-metrics-of-success/v1.tex
+INPUT ./4-metrics-of-success/metrics.tex
-INPUT 4-metrics-of-success/v1.tex
+INPUT 4-metrics-of-success/metrics.tex
 INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmbi7t.tfm
 INPUT /usr/local/texlive/2025/texmf-dist/fonts/vf/adobe/times/ptmbi7t.vf
 INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/times/ptmbi8r.tfm
-INPUT ./5-risks-and-contingencies/v1.tex
+INPUT ./5-risks-and-contingencies/risks.tex
-INPUT ./5-risks-and-contingencies/v1.tex
+INPUT ./5-risks-and-contingencies/risks.tex
-INPUT ./5-risks-and-contingencies/v1.tex
+INPUT ./5-risks-and-contingencies/risks.tex
-INPUT ./5-risks-and-contingencies/v1.tex
+INPUT ./5-risks-and-contingencies/risks.tex
-INPUT 5-risks-and-contingencies/v1.tex
+INPUT 5-risks-and-contingencies/risks.tex
-INPUT ./6-broader-impacts/v1.tex
+INPUT ./6-broader-impacts/impacts.tex
-INPUT ./6-broader-impacts/v1.tex
+INPUT ./6-broader-impacts/impacts.tex
-INPUT ./6-broader-impacts/v1.tex
+INPUT ./6-broader-impacts/impacts.tex
-INPUT ./6-broader-impacts/v1.tex
+INPUT ./6-broader-impacts/impacts.tex
-INPUT 6-broader-impacts/v1.tex
+INPUT 6-broader-impacts/impacts.tex
-INPUT ./8-schedule/v1.tex
+INPUT ./8-schedule/schedule.tex
-INPUT ./8-schedule/v1.tex
+INPUT ./8-schedule/schedule.tex
-INPUT ./8-schedule/v1.tex
+INPUT ./8-schedule/schedule.tex
-INPUT ./8-schedule/v1.tex
+INPUT ./8-schedule/schedule.tex
-INPUT 8-schedule/v1.tex
+INPUT 8-schedule/schedule.tex
 INPUT ./main.bbl
 INPUT ./main.bbl
 INPUT main.bbl

main.log

@@ -1,4 +1,4 @@
-This is pdfTeX, Version 3.141592653-2.6-1.40.27 (TeX Live 2025) (preloaded format=pdflatex 2025.3.8)  7 MAR 2026 13:54
+This is pdfTeX, Version 3.141592653-2.6-1.40.27 (TeX Live 2025) (preloaded format=pdflatex 2025.3.8)  10 MAR 2026 16:13
 entering extended mode
  restricted \write18 enabled.
  file:line:error style messages enabled.
@@ -775,31 +775,35 @@ Package: colortbl 2024/07/06 v1.0i Color table columns (DPC)
 \everycr=\toks52
 \minrowclearance=\skip68
 \rownum=\count391
+) (./todonotes.sty
+Package: todonotes 2024/01/05 v1.1.7 Todonotes source and documentation.
+Package: todonotes 2024/01/05
+\c@@todonotes@numberoftodonotes=\count392
 )
-LaTeX Font Info:    Trying to load font information for OT1+ptm on input line 10.
+LaTeX Font Info:    Trying to load font information for OT1+ptm on input line 45.
  (/usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/ot1ptm.fd
 File: ot1ptm.fd 2001/06/04 font definitions for OT1/ptm.
 ) (/usr/local/texlive/2025/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def
 File: l3backend-pdftex.def 2024-05-08 L3 backend support: PDF output (pdfTeX)
-\l__color_backend_stack_int=\count392
+\l__color_backend_stack_int=\count393
 \l__pdf_internal_box=\box100
 ) (./main.aux)
 \openout1 = `main.aux'.
 
-LaTeX Font Info:    Checking defaults for OML/cmm/m/it on input line 10.
+LaTeX Font Info:    Checking defaults for OML/cmm/m/it on input line 45.
-LaTeX Font Info:    ... okay on input line 10.
+LaTeX Font Info:    ... okay on input line 45.
-LaTeX Font Info:    Checking defaults for OMS/cmsy/m/n on input line 10.
+LaTeX Font Info:    Checking defaults for OMS/cmsy/m/n on input line 45.
-LaTeX Font Info:    ... okay on input line 10.
+LaTeX Font Info:    ... okay on input line 45.
-LaTeX Font Info:    Checking defaults for OT1/cmr/m/n on input line 10.
+LaTeX Font Info:    Checking defaults for OT1/cmr/m/n on input line 45.
-LaTeX Font Info:    ... okay on input line 10.
+LaTeX Font Info:    ... okay on input line 45.
-LaTeX Font Info:    Checking defaults for T1/cmr/m/n on input line 10.
+LaTeX Font Info:    Checking defaults for T1/cmr/m/n on input line 45.
-LaTeX Font Info:    ... okay on input line 10.
+LaTeX Font Info:    ... okay on input line 45.
-LaTeX Font Info:    Checking defaults for TS1/cmr/m/n on input line 10.
+LaTeX Font Info:    Checking defaults for TS1/cmr/m/n on input line 45.
-LaTeX Font Info:    ... okay on input line 10.
+LaTeX Font Info:    ... okay on input line 45.
-LaTeX Font Info:    Checking defaults for OMX/cmex/m/n on input line 10.
+LaTeX Font Info:    Checking defaults for OMX/cmex/m/n on input line 45.
-LaTeX Font Info:    ... okay on input line 10.
+LaTeX Font Info:    ... okay on input line 45.
-LaTeX Font Info:    Checking defaults for U/cmr/m/n on input line 10.
+LaTeX Font Info:    Checking defaults for U/cmr/m/n on input line 45.
-LaTeX Font Info:    ... okay on input line 10.
+LaTeX Font Info:    ... okay on input line 45.
 
 *geometry* driver: auto-detecting
 *geometry* detected driver: pdftex
@@ -813,7 +817,7 @@ LaTeX Font Info:    ... okay on input line 10.
 * v-part:(T,H,B)=(72.26999pt, 650.43001pt, 72.26999pt)
 * \paperwidth=614.295pt
 * \paperheight=794.96999pt
-* \textwidth=469.75502pt
+* \textwidth=361.34999pt
 * \textheight=650.43001pt
 * \oddsidemargin=0.0pt
 * \evensidemargin=0.0pt
@@ -822,11 +826,11 @@ LaTeX Font Info:    ... okay on input line 10.
 * \headsep=25.0pt
 * \topskip=12.0pt
 * \footskip=30.0pt
-* \marginparwidth=44.0pt
+* \marginparwidth=142.26378pt
-* \marginparsep=10.0pt
+* \marginparsep=8.5359pt
 * \columnsep=10.0pt
 * \skip\footins=10.8pt plus 4.0pt minus 2.0pt
-* \hoffset=0.0pt
+* \hoffset=-36.135pt
 * \voffset=0.0pt
 * \mag=1000
 * \@twocolumnfalse
@@ -839,16 +843,16 @@ LaTeX Font Info:    ... okay on input line 10.
 File: fc-english.def 2016/01/12
 ) (/usr/local/texlive/2025/texmf-dist/tex/context/base/mkii/supp-pdf.mkii
 [Loading MPS to PDF converter (version 2006.09.02).]
-\scratchcounter=\count393
+\scratchcounter=\count394
 \scratchdimen=\dimen332
 \scratchbox=\box101
-\nofMPsegments=\count394
+\nofMPsegments=\count395
-\nofMParguments=\count395
+\nofMParguments=\count396
 \everyMPshowfont=\toks53
-\MPscratchCnt=\count396
+\MPscratchCnt=\count397
 \MPscratchDim=\dimen333
-\MPnumerator=\count397
+\MPnumerator=\count398
-\makeMPintoPDFobject=\count398
+\makeMPintoPDFobject=\count399
 \everyMPtoPDFconversion=\toks54
 ) (/usr/local/texlive/2025/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty
 Package: epstopdf-base 2020-01-24 v2.11 Base part for package epstopdf
@@ -861,123 +865,311 @@ Package: pdflscape 2022-10-27 v0.13 Display of landscape pages in PDF
 Package: pdflscape-nometadata 2022-10-28 v0.13 Display of landscape pages in PDF (HO)
 Package pdflscape Info: Auto-detected driver: pdftex on input line 81.
 ))
-\c@lstlisting=\count399
+\c@lstlisting=\count400
-LaTeX Font Info:    Trying to load font information for OT1+ztmcm on input line 13.
+LaTeX Font Info:    Trying to load font information for OT1+ztmcm on input line 48.
  (/usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/ot1ztmcm.fd
 File: ot1ztmcm.fd 2000/01/03 Fontinst v1.801 font definitions for OT1/ztmcm.
 )
-LaTeX Font Info:    Trying to load font information for OML+ztmcm on input line 13.
+LaTeX Font Info:    Trying to load font information for OML+ztmcm on input line 48.
  (/usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/omlztmcm.fd
 File: omlztmcm.fd 2000/01/03 Fontinst v1.801 font definitions for OML/ztmcm.
 )
-LaTeX Font Info:    Trying to load font information for OMS+ztmcm on input line 13.
+LaTeX Font Info:    Trying to load font information for OMS+ztmcm on input line 48.
  (/usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/omsztmcm.fd
 File: omsztmcm.fd 2000/01/03 Fontinst v1.801 font definitions for OMS/ztmcm.
 )
-LaTeX Font Info:    Trying to load font information for OMX+ztmcm on input line 13.
+LaTeX Font Info:    Trying to load font information for OMX+ztmcm on input line 48.
  (/usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/omxztmcm.fd
 File: omxztmcm.fd 2000/01/03 Fontinst v1.801 font definitions for OMX/ztmcm.
 )
 LaTeX Font Info:    Font shape `OT1/ptm/bx/n' in size <14.4> not available
-(Font)              Font shape `OT1/ptm/b/n' tried instead on input line 13.
+(Font)              Font shape `OT1/ptm/b/n' tried instead on input line 48.
 LaTeX Font Info:    Font shape `OT1/ptm/bx/n' in size <10.95> not available
-(Font)              Font shape `OT1/ptm/b/n' tried instead on input line 13.
+(Font)              Font shape `OT1/ptm/b/n' tried instead on input line 48.
 LaTeX Font Info:    Font shape `OT1/ptm/bx/n' in size <8> not available
-(Font)              Font shape `OT1/ptm/b/n' tried instead on input line 13.
+(Font)              Font shape `OT1/ptm/b/n' tried instead on input line 48.
-LaTeX Font Info:    Trying to load font information for U+rsfs on input line 13.
+LaTeX Font Info:    Trying to load font information for U+rsfs on input line 48.
  (/usr/local/texlive/2025/texmf-dist/tex/latex/jknapltx/ursfs.fd
 File: ursfs.fd 1998/03/24 rsfs font definition file (jk)
 )
 
 [1
 
-{/usr/local/texlive/2025/texmf-var/fonts/map/pdftex/updmap/pdftex.map}{/usr/local/texlive/2025/texmf-dist/fonts/enc/dvips/base/8r.enc}] (./1-goals-and-outcomes/research_statement_v1.tex)
+{/usr/local/texlive/2025/texmf-var/fonts/map/pdftex/updmap/pdftex.map}{/usr/local/texlive/2025/texmf-dist/fonts/enc/dvips/base/8r.enc}] (./main.toc
-
-[1] (./main.toc
 LaTeX Font Info:    Font shape `OT1/ptm/bx/n' in size <12> not available
 (Font)              Font shape `OT1/ptm/b/n' tried instead on input line 4.
 LaTeX Font Info:    Font shape `OT1/ptm/bx/n' in size <9> not available
 (Font)              Font shape `OT1/ptm/b/n' tried instead on input line 4.
 LaTeX Font Info:    Font shape `OT1/ptm/bx/n' in size <7> not available
 (Font)              Font shape `OT1/ptm/b/n' tried instead on input line 4.
+
+Overfull \hbox (1.1784pt too wide) in paragraph at lines 10--10
+ [][] []\OT1/ptm/m/n/12 System Re-quire-ments, Spec-i-fi-ca-tions, and Dis-crete Con-trollers [][]  
+ []
+
 )
 \tf@toc=\write4
 \openout4 = `main.toc'.
 
 
 
-[2] (./1-goals-and-outcomes/v1.tex
+[1] (./1-goals-and-outcomes/goals.tex
+
+[1]
+Overfull \hbox (3.71007pt too wide) in paragraph at lines 86--98
+[]\OT1/ptm/b/n/12 Demonstrate au-tonomous re-ac-tor startup con-trol with safety guar-
+ []
+
+)
+Overfull \hbox (1.53879pt too wide) in paragraph at lines 102--56
+\OT1/ptm/m/n/12 from ex-ist-ing pro-ce-dures with math-e-mat-i-cal proof of cor-rect be-hav-ior. High-
+ []
+
+
+
+[2] (./2-state-of-the-art/state-of-art.tex
+
+LaTeX Warning: Citation `NUREG-0899' on page 3 undefined on input line 19.
+
+
+LaTeX Warning: Citation `10CFR50.34' on page 3 undefined on input line 19.
+
+
+LaTeX Warning: Citation `10CFR55.59' on page 3 undefined on input line 23.
+
+
+Overfull \hbox (2.2587pt too wide) in paragraph at lines 13--32
+\OT1/ptm/m/n/12 Se-vere Ac-ci-dent Man-age-ment Guide-lines (SAMGs) for beyond-design-basis
+ []
+
+
+LaTeX Warning: Marginpar on page 3 moved.
+
+
+LaTeX Warning: Citation `WRPS.Description' on page 3 undefined on input line 59.
+
+
+LaTeX Warning: Citation `gentillon_westinghouse_1999' on page 3 undefined on input line 59.
 
-[1])
 
-[2] (./2-state-of-the-art/v2.tex
 
 [3]
 
+LaTeX Warning: Citation `operator_statistics' on page 4 undefined on input line 68.
+
+
+LaTeX Warning: Citation `10CFR55' on page 4 undefined on input line 71.
+
+
+LaTeX Warning: Citation `10CFR50.54' on page 4 undefined on input line 72.
+
+
+LaTeX Warning: Citation `Kemeny1979' on page 4 undefined on input line 84.
+
+
+Overfull \hbox (6.91362pt too wide) in paragraph at lines 75--92
+\OT1/ptm/m/n/12 com-pelling mo-ti-va-tion for for-mal au-to-mated con-trol with math-e-mat-i-cal safety
+ []
+
+
+LaTeX Warning: Citation `WNA2020' on page 4 undefined on input line 95.
+
+
+LaTeX Warning: Citation `hogberg_root_2013' on page 4 undefined on input line 98.
+
+
+LaTeX Warning: Citation `zhang_analysis_2025' on page 4 undefined on input line 100.
+
+
+LaTeX Warning: Marginpar on page 4 moved.
+
+
+LaTeX Warning: Citation `Kiniry2024' on page 4 undefined on input line 118.
+
+
+Overfull \hbox (12.42279pt too wide) in paragraph at lines 116--119
+\OT1/ptm/m/n/12 The High As-sur-ance Rig-or-ous Dig-i-tal En-gi-neer-ing for Nu-clear Safety (HARD-
+ []
+
+
+
 [4]
+Overfull \hbox (4.45078pt too wide) in paragraph at lines 156--161
+[]\OT1/ptm/b/n/12 LIMITATION: \OT1/ptm/m/it/12 HARD-ENS ad-dressed dis-crete con-trol logic with-out con-
+ []
 
-[5])
 
-[6] (./3-research-approach/v3.tex
+LaTeX Warning: Citation `Kiniry2024' on page 5 undefined on input line 165.
 
-LaTeX Warning: Citation `HANDBOOK ON HYBRID SYSTEMS' on page 7 undefined on input line 50.
+
+
+[5]
+Overfull \hbox (1.39072pt too wide) in paragraph at lines 176--184
+[]\OT1/ptm/b/n/12 LIMITATION: \OT1/ptm/m/it/12 HARD-ENS achieved TRL 2--3 with-out ex-per-i-men-tal val-
+ []
+
+
+LaTeX Warning: Marginpar on page 6 moved.
+
+)
+
+[6]
+
+[7] (./3-research-approach/approach.tex
+
+LaTeX Warning: Citation `HANDBOOK ON HYBRID SYSTEMS' on page 8 undefined on input line 50.
+
+
+Overfull \hbox (5.73631pt too wide) in paragraph at lines 41--52
+[]\OT1/ptm/m/n/12 To build a high-assurance hy-brid au-tonomous con-trol sys-tem (HA-HACS),
+ []
 
 LaTeX Font Info:    Trying to load font information for TS1+ptm on input line 60.
 (/usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/ts1ptm.fd
 File: ts1ptm.fd 2001/06/04 font definitions for TS1/ptm.
 )
 
-[7]
+[8]
 LaTeX Font Info:    Font shape `OT1/ptm/bx/n' in size <6> not available
 (Font)              Font shape `OT1/ptm/b/n' tried instead on input line 103.
 LaTeX Font Info:    Font shape `OT1/ptm/bx/n' in size <5> not available
 (Font)              Font shape `OT1/ptm/b/n' tried instead on input line 109.
 
+Overfull \hbox (47.01094pt too wide) in paragraph at lines 128--134
+ [][] 
+ []
+
 
-[8]
 
 [9]
+Overfull \hbox (104.18398pt too wide) in paragraph at lines 203--207
+ [][] 
+ []
+
+
 
 [10]
 
-LaTeX Warning: Citation `MANYUS THESIS' on page 11 undefined on input line 383.
-
-
-
 [11]
 
 [12]
 
-[13])
+LaTeX Warning: Citation `MANYUS THESIS' on page 13 undefined on input line 383.
 
-[14] (./4-metrics-of-success/v1.tex
 
-[15])
 
-[16] (./5-risks-and-contingencies/v1.tex
+[13]
 
-[17]
+[14]
 
-[18])
+[15]
-
+Overfull \hbox (2.1067pt too wide) in paragraph at lines 578--584
-[19] (./6-broader-impacts/v1.tex)
+[]\OT1/ptm/m/n/12 Traditional safety anal-y-sis tech-niques in-form the con-struc-tion of $\OT1/ztmcm/m/n/12 ^^B[]$\OT1/ptm/m/n/12 .
-
-[20]
-
-[21] (./8-schedule/v1.tex
-Missing character: There is no , in font nullfont!
-) (./main.bbl
-
-[22]
-Underfull \hbox (badness 10000) in paragraph at lines 32--33
-\OT1/cmtt/m/n/12 nuclear . org / information -[] library / safety -[] and -[] security / safety -[] of -[]
  []
 
 
 
-[23])
+[16])
 
-[24] (./main.aux)
+[17] (./4-metrics-of-success/metrics.tex
+Overfull \hbox (3.50658pt too wide) in paragraph at lines 25--35
+\OT1/ptm/m/n/12 is in-suf-fi-cient for adop-tion; con-versely, show-ing em-pir-i-cal per-for-mance with-
+ []
+
+
+
+[18])
+
+[19] (./5-risks-and-contingencies/risks.tex
+Overfull \hbox (0.96176pt too wide) in paragraph at lines 3--13
+\OT1/ptm/m/n/12 This re-search re-lies on sev-eral crit-i-cal as-sump-tions that, if in-val-i-dated, would
+ []
+
+
+Overfull \hbox (8.87949pt too wide) in paragraph at lines 27--36
+[]\OT1/ptm/m/n/12 Several in-di-ca-tors would pro-vide early warn-ing of com-pu-ta-tional tractabil-
+ []
+
+
+Overfull \hbox (3.75879pt too wide) in paragraph at lines 49--62
+\OT1/ptm/m/n/12 The sec-ond crit-i-cal as-sump-tion con-cerns the map-ping be-tween boolean guard
+ []
+
+
+
+[20]
+
+[21]
+Overfull \hbox (2.96642pt too wide) in paragraph at lines 130--145
+\OT1/ptm/m/n/12 FRETish or sim-i-lar spec-i-fi-ca-tion lan-guages would demon-strate how to bridge
+ []
+
+
+Overfull \hbox (2.61935pt too wide) in paragraph at lines 130--145
+\OT1/ptm/m/n/12 the gap be-tween cur-rent pro-ce-dures and the pre-ci-sion needed for au-tonomous
+ []
+
+
+
+[22])
+
+[23] (./6-broader-impacts/impacts.tex
+
+LaTeX Warning: Citation `eia_lcoe_2022' on page 24 undefined on input line 13.
+
+
+LaTeX Warning: Citation `eesi_datacenter_2024' on page 24 undefined on input line 15.
+
+
+LaTeX Warning: Citation `eia_lcoe_2022' on page 24 undefined on input line 20.
+
+
+
+[24])
+
+[25] (./8-schedule/schedule.tex
+Overfull \hbox (0.69846pt too wide) in paragraph at lines 8--18
+\OT1/ptm/m/n/12 guage pro-ce-dures into machine-readable re-quire-ments. The sec-ond semester
+ []
+
+Missing character: There is no , in font nullfont!
+
+Overfull \hbox (75.92079pt too wide) in paragraph at lines 71--72
+ [][] 
+ []
+
+) (./main.bbl
+Overfull \hbox (0.29076pt too wide) in paragraph at lines 78--1
+\OT1/ptm/m/n/12 M1 (Month 4) con-firms that startup pro-ce-dures have been suc-cess-fully trans-
+ []
+
+
+
+[26]
+Underfull \hbox (badness 1360) in paragraph at lines 23--24
+[]\OT1/ptm/m/n/12 U.S. Nu-clear Reg-u-la-tory Com-mis-sion, ``Part 55|Op-er-a-tors' Li-
+ []
+
+
+Underfull \hbox (badness 10000) in paragraph at lines 32--33
+[]\OT1/ptm/m/n/12 World Nu-clear As-so-ci-a-tion, ``Safety of nu-clear power re-
+ []
+
+
+Underfull \hbox (badness 10000) in paragraph at lines 32--33
+\OT1/ptm/m/n/12 ac-tors.'' $\OT1/cmtt/m/n/12 https : / / www . world -[] nuclear . org / information -[]
+ []
+
+
+Underfull \hbox (badness 10000) in paragraph at lines 32--33
+\OT1/cmtt/m/n/12 library / safety -[] and -[] security / safety -[] of -[] plants / safety -[]
+ []
+
+
+
+[27])
+
+[28] (./main.aux)
  ***********
 LaTeX2e <2024-11-01> patch level 2
 L3 programming layer <2025-01-18>
@@ -986,20 +1178,23 @@ L3 programming layer <2025-01-18>
 
 LaTeX Warning: There were undefined references.
 
+
+LaTeX Warning: Label(s) may have changed. Rerun to get cross-references right.
+
  ) 
 Here is how much of TeX's memory you used:
- 26267 strings out of 473190
+ 26786 strings out of 473190
- 547152 string characters out of 5715801
+ 559578 string characters out of 5715801
- 964002 words of memory out of 5000000
+ 1022906 words of memory out of 5000000
- 48907 multiletter control sequences out of 15000+600000
+ 49422 multiletter control sequences out of 15000+600000
  614280 words of font info for 155 fonts, out of 8000000 for 9000
  1141 hyphenation exceptions out of 8191
- 110i,9n,107p,1062b,965s stack positions out of 10000i,1000n,20000p,200000b,200000s
+ 110i,9n,107p,1062b,966s stack positions out of 10000i,1000n,20000p,200000b,200000s
 </usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt12.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/symbols/msbm10.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/rsfs/rsfs10.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/urw/symbol/usyr.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/urw/symbol/usyr.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/urw/times/utmb8a.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/urw/times/utmbi8a.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/urw/times/utmr8a.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/urw/times/utmri8a.pfb>
-Output written on main.pdf (27 pages, 188983 bytes).
+Output written on main.pdf (30 pages, 199129 bytes).
 PDF statistics:
- 180 PDF objects out of 1000 (max. 8388607)
+ 189 PDF objects out of 1000 (max. 8388607)
- 109 compressed objects within 2 object streams
+ 115 compressed objects within 2 object streams
  0 named destinations out of 1000 (max. 500000)
  109 words of extra memory for PDF output out of 10000 (max. 10000000)
 

main.tex

@@ -7,35 +7,70 @@
 \usepackage{pgfgantt}
 \usepackage{pdfpages}        % For including PDF files
 
+% === SPLIT'S EDITING COMMENTS ===
+% Set to 1 for edit mode (wider margins, visible comments)
+% Set to 0 for final mode (normal margins, comments hidden)
+\newcommand{\editmode}{1}
+
+\ifnum\editmode=1
+  % Edit mode: load todonotes, adjust margins
+  \usepackage[colorinlistoftodos,prependcaption,textsize=small]{todonotes}
+  \setlength{\hoffset}{-0.5in}        % Shift everything left
+  \setlength{\oddsidemargin}{0in}     % Left margin
+  \setlength{\textwidth}{5in}         % Text column width
+  \setlength{\marginparwidth}{5cm}    % Wide margin for notes (2x original)
+  \setlength{\marginparsep}{0.3cm}    % Gap between text and notes
+  
+  % Color-coded comment commands
+  % Green: General observations, "nice work", vibes
+  \newcommand{\splitnote}[1]{\todo[color=green!40]{#1}}
+  % Yellow: "Hey, check this out maybe?" - suggestions
+  \newcommand{\splitsuggest}[1]{\todo[color=yellow!60]{#1}}
+  % Orange: "This needs some polish" - should fix
+  \newcommand{\splitpolish}[1]{\todo[color=orange!50]{#1}}
+  % Red: "Fix this. Not acceptable." - must fix
+  \newcommand{\splitfix}[1]{\todo[color=red!40]{#1}}
+  % Inline versions
+  \newcommand{\splitinline}[1]{\todo[inline,color=green!40]{#1}}
+\else
+  % Final mode: no comments, normal margins
+  \newcommand{\splitnote}[1]{}
+  \newcommand{\splitsuggest}[1]{}
+  \newcommand{\splitpolish}[1]{}
+  \newcommand{\splitfix}[1]{}
+  \newcommand{\splitinline}[1]{}
+\fi
+% ================================
+
 \begin{document}
 
-\pagenumbering{roman}
+% \pagenumbering{roman}
 \maketitle
-\input{1-goals-and-outcomes/research_statement_v1.tex}
+% \input{1-goals-and-outcomes/research-statement.tex}
 \newpage
 \tableofcontents
 \newpage
 \pagenumbering{arabic}
 
-\input{1-goals-and-outcomes/v1}
+\input{1-goals-and-outcomes/goals.tex}
 \newpage
 
-\input{2-state-of-the-art/v2}
+\input{2-state-of-the-art/state-of-art}
 \newpage
 
-\input{3-research-approach/v3}
+\input{3-research-approach/approach}
 \newpage
 
-\input{4-metrics-of-success/v1}
+\input{4-metrics-of-success/metrics}
 \newpage
 
-\input{5-risks-and-contingencies/v1}
+\input{5-risks-and-contingencies/risks}
 \newpage
 
-\input{6-broader-impacts/v1}
+\input{6-broader-impacts/impacts}
 \newpage
 
-\input{8-schedule/v1}
+\input{8-schedule/schedule}
 \bibliographystyle{ieeetr}
 \bibliography{references}
 

main.toc

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

todonotes.sty

@@ -0,0 +1,586 @@
+%%
+%% This is file `todonotes.sty',
+%% generated with the docstrip utility.
+%%
+%% The original source files were:
+%%
+%% todonotes.dtx  (with options: `package')
+%% 
+%% This is a generated file.
+%% 
+%% Copyright (C) 2008 by Henrik Skov Midtiby <henrikmidtiby@gmail.com>
+%% 
+%% This file may be distributed and/or modified under the conditions of
+%% the LaTeX Project Public License, either version 1.2 of this license
+%% or (at your option) any later version.  The latest version of this
+%% license is in:
+%% 
+%%    http://www.latex-project.org/lppl.txt
+%% 
+%% and version 1.2 or later is part of all distributions of LaTeX version
+%% 1999/12/01 or later.
+%% 
+\NeedsTeXFormat{LaTeX2e}[1999/12/01]
+\ProvidesPackage{todonotes}
+    [2024/01/05 v1.1.7 Todonotes source and documentation.]
+
+\ProvidesPackage{todonotes}[2024/01/05]
+\RequirePackage{ifthen}
+\RequirePackage{xkeyval}
+\RequirePackage{xcolor}
+\RequirePackage{tikz}
+\usetikzlibrary{positioning}
+\RequirePackage{calc}
+\newcommand\setuptodonotes[1]{\presetkeys{todonotes}{#1}{}}
+\newcommand{\@todonotes@text}{}%
+\newcommand{\@todonotes@backgroundcolor}{orange}
+\newcommand{\@todonotes@textcolor}{black}
+\newcommand{\@todonotes@linecolor}{orange}
+\newcommand{\@todonotes@bordercolor}{black}
+\newcommand{\@todonotes@tickmarkheight}{unused value}
+\newcommand{\@todonotes@textwidth}{\marginparwidth}
+\newcommand{\@todonotes@textsize}{\normalsize}
+\newcommand{\@todonotes@figwidth}{\linewidth}
+\newcommand{\@todonotes@figheight}{4cm}
+\newcommand{\@todonotes@figcolor}{black!40}
+\AtBeginDocument{
+\ifx\undefined\phantomsection
+\newcommand{\phantomsection}{}
+\fi
+\ifdim \marginparwidth < 2cm
+\PackageWarning{todonotes}{The length marginparwidth is
+less than 2cm and will most likely cause issues with the
+appearance of inserted todonotes.
+The issue can be solved by adding a line like
+\setlength{\marginparwidth}{2cm}
+prior to loading the todonotes package.} \else\fi%
+}
+
+\newcommand{\@todonotes@todolistname}{Todo list}
+\newcommand{\@todonotes@MissingFigureText}{Figure}
+\newcommand{\@todonotes@MissingFigureUp}{Missing}
+\newcommand{\@todonotes@MissingFigureDown}{figure}
+\newcommand{\@todonotes@SetTodoListName}[1]
+    {\renewcommand{\@todonotes@todolistname}{#1}}
+\newcommand{\@todonotes@SetMissingFigureText}[1]
+    {\renewcommand{\@todonotes@MissingFigureText}{#1}}
+\newcommand{\@todonotes@SetMissingFigureUp}[1]
+    {\renewcommand{\@todonotes@MissingFigureUp}{#1}}
+\newcommand{\@todonotes@SetMissingFigureDown}[1]
+    {\renewcommand{\@todonotes@MissingFigureDown}{#1}}
+\newif{\if@todonotes@reverseMissingFigureTriangle}
+\DeclareOptionX{catalan}{
+    \@todonotes@SetTodoListName{Llista de feines pendents}%
+    \@todonotes@SetMissingFigureText{Figura}%
+    \@todonotes@SetMissingFigureUp{Figura}%
+    \@todonotes@SetMissingFigureDown{pendent}%
+}
+\DeclareOptionX{croatian}{%
+   \@todonotes@SetTodoListName{Popis obveza}%
+   \@todonotes@SetMissingFigureText{Slika}%
+   \@todonotes@SetMissingFigureUp{Nedostaje}%
+   \@todonotes@SetMissingFigureDown{slika}%
+}
+\DeclareOptionX{danish}{%
+    \@todonotes@SetTodoListName{G\o{}rem\aa{}lsliste}%
+    \@todonotes@SetMissingFigureText{Figur}%
+    \@todonotes@SetMissingFigureUp{Manglende}%
+    \@todonotes@SetMissingFigureDown{figur}%
+}
+\DeclareOptionX{dutch}{%
+   \@todonotes@SetTodoListName{Lijst van onafgewerkte taken}%
+   \@todonotes@SetMissingFigureText{Figuur}%
+   \@todonotes@SetMissingFigureUp{Ontbrekende}%
+   \@todonotes@SetMissingFigureDown{figuur}%
+}
+\DeclareOptionX{english}{%
+   \@todonotes@SetTodoListName{Todo list}%
+   \@todonotes@SetMissingFigureText{Figure}%
+   \@todonotes@SetMissingFigureUp{Missing}%
+   \@todonotes@SetMissingFigureDown{figure}%
+}
+\DeclareOptionX{french}{%
+    \@todonotes@SetTodoListName{Liste des points \`a traiter}%
+    \@todonotes@SetMissingFigureText{Figure}%
+    \@todonotes@SetMissingFigureUp{Figure}%
+    \@todonotes@SetMissingFigureDown{manquante}%
+    \@todonotes@reverseMissingFigureTrianglefalse
+}
+\DeclareOptionX{german}{%
+    \@todonotes@SetTodoListName{Liste der noch zu erledigenden Punkte}%
+    \@todonotes@SetMissingFigureText{Abbildung}%
+    \@todonotes@SetMissingFigureUp{Fehlende}%
+    \@todonotes@SetMissingFigureDown{Abbildung}%
+}
+\DeclareOptionX{italian}{
+    \@todonotes@SetTodoListName{Elenco delle cose da fare}%
+    \@todonotes@SetMissingFigureText{Figura}%
+    \@todonotes@SetMissingFigureUp{Figura}%
+    \@todonotes@SetMissingFigureDown{mancante}%
+}
+\DeclareOptionX{ngerman}{%
+    \@todonotes@SetTodoListName{Liste der noch zu erledigenden Punkte}%
+    \@todonotes@SetMissingFigureText{Abbildung}%
+    \@todonotes@SetMissingFigureUp{Fehlende}%
+    \@todonotes@SetMissingFigureDown{Abbildung}%
+}
+\DeclareOptionX{portuguese}{
+    \@todonotes@SetTodoListName{Lista de tarefas pendentes}%
+    \@todonotes@SetMissingFigureText{Figura}%
+    \@todonotes@SetMissingFigureUp{Figura}%
+    \@todonotes@SetMissingFigureDown{pendente}%
+}
+\DeclareOptionX{spanish}{
+    \@todonotes@SetTodoListName{Lista de tareas pendientes}%
+    \@todonotes@SetMissingFigureText{Figura}%
+    \@todonotes@SetMissingFigureUp{Figura}%
+    \@todonotes@SetMissingFigureDown{pendiente}%
+}
+\DeclareOptionX{swedish}{%
+    \@todonotes@SetTodoListName{Att g\"{o}ra-lista}%
+    \@todonotes@SetMissingFigureText{Figur}%
+    \@todonotes@SetMissingFigureUp{Figur}%
+    \@todonotes@SetMissingFigureDown{saknas}%
+}
+\providecommand{\@tocrmarg}{2.55em}
+\providecommand{\@dotsep}{4.5}
+\providecommand{\@pnumwidth}{1.55em}
+\newcounter{@todonotes@numberoftodonotes}
+\newif{\if@todonotes@obeyDraft}
+\DeclareOptionX{obeyDraft}{\@todonotes@obeyDrafttrue}
+\newif{\if@todonotes@isDraft}
+\DeclareOptionX{draft}{\@todonotes@isDrafttrue}
+\DeclareOptionX{draftcls}{\@todonotes@isDrafttrue}
+\DeclareOptionX{draftclsnofoot}{\@todonotes@isDrafttrue}
+\newif{\if@todonotes@obeyFinal}
+\DeclareOptionX{obeyFinal}{\@todonotes@obeyFinaltrue}
+\newif{\if@todonotes@isFinal}
+\DeclareOptionX{final}{\@todonotes@isFinaltrue}
+\newif{\if@todonotes@disabled}
+\DeclareOptionX{disable}{\@todonotes@disabledtrue}
+\newif{\if@todonotes@colorinlistoftodos}
+\DeclareOptionX{colorinlistoftodos}{\@todonotes@colorinlistoftodostrue}
+\newif{\if@todonotes@dviStyle}
+\DeclareOptionX{dvistyle}{\@todonotes@dviStyletrue}
+\define@key{todonotes.sty}%
+    {color}{
+        \renewcommand{\@todonotes@backgroundcolor}{#1}
+        \renewcommand{\@todonotes@linecolor}{#1}}
+\define@key{todonotes.sty}%
+    {backgroundcolor}{\renewcommand{\@todonotes@backgroundcolor}{#1}}
+\define@key{todonotes.sty}%
+    {textcolor}{\renewcommand{\@todonotes@textcolor}{#1}}
+\define@key{todonotes.sty}%
+    {linecolor}{\renewcommand{\@todonotes@linecolor}{#1}}
+\define@key{todonotes.sty}%
+    {bordercolor}{\renewcommand{\@todonotes@bordercolor}{#1}}
+\newcommand{\@todonotes@defaulttickmarkheight}{0cm}
+\define@key{todonotes.sty}{tickmarkheight}{%
+    \renewcommand{\@todonotes@defaulttickmarkheight}{#1}}%
+\newif{\if@todonotes@prependcaptionglobal}
+\@todonotes@prependcaptionglobalfalse
+\DeclareOptionX{prependcaption}{\@todonotes@prependcaptionglobaltrue}
+\define@key{todonotes.sty}%
+    {textwidth}{\renewcommand{\@todonotes@textwidth}{#1}}
+\newcommand{\todoformat}[1]{#1}
+\define@key{todonotes.sty}%
+    {format}{\renewcommand{\todoformat}{\@nameuse{#1}}}
+\define@key{todonotes.sty}%
+    {textsize}{\renewcommand{\@todonotes@textsize}{#1}}
+\define@key{todonotes.sty}%
+    {size}{\renewcommand{\@todonotes@textsize}{#1}}
+\newif\if@todonotes@shadowlibraryloaded
+\@todonotes@shadowlibraryloadedfalse
+\DeclareOptionX{loadshadowlibrary}{%
+    \usetikzlibrary{shadows}%
+    \@todonotes@shadowlibraryloadedtrue}
+\newcommand{\@todonotes@shadowenabledbydefault}{noshadow}
+\DeclareOptionX{shadow}{%
+    \renewcommand{\@todonotes@shadowenabledbydefault}{shadow}}
+\define@key{todonotes.sty}%
+    {figwidth}{\renewcommand{\@todonotes@figwidth}{#1}}
+\define@key{todonotes.sty}%
+    {figheight}{\renewcommand{\@todonotes@figheight}{#1}}
+\define@key{todonotes.sty}%
+    {figcolor}{\renewcommand{\@todonotes@figcolor}{#1}}
+\ProcessOptionsX*
+\if@todonotes@disabled
+\else
+\if@todonotes@obeyDraft
+\@todonotes@disabledtrue
+\if@todonotes@isDraft
+\@todonotes@disabledfalse
+\fi
+\fi
+\if@todonotes@obeyFinal
+\@todonotes@disabledfalse
+\if@todonotes@isFinal
+\@todonotes@disabledtrue
+\fi
+\fi
+\fi
+
+\gdef\@todonotes@currentlinecolor{\@todonotes@linecolor}%
+\gdef\@todonotes@currentbackgroundcolor{\@todonotes@backgroundcolor}%
+\gdef\@todonotes@currenttextcolor{\@todonotes@textcolor}%
+\gdef\@todonotes@currentbordercolor{\@todonotes@bordercolor}%
+\define@key{todonotes}{color}{%
+    \gdef\@todonotes@currentlinecolor{#1}%
+    \gdef\@todonotes@currentbackgroundcolor{#1}}%
+\define@key{todonotes}{linecolor}{%
+    \gdef\@todonotes@currentlinecolor{#1}}%
+\define@key{todonotes}{backgroundcolor}{%
+    \gdef\@todonotes@currentbackgroundcolor{#1}}%
+\define@key{todonotes}{textcolor}{%
+    \gdef\@todonotes@currenttextcolor{#1}}%
+\define@key{todonotes}{bordercolor}{%
+    \gdef\@todonotes@currentbordercolor{#1}}%
+\newif\if@todonotes@useshadow%
+\define@key{todonotes}{shadow}[]{\@todonotes@useshadowtrue}%
+\define@key{todonotes}{noshadow}[]{\@todonotes@useshadowfalse}%
+\define@key{todonotes}{tickmarkheight}{%
+    \renewcommand{\@todonotes@tickmarkheight}{#1}}%
+\newcommand{\@todonotes@format}{\todoformat}%
+\define@key{todonotes}{format}{%
+    \renewcommand{\@todonotes@format}{\@nameuse{#1}}}%
+\newcommand{\@todonotes@sizecommand}{}%
+\define@key{todonotes}{size}{\renewcommand{\@todonotes@sizecommand}{#1}%
+}%
+\newif\if@todonotes@localdisable%
+\define@key{todonotes}{disable}[]{\@todonotes@localdisabletrue}%
+\define@key{todonotes}{nodisable}[]{\@todonotes@localdisablefalse}%
+\newif\if@todonotes@appendtolistoftodos%
+\define@key{todonotes}{list}[]{\@todonotes@appendtolistoftodostrue}%
+\define@key{todonotes}{nolist}[]{\@todonotes@appendtolistoftodosfalse}%
+\newif\if@todonotes@inlinenote%
+\define@key{todonotes}{inline}[]{\@todonotes@inlinenotetrue}%
+\define@key{todonotes}{noinline}[]{\@todonotes@inlinenotefalse}%
+\newif\if@todonotes@prependcaption%
+\define@key{todonotes}{prepend}[]{\@todonotes@prependcaptiontrue}%
+\define@key{todonotes}{noprepend}[]{\@todonotes@prependcaptionfalse}%
+\newif\if@todonotes@line%
+\define@key{todonotes}{line}[]{\@todonotes@linetrue}%
+\define@key{todonotes}{noline}[]{\@todonotes@linefalse}%
+\newif\if@todonotes@fancyline\@todonotes@fancylinefalse%
+\define@key{todonotes}{fancyline}[]{\@todonotes@fancylinetrue}%
+\define@key{todonotes}{nofancyline}[]{\@todonotes@fancylinefalse}%
+\newcommand{\@todonotes@author}{}%
+\newif\if@todonotes@authorgiven%
+\define@key{todonotes}{author}{%
+    \renewcommand{\@todonotes@author}{#1}%
+    \@todonotes@authorgiventrue}%
+\define@key{todonotes}{noauthor}[]{\@todonotes@authorgivenfalse}%
+\newcommand{\@todonotes@caption}{}%
+\newif\if@todonotes@captiongiven%
+\define@key{todonotes}{caption}%
+    {\renewcommand{\@todonotes@caption}{#1}%
+    \@todonotes@captiongiventrue}%
+\define@key{todonotes}{nocaption}[]{\@todonotes@captiongivenfalse}%
+\newcommand{\@todonotes@currentfigwidth}{\@todonotes@figwidth}
+\define@key{todonotes}%
+    {figwidth}{\renewcommand{\@todonotes@currentfigwidth}{#1-2pt}}
+\newcommand{\@todonotes@currentfigheight}{\@todonotes@figheight}
+\define@key{todonotes}%
+    {figheight}{\renewcommand{\@todonotes@currentfigheight}{#1-2pt}}
+\newcommand{\@todonotes@currentfigcolor}{\@todonotes@figcolor}
+\define@key{todonotes}%
+    {figcolor}{\renewcommand{\@todonotes@currentfigcolor}{#1}}
+\newcommand{\@todonotes@inlinewidth}{\linewidth}%
+\define@key{todonotes}%
+    {inlinewidth}{\renewcommand{\@todonotes@inlinewidth}{#1}}
+\newif\if@todonotes@inlinepar
+\@todonotes@inlinepartrue
+\define@key{todonotes}{inlinepar}[]{\@todonotes@inlinepartrue}%
+\define@key{todonotes}{noinlinepar}[]{\@todonotes@inlineparfalse}%
+\presetkeys%
+    {todonotes}%
+    {linecolor=\@todonotes@linecolor,%
+    backgroundcolor=\@todonotes@backgroundcolor,%
+    textcolor=\@todonotes@textcolor,%
+    bordercolor=\@todonotes@bordercolor,%
+    format=todoformat,%
+    tickmarkheight=\@todonotes@defaulttickmarkheight,%
+    nofancyline,%
+    nodisable,%
+    noinline,%
+    nocaption,%
+    noauthor,%
+    \@todonotes@shadowenabledbydefault,%
+    figwidth=\@todonotes@figwidth,%
+    figheight=\@todonotes@figheight,%
+    figcolor=\@todonotes@figcolor,%
+    line, list,%
+    inlinewidth=\linewidth,
+    inlinepar}{}%
+\@temptokena\expandafter{\@todonotes@textsize}
+\edef\next{\noexpand\presetkeys{todonotes}{size=\the\@temptokena}{}}
+\next
+\if@todonotes@disabled%
+    \newcommand{\listoftodos}[1][]{}
+    \newcommand{\@todo}[2][]{}
+    \newcommand{\missingfigure}[2][]{}
+\else % \if@todonotes@disabled
+\newcommand{\listoftodos}[1][\@todonotes@todolistname]
+    {\@ifundefined{chapter}{\section*{#1}}{\chapter*{#1}} \@starttoc{tdo}}
+\newcommand{\l@todo}
+    {\@dottedtocline{1}{0em}{2.3em}}
+\tikzstyle{notestyleraw} = [
+    draw=\@todonotes@currentbordercolor,
+    fill=\@todonotes@currentbackgroundcolor,
+    text=\@todonotes@currenttextcolor,
+    line width=0.5pt,
+    text width = \@todonotes@textwidth - 1.6 ex - 1pt,
+    inner sep = 0.8 ex,
+    rounded corners=4pt]
+\newcommand{\@todo}[2][]{%
+\if@todonotes@prependcaptionglobal%
+\@todonotes@prependcaptiontrue%
+\else%
+\@todonotes@prependcaptionfalse%
+\fi%
+\renewcommand{\@todonotes@text}{#2}%
+\renewcommand{\@todonotes@caption}{#2}%
+\setkeys{todonotes}{#1}%
+\if@todonotes@useshadow%
+\if@todonotes@shadowlibraryloaded%
+\tikzstyle{notestyle} = [notestyleraw,%
+    general shadow={shadow xshift=0.5ex, shadow yshift=-0.5ex,%
+        opacity=1,fill=black!50}]%
+\else%
+\PackageWarning{todonotes}{Trying to put a shadow below a todonote,%
+but the loadshadowlibrary option was not given when loading%
+the todonotes package}%
+\tikzstyle{notestyle} = [notestyleraw]%
+\fi%
+\else%
+\tikzstyle{notestyle} = [notestyleraw]%
+\fi%
+\tikzstyle{notestyleleft} = [%
+    notestyle,%
+    left]%
+\tikzstyle{connectstyle} = [%
+    thick,%
+    draw=\@todonotes@currentlinecolor]%
+\tikzstyle{inlinenotestyle} = [%
+    notestyle,%
+    text width=\@todonotes@inlinewidth - 1.6 ex - 1 pt]%
+\if@todonotes@localdisable%
+\else%
+\addtocounter{@todonotes@numberoftodonotes}{1}%
+\if@todonotes@appendtolistoftodos%
+    \phantomsection%
+    \if@todonotes@captiongiven%
+    \else%
+        \renewcommand{\@todonotes@caption}{#2}%
+    \fi%
+    \@todonotes@addElementToListOfTodos%
+\fi%
+\if@todonotes@captiongiven%
+    \if@todonotes@prependcaption%
+        \renewcommand{\@todonotes@text}{\@todonotes@caption: #2}%
+    \fi%
+\fi%
+\if@todonotes@inlinenote%
+    \@todonotes@drawInlineNote%
+\else%
+    \@todonotes@drawMarginNoteWithLine%
+\fi%\if@todonotes@inlinenote
+\fi%\if@todonotes@localdisable
+}%
+\newcommand{\@todonotes@drawMarginNoteWithLine}{%
+\ifvmode
+  \vspace*{-\parskip}%   % backup if we are already in vertical mode
+  \vskip-\baselineskip   % (and don't loose that space after a
+                         %  pagebreak ...
+  \noindent
+\fi
+\begin{tikzpicture}[remember picture, overlay, baseline=-0.75ex]%
+    \node [coordinate] (inText) {};%
+\end{tikzpicture}%
+\marginpar[{% Draw note in left margin
+    \@todonotes@drawMarginNote%
+    \@todonotes@drawLineToLeftMargin%
+}]{% Draw note in right margin
+    \@todonotes@drawMarginNote%
+    \@todonotes@drawLineToRightMargin%
+}%
+}%
+\newcommand{\@todonotes@addElementToListOfTodos}{%
+    \if@todonotes@colorinlistoftodos%
+        \addcontentsline{tdo}{todo}{%
+            \fcolorbox{\@todonotes@currentbordercolor}%
+                {\@todonotes@currentbackgroundcolor}%
+                {\textcolor{\@todonotes@currentbackgroundcolor}{o}}%
+            \ \@todonotes@caption}%
+    \else%
+        \addcontentsline{tdo}{todo}{\@todonotes@caption}%
+    \fi}%
+\newcommand{\@todonotes@useSizeCommand}{%
+\ifcsname \expandafter\string\@todonotes@sizecommand\endcsname
+\csname \expandafter\string\@todonotes@sizecommand\endcsname%
+\else
+\@todonotes@sizecommand
+\fi%
+}%
+\newcommand{\@todonotes@drawInlineNote}{%
+    \if@todonotes@dviStyle%
+        {\if@todonotes@inlinepar\par\noindent\fi%
+         \begin{tikzpicture}[remember picture]%
+            \draw node[inlinenotestyle] {};
+         \end{tikzpicture}%
+         \if@todonotes@inlinepar\par\fi}%
+            \if@todonotes@authorgiven%
+                {\noindent \@todonotes@useSizeCommand \@todonotes@author:\,\@todonotes@format{\@todonotes@text}}%
+            \else%
+                {\noindent \@todonotes@useSizeCommand%
+                    \@todonotes@format{\@todonotes@text}}%
+            \fi
+        {\if@todonotes@inlinepar\par\noindent\fi%
+         \begin{tikzpicture}[remember picture]%
+            \draw node[inlinenotestyle] {};
+         \end{tikzpicture}%
+         \if@todonotes@inlinepar\par\fi}%
+    \else%
+        {\if@todonotes@inlinepar\par\noindent\fi%
+         \begin{tikzpicture}[remember picture]%
+            \draw node[inlinenotestyle,font=\@todonotes@useSizeCommand]{%
+                \if@todonotes@authorgiven%
+                    {\noindent \@todonotes@author:\,%
+                        \@todonotes@format{\@todonotes@text}}%
+                \else%
+                    {\noindent \@todonotes@format{\@todonotes@text}}%
+                \fi};%
+         \end{tikzpicture}%
+         \if@todonotes@inlinepar\par\fi}%
+    \fi}%
+\newcommand{\@todonotes@drawMarginNote}{%
+\if@todonotes@dviStyle%
+    \begin{tikzpicture}[remember picture]%
+        \draw node[notestyle] {};%
+    \end{tikzpicture}\\%
+    \begin{minipage}{\@todonotes@textwidth}%
+    \if@todonotes@authorgiven%
+      \@todonotes@useSizeCommand \@todonotes@author:\,
+         \@todonotes@format{\@todonotes@text}%
+    \else%
+      \@todonotes@useSizeCommand\@todonotes@format{\@todonotes@text}%
+    \fi%
+    \end{minipage}\\%
+    \begin{tikzpicture}[remember picture]%
+        \draw node[notestyle] (inNote) {};%
+    \end{tikzpicture}%
+\else%
+    \let\originalHbadness\hbadness%
+    \hbadness 100000%
+    \begin{tikzpicture}[remember picture,baseline=(X.base)]%
+        \node(X){\vphantom{\@todonotes@useSizeCommand X}};%
+        \if@todonotes@authorgiven%
+            \draw node[notestyle,font=\@todonotes@useSizeCommand,anchor=north] (inNote) at (X.north)%
+                {\@todonotes@author};%
+            \node(Y)[below=of X]{};%
+            \draw node[notestyle,font=\@todonotes@useSizeCommand,anchor=north] (inNote) at (X.south)%
+                {\@todonotes@format{\@todonotes@text}};%
+        \else%
+            \draw node[notestyle,font=\@todonotes@useSizeCommand,anchor=north] (inNote) at (X.north)%
+                {\@todonotes@format{\@todonotes@text}};%
+        \fi%
+    \end{tikzpicture}%
+    \hbadness \originalHbadness%
+\fi}%
+\newcommand{\@todonotes@drawLineToRightMargin}{%
+\if@todonotes@line%
+\if@todonotes@fancyline%
+\tikz[remember picture,overlay]{%
+\tikzstyle{both}=[line width=3pt, draw, opacity=0.15]%
+\tikzstyle{line}=[shorten >=5pt, line cap=round]%
+\tikzstyle{head}=[shorten >=-1pt, dash pattern=on 0pt off 1pt, ->]%
+\foreach \s in {line,head}{%
+\draw[both,\s]%
+(inNote.north west).. controls +(0:0) and +(90:1.5)..([yshift=1ex] inText);%
+}%
+}%
+\else%
+\begin{tikzpicture}[remember picture, overlay]%
+\draw[connectstyle]%
+([yshift=-0.2cm + \@todonotes@tickmarkheight] inText)%
+-| ([yshift=-0.2cm] inText)%
+-| ([xshift=-0.2cm] inNote.west)%
+-| (inNote.west);%
+\end{tikzpicture}%
+\fi%
+\fi}%
+\newcommand{\@todonotes@drawLineToLeftMargin}{%
+\if@todonotes@line%
+\if@todonotes@fancyline%
+\tikz[remember picture,overlay]{%
+\tikzstyle{both}=[line width=3pt, draw, opacity=0.15]%
+\tikzstyle{line}=[shorten >=5pt, line cap=round]%
+\tikzstyle{head}=[shorten >=-1pt, dash pattern=on 0pt off 1pt,->]%
+\foreach \s in {line,head}{%
+\draw[both,\s]%
+(inNote.north east).. controls +(0:0) and +(90:1.5)..([yshift=1ex] inText);%
+}%
+}%
+\else%
+\begin{tikzpicture}[remember picture, overlay]%
+\draw[connectstyle]%
+([yshift=-0.2cm + \@todonotes@tickmarkheight] inText)%
+-| ([yshift=-0.2cm] inText)%
+-| ([xshift=0.2cm] inNote.east)%
+-| (inNote.east);%
+\end{tikzpicture}%
+\fi%
+\fi}%
+\newcommand{\missingfigure}[2][]{%
+\setkeys{todonotes}{#1}%
+\addcontentsline{tdo}{todo}{\@todonotes@MissingFigureText: #2}%
+\par
+\noindent
+\hfill
+\begin{tikzpicture}
+\draw[fill=\@todonotes@currentfigcolor, draw = black!40, line width=2pt]
+    (-2, -0.5*\@todonotes@currentfigheight-0.5cm)
+    rectangle +(\@todonotes@currentfigwidth, \@todonotes@currentfigheight);
+\draw (2, -0.5) node[right, text
+    width=\@todonotes@currentfigwidth-4.5cm, font=\@todonotes@useSizeCommand] {#2};
+\draw[red, fill=white, rounded corners = 5pt, line width=10pt]
+    (30:2cm) -- (150:2cm) -- (270:2cm) -- cycle;
+\draw (0, 0.3) node {\@todonotes@MissingFigureUp};
+\draw (0, -0.3) node {\@todonotes@MissingFigureDown};
+\end{tikzpicture}\hfill
+\null\par
+}% Ending \missingfigure command
+\fi% Ending \@todonotes@ifdisabled
+\newcommand{\todototoc}
+{%
+    \if@todonotes@disabled
+    \else
+\addcontentsline{toc}{\@ifundefined{chapter}{section}{chapter}}{\@todonotes@todolistname}%
+    \fi
+}
+\newcommand{\todo}[2][]{%
+  % Needed to output any dangling \item of a noskip section (see #36):
+  \if@inlabel \leavevmode \fi
+  \if@noskipsec \leavevmode \fi
+  \if@todonotes@inlinepar
+    \ifhmode
+      \@bsphack
+      \@todonotes@vmodefalse
+    \else
+      \@savsf\@m
+      \@savsk\z@
+      \@todonotes@vmodetrue
+    \fi
+    {\@todo[#1]{#2}}%
+    \@esphack%
+    \if@todonotes@vmode \par \fi
+  \else%
+    \@todo[#1]{#2}%
+  \fi}
+\newif\if@todonotes@vmode
+\newcommand*{\todostyle}[2]{%
+    \define@key{todonotes}{#1}[]{%
+        \setkeys{todonotes}{#2}}}
+\endinput
+%%
+%% End of file `todonotes.sty'.