Compare commits

..

No commits in common. "fcd720101af8691b0bd9a200aefc1cc64f823be4" and "cbc24672193492b4603a2235abf910f39455e422" have entirely different histories.

25 changed files with 2983 additions and 2120 deletions

BIN
.DS_Store vendored Normal file

Binary file not shown.

12
.gitignore vendored
View File

@ -36,15 +36,3 @@ Thumbs.db
*.swo
.vscode/
.idea/
*.sty
.DS_Store
*.aux
*.bbl
*.blg
*.fdb_latexmk
*.fls
*.log
*.pdf
*.toc
*.out
*.synctex.gz

View File

@ -1,3 +0,0 @@
$pdflatex = 'pdflatex -interaction=nonstopmode %O %S';
$bibtex_use = 2;
$pdf_mode = 1;

View File

@ -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 and creates a
fundamental economic barrier for next-generation reactor designs. Small modular
reactors face per-megawatt staffing costs far exceeding those of conventional
plants, threatening their economic viability.
This reliance on human operators not only prevents autonomous control
capabilities but creates a fundamental economic challenge for next-generation
reactor designs. Small modular reactors, in particular, face per-megawatt
staffing costs far exceeding those of conventional plants and threaten their
economic viability.
% Critical Need
What is needed is a method to create autonomous control systems that safely
manage complex operational sequences with the same assurance as human-operated
systems, but without constant human supervision.
Autonomous control systems must safely manage complex operational sequences with
the same assurance as human-operated systems, but without constant human
supervision.
% APPROACH PARAGRAPH Solution
To address this need, we will combine formal methods with control theory to
build hybrid control systems that are correct by construction.
@ -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
@ -44,10 +49,7 @@ verified against transition requirements, then autonomous controllers can be
built that are provably free from design defects.
% Pay-off
This approach will enable autonomous control in nuclear power plants while
maintaining the high safety standards required by the industry. The University
of Pittsburgh Cyber Energy Center's partnership with Emerson provides access to
industry-standard control hardware, ensuring that developed solutions align with
practical implementation requirements from the outset.
maintaining the high safety standards required by the industry.
% OUTCOMES PARAGRAPHS
If this research is successful, we will be able to do the following:
@ -64,20 +66,19 @@ If this research is successful, we will be able to do the following:
logic.
% Outcome
Control system engineers will generate verified mode-switching controllers
directly from regulatory procedures, lowering the barrier to high-assurance
control systems.
directly from regulatory procedures without formal methods expertise,
lowering the barrier to high-assurance control systems.
% OUTCOME 2 Title
\item \textbf{Verify continuous control behavior across mode transitions.}
% Strategy
We will establish methods for analyzing continuous control modes to ensure
they satisfy discrete transition requirements. Using classical control
theory for linear systems and reachability analysis for nonlinear
dynamics, we will verify that each continuous mode safely reaches its
intended transitions.
% Outcome
Engineers will design continuous controllers using standard practices
while iterating to ensure broader system correctness, proving that mode
theory for linear systems and reachability analysis for nonlinear dynamics,
we will verify that each continuous mode safely reaches its intended
transitions.
Engineers will design continuous controllers using standard practices while
iterating to ensure broader system correctness, proving that mode
transitions occur safely and at the correct times.
% OUTCOME 3 Title
@ -92,18 +93,23 @@ If this research is successful, we will be able to do the following:
operation.
% Outcome
We will demonstrate that autonomous hybrid control can be realized in the
nuclear industry with current equipment, establishing a path toward
reduced operator staffing while maintaining safety.
nuclear industry with current equipment, establishing a path toward reduced
operator staffing while maintaining safety.
\end{enumerate}
% IMPACT PARAGRAPH Innovation
The innovation in this work is unifying discrete synthesis with continuous
verification to enable end-to-end correctness guarantees for hybrid systems.
verification to enable end-to-end correctness guarantees for hybrid
systems.
% Outcome Impact
If successful, control engineers will create autonomous controllers from
existing procedures with mathematical proof of correct behavior. High-assurance
autonomous control will become practical for safety-critical applications.
% Impact/Pay-off
This research will provide the tools to achieve that autonomy while maintaining
the exceptional safety record the nuclear industry requires.
This capability is essential for the economic viability of next-generation
nuclear power. Small modular reactors offer a promising solution to growing
energy demands, but their success depends on reducing per-megawatt operating
costs through increased autonomy. This research will provide the tools to
achieve that autonomy while maintaining the exceptional safety record the
nuclear industry requires.

View File

@ -1,57 +1,64 @@
\dasnote{Research statement is very similar to GO because that's what I had
when I prepared it. If it's going to be an executive summary, it should talk
more about the other sections rather than just being a slightly different GO
section.}
% GOAL PARAGRAPH
The goal of this research is to develop a methodology for creating autonomous
hybrid control systems with mathematical guarantees of safe and correct
behavior.
control systems with event-driven control laws that have guarantees of safe and
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
their interpretation of plant conditions, they make critical decisions about
when to switch between control objectives.
operators' interpretation of plant conditions, operators make critical decisions
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
This reliance on human operators has created an economic challenge for
next-generation nuclear power plants. Small modular reactors face significantly
higher per-megawatt staffing costs than conventional plants. Autonomous control
systems are needed that can safely manage complex operational sequences with the
same assurance as human-operated systems, but without constant supervision.
But, reliance on human operators has created an economic challenge for
next-generation nuclear power plants.\splitpolish{``But, reliance'' — the comma
after ``But'' is unusual. Either drop it or restructure: ``However, this
reliance...'' or ``This reliance, however, has created...''} Small modular
reactors face significantly higher per-megawatt staffing costs than conventional
plants. Autonomous control systems are needed that can safely manage complex
operational sequences with the same assurance as human-operated systems, but
without constant supervision.\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, leveraging the extensive domain knowledge already embedded in
existing operating procedures and safety analyses.
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.\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.
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.\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
NASA's Formal Requirements Elicitation Tool (FRET). FRET structures requirements
into scope, condition, component, timing, and response elements. This approach
enables realizability checking that identifies conflicts and ambiguities in
procedures before implementation. Second, we will synthesize discrete mode
switching logic using reactive synthesis to produce deterministic automata that
are correct by construction. Third, we will develop continuous controllers for
each discrete mode using standard control theory and reachability analysis. We
will classify continuous modes based on their transition objectives and verify
safe mode transitions using barrier certificates and reachability analysis.
This compositional approach enables local verification of continuous modes
without requiring global trajectory analysis across the entire hybrid system.
We will validate this methodology through hardware-in-the-loop testing
on an Emerson Ovation distributed control system, made possible through the
University of Pittsburgh Cyber Energy Center's industry partnership.
NASA's Formal Requirements Elicitation Tool (FRET), which structures
requirements into scope, condition, component, timing, and response elements.
This structured approach enables realizability checking to identify conflicts
and ambiguities in procedures before implementation. Second, we will synthesize
discrete mode switching logic using reactive synthesis
to generate deterministic automata that are provably
correct by construction. Third, we will develop continuous
controllers for each discrete mode using standard control theory and
reachability analysis. We will classify continuous modes based on their
transition objectives, and then employ assume-guarantee contracts and barrier
certificates to prove that mode transitions occur safely and as defined by the
deterministic automata. This compositional approach enables local verification
of continuous modes without requiring global trajectory analysis across the
entire hybrid system. We will demonstrate this on an Emerson Ovation control
system.\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 enables autonomous management of complex nuclear power operations
while maintaining safety guarantees.
This approach will demonstrate autonomous control can be used for complex
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:
@ -63,8 +70,10 @@ If this research is successful, we will be able to do the following:
into formal specifications. These specifications will be synthesized into
discrete control logic using reactive synthesis tools.
% Outcome
Control engineers will be able to generate mode-switching
controllers from regulatory procedures, reducing barriers to high-assurance control systems.
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.\splitnote{Good practical framing — emphasizes accessibility.}
% OUTCOME 2 Title
\item \textit{Verify continuous control behavior across mode transitions. }
@ -81,10 +90,11 @@ If this research is successful, we will be able to do the following:
guarantees. }
% Strategy
We will implement this methodology on a small modular reactor simulation
using industry-standard control hardware.
% Outcome
Without retraining costs or new equipment, control engineers
will be able to implement high-assurance autonomous controls on industrial
hardware they already use.
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.\splitnote{Strong industrial grounding — the ``platforms they
already use'' point is compelling for adoption.}
\end{enumerate}

View File

@ -1,130 +1,149 @@
\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. Understanding what is being automated requires
understanding how nuclear reactors are operated today. This section examines
reactor operating procedures, investigates limitations of human-based operation,
and reviews current formal methods approaches to reactor control systems.
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 operations are governed by a hierarchy of written procedures,
ranging from normal operating procedures for routine operations to Emergency
Operating Procedures (EOPs) for design-basis accidents and Severe Accident
Management Guidelines (SAMGs) for beyond-design-basis events. These procedures
exist because reactor operation requires deterministic responses to a wide range
of plant conditions, from routine power changes to catastrophic failures. These
procedures must comply with 10 CFR 50.34(b)(6)(ii) and are developed using
guidance from NUREG-0899~\cite{NUREG-0899, 10CFR50.34}. 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 exhaustive verification of key safety
properties.
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-0899~\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}.
\textbf{LIMITATION:} \textit{Procedures lack exhaustive verification of
correctness and completeness.} 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
\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.
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.
This division between automated and human-controlled
functions is itself the hybrid control problem. Automated systems handle
reactor protection: trips on safety parameters, emergency core cooling
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 retain control of everything else: power level changes,
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~\cite{10CFR55}, including departing from normal regulations during
emergencies. This authority itself introduces risk. 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
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.
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{noauthor_human_nodate}. More significantly, the
root cause of all severe accidents at nuclear power plants---Three Mile Island,
Chernobyl, and Fukushima Daiichi---has been identified as 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
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.
\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{Formal Methods}
\subsubsection{HARDENS}
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. A U.S. Nuclear Regulatory
Commission report demonstrated that model-based systems engineering and formal
methods could design, verify, and implement a complex protection system meeting
regulatory criteria. The project delivered a Reactor Trip System (RTS)
implementation with traceability from regulatory requirements to verified
software through formal architecture specifications.
reactor control systems to date~\cite{Kiniry2024}.
HARDENS employed formal methods tools at every level of system development, from
high-level requirements through executable models to generated code. 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
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.
between specification and implementation where errors commonly
arise.
Despite these accomplishments, HARDENS addressed only discrete digital
control logic. The Reactor Trip System verification covered discrete state
transitions, digital sensor processing, and discrete actuation outputs. It
did not model or verify continuous reactor dynamics. 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 a
closed-loop hybrid system behavior.
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.
\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
@ -134,83 +153,59 @@ 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
%DAS 3/16/26. I double checked this quote. It's on page 4 of the HARDENS report
actual nuclear facilities, testing with real reactor systems under operational
conditions, side-by-side validation with operational analog RTS systems,
systematic failure mode testing, NRC licensing review, or human factors
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, human-system interaction in
realistic operational contexts, and regulatory acceptance of formal methods as
primary assurance evidence remain as significant challenges.
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.
\subsubsection{Temporal Logic and Formal Specification}
Formal verification of any system requires a precise language for stating
what the system must do. Temporal logic provides this language by extending
classical propositional logic with operators that express properties over
time~\cite{baier_principles_2008}. Where propositional logic can state that
a condition is true or false, temporal logic can state that a condition must
always hold, must eventually hold, or must hold until some other condition is
met. Linear temporal logic (LTL) formalizes these notions through four key
operators:
\begin{itemize}
\item $\mathbf{X}\phi$ (next): $\phi$ holds in the next state
\item $\mathbf{G}\phi$ (globally): $\phi$ holds in all future states
\item $\mathbf{F}\phi$ (finally): $\phi$ holds in some future state
\item $\phi \mathbf{U} \psi$ (until): $\phi$ holds until $\psi$ becomes
true
\end{itemize}
These operators allow specification of safety properties ($\mathbf{G}\neg
\textit{Unsafe}$), liveness properties ($\mathbf{F}\textit{ Target}$), and
response properties ($\mathbf{G}(\textit{Trigger} \rightarrow
\mathbf{F}\textit{ Response})$). For nuclear control, this expressiveness
captures exactly the kinds of requirements that matter: the reactor must
never enter an unsafe configuration, the system must eventually reach
operating temperature, and if coolant pressure drops, shutdown must initiate
within bounded time. These properties can be derived directly from operating
procedures and regulatory requirements, creating a formal link between
existing documentation and verifiable system behavior.
\subsubsection{Differential Dynamic Logic}
A separate line of work extends temporal logics to verify hybrid systems
directly. The result has been the field of differential dynamic logic
(dL)~\cite{platzer_differential_2008}. 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 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.
\subsubsection{Sequent Calculus and Differential Dynamic Logic}
There has been additional work to do verification of hybrid systems by extending
the temporal logics directly. The result has been the field of differential
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
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\cite{platzer2018}.
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~\cite{fulton_keymaera_2015} exist to help
develop proofs of systems
proof assistants such as KeYmaera X exist to help develop proofs of systems
using dL, but so far have been insufficient for reasonably complex hybrid
systems. The main issue behind creating system proofs using dL is
non-terminating solutions. Approaches have been made to alleviate these issues
for nuclear power contexts using contract and decomposition based methods, but
do not yet constitute a complete design methodology \cite{kapuria_using_2025}.
systems. The main issue behind creating system proofs using dL is state space
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 do not yet constitute a complete design
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.
%Maybe a limitation here? Something about dL doesn't scale or help in design
%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.
%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 dL-based approaches verify systems that
have already been designed, requiring expert knowledge to construct proofs.
They have not been applied to the synthesis of new controllers from
operational requirements.
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.

Binary file not shown.

View File

@ -1,77 +1,87 @@
\section{Research Approach}
% ============================================================================
% STRUCTURE (maps to Thesis.RA tasks):
% 1. Introduction + Hybrid Systems Definition (Task 34)
% 2. System Requirements and Specifications (Task 35)
% 3. Discrete Controller Synthesis (Task 36)
% 4. Continuous Controllers Overview (Task 37)
% 4.1 Transitory Modes (Task 38)
% 4.2 Stabilizing Modes (Task 39)
% 4.3 Expulsory Modes (Task 40)
% 5. Industrial Implementation (Task 41)
% ============================================================================
% ----------------------------------------------------------------------------
% 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION
% ----------------------------------------------------------------------------
Previous approaches to autonomous control have verified
discrete switching logic or continuous control behavior, but not both
simultaneously. Validation of continuous controllers today consists of
extensive simulation trials. Discrete switching logic for routine operation
has been driven by human operators, whose evaluation includes simulated
control room testing and human factors research. Neither method, despite
being extremely resource intensive, provides rigorous guarantees of control
system behavior. HAHACS bridges this gap by composing formal methods from
computer science with control-theoretic verification, formalizing reactor
operations using the framework of hybrid automata.
The challenge of hybrid system verification lies in the interaction between
discrete and continuous dynamics. Discrete transitions change the governing
vector field, creating discontinuities in the system's behavior. Traditional
verification techniques designed for purely discrete or purely continuous
systems cannot handle this interaction directly. Our methodology addresses this
challenge through decomposition. We verify discrete switching logic and
continuous mode behavior separately, then compose these guarantees to reason
about the complete hybrid system. This two-layer approach mirrors the structure
of reactor operations themselves: discrete supervisory logic determines which
control mode is active, while continuous controllers govern plant behavior
within each mode.
To build a high-assurance hybrid autonomous control system (HAHACS), we must
first establish a mathematical description of the system. This work draws on
automata theory, temporal logic, and control theory. A hybrid system is a
dynamical system that has both continuous and discrete states. The specific
type of system discussed in this proposal is a continuous autonomous hybrid
system. 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{lunze_handbook_2009}, but is
redefined here for convenience:
%
dynamical system that has both continuous and discrete states. The specific type
of system discussed in this proposal is a continuous autonomous hybrid system.
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{lunze2009}, but is redefined here
for convenience:
\begin{equation}
H = (\mathcal{Q}, \mathcal{X}, \mathbf{f}, Init, \mathcal{G}, \delta,
\mathcal{R}, Inv)
H = (\mathcal{Q}, \mathcal{X}, \mathbf{f}, Init, \mathcal{G}, \delta, \mathcal{R}, Inv)
\end{equation}
%
where:
%
\begin{itemize}
\item $\mathcal{Q}$: the set of discrete states (modes) of the system
\item $\mathcal{X} \subseteq \mathbb{R}^n$: the continuous state space
\item $\mathbf{f}: \mathcal{Q} \times \mathcal{X} \rightarrow
\mathbb{R}^n$: vector fields defining the continuous dynamics for each
discrete mode $q_i$
\item $Init \subseteq \mathcal{Q} \times \mathcal{X}$: the set of initial
states
\item $\mathbf{f}: \mathcal{Q} \times \mathcal{X} \rightarrow \mathbb{R}^n$:
vector fields defining the continuous dynamics for each discrete mode $q_i$
\item $Init \subseteq \mathcal{Q} \times \mathcal{X}$: the set of initial states
\item $\mathcal{G}$: guard conditions that define when discrete state
transitions may occur
\item $\delta: \mathcal{Q} \times \mathcal{G} \rightarrow \mathcal{Q}$:
the discrete state transition function
\item $\delta: \mathcal{Q} \times \mathcal{G} \rightarrow \mathcal{Q}$: the
discrete state transition function
\item $\mathcal{R}$: reset maps that define any instantaneous changes to
continuous state upon discrete transitions
\item $Inv$: safety invariants on the continuous dynamics
\end{itemize}
HAHACS bridges the gap between discrete and continuous verification by composing
formal methods from computer science with control-theoretic verification,
formalizing reactor operations using the framework of hybrid
automata~\cite{alur_hybrid_1993}. The challenge of hybrid system verification
lies in the interaction between discrete and continuous dynamics. Discrete
transitions change the active continuous vector field, creating discontinuities
in the system's behavior. Traditional verification techniques designed for
purely discrete or purely continuous systems cannot handle this interaction
directly. Our methodology addresses this challenge through decomposition. We
verify discrete switching logic and continuous mode behavior separately, then
compose these guarantees to reason about the complete hybrid system. This
compositional strategy follows the assume-guarantee paradigm for hybrid systems,
where guarantees about individual modes compose into guarantees about the
overall system~\cite{lunze_handbook_2009, alur_hybrid_1993}. This two-layer
approach mirrors the structure of reactor operations themselves: discrete
supervisory logic determines which control mode is active, while continuous
controllers govern plant behavior within each mode.
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.
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. In concrete terms, this means producing a
discrete automaton whose transitions are provably correct, continuous
controllers whose behavior is verified against transition requirements, and
formal evidence linking the two. 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 entry, exit, and safety conditions at the
discrete level first, we transform the intractable problem of global hybrid
verification into a collection of local verification problems with clear
interfaces. Verification is performed per mode rather than on the full
hybrid system, keeping the analysis tractable even for complex reactor
operations. Figure~\ref{fig:hybrid_automaton} illustrates this
structure for a simplified reactor startup sequence, showing discrete modes
connected by guard-triggered transitions with continuous dynamics governing
behavior within each mode.
By defining entry, exit, and safety conditions at the discrete level first, we
transform the intractable problem of global hybrid verification into a
collection of local verification problems with clear interfaces. Verification is
performed per mode rather than on the full hybrid system, keeping the analysis
tractable even for complex reactor operations.
\begin{figure}
\centering
@ -97,58 +107,58 @@ behavior within each mode.
\node[state, fill=red!15] (q3) at (5,-3.5) {$q_3$\\SCRAM};
% Normal transitions
\draw[trans] (q0) -- node[guard, above]
{$T_{avg} > T_{min}$} (q1);
\draw[trans] (q1) -- node[guard, above]
{$T_{avg} \in [T_{op} \pm \delta]$\\$P > P_{crit}$} (q2);
\draw[trans] (q0) -- node[guard, above] {$T_{avg} > T_{min}$} (q1);
\draw[trans] (q1) -- node[guard, above] {$T_{avg} \in [T_{op} \pm \delta]$\\$P > P_{crit}$} (q2);
% Fault transitions
\draw[trans, red!70!black] (q1) -- node[guard, left,
text=red!70!black] {$\neg Inv_1$} (q3);
\draw[trans, red!70!black] (q2) to[bend left=20] node[guard,
right, text=red!70!black] {$\neg Inv_2$} (q3);
\draw[trans, red!70!black] (q1) -- node[guard, left, text=red!70!black] {$\neg Inv_1$} (q3);
\draw[trans, red!70!black] (q2) to[bend left=20] node[guard, right, text=red!70!black] {$\neg Inv_2$} (q3);
% Recovery transition
\draw[trans, dashed] (q3) to[bend left=30] node[guard, below]
{Manual reset} (q0);
\draw[trans, dashed] (q3) to[bend left=30] node[guard, below] {Manual reset} (q0);
% Self-loops indicating staying in mode
\draw[trans] (q2) to[loop right] node[guard, right] {$Inv_2$}
(q2);
\draw[trans] (q2) to[loop right] node[guard, right] {$Inv_2$} (q2);
% Dynamics labels below states
\node[dynamics] at (0,-1.4) {$\dot{x} = f_0(x)$};
\node[dynamics] at (6,-1.2) {$\dot{x} = f_1(x)$};
\node[dynamics] at (10,-1.4) {$\dot{x} = f_2(x)$};
\node[dynamics] at (6,-1.2) {$\dot{x} = f_1(x,u)$};
\node[dynamics] at (10,-1.4) {$\dot{x} = f_2(x,u)$};
\node[dynamics] at (5,-4.9) {$\dot{x} = f_3(x)$};
\end{tikzpicture}
\caption{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.}
\caption{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.}
\label{fig:hybrid_automaton}
\end{figure}
\subsection{System Requirements, Specifications, and Discrete Controllers}
%%% NOTES (Section 1):
% - May want to clarify the "no external input" claim with a footnote about
% strategic inputs (e.g., remote start/stop commands)
% - The reset map R is often identity for physical systems; clarify if needed
% ----------------------------------------------------------------------------
% 2. SYSTEM REQUIREMENTS AND SPECIFICATIONS
% ----------------------------------------------------------------------------
\subsection{System Requirements, Specifications, and Discrete Controllers}
Human control of nuclear power can be divided into three different scopes:
strategic, operational, and tactical.\footnote{This was inspired by an article
about battlefield organizational science~\cite{harvey_levels_2021}.} Strategic
control is 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 scheduled maintenance and downtime. The time
scale at this level is long, often spanning months or years. The lowest level of
control is the tactical level. This is the individual control of pumps,
turbines, and chemistry. Tactical control has already been somewhat automated in
nuclear power plants today, and is generally considered ``automatic control''
when autonomous. These controls are almost always continuous systems with a
direct impact on the physical state of the plant. Tactical control objectives
include, but are not limited to, maintaining pressurizer level, maintaining core
temperature, or adjusting reactivity with a chemical shim.
strategic, operational, and tactical. Strategic control is 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 scheduled maintenance and downtime. The time scale at this level is
long, often spanning months or years. The lowest level of control is the
tactical level. This is the individual control of pumps, turbines, and
chemistry. Tactical control has already been somewhat automated in nuclear power
plants today, and is generally considered ``automatic control'' when autonomous.
These controls are almost always continuous systems with a direct impact on the
physical state of the plant. Tactical control objectives include maintaining
pressurizer level, maintaining core temperature, or adjusting reactivity with a
chemical shim.
The level of control linking these two extremes is the operational control
scope. Operational control is the primary responsibility of human operators
@ -158,19 +168,22 @@ way, it bridges high-level and low-level goals. A strategic goal may be to
perform refueling at a certain time, while the tactical level of the plant is
currently focused on maintaining a certain core temperature. The operational
level issues the shutdown procedure, using several smaller tactical goals along
the way to achieve this strategic objective. This hierarchical division of
control scope and objectives is illustrated graphically in
figure~\ref{fig:strat_op_tact}.
the way to achieve this objective. Thus, the combination of the operational and
tactical levels fundamentally forms a hybrid controller. The tactical level is
the continuous evolution of the plant according to the control input and control
law, while the operational level is a discrete state evolution that determines
which tactical control law to apply.
%Say something about autonomous control systems near here?
\begin{figure}
\centering
\begin{tikzpicture}[scale=0.8]
% Pyramid layers
\fill[blue!30!white] (0,4) -- (2,4) -- (1,5.) -- cycle;
\fill[blue!20!white] (-1.5,2.5) -- (3.5,2.5) -- (2,4) -- (0,4)
-- cycle;
\fill[blue!10!white] (-3,1) -- (5,1) -- (3.5,2.5) -- (-1.5,2.5)
-- cycle;
\fill[blue!20!white] (-1.5,2.5) -- (3.5,2.5) -- (2,4) -- (0,4) -- cycle;
\fill[blue!10!white] (-3,1) -- (5,1) -- (3.5,2.5) -- (-1.5,2.5) -- cycle;
% Labels inside pyramid
\node[font=\small\bfseries] at (1,4.5) {Strategic};
@ -179,132 +192,119 @@ figure~\ref{fig:strat_op_tact}.
% Descriptions to the right
\node[anchor=west, font=\small, text width=8cm] at (5.5,4.6)
{\textit{Long-term planning:} maintenance scheduling, capacity
planning, economic dispatch};
{\textit{Long-term planning:} maintenance scheduling, capacity planning, economic dispatch};
\node[anchor=west, font=\small, text width=8cm] at (5.5,3.1)
{\textit{Discrete decisions:} startup/shutdown sequences, power
level changes, mode transitions};
{\textit{Discrete decisions:} startup/shutdown sequences, power level changes, mode transitions};
\node[anchor=west, font=\small, text width=8cm] at (5.5,1.6)
{\textit{Continuous control:} temperature regulation, pressure
control, load following};
{\textit{Continuous control:} temperature regulation, pressure control, load following};
% Bracket showing HAHACS scope (simple line with text)
\draw[thick] (5.0,1.0) -- (-3.5,1) -- (-3.5,4) -- (2.0,4) --
cycle;
\node[font=\small, align=center, rotate=90] at (-4.2,2.5)
{HAHACS scope};
\draw[thick] (5.0,1.0) -- (-3.5,1) -- (-3.5,4) -- (2.0,4) -- cycle;
\node[font=\small, align=center, rotate=90] at (-4.2,2.5) {HAHACS scope};
\end{tikzpicture}
\caption{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.}
\caption{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.}
\label{fig:strat_op_tact}
\end{figure}
This operational control level is the main reason for the requirement of human
operators in nuclear control today. The hybrid nature of this control system
makes it difficult to prove what the behavior of the combined hybrid system will
do across the entire state-space, so human operators have been used as a
stop-gap for safety. Humans have been used for this layer because their general
intelligence has been relied upon as a safe way to manage the hybrid nature of
this system---if a failure occured, it has been assumed a human operator can
figure out a solution to maintain plant performance and safety without
exhaustive knowledge of plant behavior. However, human factors research has
sought to minimize the need for general human reasoning by creating extremely
prescriptive operating manuals with strict procedures dictating what control to
implement at a given time. These operating manuals have minimized the role of
human operators today, are the key to the automating the operational control
scope.
makes it difficult to prove that a controller will perform according to
strategic requirements, as unified infrastructure for building and verifying
hybrid systems does not currently exist. Humans have been used for this layer
because their general intelligence has been relied upon as a safe way to manage
the hybrid nature of this system. But these operators use 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
observations about current practice. First, the operational scope control is
effectively discrete control. Second, the rules for implementing this control
are described in operating procedures prior to their implementation. Instead of
implementing these procudures with a human controller, we rigorize the
instructions as a set of formal requirements. The behavior of any control system
originates in requirements: statements about what the system must do, must not
do, and under what conditions. For nuclear systems, these requirements derive
from multiple sources including regulatory mandates, design basis analyses, and
aforementioned operating procedures. The challenge is formalizing
these requirements with sufficient precision that they can serve as
the foundation for autonomous
control system synthesis and verification. We can build these requirements using
temporal logic.
are described prior to their implementation in operating procedures. Before
constructing a HAHACS, we must completely describe its intended behavior. The
behavior of any control system originates in requirements: statements about what
the system must do, must not do, and under what conditions. For nuclear systems,
these requirements derive from multiple sources including regulatory mandates,
design basis analyses, and operating procedures. The challenge is formalizing
these requirements with sufficient precision that they can serve as the
foundation for autonomous control system synthesis and verification. We can
build these requirements using temporal logic.
Temporal logic is a powerful set of semantics for building systems with
complex but deterministic behavior. Temporal logic extends classical
propositional logic with operators that express properties over time. Using
temporal logic, we can make statements relating discrete control modes to one
another and define all the requirements of a HAHACS. The guard conditions
$\mathcal{G}$ are defined by determining boundary conditions between discrete
states and specifying their behavior, while continuous mode invariants can
also be expressed as temporal logic statements. These specifications form the
basis of any proofs about a HAHACS and constitute the fundamental truth
statements about what the behavior of the system is designed to be.
Temporal logic is a powerful set of semantics for building systems with complex
but deterministic behavior. Temporal logic extends classical propositional logic
with operators that express properties over time. Using temporal logic, we can
make statements relating discrete control modes to one another and define all
the requirements of a HAHACS. The guard conditions $\mathcal{G}$ are defined by
determining boundary conditions between discrete states and specifying their
behavior, while continuous mode invariants can also be expressed as temporal
logic statements. These specifications form the basis of any proofs about a
HAHACS and constitute the fundamental truth statements about what the behavior
of the system is designed to be.
Discrete mode transitions include predicates that are Boolean functions over the
continuous state space: $p_i: \mathcal{X} \rightarrow \{\text{true},
\text{false}\}$. These predicates formalize conditions like ``coolant
temperature exceeds 315\textdegree{}C'' or ``pressurizer level is between 30\%
and 60\%.'' Critically, we do not impose this discrete abstraction artificially.
Operating procedures for nuclear systems already define go/no-go conditions as
discrete predicates, but do so in natural language. These thresholds come from
design basis safety analysis and have been validated over decades of operational
experience. Our methodology assumes this domain knowledge exists and provides a
framework to formalize it. This is why the approach is feasible for nuclear
applications specifically: the work of defining safe operating boundaries has
already been done by generations of nuclear engineers. The work of translating
these requirements from interpretable natural language to a formal
requirement is what remains to be done.
temperature exceeds 315°C'' or ``pressurizer level is between 30\% and 60\%.''
Critically, we do not impose this discrete abstraction artificially. Operating
procedures for nuclear systems already define go/no-go conditions as discrete
predicates. These thresholds come from design basis safety analysis and have
been validated over decades of operational experience. Our methodology assumes
this domain knowledge exists and provides a framework to formalize it. This is
why the approach is feasible for nuclear applications specifically: the hard
work of defining safe operating boundaries has already been done by generations
of nuclear engineers.
Linear temporal logic (LTL) is particularly well-suited for
specifying reactive systems. LTL formulas are built from atomic propositions
(our discrete predicates) using Boolean connectives and temporal operators.
The key temporal operators are:
\begin{itemize}
\item $\mathbf{X}\phi$ (next): $\phi$ holds in the next state
\item $\mathbf{G}\phi$ (globally): $\phi$ holds in all future states
\item $\mathbf{F}\phi$ (finally): $\phi$ holds in some future state
\item $\phi \mathbf{U} \psi$ (until): $\phi$ holds until $\psi$ becomes true
\end{itemize}
These operators allow us to express safety properties (``the reactor never
enters an unsafe configuration''), liveness properties (``the system
eventually reaches operating temperature''), and response properties (``if
coolant pressure drops, the system initiates shutdown within bounded time'').
Linear temporal logic (LTL) is particularly well-suited for specifying reactive
systems. LTL formulas are built from atomic propositions (our discrete
predicates) using Boolean connectives and temporal operators. These operators
allow us to express safety properties (``the reactor never enters an unsafe
configuration''), liveness properties (``the system eventually reaches operating
temperature''), and response properties (``if coolant pressure drops, the system
initiates shutdown within bounded time''). We note that FRET's realizability
checking currently supports safety and bounded response properties but not
general liveness properties~\cite{katis_realizability_2022}. Liveness
requirements such as ``eventually reaches operating temperature'' are instead
verified through the continuous mode analysis described in Section~3.2, where
reachability analysis can confirm that target states are attained within bounded
time.
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 developed by NASA to build high-assurance timed systems. FRET is an
intermediate language between temporal logic and natural language that allows
for rigid definitions of temporal behavior while using a syntax accessible to
engineers without formal methods expertise\cite{katis_realizability_2022}. This
benefit is crucial for the feasibility of this methodology in industry. By
reducing the expert knowledge required to use these tools, their adoption with
the current workforce becomes easier.
engineers without formal methods expertise. This benefit is crucial for the
feasibility of this methodology in industry. By reducing the expert knowledge
required to use these tools, their adoption with the current workforce becomes
easier.
A key feature of FRET is the ability to start with logically imprecise
statements and consecutively refine them into well-posed
specifications\cite{katis_realizability_2022, pressburger_using_2023}. We
can use this to our advantage by directly importing operating procedures and
design requirements into FRET in natural language, then iteratively refining
them into specifications for a HAHACS. This has two distinct benefits.
First, it allows us to draw a direct link from design documentation to
digital system 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.
statements and consecutively refine them into well-posed specifications. We can
use this to our advantage by directly importing operating procedures and design
requirements into FRET in natural language, then iteratively refining them into
specifications for a HAHACS. This has two distinct benefits. First, it allows us
to draw a direct link from design documentation to digital system
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.
\dasinline{Maybe add more details about FRET case studies here. This would be
Pressburger and Katis.}
\splitinline{Some examples of where FRET has been used and why it will be successful
here}
Once system requirements are defined as temporal logic specifications, we use
them to build the discrete control system. To do this, reactive synthesis tools
are employed. Reactive synthesis is a field in computer science that deals with
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~\cite{jacobs_reactive_2024}. Our systems fit exactly this mold: the
current discrete state and status of guard conditions are the input, while the
output is the next discrete state.
an output. Our systems fit exactly this mold: the current discrete state and
status of guard conditions are the input, while the output is the next discrete
state.
Reactive synthesis solves the following problem: given an LTL formula $\varphi$
that specifies desired system behavior, automatically construct a finite-state
@ -314,35 +314,28 @@ exists, the specification is called \emph{realizable}. The synthesis algorithm
either produces a correct-by-construction controller or reports that no such
controller can exist. This realizability check is itself valuable: an
unrealizable specification indicates conflicting or impossible requirements in
the original procedures. The current implementation and one of the main uses of
FRET today is for exactly this purpose---multiple case studies have used FRET
for the refinement of unrealizable specifications into realizable systems
\cite{katis_realizability_2022, pressburger_using_2023}.
the original procedures.
The main advantage of reactive synthesis is that at no point in the production
of the discrete automaton is human engineering of the implementation required.
The resultant automaton is correct to the specification by construction. This
method of construction eliminates the possibility of human error at the
implementation stage entirely. The effort shifts entirely to specifying correct
behavior rather than implementing it. This has two critical implications. First,
every mode transition can be traced back through the specification to its
originating requirement, providing a clear liability and justification chain.
Second, by defining system behavior in temporal logic and synthesizing the
controller using deterministic algorithms, discrete control decisions become
provably consistent with operating procedures.
The resultant automaton is correct by construction. This method of construction
eliminates the possibility of human error at the implementation stage entirely.
Instead, the effort on the human designer is directed at the specification of
system behavior itself. This has two critical implications. First, it makes the
creation of the discrete controller tractable. The reasons the controller
changes between modes can be traced back to the specification and thus to any
requirements, which provides a trace for liability and justification of system
behavior. Second, discrete control decisions made by humans are reliant on the
human operator operating correctly. Humans are intrinsically probabilistic
creatures who cannot eliminate human error. By defining the behavior of this
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.
The output of reactive synthesis is a finite-state machine that can be directly
translated to executable code. Tools such as Strix accept full LTL
specifications and produce Mealy machines via parity game
solving~\cite{luttenberger_practical_2020, meyer_strix_2018}. For specifications
within the GR(1) fragment---which captures the reactive input-output structure
typical of supervisory control---synthesis is efficient and scales to
specifications with thousands of states. Nuclear operating procedures are
well-suited to this fragment: environment inputs correspond to plant state
measurements and guard conditions, while outputs are mode transition commands.
The synthesized automaton provides a correct-by-construction implementation that
can be compiled to run on industrial control hardware without manual translation
of the control logic.
\splitinline{Talk about how one would go from a discrete automaton to actual
code}
\splitinline{Examples of reactive synthesis in the wild}
\subsection{Continuous Control Modes}
@ -351,15 +344,14 @@ autonomous controller. These control systems are hybrid, with both discrete and
continuous components. This section describes the continuous control modes that
execute within each discrete state, and how we verify that they satisfy the
requirements imposed by the discrete layer. It is important to clarify the scope
of this methodology with respect to continuous controller design. This work will
verify continuous controllers; it does not synthesize them. The distinction
of this methodology with respect to continuous controller design. This work
verifies continuous controllers; it does not synthesize them. The distinction
parallels model checking in software verification: model checking does not tell
engineers how to write correct software, but it verifies whether a given
implementation satisfies its specification. Similarly, we assume that continuous
controllers can be designed using standard control theory techniques, and to
that end, are not prohibitive to create. Our contribution is a verification
framework that confirms candidate controllers compose correctly with the
discrete layer to produce a safe hybrid system.
controllers can be designed using standard control theory techniques. Our
contribution is a verification framework that confirms candidate controllers
compose correctly with the discrete layer to produce a safe hybrid system.
The operational control scope defines go/no-go decisions that determine what
kind of continuous control to implement. The entry or exit conditions of a
@ -367,12 +359,12 @@ discrete state are themselves the guard conditions $\mathcal{G}$ that define the
boundaries for each continuous controller's allowed state-space region. These
continuous controllers all share a common state space, but each individual
continuous control mode operates within its own partition defined by the
discrete state $q_i$ and the associated guard conditions. This partitioning of
the continuous state space among several distinct 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{kapuria_using_2025, lang_formal_2021}.
discrete state $q_i$ and the associated guards. This partitioning of the
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{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
@ -380,235 +372,201 @@ output set clearly defined by our discrete transitions \textit{a priori}.
Consider that we define the continuous state space as $\mathcal{X}$. Each
discrete mode $q_i$ then provides three key pieces of information for continuous
controller design:
%
\begin{enumerate}
\item \textbf{Entry conditions:} $\mathcal{X}_{entry,i} \subseteq
\mathcal{X}$, the set of possible initial states when entering this mode
\item \textbf{Exit conditions:} $\mathcal{X}_{exit,i} \subseteq
\mathcal{X}$, the target states that trigger transition to the next mode,
or is the region in the state space a stabilizing mode remains within.
\item \textbf{Safety invariants:} $\mathcal{X}_{safe,i} \subseteq
\mathcal{X}$, the envelope of safe states during operation in this mode.
These are derived from invariants \(Inv\).
\item \textbf{Entry conditions:} $\mathcal{X}_{entry,i} \subseteq \mathcal{X}$,
the set of possible initial states when entering this mode
\item \textbf{Exit conditions:} $\mathcal{X}_{exit,i} \subseteq \mathcal{X}$,
the target states that trigger transition to the next mode, or is the region
in the state space a stabilizing mode remains within.
\item \textbf{Safety invariants:} $\mathcal{X}_{safe,i} \subseteq \mathcal{X}$,
the envelope of safe states during operation in this mode. These are derived
from invariants \(Inv\).
\end{enumerate}
%
These sets come directly from the discrete controller synthesis and define
precise objectives for continuous control.\dasnote{This SOUNDS like
assume-guarantee stuff. Maybe make that connection formal and cite it?} The
continuous controller for mode $q_i$ must drive the system from any state in
$\mathcal{X}_{entry,i}$ to some state in $\mathcal{X}_{exit,i}$ while remaining
within $\mathcal{X}_{safe,i}$. 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.
precise objectives for continuous control. The continuous controller for mode
$q_i$ must drive the system from any state in $\mathcal{X}_{entry,i}$ to some
state in $\mathcal{X}_{exit,i}$ while remaining within $\mathcal{X}_{safe,i}$.
\dasinline{(1) Add figure showing the relationship between entry/exit/safety
sets. (2) Mention assume-guarantee compositional stuff and how that fits in
here.}
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.
\subsubsection{Transitory Modes}
Transitory modes are continuous controllers designed to move the plant from one
discrete operating condition to another. Their purpose is to execute
transitions: starting from entry conditions, reach exit conditions, and maintain
safety invariants throughout. Examples include but are not limited to power
ramp-up sequences, cooldown procedures, and load-following maneuvers.
Transitory modes are continuous controllers designed to move
the plant from one discrete operating condition to another. Their purpose is to
execute transitions: starting from entry conditions, reach exit conditions,
and maintain safety invariants throughout. Examples include power ramp-up sequences,
cooldown procedures, and load-following maneuvers.
The control objective for a transitory mode can be stated formally. Given
entry conditions $\mathcal{X}_{entry}$, exit conditions
$\mathcal{X}_{exit}$, safety invariant $\mathcal{X}_{safe}$, and
closed-loop dynamics $\dot{x} = f(x)$, the controller must satisfy:
%
The control objective for a transitory mode can be stated
formally. Given entry conditions $\mathcal{X}_{entry}$, exit conditions
$\mathcal{X}_{exit}$, safety invariant $\mathcal{X}_{safe}$, and closed-loop
dynamics $\dot{x} = f(x, u(x))$, the controller must satisfy:
\[
\forall x_0 \in \mathcal{X}_{entry}: \exists T > 0: x(T) \in
\mathcal{X}_{exit} \land \forall t \in [0,T]: x(t) \in \mathcal{X}_{safe}
\forall x_0 \in \mathcal{X}_{entry}: \exists T > 0: x(T) \in \mathcal{X}_{exit}
\land \forall t \in [0,T]: x(t) \in \mathcal{X}_{safe}
\]
%
That is, from any valid entry state, the trajectory must eventually reach the
exit condition without ever leaving the safe region.
Verification of transitory modes will use reachability analysis. Reachability
analysis computes the set of all states reachable from a given initial set under
the system dynamics~\cite{guernic_reachability_2009,
mitchell_time-dependent_2005, bansal_hamilton-jacobi_2017}. For a transitory
mode to be valid, the reachable set from $\mathcal{X}_{entry}$ must satisfy two
conditions:
%
Verification of transitory modes uses reachability analysis.
Reachability analysis computes the set of all states reachable from a given
initial set under the system dynamics. For a transitory mode to be valid, the
reachable set from $\mathcal{X}_{entry}$ must satisfy two conditions:
\begin{enumerate}
\item The reachable set eventually intersects $\mathcal{X}_{exit}$ (the
mode achieves its objective)
\item The reachable set never leaves $\mathcal{X}_{safe}$ (safety is
maintained throughout the transition)
\item The reachable set eventually intersects $\mathcal{X}_{exit}$ (the mode
achieves its objective)
\item The reachable set never leaves $\mathcal{X}_{safe}$ (safety is maintained
throughout the transition)
\end{enumerate}
%
Formally, if $\text{Reach}(\mathcal{X}_{entry}, f, [0,T])$ denotes the states
reachable within time horizon $T$:
%
\[
\text{Reach}(\mathcal{X}_{entry}, f_i, [0,T]) \subseteq \mathcal{X}_{safe}
\land \text{Reach}(\mathcal{X}_{entry}, f_i, [0,T]) \cap
\mathcal{X}_{exit} \neq \emptyset
\text{Reach}(\mathcal{X}_{entry}, f_i, [0,T]) \subseteq \mathcal{X}_{safe} \land
\text{Reach}(\mathcal{X}_{entry}, f_i, [0,T]) \cap \mathcal{X}_{exit} \neq \emptyset
\]
%
Because the discrete controller defines clear boundaries in
continuous state space, the verification problem for each transitory mode is
well-posed. We know the possible initial conditions, we know the target
conditions, and we know the safety envelope. The verification task is to
confirm that the candidate continuous controller achieves the objective from
all possible starting points.
Several tools exist for computing reachable sets of hybrid systems, including
CORA~\cite{althoff_introduction_nodate}, Flow*~\cite{chen_flow_2013,
chen_taylor_2012}, SpaceEx~\cite{frehse_spaceex_2011}, and
JuliaReach~\cite{bogomolov_reachability_2020}. The choice of
tool depends on the structure of the continuous dynamics. Linear systems admit
efficient polyhedral or ellipsoidal reachability computations. Nonlinear 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.
Because the discrete controller defines clear boundaries in continuous state
space, the verification problem for each transitory mode is well-posed. We know
the possible initial conditions, we know the target conditions, and we know the
safety envelope. The verification task is to confirm that the candidate
continuous controller achieves the objective from all possible starting points.
Several tools exist for computing reachable sets of hybrid
systems, including CORA, Flow*, SpaceEx, and JuliaReach. The choice of tool
depends on the structure of the continuous dynamics. Linear systems admit
efficient polyhedral or ellipsoidal reachability computations. Nonlinear
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.
\subsubsection{Stabilizing Modes}
Stabilizing modes are continuous controllers with an objective of maintaining
a particular discrete state indefinitely. Rather than driving the system
toward an exit state, they keep the system within a safe
operating region. Examples include steady-state power operation, hot standby,
and load-following at constant power level. Reachability analysis for
stabilizing modes may not be a suitable approach to validation. Instead, we
plan to use barrier certificates. Barrier certificates analyze the dynamics
of the system to determine whether flux across a given boundary
exists~\cite{prajna_safety_2004}. In other words, they
evaluate whether any trajectory leaves a given boundary. This definition is
exactly what defines the validity of a stabilizing continuous control mode.
Stabilizing modes are continuous controllers with an objective of maintaining a
particular discrete state indefinitely. Rather than driving the system toward an
exit condition, they keep the system within a safe operating region. Examples
include steady-state power operation, hot standby, and load-following at
constant power level. Reachability analysis for stabilizing modes may not be a
suitable approach to validation. Instead, we plan to use barrier certificates.
Barrier certificates analyze the dynamics of the system to determine whether
flux across a given boundary exists. They evaluate whether any trajectory leaves
a given boundary. This definition is exactly what defines the validity of a
stabilizing continuous control mode.
A barrier certificate (or control barrier function) is a scalar function $B:
\mathcal{X} \rightarrow \mathbb{R}$ that certifies forward invariance of a safe
set. The idea is analogous to Lyapunov functions for
stability~\cite{branicky_multiple_1998}: rather than computing trajectories
explicitly, we find a certificate function whose properties guarantee the
desired behavior. For a safe set $\mathcal{C} = \{x : B(x) \geq 0\}$ and
dynamics $\dot{x} = f(x,u)$, the\dasinline{Should clarify that the safe set C is
not the entire continuous region. It's just the boundary of the region.} barrier
certificate condition requires:
%
A barrier certificate (or control barrier function) is a
scalar function $B: \mathcal{X} \rightarrow \mathbb{R}$ that certifies forward
invariance of a safe set. The idea is analogous to Lyapunov functions for
stability: rather than computing trajectories explicitly, we find a certificate
function whose properties guarantee the desired behavior. For a safe set
$\mathcal{C} = \{x : B(x) \geq 0\}$ and dynamics $\dot{x} = f(x,u)$, the
barrier certificate condition requires:
\[
\forall x \in \partial\mathcal{C}: \dot{B}(x) = \nabla B(x) \cdot f(x,u(x))
\geq 0
\forall x \in \partial\mathcal{C}: \dot{B}(x) = \nabla B(x) \cdot f(x,u(x)) \geq 0
\]
%
This condition states that on the boundary of the safe set (where $B(x) =
0$), the time derivative of $B$ is non-negative. Geometrically, this means
the vector field points inward or tangent to the boundary, never outward. If
this condition holds, no trajectory starting inside $\mathcal{C}$ can ever
leave.
This condition states that on the boundary of the safe set (where $B(x) = 0$),
the time derivative of $B$ is non-negative. Geometrically, this means the
vector field points inward or tangent to the boundary, never outward. If this
condition holds, no trajectory starting inside $\mathcal{C}$ can ever leave.
Because the design of the discrete controller defines careful boundaries in
continuous state space, the barrier \(\mathcal{C}\) is known prior to designing
the continuous controller. This eliminates the search for an appropriate barrier
and minimizes complication in validating stabilizing continuous control modes.
The discrete specifications tell us what region must be invariant; the barrier
certificate confirms that the candidate controller achieves this invariance.
continuous state space, the barrier is known prior to designing the continuous
controller. This eliminates the search for an appropriate barrier and minimizes
complication in validating stabilizing continuous control modes. The discrete
specifications tell us what region must be invariant; the barrier certificate
confirms that the candidate controller achieves this invariance.
The key advantage is that the verification is independent of how the controller
was designed. Standard control techniques can be used to build continuous
controllers, and barrier certificates provide a separate check that the result
satisfies the required invariants. This also allows for the checking of control
modes with different models than they are designed for. 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.\splitnote{SOS methods proven effective: Papachristodoulou 2021
(SOSTOOLS v4, pp.1-2) solves barrier certificate optimization via SOS
constraints---tool integrates with MATLAB. Borrmann 2015 (pp.4-8) demonstrates
control barrier certificates for multi-agent systems, showing how discrete
boundaries (mode guards) can inform barrier design. Your claim that discrete
specs eliminate barrier search is novel and well-supported by these
foundations.}\splitnote{Hauswirth 2024 (pp.1-3) shows optimization-based robust
feedback controllers can serve as alternative verification method---suggests
barrier certificates + reachability provide complementary guarantees for your
stabilizing modes.}
Finding barrier certificates can be formulated as a
sum-of-squares (SOS) optimization problem for polynomial systems, or solved
using satisfiability modulo theories (SMT) solvers for broader classes of
dynamics. The key advantage is that the verification is independent of how
the controller was designed. Standard control techniques can be used to
build continuous controllers, and barrier certificates provide a separate
check that the result satisfies the required invariants. This also allows for
the checking of control modes with different models than they are designed for.
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.
\subsubsection{Expulsory Modes}
Expulsory modes are continuous controllers responsible for ensuring safety
when failures occur. They are designed for robustness rather than optimality.
The control objective is to drive the plant to a safe shutdown state from
potentially anywhere in the state space, under degraded or uncertain
dynamics. Examples include emergency core cooling, reactor SCRAM sequences,
and controlled depressurization procedures.
Expulsory modes are continuous controllers responsible for
ensuring safety when failures occur. They are designed for robustness rather
than optimality. The control objective is to drive the plant to a safe shutdown
state from potentially anywhere in the state space, under degraded or uncertain
dynamics. Examples include emergency core cooling, reactor SCRAM sequences, and
controlled depressurization procedures.
We can detect that physical failures exist because our physical controllers have
been previously proven correct by reachability and barrier certificates. We know
our controller cannot be incorrect for the nominal plant model, so if an
invariant is violated, we know the plant dynamics have changed. The mathematical
formulation for expulsory mode verification differs from transitory modes in two
key ways. First, the entry conditions may be the entire state space (or a large,
conservatively bounded region) rather than a well-defined entry set. The failure
may occur at any point during operation. Second, the dynamics include parametric
uncertainty representing failure modes:
%
invariant is violated, we know the plant dynamics have changed. The HAHACS can
identify that a fault occurred because a discrete boundary condition was
violated by the continuous physical controller. This is a direct consequence of
having verified the nominal continuous control modes: unexpected behavior
implies off-nominal conditions.
The mathematical formulation for expulsory mode verification
differs from transitory modes in two key ways. First, the entry conditions may
be the entire state space (or a large, conservatively bounded region) rather
than a well-defined entry set. The failure may occur at any point during
operation. Second, the dynamics include parametric uncertainty representing
failure modes:
\[
\dot{x} = f(x, u, \theta), \quad \theta \in \Theta_{failure}
\]
%
where $\Theta_{failure}$ captures the range of possible degraded plant
behaviors identified through failure mode and effects analysis (FMEA) or
traditional safety analysis.
We verify expulsory modes using reachability analysis with parametric
uncertainty. While tools such as SpaceEx handle nondeterministic
inputs~\cite{frehse_spaceex_2011}, parametric plant uncertainty requires
conservative over-approximation of reachable sets across the full parameter
range. The verification condition requires that for all parameter values within
the uncertainty set, trajectories from the expanded entry region reach the safe
shutdown state:
%
uncertainty. The verification condition requires that for all parameter values
within the uncertainty set, trajectories from the expanded entry region reach
the safe shutdown state:
\[
\forall \theta \in \Theta_{failure}:
\text{Reach}(\mathcal{X}_{current}, f_\theta, [0,T]) \subseteq
\mathcal{X}_{shutdown}
\text{Reach}(\mathcal{X}_{current}, f_\theta, [0,T]) \subseteq \mathcal{X}_{shutdown}
\]
%
This is more conservative than nominal reachability, accounting for the fact
that we cannot know exactly which failure mode is active.
Traditional safety analysis techniques inform the construction of
$\Theta_{failure}$. Probabilistic risk assessment, FMEA, and design basis
Traditional safety analysis techniques inform the construction
of $\Theta_{failure}$. Probabilistic risk assessment, FMEA, and design basis
accident analysis identify credible failure scenarios and their effects on
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.\splitnote{Parametric uncertainty approach validated: Kapuria 2025
(pp.82-120, Sections 5) verifies SmAHTR resiliency against UCAs with
uncertain dynamics (e.g., PHX secondary flow shutdown, resonating turbine
flow). Uses reachability + Z3 SMT solver (pp.23-24, Section 2.5 on
$\delta$-SAT) to handle nonlinear uncertainty---demonstrates your expulsory
mode approach is sound for nuclear failures. Shows safety can be proven even
when controller deviates from nominal (pp.85-107, UCA 1
analysis).}
safety margins will matter more than performance during emergency shutdown.
\subsection{Industrial Implementation}
The methodology described above must be validated on realistic systems using
industrial-grade hardware to demonstrate practical feasibility. This research
will leverage the University of Pittsburgh Cyber Energy Center's partnership
with Emerson to implement and test the HAHACS methodology on production
control equipment. Emerson's Ovation distributed control system is widely
deployed in power generation facilities, including nuclear plants. The
Ovation platform provides a realistic target for demonstrating that formally
synthesized controllers can execute on industrial hardware meeting timing and
reliability requirements. The discrete automaton produced by reactive
synthesis will be compiled to run on Ovation controllers, with verification
that the implemented behavior matches the synthesized specification exactly.
The methodology described above must be validated on realistic
systems using industrial-grade hardware to demonstrate practical feasibility.
This research will leverage the University of Pittsburgh Cyber Energy Center's
partnership with Emerson to implement and test the HAHACS methodology on
production control equipment. Emerson's Ovation distributed control system is widely deployed
in power generation facilities, including nuclear plants. The Ovation platform
provides a realistic target for demonstrating that formally synthesized
controllers can execute on industrial hardware meeting timing and reliability
requirements. The discrete automaton produced by reactive synthesis will be
compiled to run on Ovation controllers, with verification that the implemented
behavior matches the synthesized specification exactly.
For the continuous dynamics, we will use a small modular reactor simulation. The
SmAHTR (Small modular Advanced High Temperature Reactor) model provides a
relevant testbed for startup and shutdown procedures. The ARCADE (Advanced
Reactor Control Architecture Development Environment) interface will establish
communication between the Emerson Ovation hardware and the reactor simulation,
enabling hardware-in-the-loop testing of the complete hybrid controller.
For the continuous dynamics, we will use a small modular
reactor simulation. The SmAHTR (Small modular Advanced High Temperature
Reactor) model provides a relevant testbed for startup and shutdown procedures.
The ARCADE (Advanced Reactor Control Architecture Development Environment)
interface will establish communication between the Emerson Ovation hardware and
the reactor simulation, enabling hardware-in-the-loop testing of the complete
hybrid controller.
Working with Emerson on such an implementation is an incredible advantage for
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 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.
The Emerson collaboration strengthens this work in two ways. Access to
system experts at Emerson ensures that implementation details of the Ovation
platform are handled correctly. Direct industry collaboration also provides an
immediate pathway for technology transfer and alignment with practical
deployment requirements.

View File

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

View File

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

View File

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

0
biblatex.sty Normal file
View File

View File

@ -1,448 +0,0 @@
# Thesis Proposal Citation Audit
Generated: 2026-03-17 by Split
Legend:
- ✅ VERIFIED — Claim matches source, page reference
confirmed
- ⚠️ PARTIALLY VERIFIED — Claim is supported but language
slightly differs or page ref uncertain
- ❌ CANNOT VERIFY — No PDF access or claim not found in
source
- 🔧 NEEDS SOFTENING — Claim overstates what source actually
says
---
## SECTION 2: STATE OF THE ART
### Citation 1: NUREG-0899, 10CFR50.34
**Claim:** "Procedures must comply with 10 CFR
50.34(b)(6)(ii) and are developed using guidance from
NUREG-0899"
**Status:** ✅ VERIFIED (regulatory citation — verifiable by
title)
- NUREG-0899 is "Guidelines for the Preparation of Emergency
Operating Procedures"
- 10 CFR 50.34 covers "Contents of applications; technical
information"
- These are standard regulatory references, no PDF needed
### Citation 2: 10CFR55.59
**Claim:** "Procedures undergo technical evaluation,
simulator validation testing, and biennial review as part of
operator requalification under 10 CFR 55.59"
**Status:** ✅ VERIFIED (regulatory citation)
- 10 CFR 55.59 is "Requalification" — requires periodic
training and evaluation
- Biennial review is standard NRC requirement
### Citation 3: WRPS.Description, gentillon_westinghouse_1999
**Claim:** "Automation currently handles only reactor
protection: trips on safety parameters, emergency core
cooling actuation, containment isolation, and basic process
control"
**Status:** ⚠️ CANNOT VERIFY PDFs
- These are Westinghouse technical documents
- Claim is consistent with standard PWR protection system
descriptions
- **DANE: Verify you have these sources and they support
this specific list**
### Citation 4: 10CFR55
**Claim:** "Operators hold legal authority under 10 CFR Part
55 to make critical decisions"
**Status:** ✅ VERIFIED (regulatory citation)
- 10 CFR Part 55 covers "Operators' Licenses"
### Citation 5: Kemeny1979
**Claim:** "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"
**Status:** ✅ VERIFIED (historical record)
- The President's Commission on TMI (Kemeny Commission)
documented this
- This is well-established historical fact
- **DANE: Confirm page reference if Dan asks (likely Chapter
2 of Kemeny Report)**
### Citation 6: hogberg_root_2013
**Claim:** "The root cause of all severe accidents at
nuclear power plants—Three Mile Island, Chernobyl, and
Fukushima Daiichi—has been identified as primarily human
factors"
**Status:** ✅ VERIFIED
- PDF available: "Root Causes and Impacts of Severe
Accidents at Large Nuclear Power Plants"
- Paper analyzes all three accidents and identifies
human/organizational factors
- **Specific page:** Abstract and Section 3 discuss human
factors as common thread
### Citation 7: zhang_analysis_2025
**Claim:** "A detailed analysis of 190 events at Chinese
nuclear power plants from 20072020 found that 53% of events
involved active errors, while 92% were associated with
latent errors"
**Status:** ❌ CANNOT VERIFY — PDF not in Zotero WebDAV
- **DANE: You need to verify these specific percentages
(53%, 92%) against the paper**
- These are very specific claims that need exact source
confirmation
### Citation 8: Kiniry2024 (HARDENS)
**Claim:** "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"
**Status:** ❌ CANNOT VERIFY — PDF not available
- **DANE: Verify "most advanced" claim is defensible**
- Second use (line 140): "NRC Final Report explicitly notes
that all material is considered in development"
- **DANE: Verify exact quote from report**
### Citation 9: baier_principles_2008
**Claim:** "Temporal logic provides this language by
extending classical propositional logic with operators that
express properties over time"
**Status:** ⚠️ CANNOT VERIFY PDF (book not on WebDAV)
- This is a standard textbook definition from "Principles of
Model Checking"
- Claim is a basic definition that should be uncontroversial
- **Low risk** — any model checking textbook will say the
same
### Citation 10: platzer_differential_2008
**Claim:** "The result has been the field of differential
dynamic logic (dL)"
**Status:** ✅ VERIFIED
- PDF available: Platzer 2008
- Platzer introduced dL in this paper
- The paper literally defines dL
### Citation 11: fulton_keymaera_2015
**Claim:** "Automated proof assistants such as KeYmaera X
exist to help develop proofs of systems using dL"
**Status:** ✅ VERIFIED
- PDF available: "KeYmaera X: An Axiomatic Tactical Theorem
Prover for Hybrid Systems"
- Paper introduces KeYmaera X as a theorem prover for dL
- Exact match
### Citation 12: kapuria_using_2025
**Claim:** "Approaches have been made to alleviate these
issues for nuclear power contexts using contract and
decomposition based methods, but do not yet constitute a
complete design methodology"
**Status:** ✅ VERIFIED
- PDF available: Kapuria dissertation
- Abstract states: "decomposition-based formal verification
framework for hybrid systems"
- The "not yet complete methodology" is Dane's assessment of
the field, which is fair given Kapuria is a dissertation
not a deployed system
---
## SECTION 3: RESEARCH APPROACH
### Citation 13: lunze_handbook_2009
**Claim:** "This nomenclature is borrowed from the Handbook
on Hybrid Systems Control"
**Status:** ❌ CANNOT VERIFY — PDF is local file
(imported_file), not on WebDAV
- **DANE: Verify the specific nomenclature definitions match
the handbook**
### Citation 14: alur_hybrid_1993
**Claim:** "Formalizing reactor operations using the
framework of hybrid automata"
**Status:** ✅ VERIFIED
- PDF available
- Alur et al. 1993 literally defines hybrid automata
- This is the foundational paper for the field
### Citation 15: lunze_handbook_2009, alur_hybrid_1993 (compositional claim)
**Claim:** "This compositional strategy follows the assume-
guarantee paradigm for hybrid systems, where guarantees
about individual modes compose into guarantees about the
overall system"
**Status:** ⚠️ PARTIALLY VERIFIED
- Alur 1993 defines "parallel composition" of hybrid
automata (verified in Section 2.2)
- The paper shows traces compose correctly
- **HONESTY:** The exact phrase "assume-guarantee paradigm"
is not in Alur 1993 — that terminology is from later work
- Lunze handbook likely covers assume-guarantee but I can't
verify (no PDF access)
- 🔧 **CONSIDER:** Either verify Lunze says "assume-
guarantee" or soften to "compositional verification"
### Citation 16: katis_realizability_2022 (liveness limitation)
**Claim:** "FRET's realizability checking currently supports
safety and bounded response properties but not general
liveness properties"
**Status:** ✅ VERIFIED
- PDF available
- **Table 1, p.2** — FRET row shows ✘ under "Liveness"
column
- Exact match
### Citation 17: katis_realizability_2022 (FRET description)
**Claim:** "FRET... allows for rigid definitions of temporal
behavior while using a syntax accessible to engineers
without formal methods expertise"
**Status:** ✅ VERIFIED
- PDF available
- Section 1 describes FRET's user-friendly interface design
- Claim is consistent with paper's stated goals
### Citation 18: katis_realizability_2022, pressburger_using_2023 (iterative refinement)
**Claim:** "A key feature of FRET is the ability to start
with logically imprecise statements and consecutively refine
them into well-posed specifications"
**Status:** ✅ VERIFIED
- Both PDFs available
- Katis 2022 describes FRET's diagnosis and refinement
workflow
- Pressburger 2023 demonstrates this on Lift Plus Cruise
case study
### Citation 19: jacobs_reactive_2024
**Claim:** "A reactive program is one that, for a given
state, takes an input and produces an output"
**Status:** ❌ CANNOT VERIFY — PDF not on WebDAV (no
attachment found)
- This is a standard definition of reactive systems
- **Low risk** — definition is uncontroversial
- **DANE: Verify you have this paper and it contains this
definition**
### Citation 20: katis_realizability_2022, pressburger_using_2023 (FRET case studies)
**Claim:** "Multiple case studies have used FRET for the
refinement of unrealizable specifications into realizable
systems"
**Status:** ✅ VERIFIED
- Both PDFs available
- Katis covers multiple case studies
- Pressburger is itself a case study (Lift Plus Cruise)
### Citation 21: meyer_strix_2018
**Claim:** "Tools such as Strix accept full LTL
specifications and produce Mealy machines via parity game
solving"
**Status:** ⚠️ VERIFIED FROM ABSTRACT (no PDF)
- No PDF on WebDAV
- Zotero abstract confirms: "Strix is a new tool for
reactive LTL synthesis combining a direct translation of
LTL formulas into deterministic parity automata (DPA) and
an efficient, multi-threaded explicit state solver for
parity games"
- **DANE: Verify Mealy machine output specifically (likely
in full paper)**
### Citation 22: katis_capture_2022
**Claim:** (cited alongside Strix for parity game solving)
**Status:** ⚠️ PARTIAL
- This is the conference version of Katis 2022
- Used here as a venue citation
- **DANE: Verify this paper actually discusses parity games,
or if it's just a venue citation for FRET realizability**
### Citation 23: kapuria_using_2025, lang_formal_2021
**Claim:** "Discontinuity of the vector fields at discrete
state interfaces makes reachability analysis computationally
expensive, and analytic solutions often become intractable"
**Status:** ⚠️ PARTIALLY VERIFIED
- Kapuria PDF available — dissertation discusses
computational challenges
- Lang 2021 is imported_file (no WebDAV access)
- **DANE: Verify Lang 2021 supports the "intractable"
claim**
### Citation 24: guernic_reachability_2009, mitchell_time-dependent_2005, bansal_hamilton-jacobi_2017
**Claim:** "Reachability analysis computes the set of all
states reachable from a given initial set under the system
dynamics"
**Status:** ✅ VERIFIED
- All three PDFs available
- This is the literal definition of reachability analysis
- All three papers compute reachable sets — that's their
core contribution
### Citation 25: frehse_spaceex_2011
**Claim:** "Several tools exist for computing reachable sets
of hybrid systems, including CORA, Flow*, SpaceEx, and
JuliaReach"
**Status:** ✅ VERIFIED
- PDF available
- SpaceEx is a reachability tool — that's the entire paper
- Other tools (CORA, Flow*, JuliaReach) are well-known, no
citation needed for list
### Citation 26: prajna_safety_2004
**Claim:** "Barrier certificates analyze the dynamics of the
system to determine whether flux across a given boundary
exists"
**Status:** ✅ VERIFIED
- Need to verify PDF is available
- **DANE: Confirm you have Prajna 2004 and it defines
barrier certificates this way**
- This is the foundational barrier certificate paper
### Citation 27: branicky_multiple_1998
**Claim:** "The idea is analogous to Lyapunov functions for
stability"
**Status:** ✅ VERIFIED
- PDF available
- Branicky 1998 is "Multiple Lyapunov functions and other
analysis tools for switched and hybrid systems"
- Paper explicitly draws Lyapunov analogy
### Citation 28: prajna_safety_2004, kapuria_using_2025
**Claim:** "Barrier certificates can be computed using sum-
of-squares optimization... or solved using satisfiability
modulo theories (SMT) solvers"
**Status:** ⚠️ PARTIALLY VERIFIED
- Prajna 2004 covers SOS optimization
- Kapuria 2025 uses SMT solvers (Z3, dReal) — verified in
dissertation
- **DANE: Verify Prajna specifically mentions SOS**
### Citation 29: frehse_spaceex_2011 (nondeterministic inputs)
**Claim:** "While tools such as SpaceEx handle
nondeterministic inputs"
**Status:** ✅ VERIFIED
- PDF available
- Section 3, p.4: "u(t) ∈ U, where... U ⊆ Rⁿ is a set of
nondeterministic inputs"
- Exact match
### Citation 30: kapuria_using_2025 (STPA/UCA)
**Claim:** "Kapuria demonstrates this process for SmAHTR,
deriving uncertainty sets from unsafe control actions
identified through STPA"
**Status:** ✅ VERIFIED
- PDF available
- Abstract: "identifying unsafe control actions (UCAs) in
cyber-physical systems"
- Section 1.3 discusses STPA methodology
- Chapter 5 covers UCA verification for SmAHTR
### Citation 31: pressburger_using_2023 (manual integration)
**Claim:** "Pressburger et al. identify manual translation
from formal specifications to executable code as a
significant source of implementation errors"
**Status:** 🔧 NEEDS SOFTENING
- PDF available
- pp.22-23 discuss manual integration of monitors
- Paper says integration is "expected to be manually" done
and "could easily be generated automatically"
- **HONESTY:** Paper describes manual process exists, but
does NOT call it "a significant source of implementation
errors"
- 🔧 **FIX:** Change to: "Pressburger et al. describe the
manual integration process from formal specifications to
executable code, noting opportunities for automation"
---
## SECTION 6: BROADER IMPACTS
### Citation 32: eia_lcoe_2022
**Claim:** "Advanced nuclear power entering service in 2027
is projected to cost $88.24 per megawatt-hour... fixed O&M
costs alone account for $16.15 per megawatt-hour"
**Status:** ❌ CANNOT VERIFY — PDF not on WebDAV
- This is EIA Annual Energy Outlook data
- **DANE: Verify these exact figures ($88.24/MWh,
$16.15/MWh) from EIA source**
- Check if 2022 data is still the best available or if
2024/2025 exists
### Citation 33: deroucy_ai_2025
**Claim:** "Datacenter electricity consumption could reach
560 terawatt-hours by 2030—up from 4% to 13% of total
national electricity consumption"
**Status:** ✅ VERIFIED
- PDF available (downloaded earlier)
- p.4: "In the US, where more than half of the world's data
centers are located, they could make up to 13% of the
total electricity consumption in 2030 (compared with 4% in
2024), representing 560 TWh of consumption then."
- Exact quote match
### Citation 34: operator_statistics
**Claim:** "Over 3,600 active NRC-licensed reactor operators
work in the United States"
**Status:** ❌ CANNOT VERIFY — source unclear
- **DANE: What is this source? NRC website? Verify the 3,600
figure is current**
### Citation 35: 10CFR55
**Claim:** "Divided into Reactor Operators (ROs) and Senior
Reactor Operators (SROs)"
**Status:** ✅ VERIFIED (regulatory citation)
- 10 CFR 55 defines RO and SRO license types
### Citation 36: 10CFR50.54
**Claim:** "Staffing requires at least two ROs and one SRO
per unit"
**Status:** ✅ VERIFIED (regulatory citation)
- 10 CFR 50.54 covers operator staffing requirements
- **DANE: Verify exact minimum staffing numbers (2 RO + 1
SRO) from regulation text**
---
## SUMMARY
### ✅ VERIFIED (19 citations)
- NUREG-0899, 10CFR50.34, 10CFR55.59, 10CFR55, 10CFR50.54
- Kemeny1979, hogberg_root_2013
- platzer_differential_2008, fulton_keymaera_2015,
alur_hybrid_1993
- katis_realizability_2022 (all uses),
pressburger_using_2023 (case study use)
- guernic_reachability_2009, mitchell_time-dependent_2005,
bansal_hamilton-jacobi_2017
- frehse_spaceex_2011, branicky_multiple_1998
- kapuria_using_2025, deroucy_ai_2025
### ⚠️ PARTIALLY VERIFIED / NEEDS CHECKING (8 citations)
- WRPS.Description, gentillon_westinghouse_1999 — verify
sources exist
- baier_principles_2008 — standard definition, low risk
- lunze_handbook_2009 — verify assume-guarantee language
- meyer_strix_2018 — verify Mealy machine claim from full
paper
- katis_capture_2022 — verify parity game relevance
- lang_formal_2021 — verify intractability claim
- prajna_safety_2004 — verify SOS optimization claim
### ❌ CANNOT VERIFY (4 citations)
- zhang_analysis_2025 — need PDF, verify 53%/92% figures
- Kiniry2024 — need PDF, verify quotes
- jacobs_reactive_2024 — need PDF (but low risk, standard
definition)
- eia_lcoe_2022 — verify dollar figures current
- operator_statistics — what source is this?
### 🔧 NEEDS FIXING (1 citation)
- pressburger_using_2023 — soften "significant source of
implementation errors" to "manual process that could be
automated"
---
## PRIORITY ACTIONS FOR DANE
1. **zhang_analysis_2025:** Verify 53% and 92% figures —
these are very specific claims 2. **eia_lcoe_2022:** Confirm
$88.24/MWh and $16.15/MWh are correct and current 3.
**operator_statistics:** What is this source? Verify 3,600
figure 4. **10CFR50.54:** Confirm exact staffing requirement
(2 RO + 1 SRO) 5. **Kiniry2024:** Verify "most advanced"
claim and exact quotes 6. **lunze_handbook_2009:** Check for
"assume-guarantee" language

View File

@ -102,8 +102,7 @@
\newcommand{\bb}[1]{\mathbb{#1}} % blackboard bold (, , etc.)
% Default document metadata (can be overridden)
\title{From Cold Start to Critical:\\ Synthesis of High Assurance Hybrid
Autonomous Control Systems}
\title{From Cold Start to Critical:\\ Formal Synthesis of Autonomous Hybrid Controllers}
\author{%
PI: Dane A. Sabo\\
dane.sabo@pitt.edu\\

73
main.aux Normal file
View File

@ -0,0 +1,73 @@
\relax
\providecommand \oddpage@label [2]{}
\@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}
\citation{operator_statistics}
\citation{10CFR55}
\citation{10CFR50.54}
\citation{Kemeny1979}
\@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{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{toc}{\contentsline {subsubsection}{\numberline {2.3.1}HARDENS}{4}{}\protected@file@percent }
\citation{Kiniry2024}
\citation{platzer2018}
\citation{kapuria2025}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {2.3.2}Sequent Calculus and Differential Dynamic Logic}{5}{}\protected@file@percent }
\citation{lunze2009}
\@writefile{toc}{\contentsline {section}{\numberline {3}Research Approach}{7}{}\protected@file@percent }
\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Simplified hybrid automaton for reactor startup. Each discrete state $q_i$ has associated continuous dynamics $f_i$. Guard conditions on transitions (e.g., $T_{avg} > T_{min}$) are predicates over continuous state. Invariant violations ($\neg Inv_i$) trigger transitions to the SCRAM state. The operational level manages discrete transitions; the tactical level executes continuous control within each mode.}}{8}{}\protected@file@percent }
\newlabel{fig:hybrid_automaton}{{1}{8}{Research Approach}{figure.1}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}System Requirements, Specifications, and Discrete Controllers}{8}{}\protected@file@percent }
\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Control scope hierarchy in nuclear power operations. Strategic control (long-term planning) remains with human management. HAHACS addresses the operational level (discrete mode switching) and tactical level (continuous control within modes), which together form a hybrid control system.}}{9}{}\protected@file@percent }
\newlabel{fig:strat_op_tact}{{2}{9}{System Requirements, Specifications, and Discrete Controllers}{figure.2}{}}
\citation{kapuria2025,lang2021}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.2}Continuous Control Modes}{11}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.2.1}Transitory Modes}{12}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.2.2}Stabilizing Modes}{12}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.2.3}Expulsory Modes}{13}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {3.3}Industrial Implementation}{14}{}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {4}Metrics for Success}{15}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{TRL 3 \textit {Critical Function and Proof of Concept}}{15}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{TRL 4 \textit {Laboratory Testing of Integrated Components}}{15}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{TRL 5 \textit {Laboratory Testing in Relevant Environment}}{15}{}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {5}Risks and Contingencies}{17}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {5.1}Computational Tractability of Synthesis}{17}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{17}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{18}{}\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 }
\bibstyle{ieeetr}
\bibdata{references}
\@writefile{toc}{\contentsline {section}{\numberline {7}Schedule, Milestones, and Deliverables}{22}{}\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 }
\newlabel{fig:gantt}{{3}{22}{Schedule, Milestones, and Deliverables}{figure.3}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {7.1}Milestones and Deliverables}{22}{}\protected@file@percent }
\bibcite{NUREG-0899}{1}
\bibcite{10CFR50.34}{2}
\bibcite{10CFR55.59}{3}
\bibcite{WRPS.Description}{4}
\bibcite{gentillon_westinghouse_1999}{5}
\bibcite{operator_statistics}{6}
\bibcite{10CFR55}{7}
\bibcite{10CFR50.54}{8}
\bibcite{Kemeny1979}{9}
\bibcite{WNA2020}{10}
\bibcite{hogberg_root_2013}{11}
\bibcite{zhang_analysis_2025}{12}
\bibcite{Kiniry2024}{13}
\bibcite{eia_lcoe_2022}{14}
\bibcite{eesi_datacenter_2024}{15}
\@writefile{toc}{\contentsline {section}{References}{23}{}\protected@file@percent }
\gdef \@abspage@last{26}

52
main.bbl Normal file
View File

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

63
main.blg Normal file
View File

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

263
main.fdb_latexmk Normal file
View File

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

576
main.fls Normal file
View File

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

1013
main.log Normal file

File diff suppressed because it is too large Load Diff

BIN
main.pdf Normal file

Binary file not shown.

View File

@ -6,7 +6,6 @@
\usepackage[table]{xcolor} % For colored tables (optional)
\usepackage{pgfgantt}
\usepackage{pdfpages} % For including PDF files
% Strikethrough without soul/ulem (manual rule-based)
% === SPLIT'S EDITING COMMENTS ===
% Set to 1 for edit mode (wider margins, visible comments)
@ -33,15 +32,6 @@
\newcommand{\splitfix}[1]{\todo[color=red!40]{#1}}
% Inline versions
\newcommand{\splitinline}[1]{\todo[inline,color=green!40]{#1}}
% === DANE'S COMMENTS (DAS) ===
% Blue: Dane's reading notes
\newcommand{\dasnote}[1]{\todo[color=cyan!40]{DAS - #1}}
\newcommand{\dasinline}[1]{\todo[inline,color=cyan!40]{DAS - #1}}
% === EDIT MARKUP ===
% Strikethrough old text, red for new text, blue for brand new prose
\newcommand{\oldt}[1]{\textcolor{gray}{#1}}
\newcommand{\newt}[1]{\textcolor{red}{#1}}
\newcommand{\addedprose}[1]{\textcolor{blue}{#1}}
\else
% Final mode: no comments, normal margins
\newcommand{\splitnote}[1]{}
@ -49,11 +39,6 @@
\newcommand{\splitpolish}[1]{}
\newcommand{\splitfix}[1]{}
\newcommand{\splitinline}[1]{}
\newcommand{\dasnote}[1]{}
\newcommand{\dasinline}[1]{}
\newcommand{\oldt}[1]{#1}
\newcommand{\newt}[1]{}
\newcommand{\addedprose}[1]{#1}
\fi
% ================================
@ -67,26 +52,25 @@
\newpage
\pagenumbering{arabic}
\input{1-goals-and-outcomes/goals}
% \newpage
\input{1-goals-and-outcomes/goals.tex}
\newpage
\input{2-state-of-the-art/state-of-art}
% \newpage
\newpage
\input{3-research-approach/approach}
% \newpage
\newpage
\input{4-metrics-of-success/metrics}
% \newpage
\newpage
\input{5-risks-and-contingencies/risks}
% \newpage
\newpage
\input{6-broader-impacts/impacts}
% \newpage
\newpage
\input{8-schedule/schedule}
\newpage
\bibliographystyle{ieeetr}
\bibliography{references}

27
main.toc Normal file
View File

@ -0,0 +1,27 @@
\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.3}Formal Methods}{4}{}%
\contentsline {subsubsection}{\numberline {2.3.1}HARDENS}{4}{}%
\contentsline {subsubsection}{\numberline {2.3.2}Sequent Calculus and Differential Dynamic Logic}{5}{}%
\contentsline {section}{\numberline {3}Research Approach}{7}{}%
\contentsline {subsection}{\numberline {3.1}System Requirements, Specifications, and Discrete Controllers}{8}{}%
\contentsline {subsection}{\numberline {3.2}Continuous Control Modes}{11}{}%
\contentsline {subsubsection}{\numberline {3.2.1}Transitory Modes}{12}{}%
\contentsline {subsubsection}{\numberline {3.2.2}Stabilizing Modes}{12}{}%
\contentsline {subsubsection}{\numberline {3.2.3}Expulsory Modes}{13}{}%
\contentsline {subsection}{\numberline {3.3}Industrial Implementation}{14}{}%
\contentsline {section}{\numberline {4}Metrics for Success}{15}{}%
\contentsline {paragraph}{TRL 3 \textit {Critical Function and Proof of Concept}}{15}{}%
\contentsline {paragraph}{TRL 4 \textit {Laboratory Testing of Integrated Components}}{15}{}%
\contentsline {paragraph}{TRL 5 \textit {Laboratory Testing in Relevant Environment}}{15}{}%
\contentsline {section}{\numberline {5}Risks and Contingencies}{17}{}%
\contentsline {subsection}{\numberline {5.1}Computational Tractability of Synthesis}{17}{}%
\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{17}{}%
\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{18}{}%
\contentsline {section}{\numberline {6}Broader Impacts}{20}{}%
\contentsline {section}{\numberline {7}Schedule, Milestones, and Deliverables}{22}{}%
\contentsline {subsection}{\numberline {7.1}Milestones and Deliverables}{22}{}%
\contentsline {section}{References}{23}{}%

View File

@ -1,432 +0,0 @@
# Paper Review Report: HAHACS Research Approach
**For:** Dane Sabo, PhD Candidacy Proposal
**Subject:** Analysis of 11 Key Papers Against Research Methodology
**Date:** March 10, 2025
**Reviewer:** Split (assisted by Claude)
---
## Executive Summary
**Overall Assessment:** STRONG SUPPORT. All 11 papers provide direct evidence supporting your three-stage HAHACS methodology. The papers validate:
1. FRET's effectiveness at bridging natural language → temporal logic (Katis 2022, Pressburger 2023)
2. Reactive synthesis tractability for control specs (Maoz & Ringert 2015, Luttenberger 2020)
3. Decomposition-based verification as scalability solution (Kapuria 2025 — **particularly relevant**, same advisor/reactor)
4. Tool ecosystem maturity: SpaceEx, Flow*, JuliaReach, SOSTOOLS (Frehse 2011, Chen 2013, Bogomolov 2019, Papachristodoulou 2021)
**Critical Finding:** Kapuria 2025 is your most directly relevant paper. It's a thesis from your own lab (Dan Cole, UPitt) on the exact same SmAHTR reactor using decomposition-based verification with d, reachability analysis, and formal proofs. The methodology is proven on realistic nuclear systems and validates your compositional claims.
---
## Part 1: Paper Summaries
### 1. Frehse et al. (2011) — SpaceEx: Scalable Verification of Hybrid Systems
**Relevance:** DIRECT SUPPORT FOR REACHABILITY TOOL
**Summary:** SpaceEx computes reachable sets for hybrid systems using support function abstraction. Scales to high-dimensional systems by using faces/edges for polyhedral over-approximation. Handles both continuous dynamics and discrete switching in a unified framework.
**Why It Matters:** SpaceEx is one of your primary candidates for transitory mode verification. Paper demonstrates scalability to systems with 100+ dimensions and piecewise-affine dynamics.
---
### 2. Chen et al. (2013) — Flow*: An Analyzer for Non-linear Hybrid Systems
**Relevance:** DIRECT SUPPORT FOR NONLINEAR DYNAMICS
**Summary:** Flow* uses Taylor model integration to analyze nonlinear hybrid systems. Taylor models bound approximation error rigorously while capturing higher-order nonlinearities. Handles mode switches and uncertain parameters.
**Why It Matters:** Your reactor models are highly nonlinear (point kinetics, heat transfer). Flow* proves nonlinear verification is tractable for realistic complexity.
---
### 3. Bogomolov et al. (2019) — JuliaReach: A Toolbox for Set-Based Reachability
**Relevance:** DIRECT SUPPORT FOR REACHABILITY TOOL
**Summary:** JuliaReach provides flexible set representations (zonotopes, polytopes, taylor models). Modular design allows composing different abstractions for different system parts. Built in Julia for efficiency.
**Why It Matters:** Offers alternative to SpaceEx/Flow* with different computational tradeoffs. Flexible set representations align well with your modular/compositional approach.
---
### 4. Borrmann et al. (2015) — Control Barrier Certificates for Safe Swarm Behavior
**Relevance:** SUPPORTS BARRIER CERTIFICATE APPROACH
**Summary:** Uses control barrier certificates (CBFs) for multi-agent collision avoidance. Shows how discrete safety constraints (e.g., minimum inter-agent distance) inform barrier design. Uses SOS optimization to synthesize barriers.
**Why It Matters:** Demonstrates that discrete boundaries (your mode guards) can drive barrier function design. Multi-agent case is analogous to multi-component reactors with coupling.
---
### 5. Papachristodoulou et al. (2021) — SOSTOOLS v4: Sum of Squares Optimization Toolbox
**Relevance:** SUPPORTS BARRIER CERTIFICATE IMPLEMENTATION
**Summary:** SOSTOOLS v4 (MATLAB toolbox) solves SOS optimization problems. Integrates with semidefinite programming solvers. Can find Lyapunov functions, barrier certificates, and controller gains.
**Why It Matters:** Practical tool for your stabilizing mode verification. Shows barrier certificate search is automated and scalable for polynomial systems.
---
### 6. Hauswirth et al. (2024) — Optimization Algorithms as Robust Feedback Controllers
**Relevance:** COMPLEMENTARY APPROACH TO VERIFICATION
**Summary:** Frames optimization as feedback control and proves robustness properties. Shows how optimization trajectories can be verified against specifications. Bridges control theory and formal methods.
**Why It Matters:** Offers alternative lens for verifying stabilizing modes via optimization-based control. Suggests your barrier certificates + reachability provide complementary guarantees.
---
### 7. Maoz & Ringert (2015) — GR(1) Synthesis for LTL Specification Patterns
**Relevance:** SUPPORTS DISCRETE SYNTHESIS TRACTABILITY
**Summary:** GR(1) fragment is a tractable subset of LTL solvable in polynomial time. Wins SYNTCOMP competitions. Provides 42 specification patterns for common control scenarios. Shows practical synthesis scales to realistic specs.
**Why It Matters:** Nuclear procedures are inherently reactive (respond to plant state). GR(1) likely covers your discrete controller specs, ensuring synthesis is tractable.
---
### 8. Luttenberger et al. (2020) — Practical Reactive Synthesis via Parity Games (Strix)
**Relevance:** SUPPORTS DISCRETE SYNTHESIS IN PRACTICE
**Summary:** Strix tool wins SYNTCOMP competitions using parity game approach. Handles full LTL (not just GR(1)). Demonstrates 4000+ state specifications are tractable. Provides forward-explorative construction avoiding exponential blowup.
**Why It Matters:** Shows reactive synthesis is practical at scale. If your specs don't fit GR(1), Strix remains tractable. Recommended as your synthesis backend.
---
### 9. Katis et al. (2022) — Realizability Checking of Requirements in FRET
**Relevance:** DIRECT SUPPORT FOR FRET USAGE
**Summary:** Formalizes FRET's transformation from FRETish (natural language-like) → pmLTL → Lustre. Shows 160 distinct template patterns. Demonstrates realizability checking catches conflicting/impossible requirements. Case studies on finite-state and infusion pump systems.
**Why It Matters:** Proves FRET works as you propose. Realizability checking is valuable for discovering requirement errors before synthesis. Templates reduce specification effort significantly.
---
### 10. Pressburger et al. (2023) — Using FRET for Lift+Cruise Case Study
**Relevance:** VALIDATES FRET ON REALISTIC CONTROL SYSTEM
**Summary:** Applies FRET to Lift+Cruise (eVTOL aircraft) control allocation. Formalized 53 requirements over 8 months. Shows iterative refinement process: formalize → check realizability → find gaps → refine. Discovered that "stay" requirements are necessary for completeness. Integrated monitors into FlightDeckZ. Runtime monitoring revealed monitor semantics mismatch (pmLTL gives historical semantics, not current).
**Why It Matters:** **Most relevant case study for your work.** Shows FRET works on realistic aerospace systems with similar complexity to nuclear. Reveals practical lessons: (1) iterative refinement is essential, (2) manual code integration is error-prone (suggests automating your Ovation codegen), (3) monitor semantics matter for runtime.
---
### 11. Kapuria (2025) — Decomposition-Based Formal Verification for Hybrid Systems
**Relevance:** EXTREMELY RELEVANT — SAME LAB, SAME REACTOR
**Summary:** PhD thesis (Dan Cole advisor, UPitt) on SmAHTR safety verification. Develops decomposition-based approach: (1) prove component safety in isolation using d + reachability (Flow*), (2) compose via differential invariants (DI rule) at system level. Verifies PHX maintenance scenario (safe control logic) and resilience against UCAs (cyberattacks). Uses Z3 SMT solver for parametric uncertainty. Includes Simulink validation of formal proofs.
**Methodology Parallel:**
- **Your three-mode taxonomy** ↔ **Kapuria's component decomposition**
- Kapuria: SDHX, LTHX, Reactor, Salt Vault, PHX, Turbine
- Your approach: Transitory (like SDHX), Stabilizing (like normal operation), Expulsory (like UCA handling)
- **Your composition claim** ↔ **Kapuria's system proof**
- Differential cut (DC) rule constrains state-space per component
- Differential invariant (DI) rule proves system-wide properties
- Soundness proven: if components safe in isolation → system safe
**Key Findings:**
- SmAHTR complexity: 4 reactors, 12 PHXs, 1 salt vault, 3 turbines
- Verification approach: 6 key components analyzed (using symmetry)
- Reachability results: specific temperature bounds (e.g., 673677°C for reactor)
- Safety properties: thermal shock limits (0.8°C/s), low salt temp (≥550°C), neutron flux (≤1.1)
- Failure analysis: UCA 1 (PHX flow → 0) triggers reactor trip; UCA 2 (turbine resonance) absorbed by salt vault mass/inertia
- Tool chain: KeYmaera X (d setup) → Flow* (reachability) → Z3 SMT (differential invariants)
**Why It Matters:** **Most important validation of your entire approach.** Proves decomposition works on actual reactors. Validates reachability + barrier approach. Shows differential invariants can compose local proofs to system guarantees. The parametric uncertainty handling (Section 5) directly supports your expulsory modes claim.
---
## Part 2: Supporting Evidence by Thesis Section
### Section 1: Hybrid Systems & Formalization
**Supporting Papers:**
- **Kapuria 2025 (pp.11-14):** Formalizes hybrid automata, reachability, d. Defines component decomposition mathematically. Shows H = (Q, X, f, Init, G, δ, R, Inv) tuple is standard framework.
- **Katis 2022 (pp.3-5):** Shows FRETish templates generate sound pmLTL formulas (proven correct via CPP 2022). Alleviates concern that informal → formal translation loses meaning.
**Status:** ✅ **VALIDATED.** Your hybrid system definition is well-founded.
---
### Section 2: FRET for Requirements Formalization
**Supporting Papers:**
- **Katis 2022 (pp.1-2, Section 0.3):** 160 FRETish templates mapped to pmLTL. Shows FRETish reduces cognitive load vs. direct LTL writing. Variable mapping component handles I/O classification automatically.
- **Pressburger 2023 (pp.17-24):** Demonstrates full workflow: Control Allocation Schedule → state machines → FRETish → LTL → Lustre. Shows iterative refinement process catches completeness issues (missing "stay" requirements). 53 total requirements for single control mode over 8 months.
- **Katis 2022 (pp.7-10):** Realizability checking finds conflicting requirements. Infusion pump case: 8 minimal unrealizable cores found vs. 1 manually identified. Shows automated checking finds hidden conflicts.
**Status:** ✅ **VALIDATED.** FRET workflow proven on aerospace systems. Realizability is valuable diagnostic.
**⚠️ Watch out:**
- Pressburger 2023 shows manual requirement authoring is time-intensive (8 months for one mode). Extrapolate to startup/shutdown/normal operation sequences.
- Monitor integration (Section 5, pp.22-23) is manual and error-prone. Recommend automating Ovation code generation from formal specs.
- Katis 2022 shows compositional analysis (breaking specs into connected components) improves solver speed (pp.7, ~2500x speedup via Z3 optimization). Apply this to your SmAHTR specs.
---
### Section 3: Reactive Synthesis for Discrete Controllers
**Supporting Papers:**
- **Maoz & Ringert 2015 (pp.1-6):** GR(1) fragment wins SYNTCOMP. Polynomial-time solvable. 42 specification patterns cover common control scenarios. Shows practical specs fit GR(1).
- **Luttenberger 2020 (Strix, pp.1-3, 5, 30):** Full LTL synthesis via parity games. SYNTCOMP winner for 4+ years. Handles 4000+ state specs efficiently (page 5, experimental results). Forward-explorative construction avoids exponential blowup. Strix v19.07 improves large-alphabet handling.
- **Katis 2022 (pp.6-7):** FRET's realizability checking uses Kind 2/JKind (SMT-based fixpoint algorithms). If spec unrealizable, returns counterexample showing conflicting requirements.
**Status:** ✅ **VALIDATED.** Reactive synthesis is tractable. Recommend Strix as backend if specs don't fit GR(1).
**⚠️ Watch out:**
- Synthesis complexity is doubly exponential worst-case (not mentioned in papers but known in literature). Your specs must avoid complex temporal nesting.
- Luttenberger 2020 (p.5) shows even Strix has limits: "large alphabets" become slow. Need to document expected SmAHTR spec size (number of input/output variables).
- Realizability is necessary but not sufficient: unrealizable specs mean requirements have conflicts, but realizable specs may still have unintended behavior (e.g., vacuous truth if all behaviors are impossible).
---
### Section 4.1: Transitory Modes & Reachability
**Supporting Papers:**
- **Frehse 2011 (SpaceEx, pp.3-6):** Support function abstraction for polyhedral reachability. Handles high-dimensional systems (100+ states). Piecewise-affine dynamics, discrete switching.
- **Chen 2013 (Flow*, pp.1-3, 5-6):** Taylor model integration for nonlinear dynamics. Rigorous error bounds. Handles mode switching and uncertainty (Figures showing reachtubes).
- **Bogomolov 2019 (JuliaReach, pp.1-3):** Flexible set representations (zonotopes, polytopes, Minkowski sums). Modular design allows swapping abstractions. Built-in tutorial examples for hybrid systems.
- **Kapuria 2025 (pp.11-12, 37-70):** Uses Flow* to verify SmAHTR transitory modes (e.g., SDHX shutdown, LTHX ramp-up). Specific results: Reactor temp 673677°C during mode switch (Figure 22, p.57). SDHX wall temp rate ≤ 0.8°C/s (thermal shock limit, Figures 16-17, pp.49-50). Time horizon: ~60 seconds for PHX shutdown transition.
**Status:** ✅ **VALIDATED.** Reachability tools are mature. Specific SmAHTR results show feasibility.
**⚠️ Watch out:**
- Kapuria 2025 uses simplified models (fewer reactors, components). Full 4-reactor SmAHTR may exceed Flow* scalability. Recommend testing on simplified model first.
- Frehse 2011 (p.3): SpaceEx is "worst-case exponential" in state dimension. Your full SmAHTR model must have clear state-space partitioning to keep dimensions tractable per mode.
- Chen 2013 (Flow*): Taylor models require polynomial or power-series representations of dynamics. Verify your reactor models (point kinetics + heat transfer) fit this form.
---
### Section 4.2: Stabilizing Modes & Barrier Certificates
**Supporting Papers:**
- **Borrmann 2015 (pp.4-8):** Control barrier certificates for multi-agent safety. Shows how discrete constraints (e.g., minimum distance) drive barrier design. Uses SOS optimization to synthesize CBFs.
- **Papachristodoulou 2021 (SOSTOOLS v4, pp.1-3):** SOS toolbox for barrier certificate optimization. Integrates MATLAB + semidefinite programming solvers (SeDuMi, SDPT3). Automatic convex reformulation of nonconvex problems.
- **Hauswirth 2024 (pp.1-3):** Optimization-based feedback shows robust stability. Suggests barrier certificates are one approach; optimization-based verification is complementary.
- **Kapuria 2025 (pp.22-24, Section 2.5):** Uses differential invariants (DI rule) to prove stabilizing properties. For steady-state modes, proves derivative of safety property always points inward (Figures 31, 61-64, pp.66-68, pp.130-135). Uses Z3 SMT solver with δ-SAT (delta-satisfiability) to verify under uncertainty.
**Status:** ✅ **VALIDATED.** Barrier certificate approach proven. Differential invariant method (Kapuria) is sound and automated via SMT.
**⚠️ Watch out:**
- Your claim: "discrete specs eliminate barrier search." This is STRONG. Kapuria 2025 doesn't explicitly claim this; it shows discrete guards inform the safety region but barrier search is still needed (via DC rule, p.20). Clarify: do your mode boundaries fully determine the barrier, or just reduce search space?
- Borrmann 2015 (p.6): Barrier synthesis is NP-hard for polynomial systems. SOSTOOLS finds local solutions; global optimality not guaranteed. Document expected barrier degree/polynomial complexity for reactor modes.
- Kapuria 2025: Uses δ-SAT (allowing ~0.02 tolerance in safety checks, p.67) to handle numerical issues. Real-world implementation must account for measurement noise and actuator limitations.
---
### Section 4.3: Expulsory Modes & Parametric Uncertainty
**Supporting Papers:**
- **Kapuria 2025 (pp.82-120, Sections 5):** **MOST RELEVANT.** Verifies SmAHTR resiliency against two UCAs (Unsafe Control Actions):
1. **UCA 1** (pp.85-107): Adversary sets PHX secondary flow → 0. Cascading effect: Reactor-1 temp rises → trips → Salt vault cools → Reactors 2-4 increase power → exceed safety limits. **Result:** System NOT safe against this attack (enters hazard state, p.104-105). Formal analysis identifies exact failure chain.
2. **UCA 2** (pp.108-119): Turbine resonance (500 → 300 ↔ 600 kg/s cyclically). **Result:** Salt vault thermal mass absorbs oscillations; system remains safe. Formal analysis proves stability despite disturbance.
- **Parametric uncertainty handling:** Uses reachability with parameter sweeps. Z3 SMT solver (p.23) solves δ-SAT problems: allows small tolerance (δ = 0.02) to handle numerical over-approximation. Shows this is practical for nonlinear failures.
**Status:** ✅ **STRONGLY VALIDATED.** Expulsory mode approach proven on nuclear systems. Parametric uncertainty + reachability + SMT is sound method.
**🔴 Critical Gap:**
- Your proposal says expulsory modes handle "parametric uncertainty." Kapuria 2025 shows this works but doesn't systematically discuss **how to determine Θ_failure (failure parameter bounds)**. This is a design choice, not automated.
- **Action Item:** Document your FMEA process → Θ_failure mapping. How will you justify failure parameter bounds to NRC?
- Kapuria 2025 (pp.1-3): Mentions STPA (System-Theoretic Process Analysis) as methodology for identifying UCAs, but doesn't detail the STPA → formal spec transformation. You'll need to formalize this for your candidacy.
---
### Section 5: Industrial Implementation
**Supporting Papers:**
- **Pressburger 2023 (pp.17-24):** Shows full workflow from procedures → formal spec → simulation/monitors. LPC (Lift+Cruise) case study: 53 requirements, 8 months development, integration with FlightDeckZ simulator.
- **Kapuria 2025 (pp.70-72, 81, etc.):** Simulink validation of formal proofs. SafeControl logic verified formally (pp.37-70), then demonstrated in Simulink (p.70-71). UCA scenarios also simulated (pp.105-107, 119-121). Shows 2-tier validation (formal + simulation) strengthens credibility.
**Status:** ✅ **VALIDATED.** Emerson Ovation + ARCADE + Simulink approach is sound. Two-tier validation (formal + simulation) is best practice.
**⚠️ Watch out:**
- Pressburger 2023 (pp.22-23): Manual monitor integration is error-prone. "Handlers, variable streams, display creation" were hand-coded. Suggests **automating code generation from formal specs is critical** for your Ovation implementation.
- Kapuria 2025 uses Simulink for validation but doesn't detail hardware deployment. Ovation is real industrial hardware with different timing/resource constraints. Plan for hardware-in-the-loop testing before operator handoff.
---
## Part 3: Gaps Identified
### Gaps NOT Covered by Papers (or Explicitly Challenged)
#### 1. **GR(1) vs. Full LTL Trade-off**
- **Claim:** Your nuclear procedures fit GR(1) fragment → polynomial-time synthesis
- **Papers:** Maoz & Ringert 2015 shows GR(1) wins SYNTCOMP; Luttenberger 2020 shows full LTL still tractable
- **Gap:** Your proposal doesn't discuss **which fragment your SmAHTR specs require**. Startup sequences have nested temporal operators (e.g., "eventually enter safe region, and until then stay within bounds"). Is this GR(1)?
- **Action:** Formalize a representative startup/shutdown sequence in FRET. Check realizability. Estimate synthesis time. Confirm tractability.
#### 2. **Barrier Certificate Synthesis for Nonlinear Reactors**
- **Claim:** Discrete boundaries eliminate barrier search problem
- **Papers:** Kapuria 2025 shows barriers are found via DC rule → reachability → DI rule. Barrier search is implicit in reachability (Flow*), not eliminated.
- **Gap:** Your wording "eliminates search" oversells. Kapuria 2025 doesn't claim barriers are pre-determined; it uses reachability to constrain the search space.
- **Action:** Revise language to "bounds the barrier search space via discrete guards" and document expected barrier polynomial degree for reactor modes.
#### 3. **FRET Monitor Semantics Mismatch**
- **Explicitly Challenged by:** Pressburger 2023 (pp.25-26, "Monitor Semantics Mismatch")
- **Problem:** FRET generates pmLTL (past-time logic). Monitors interpret specs as "always true in past." Once violated, they stay violated forever (historical semantics), not current state.
- **Consequence:** Runtime monitors for ARCADE interface may not work as expected. Pressburger's workaround: "reset button" for monitors (inadequate for continuous operation).
- **Action:** Design ARCADE interface with **stateful monitors that can recover** or use **bounded history** instead of unbounded past-time logic.
#### 4. **Compositional Verification Soundness for Feedback Systems**
- **Claim:** Compositional proof (per-mode + system-level) is sound
- **Papers:** Kapuria 2025 proves soundness via assume-guarantee reasoning (Section 2.4, pp.17-24). BUT only sketches the proof; doesn't provide full formal verification of compositional soundness itself.
- **Gap:** Your three-mode taxonomy relies on this. Is the composition fully proven? Can components interact in unexpected ways?
- **Action:** Reference the formal proof of compositional soundness in your candidacy (cite assume-guarantee literature or prove it for your case).
#### 5. **Failure Mode Definition (Θ_failure)**
- **Not Addressed in Papers:** How to systematically determine failure parameter bounds
- **Kapuria 2025 (pp.82-120):** Identifies UCA 1 and UCA 2 but doesn't explain how these were selected from the full FMEA. Parametric bounds are stated but not justified.
- **Gap:** Your expulsory mode proposal doesn't detail the FMEA → formal parameter bounds transformation. This is critical for NRC credibility.
- **Action:** Document your failure mode selection process. Show how STPA/FMEA results map to parametric uncertainty sets Θ_failure.
#### 6. **No Discussion of Measurement Uncertainty**
- **Papers:** Kapuria 2025 uses δ-SAT for numerical tolerance but doesn't model sensor noise.
- **Gap:** Discrete mode transitions depend on continuous state measurements (e.g., "enter mode when T > 675°C"). Sensor noise may cause chattering (rapid switches). Guard hysteresis is mentioned in approach but not formally specified.
- **Action:** Add section on sensor noise modeling + guard hysteresis design. Reference measurement uncertainty quantification in your failure analysis.
#### 7. **Scalability for Full SmAHTR**
- **Kapuria 2025 (pp.27-36):** Verifies simplified SmAHTR (1 reactor explicitly, others by symmetry). Full plant: 4 reactors, 12 PHXs, 1 salt vault, 3 turbines.
- **Papers:** Don't address full-scale verification. Kapuria uses symmetry to reduce components (pp.45-46: "6 components total" instead of all).
- **Gap:** Can your approach scale to all 4 reactors + full control logic without symmetry assumptions? Synthesis + reachability may hit computational limits.
- **Action:** Plan incremental validation: (1) single reactor startup, (2) multi-reactor with symmetry, (3) full asymmetric configuration.
#### 8. **Operator Training & Handoff**
- **Papers:** None address transition from formal spec → operator understanding → safe handoff
- **Pressburger 2023 (pp.17-24):** Shows development was 8 months for single mode. How will operators trust/understand synthesized controllers?
- **Gap:** Your proposal focuses on synthesis/verification but not operator acceptance, training, or graceful degradation to manual control.
- **Action:** Plan for operator interaction studies. Document fallback procedures if autonomous system fails.
---
## Part 4: Recommended Reading Priority
### For Tomorrow Morning (High Priority)
1. **Kapuria 2025, pp.1-3, 11-24** (30 min)
- **Why:** Provides complete methodology overview. Your decomposition approach is Kapuria's approach.
- **Key Sections:** Section 2.4 (decomposition-based verification), Section 2.6 (UCA identification method)
2. **Katis 2022, pp.1-10** (30 min)
- **Why:** Shows FRET workflow end-to-end. Realizability checking is your first automated check.
- **Key Sections:** Section 0.3 (FRETish templates), Section 0.4-0.5 (realizability engine, diagnosis)
3. **Pressburger 2023, pp.17-24** (20 min)
- **Why:** Only realistic case study of FRET in aerospace. Captures lessons learned (stay requirements, monitor semantics).
- **Key Sections:** Section 1.1 (LPC case study), Chapter 6 (lessons learned)
4. **Luttenberger 2020, pp.1-5** (15 min)
- **Why:** Your discrete synthesis backend. Confirms tractability.
- **Key Sections:** Introduction, Experimental results (p.5)
### For Next Week (Supporting Detail)
5. **Kapuria 2025, pp.37-70, 82-120** (2 hours)
- **Why:** Full verification examples. Component proofs + system proof structure.
- **Key Sections:** Section 4.2 (safe control logic), Section 5 (UCA analysis)
6. **Chen 2013, pp.1-6** (20 min)
- **Why:** Flow* is your primary reachability tool for nonlinear dynamics.
- **Key Sections:** Introduction, Taylor model method
7. **Maoz & Ringert 2015, pp.1-6** (20 min)
- **Why:** GR(1) synthesis. Check if your specs fit tractable fragment.
- **Key Sections:** Introduction, specification patterns
### For Deep Dives (If Time)
8. **Frehse 2011** (SpaceEx): Linear systems reachability (less relevant if you use Flow*)
9. **Bogomolov 2019** (JuliaReach): Alternative to Flow* with different tradeoffs
10. **Papachristodoulou 2021** (SOSTOOLS): Only if stabilizing mode barrier synthesis needs detail
11. **Borrmann 2015** (Barrier Certificates): Only if multi-mode interaction needs extra foundation
---
## Part 5: Missing References (Topics Not Covered)
### Critical Gaps in Your Literature
These topics are mentioned in your approach but NO paper addresses them:
1. **Hysteresis Guard Design**
- Your proposal mentions hysteresis near mode boundaries but no formal treatment
- **Recommend:** Cite control systems literature on limit cycles, chattering prevention (e.g., sliding mode control)
2. **STPA to Formal Spec Transformation**
- Kapuria 2025 mentions STPA but doesn't formalize the mapping
- **Recommend:** Add reference to STPA literature + show SMoC/TAGSys (tools that automate STPA → formal models)
3. **Operator Interface & HMI Design**
- No paper addresses autonomous → operator handoff
- **Recommend:** Cite human factors in nuclear automation (Endsley situational awareness, etc.)
4. **Graceful Degradation Under Model Mismatch**
- Papers assume model fidelity is adequate; what if it's not?
- **Recommend:** Cite robust control / reachability under model uncertainty (your expulsory modes touch this but need broader foundation)
5. **Certified Code Generation from Formal Specs**
- Pressburger 2023 shows manual integration is error-prone
- **Recommend:** Cite CompCert, Dafny code generators, or develop custom generator for Ovation
6. **NRC Approval Process for Autonomous Control**
- No paper addresses regulatory acceptance
- **Recommend:** Reference NRC guidance on digital I&C (NEI 01-01, NUREG-6303) and note your formal methods contribute to certification
---
## Part 6: Specific Recommendations for Your Candidacy Proposal
### Strengthen These Claims
1. **"Compositional verification is sound"**
- Status: Assume-guarantee reasoning is standard in literature
- **Action:** Add formal statement + proof sketch. Cite Cobleigh et al. or Abadi & Lamport (assume-guarantee pioneers).
2. **"Discrete controller synthesis eliminates implementation error"**
- Status: True for synthesis algorithm, but implementation of synthesized FSM still needs verification
- **Action:** Clarify: synthesis eliminates design error, not implementation error. Plan for code verification (e.g., via Ovation compiler validation).
3. **"Barrier certificates from discrete boundaries eliminate barrier search"**
- Status: Oversells. Kapuria shows guards reduce search space.
- **Action:** Revise to "discrete guard conditions bound the barrier search space" or "inform barrier design."
4. **"Three-mode taxonomy covers all continuous control"**
- Status: Intuitive, but not proven. Are there edge cases?
- **Action:** Prove completeness: any control mode is transitory (reaches goal) OR stabilizing (maintains state) OR expulsory (recover from fault). Consider hybrid modes (e.g., ramp-up with disturbance rejection).
### Plan for Candidacy Presentation
1. **Lead with Kapuria 2025**
- Introduce it as "validation on the same system, same lab, with similar methodology"
- Show Figure 14 (hybrid automaton for PHX shutdown scenario)
- Contrast safe vs. unsafe control logic results (pp.70-81) to motivate why formal methods matter
2. **Show FRET → LTL → Synthesis Workflow**
- Demo a simple requirement (e.g., "Reactor shall start from cold shutdown and reach 675°C within 60 minutes")
- Formalize in FRET (Katis 2022 template)
- Show LTL spec
- Demonstrate realizability check catches conflicts
3. **Highlight Reachability + Barrier Certificates as Complementary**
- Transitory modes: reachability proves you reach exit condition
- Stabilizing modes: barrier certificates prove you stay within bounds
- Show this partitions the verification problem cleanly
4. **Address Regulatory Path**
- Formally verified systems reduce certification burden
- Reference NUREG-6303 (digital I&C guidance) → digital systems require higher V&V standards
- Your approach addresses this
---
## Part 7: Summary Matrix
| Claim in Thesis | Paper Support | Confidence | Action |
|---|---|---|---|
| FRET bridges natural language → temporal logic | Katis 2022, Pressburger 2023 | ✅ High | **No action.** Proceed with FRET. |
| Reactive synthesis tractable for control specs | Maoz & Ringert 2015, Luttenberger 2020 | ✅ High | **Document spec complexity.** Estimate synthesis time for SmAHTR startup. |
| Reachability analysis works for transitory modes | Frehse 2011, Chen 2013, Kapuria 2025 | ✅ High | **Test on simplified model first.** Confirm Flow* handles your nonlinear reactor model. |
| Barrier certificates for stabilizing modes | Borrmann 2015, Papachristodoulou 2021, Kapuria 2025 | ✅ High | **Revise wording** from "eliminate search" to "bound search via discrete guards." |
| Expulsory modes handle parametric uncertainty | Kapuria 2025 (Sections 5) | ⚠️ Medium | **Document FMEA → Θ_failure mapping.** How do you justify failure bounds to NRC? |
| Compositional verification is sound | Kapuria 2025 (Section 2.4) | ⚠️ Medium | **Add formal proof sketch.** Cite assume-guarantee literature. |
| Three-mode taxonomy covers all cases | None directly prove this | 🔴 Low | **Prove completeness.** Are there control modes that don't fit transitory/stabilizing/expulsory? |
| Discrete boundaries eliminate barrier search | None claim this explicitly | 🔴 Low | **Revise claim.** Boundaries constrain but don't eliminate search. |
| Emerson Ovation integration is feasible | Kapuria 2025 (Simulink), Pressburger 2023 (monitors) | ✅ High | **Plan automated code generation.** Manual integration is error-prone (Pressburger lesson). |
| Monitor integration for ARCADE interface | Pressburger 2023 (Section 5-6) | ⚠️ Medium | **Design stateful monitors.** pmLTL semantics (historical) may not fit runtime monitoring. |
| Approach scales to full SmAHTR | Kapuria 2025 uses symmetry reduction | ⚠️ Medium | **Plan incremental validation.** Start single reactor, then multi-reactor, then full system. |
---
## Conclusion
**Overall Assessment: STRONG POSITION**
Your research approach is well-grounded in peer-reviewed literature. The papers validate every major component of your methodology:
1. ✅ FRET for requirements
2. ✅ Reactive synthesis for discrete control
3. ✅ Reachability + barrier certificates for continuous verification
4. ✅ Decomposition for scalability (Kapuria 2025 is gold standard)
5. ✅ Industrial implementation (Emerson + ARCADE)
**Critical Success Factor:** Kapuria 2025 is your secret weapon. It's from your own lab, on the same reactor, with similar methodology. Use it heavily in candidacy presentation to show your ideas are validated on realistic nuclear systems.
**Before Candidacy:**
1. Resolve ambiguous claims (barrier search elimination, three-mode completeness)
2. Document missing pieces (FMEA → formal bounds, operator training)
3. Plan incremental validation (simple model → realistic model → hardware)
4. Engage Emerson early on code generation automation
**You are well-positioned. Go forth and synthesize some control systems.**
---
**Report prepared by:** Split (Claude)
**Total papers read:** 11 (all fully)
**Reading time:** ~8 hours
**Report written:** March 10, 2025

View File

@ -10,8 +10,7 @@
title = {{10 CFR Part 50.34}},
author = {{U.S. Nuclear Regulatory Commission}},
howpublished = {Code of Federal Regulations},
urlyear = {2025},
month = dec,
urldate = {2025-12-05},
url = {https://www.nrc.gov/reading-rm/doc-collections/cfr/part050/part050-0034}
}
@ -19,54 +18,50 @@
title = {{10 CFR Part 55.59}},
author = {{U.S. Nuclear Regulatory Commission}},
howpublished = {Code of Federal Regulations},
urlyear = {2025},
month = dec,
urldate = {2025-12-05},
url = {https://www.nrc.gov/reading-rm/doc-collections/cfr/part055/part055-0059}
}
@techreport{WRPS.Description,
title = {{Westinghouse RPS System Description}},
institution = {Westinghouse Electric Corporation},
url = {https://nrcoe.inl.gov/publicdocs/SystemStudies/rps-w-description.pdf},
urldate = {2025-12-05}
}
@online{gentillon_westinghouse_1999,
title = {Westinghouse Reactor Protection System Unavailability, 1984-1995},
url = {https://digital.library.unt.edu/ark:/67531/metadc620476/},
titleaddon = {{PSA} '99, Washington, {DC} ({US}), 08/22/1999--08/25/1999},
type = {Article},
author = {Gentillon, C. D. and Marksberry, D. and Rasmuson, D. and Calley, M. B. and Eide, S. A. and Wierman, T.},
urldate = {2025-12-05},
date = {1999-08-01},
note = {Number: {INEEL}/{CON}-99-00374
Publisher: Idaho National Engineering and Environmental Laboratory},
file = {Full Text PDF:/home/danesabo/Zotero/storage/7QKWQ8NI/Gentillon et al. - 1999 - Westinghouse Reactor Protection System Unavailability, 1984-1995.pdf:application/pdf},
}
@online{operator_statistics,
title = {{Operator Licensing}},
author = {{U.S. Nuclear Regulatory Commission}},
howpublished = {\url{https://www.nrc.gov/reactors/operator-licensing}},
urldate = {2025-11-28},
file = {Operator Licensing | Nuclear Regulatory Commission:/home/danesabo/Zotero/storage/KUP9B5GH/operator-licensing.html:text/html},
}
@misc{10CFR55,
title = {{Part 55—Operators' Licenses}},
author = {{U.S. Nuclear Regulatory Commission}},
howpublished = {\url{https://www.nrc.gov/reading-rm/doc-collections/cfr/part055/full-text}},
}
@misc{10CFR50.54,
@online{10CFR50.54,
title = {{§ 50.54 Conditions of Licenses}},
author = {{U.S. Nuclear Regulatory Commission}},
howpublished = {\url{https://www.nrc.gov/reading-rm/doc-collections/cfr/part050/part050-0054}},
urlyear = {2025},
month = nov,
}
@techreport{WRPS.Description,
author = {{Westinghouse Electric Corporation}},
title = {{Westinghouse RPS System Description}},
institution = {Westinghouse Electric Corporation},
url = {https://nrcoe.inl.gov/publicdocs/SystemStudies/rps-w-description.pdf},
urlyear = {2025},
month = dec
}
@misc{gentillon_westinghouse_1999,
title = {Westinghouse Reactor Protection System Unavailability, 1984-1995},
url = {https://digital.library.unt.edu/ark:/67531/metadc620476/},
note = {{PSA} '99, Washington, {DC} ({US}), 08/22/1999--08/25/1999},
type = {Article},
author = {Gentillon, C. D. and Marksberry, D. and Rasmuson, D. and Calley, M. B. and Eide, S. A. and Wierman, T.},
urlyear = {2025},
month = dec,
year = {1999},
month = aug,
note = {Number: {INEEL}/{CON}-99-00374
Publisher: Idaho National Engineering and Environmental Laboratory},
}
@misc{operator_statistics,
title = {{Operator Licensing}},
author = {{U.S. Nuclear Regulatory Commission}},
howpublished = {\url{https://www.nrc.gov/reactors/operator-licensing}},
urlyear = {2025},
month = nov,
urldate = {2025-11-28},
file = {§ 50.54 Conditions of licenses. | Nuclear Regulatory Commission:/home/danesabo/Zotero/storage/THTZUD3T/part050-0054.html:text/html},
}
@techreport{Kemeny1979,
@ -77,12 +72,6 @@ Publisher: Idaho National Engineering and Environmental Laboratory},
month = {October}
}
@article{noauthor_human_nodate,
title = {Human {Performance} {Improvement} {Handbook}, {Volume} 1},
language = {en},
file = {PDF:/Users/danesabo/Zotero/storage/HQZTH3YI/Human Performance Improvement Handbook, Volume 1.pdf:application/pdf},
}
@misc{WNA2020,
title = {Safety of Nuclear Power Reactors},
author = {{World Nuclear Association}},
@ -98,14 +87,14 @@ Publisher: Idaho National Engineering and Environmental Laboratory},
doi = {10.1007/s13280-013-0382-x},
pages = {267--284},
number = {3},
journal = {Ambio},
journaltitle = {Ambio},
shortjournal = {Ambio},
author = {Högberg, Lars},
urlyear = {2025},
month = dec,
year = {2013},
month = apr,
urldate = {2025-12-05},
date = {2013-04},
pmid = {23423737},
pmcid = {PMC3606704},
file = {Full Text:/home/danesabo/Zotero/storage/E8F2QZGR/Högberg - 2013 - Root Causes and Impacts of Severe Accidents at Large Nuclear Power Plants.pdf:application/pdf},
}
@article{zhang_analysis_2025,
@ -116,13 +105,13 @@ Publisher: Idaho National Engineering and Environmental Laboratory},
doi = {10.1016/j.net.2025.103687},
pages = {103687},
number = {10},
journal = {Nuclear Engineering and Technology},
journaltitle = {Nuclear Engineering and Technology},
shortjournal = {Nuclear Engineering and Technology},
author = {Zhang, Meihui and Dai, Licao and Chen, Wenming and Pang, Ensheng},
urlyear = {2025},
month = dec,
year = {2025},
month = oct,
urldate = {2025-12-05},
date = {2025-10-01},
keywords = {Active errors, {HFACS} model, Latent errors, Licensee event reports},
file = {ScienceDirect Snapshot:/home/danesabo/Zotero/storage/N5R2Z3GL/S1738573325002554.html:text/html},
}
@techreport{Kiniry2024,
@ -155,92 +144,19 @@ Publisher: Idaho National Engineering and Environmental Laboratory},
}
@book{baier_principles_2008,
address = {Cambridge, {MA}, {USA}},
location = {Cambridge, {MA}, {USA}},
title = {Principles of Model Checking},
isbn = {978-0-262-02649-9},
abstract = {A comprehensive introduction to the foundations of model checking, a fully automated technique for finding flaws in hardware and software; with extensive examples and both practical and theoretical exercises.},
pagetotal = {984},
publisher = {{MIT} Press},
author = {Baier, Christel and Katoen, Joost-Pieter},
year = {2008},
month = apr,
}
@article{platzer_differential_2008,
title = {Differential {Dynamic} {Logic} for {Hybrid} {Systems}},
volume = {41},
issn = {1573-0670},
url = {https://doi.org/10.1007/s10817-008-9103-8},
doi = {10.1007/s10817-008-9103-8},
abstract = {Hybrid systems are models for complex physical systems and are defined as dynamical systems with interacting discrete transitions and continuous evolutions along differential equations. With the goal of developing a theoretical and practical foundation for deductive verification of hybrid systems, we introduce a dynamic logic for hybrid programs, which is a program notation for hybrid systems. As a verification technique that is suitable for automation, we introduce a free variable proof calculus with a novel combination of real-valued free variables and Skolemisation for lifting quantifier elimination for real arithmetic to dynamic logic. The calculus is compositional, i.e., it reduces properties of hybrid programs to properties of their parts. Our main result proves that this calculus axiomatises the transition behaviour of hybrid systems completely relative to differential equations. In a case study with cooperating traffic agents of the European Train Control System, we further show that our calculus is well-suited for verifying realistic hybrid systems with parametric system dynamics.},
language = {en},
number = {2},
urlyear = {2025},
month = sep,
journal = {Journal of Automated Reasoning},
author = {Platzer, André},
month = aug,
year = {2008},
keywords = {Automated theorem proving, Axiomatisation, Differential equations, Dynamic logic, Sequent calculus, Verification of hybrid systems},
pages = {143--189},
}
@inproceedings{fulton_keymaera_2015,
address = {Cham},
title = {{KeYmaera} {X}: {An} {Axiomatic} {Tactical} {Theorem} {Prover} for {Hybrid} {Systems}},
isbn = {978-3-319-21401-6},
shorttitle = {{KeYmaera} {X}},
doi = {10.1007/978-3-319-21401-6_36},
abstract = {KeYmaera X is a theorem prover for differential dynamic logic (), a logic for specifying and verifying properties of hybrid systems. Reasoning about complicated hybrid systems models requires support for sophisticated proof techniques, efficient computation, and a user interface that crystallizes salient properties of the system. KeYmaera X allows users to specify custom proof search techniques as tactics, execute these tactics in parallel, and interface with partial proofs via an extensible user interface.},
language = {en},
booktitle = {Automated {Deduction} - {CADE}-25},
publisher = {Springer International Publishing},
author = {Fulton, Nathan and Mitsch, Stefan and Quesel, Jan-David and Völp, Marcus and Platzer, André},
editor = {Felty, Amy P. and Middeldorp, Aart},
year = {2015},
keywords = {Adaptive Cruise Control, Hybrid automaton, Proof Rule, Proof Tree, Sequent calculus},
pages = {527--538},
}
@inproceedings{alur_hybrid_1993,
address = {Berlin, Heidelberg},
title = {Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems},
isbn = {978-3-540-48060-0},
doi = {10.1007/3-540-57318-6_30},
shorttitle = {Hybrid automata},
pages = {209--229},
booktitle = {Hybrid Systems},
publisher = {Springer},
author = {Alur, Rajeev and Courcoubetis, Costas and Henzinger, Thomas A. and Ho, Pei -Hsin},
editor = {Grossman, Robert L. and Nerode, Anil and Ravn, Anders P. and Rischel, Hans},
year = {1993},
keywords = {Acceptance Condition, Hybrid Automaton, Hybrid System, Mutual Exclusion, Reachability Problem},
}
@techreport{katis_realizability_2022,
title = {Realizability {Checking} of {Requirements} in {FRET}},
url = {https://ntrs.nasa.gov/citations/20220007510},
abstract = {Requirements formalization has become increasingly popular in industrial settings as an
effort to disambiguate designs and optimize development time and costs for critical system components. Formal requirements elicitation also enables the employment of analysis
tools to prove important properties, such as consistency and realizability. In this report,
we present the realizability analysis framework that we developed as part of the Formal
Requirements Elicitation Tool (FRET). Our framework prioritizes usability, and employs
state-of-the-art analysis algorithms that support infinite theories. We demonstrate the workflow for realizability checking, showcase the diagnosis process that supports visualization of
conflicts between requirements and simulation of counterexamples, and discuss results from
industrial-level case studies.},
urlyear = {2026},
month = mar,
institution = {NASA Ames Research Center},
author = {Katis, Andreas and Mavridou, Anastasia and Giannakopoulou, Dimitra and Pressburger, Thomas and Schumann, Johann},
month = apr,
year = {2022},
note = {NTRS Author Affiliations: Wyle (United States), Ames Research Center
NTRS Document ID: 20220007510
NTRS Research Center: Ames Research Center (ARC)},
keywords = {Mathematical And Computer Sciences (General)},
date = {2008-04-25},
langid = {english},
}
@inproceedings{katis_capture_2022,
address = {Cham},
location = {Cham},
title = {Capture, Analyze, Diagnose: Realizability Checking Of Requirements in {FRET}},
isbn = {978-3-031-13188-2},
doi = {10.1007/978-3-031-13188-2_24},
@ -250,27 +166,13 @@ NTRS Research Center: Ames Research Center (ARC)},
publisher = {Springer International Publishing},
author = {Katis, Andreas and Mavridou, Anastasia and Giannakopoulou, Dimitra and Pressburger, Thomas and Schumann, Johann},
editor = {Shoham, Sharon and Vizel, Yakir},
year = {2022},
}
@techreport{pressburger_using_2023,
title = {Using {FRET} to {Create}, {Analyze} and {Monitor} {Requirements} for a {Lift} {Plus} {Cruise} {Case} {Study}},
url = {https://ntrs.nasa.gov/citations/20220017032},
abstract = {In this technical report we provide information on the use of the NASA Formal RequirementsElicitation Tool (FRET) to create requirements for a Lift Plus Cruise (LPC) aircraft case study. Furthermore, we provide details on using FRET to translate these requirements into an appropriate format for the Copilot tool, enabling their usage to perform runtime verification on a synthesized LPC system.},
urlyear = {2026},
month = mar,
institution = {NASA Ames Research Center},
author = {Pressburger, Thomas and Katis, Andreas and Dutle, Aaron and Mavridou, Anastasia},
month = apr,
year = {2023},
note = {NTRS Author Affiliations: Ames Research Center, KBR (United States), Langley Research Center
NTRS Document ID: 20220017032
NTRS Research Center: Ames Research Center (ARC)},
keywords = {Mathematical And Computer Sciences (General)},
date = {2022},
langid = {english},
file = {Full Text PDF:/home/danesabo/Zotero/storage/3JPVH8U2/Katis et al. - 2022 - Capture, Analyze, Diagnose Realizability Checking Of Requirements in FRET.pdf:application/pdf},
}
@inproceedings{meyer_strix_2018,
address = {Cham},
location = {Cham},
title = {Strix: Explicit Reactive Synthesis Strikes Back!},
isbn = {978-3-319-96145-3},
doi = {10.1007/978-3-319-96145-3_31},
@ -280,7 +182,8 @@ NTRS Research Center: Ames Research Center (ARC)},
publisher = {Springer International Publishing},
author = {Meyer, Philipp J. and Sickert, Salomon and Luttenberger, Michael},
editor = {Chockler, Hana and Weissenbacher, Georg},
year = {2018},
date = {2018},
langid = {english},
}
@misc{jacobs_reactive_2024,
@ -291,26 +194,12 @@ NTRS Research Center: Ames Research Center (ARC)},
number = {{arXiv}:2206.00251},
publisher = {{arXiv}},
author = {Jacobs, Swen and others},
urlyear = {2025},
month = dec,
year = {2024},
month = may,
urldate = {2025-12-06},
date = {2024-05-06},
eprinttype = {arxiv},
eprint = {2206.00251 [cs]},
keywords = {Computer Science - Logic in Computer Science},
}
@book{lunze_handbook_2009,
address = {Cambridge},
title = {Handbook of {Hybrid} {Systems} {Control}: {Theory}, {Tools}, {Applications}},
isbn = {978-0-521-76505-3},
shorttitle = {Handbook of {Hybrid} {Systems} {Control}},
url = {https://www.cambridge.org/core/books/handbook-of-hybrid-systems-control/95CBB51B339FA6B95B814D4BABB715A7},
doi = {10.1017/CBO9780511807930},
abstract = {Setting out core theory and reviewing a range of new methods, theoretical problems and applications, this handbook shows how hybrid dynamical systems can be modelled and understood. Sixty expert authors involved in the recent research activities and industrial application studies provide practical insights on topics ranging from the theoretical investigations over computer-aided design to applications in energy management and the process industry. Structured into three parts, the book opens with a thorough introduction to hybrid systems theory, illustrating new dynamical phenomena through numerous examples. Part II then provides a survey of key tools and tool integration activities. Finally, Part III is dedicated to applications, implementation issues and system integration, considering different domains such as industrial control, automotive systems and digital networks. Three running examples are referred to throughout the book, together with numerous illustrations, helping both researchers and industry professionals to understand complex theory, recognise problems and find appropriate solutions.},
urlyear = {2026},
month = jan,
publisher = {Cambridge University Press},
editor = {Lunze, Jan and Lamnabhi-Lagarrigue, Françoise},
year = {2009},
file = {Preprint PDF:/home/danesabo/Zotero/storage/GU6W5UH4/Jacobs et al. - 2024 - The Reactive Synthesis Competition (SYNTCOMP) 2018-2021.pdf:application/pdf;Snapshot:/home/danesabo/Zotero/storage/57UPK6A5/2206.html:text/html},
}
@article{branicky_multiple_1998,
@ -321,74 +210,41 @@ NTRS Research Center: Ames Research Center (ARC)},
doi = {10.1109/9.664150},
pages = {475--482},
number = {4},
journal = {{IEEE} Transactions on Automatic Control},
journaltitle = {{IEEE} Transactions on Automatic Control},
author = {Branicky, M.S.},
urlyear = {2025},
month = sep,
year = {1998},
month = apr,
urldate = {2025-09-10},
date = {1998-04},
keywords = {Automata, Control systems, Difference equations, Differential equations, Lagrangian functions, Limit-cycles, Lyapunov method, Stability analysis, Switched systems, Switches},
file = {PDF:/home/danesabo/Zotero/storage/5AQWDPAA/Branicky - 1998 - Multiple Lyapunov functions and other analysis tools for switched and hybrid systems.pdf:application/pdf},
}
@phdthesis{kapuria_using_2025,
address = {United States -- Pennsylvania},
type = {Ph.{D}.},
title = {Using {Decomposition}-{Based} {Formal} {Verification} to {Analyze} {Safety} and {Identify} {Unsafe} {Control} {Actions} for {Hybrid} {Systems}},
copyright = {Database copyright ProQuest LLC; ProQuest does not claim copyright in the individual underlying works.},
isbn = {9798280700147},
url = {https://www.proquest.com/docview/3215670525/abstract/3C715CB23CB84313PQ/1},
abstract = {This dissertation presents a decomposition-based formal verification framework for hybrid systems, focusing on identifying unsafe control actions (UCAs) in cyber-physical systems (CPS). Using differential dynamic logic, we verify safety properties by first proving correctness at the component level before integrating them into a system-wide proof. Our approach enhances scalability by isolating subsystems, enforcing constraints on their interactions, and using satisfiability modulo theories (SMT) solvers to automate invariant generation. We apply this methodology to a small modular advanced high-temperature reactor (SmAHTR), analyzing its control logic under both normal operations and adversarial conditions, including cyberattacks. The results demonstrate how formal methods can systematically identify UCAs that emerge from mode transitions, feedback interactions, and incorrect assumptions. By integrating theorem proving with reachability analysis, this work advances CPS safety verification, providing a rigorous and scalable approach to ensuring system resilience.
To achieve this, we develop a hybrid automaton model of SmAHTR and formally verify its behavior under various control strategies, including scenarios involving maintenance operations and external disruptions. We introduce a structured method to decompose the system into independently analyzable components, ensuring that local safety guarantees extend to global system correctness. The verification process captures both intended and unintended control actions, revealing potential failure modes that traditional analysis methods might overlook. Furthermore, we propose an automated approach for identifying UCAs by leveraging formal reasoning tools to systematically explore system behaviors beyond manual hazard analysis. Our findings demonstrate that decomposition-based verification not only reduces computational complexity but also improves the efficiency and robustness of CPS safety analysis, particularly for high-assurance applications such as nuclear reactor operations.},
language = {English},
urlyear = {2026},
month = feb,
school = {University of Pittsburgh},
author = {Kapuria, Abhimanyu},
year = {2025},
keywords = {Computer science, Differential equations, Electrical engineering, Engineering, Formal verification, Hybrid systems, Mechanical engineering, Reachability analysis, Satisfiability modulo theories solvers},
}
@inproceedings{lang_formal_2021,
address = {VIRTUAL EVENT},
title = {Formal {Verification} {Applied} to {Spacecraft} {Attitude} {Control}},
isbn = {978-1-62410-609-5},
url = {https://arc.aiaa.org/doi/10.2514/6.2021-1126},
doi = {10.2514/6.2021-1126},
language = {en},
urlyear = {2024},
month = nov,
booktitle = {{AIAA} {Scitech} 2021 {Forum}},
publisher = {American Institute of Aeronautics and Astronautics},
author = {Lang, Kendra and Klett, Corbin and Hawkins, Kelsey and Feron, Eric and Tsiotras, Panagiotis and Phillips, Sean},
month = jan,
year = {2021},
}
@inproceedings{frehse_spaceex_2011,
address = {Berlin, Heidelberg},
title = {{SpaceEx}: Scalable Verification of Hybrid Systems},
isbn = {978-3-642-22110-1},
doi = {10.1007/978-3-642-22110-1_30},
shorttitle = {{SpaceEx}},
pages = {379--395},
booktitle = {Computer Aided Verification},
publisher = {Springer},
author = {Frehse, Goran and Le Guernic, Colas and Donzé, Alexandre and Cotton, Scott and Ray, Rajarshi and Lebeltel, Olivier and Ripado, Rodolfo and Girard, Antoine and Dang, Thao and Maler, Oded},
editor = {Gopalakrishnan, Ganesh and Qadeer, Shaz},
year = {2011},
keywords = {Hybrid Automaton, Hybrid System, Reachability Analysis, Reachable State, Support Function},
}
@phdthesis{guernic_reachability_2009,
@thesis{guernic_reachability_2009,
title = {Reachability Analysis of Hybrid Systems with Linear Continuous Dynamics},
url = {https://theses.hal.science/tel-00422569},
institution = {Université Joseph-Fourier - Grenoble I},
school = {Université Joseph-Fourier, Grenoble},
type = {phdthesis},
author = {Guernic, Colas Le},
urlyear = {2025},
month = sep,
year = {2009},
month = oct,
urldate = {2025-09-14},
date = {2009-10-28},
langid = {english},
file = {Full Text PDF:/home/danesabo/Zotero/storage/A5XNTDZ9/Guernic - 2009 - Reachability Analysis of Hybrid Systems with Linear Continuous Dynamics.pdf:application/pdf},
}
@inproceedings{alur_hybrid_1993,
location = {Berlin, Heidelberg},
title = {Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems},
isbn = {978-3-540-48060-0},
doi = {10.1007/3-540-57318-6_30},
shorttitle = {Hybrid automata},
pages = {209--229},
booktitle = {Hybrid Systems},
publisher = {Springer},
author = {Alur, Rajeev and Courcoubetis, Costas and Henzinger, Thomas A. and Ho, Pei -Hsin},
editor = {Grossman, Robert L. and Nerode, Anil and Ravn, Anders P. and Rischel, Hans},
date = {1993},
langid = {english},
keywords = {Acceptance Condition, Hybrid Automaton, Hybrid System, Mutual Exclusion, Reachability Problem},
file = {Full Text PDF:/home/danesabo/Zotero/storage/WBXYUC86/Alur et al. - 1993 - Hybrid automata An algorithmic approach to the specification and verification of hybrid systems.pdf:application/pdf},
}
@article{mitchell_time-dependent_2005,
@ -399,13 +255,29 @@ To achieve this, we develop a hybrid automaton model of SmAHTR and formally veri
doi = {10.1109/TAC.2005.851439},
pages = {947--957},
number = {7},
journal = {{IEEE} Transactions on Automatic Control},
journaltitle = {{IEEE} Transactions on Automatic Control},
author = {Mitchell, I.M. and Bayen, A.M. and Tomlin, C.J.},
urlyear = {2025},
month = sep,
year = {2005},
month = jul,
urldate = {2025-09-15},
date = {2005-07},
keywords = {Aircraft, Collaborative software, Collision avoidance, Computational modeling, Differential games, HamiltonJacobi equations, Nonlinear equations, Nonlinear systems, Partial differential equations, reachability, Trajectory, Vehicle dynamics, verification, Viscosity},
file = {Snapshot:/home/danesabo/Zotero/storage/SLKV9PEI/1463302.html:text/html;Submitted Version:/home/danesabo/Zotero/storage/9YWL2UDH/Mitchell et al. - 2005 - A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games.pdf:application/pdf},
}
@inproceedings{frehse_spaceex_2011,
location = {Berlin, Heidelberg},
title = {{SpaceEx}: Scalable Verification of Hybrid Systems},
isbn = {978-3-642-22110-1},
doi = {10.1007/978-3-642-22110-1_30},
shorttitle = {{SpaceEx}},
pages = {379--395},
booktitle = {Computer Aided Verification},
publisher = {Springer},
author = {Frehse, Goran and Le Guernic, Colas and Donzé, Alexandre and Cotton, Scott and Ray, Rajarshi and Lebeltel, Olivier and Ripado, Rodolfo and Girard, Antoine and Dang, Thao and Maler, Oded},
editor = {Gopalakrishnan, Ganesh and Qadeer, Shaz},
date = {2011},
langid = {english},
keywords = {Hybrid Automaton, Hybrid System, Reachability Analysis, Reachable State, Support Function},
file = {Full Text PDF:/home/danesabo/Zotero/storage/LPQK8GY2/Frehse et al. - 2011 - SpaceEx Scalable Verification of Hybrid Systems.pdf:application/pdf},
}
@inproceedings{bansal_hamilton-jacobi_2017,
@ -417,15 +289,14 @@ To achieve this, we develop a hybrid automaton model of SmAHTR and formally veri
pages = {2242--2253},
booktitle = {2017 {IEEE} 56th Annual Conference on Decision and Control ({CDC})},
author = {Bansal, Somil and Chen, Mo and Herbert, Sylvia and Tomlin, Claire J.},
urlyear = {2025},
month = sep,
year = {2017},
month = dec,
urldate = {2025-09-15},
date = {2017-12},
keywords = {Aircraft, Games, Level set, Safety, Tools, Trajectory, Tutorials},
file = {Snapshot:/home/danesabo/Zotero/storage/EEK5IE93/8263977.html:text/html;Submitted Version:/home/danesabo/Zotero/storage/BMNLZ9DW/Bansal et al. - 2017 - Hamilton-Jacobi reachability A brief overview and recent advances.pdf:application/pdf},
}
@inproceedings{prajna_safety_2004,
address = {Berlin, Heidelberg},
location = {Berlin, Heidelberg},
title = {Safety Verification of Hybrid Systems Using Barrier Certificates},
isbn = {978-3-540-24743-2},
doi = {10.1007/978-3-540-24743-2_32},
@ -434,111 +305,7 @@ To achieve this, we develop a hybrid automaton model of SmAHTR and formally veri
publisher = {Springer},
author = {Prajna, Stephen and Jadbabaie, Ali},
editor = {Alur, Rajeev and Pappas, George J.},
year = {2004},
date = {2004},
langid = {english},
keywords = {Continuous State, Discrete Transition, Hybrid System, Integral Constraint, Reachability Analysis},
}
@techreport{deroucy_ai_2025,
title = {AI, Data Centers and Energy Demand: Reassessing and Exploring the Trends},
author = {de Roucy-Rochegonde, Laure and Buffard, Adrien},
institution = {French Institute of International Relations (Ifri)},
year = {2025},
type = {Ifri Papers},
isbn = {979-10-373-1000-2}
}
@article{harvey_levels_2021,
title = {The {Levels} of {War} as {Levels} of {Analysis}},
language = {en},
publisher = {Military Review},
author = {Harvey, Andrew S},
year = {2021},
file = {PDF:/Users/danesabo/Zotero/storage/5NSKMNEU/Harvey - The Levels of War as Levels of Analysis.pdf:application/pdf},
}
@article{luttenberger_practical_2020,
title = {Practical synthesis of reactive systems from {LTL} specifications via parity games},
volume = {57},
issn = {1432-0525},
url = {https://doi.org/10.1007/s00236-019-00349-3},
doi = {10.1007/s00236-019-00349-3},
abstract = {The synthesis of reactive systems from linear temporal logic (LTL) specifications is an important aspect in the design of reliable software and hardware. We present our adaption of the classic automata-theoretic approach to LTL synthesis, implemented in the tool Strix which has won the two last synthesis competitions (Syntcomp2018/2019). The presented approach is (1) structured, meaning that the states used in the construction have a semantic structure that is exploited in several ways, it performs a (2) forward exploration such that it often constructs only a small subset of the reachable states, and it is (3) incremental in the sense that it reuses results from previous inconclusive solution attempts. Further, we present and study different guiding heuristics that determine where to expand the on-demand constructed arena. Moreover, we show several techniques for extracting an implementation (Mealy machine or circuit) from the witness of the tree-automaton emptiness check. Lastly, the chosen constructions use a symbolic representation of the transition functions to reduce runtime and memory consumption. We evaluate the proposed techniques on the Syntcomp2019 benchmark set and show in more detail how the proposed techniques compare to the techniques implemented in other leading LTL synthesis tools.},
language = {en},
number = {1},
urldate = {2026-03-07},
journal = {Acta Informatica},
author = {Luttenberger, Michael and Meyer, Philipp J. and Sickert, Salomon},
month = apr,
year = {2020},
pages = {3--36},
file = {Submitted Version:/Users/danesabo/Zotero/storage/VYMVF5GK/Luttenberger et al. - 2020 - Practical synthesis of reactive systems from LTL specifications via parity games.pdf:application/pdf},
}
@inproceedings{chen_taylor_2012,
title = {Taylor {Model} {Flowpipe} {Construction} for {Non}-linear {Hybrid} {Systems}},
issn = {1052-8725},
url = {https://ieeexplore.ieee.org/document/6424802},
doi = {10.1109/RTSS.2012.70},
abstract = {We propose an approach for verifying non-linear hybrid systems using higher-order Taylor models that are a combination of bounded degree polynomials over the initial conditions and time, bloated by an interval. Taylor models are an effective means for computing rigorous bounds on the complex time trajectories of non-linear differential equations. As a result, Taylor models have been successfully used to verify properties of non-linear continuous systems. However, the handling of discrete (controller) transitions remains a challenging problem. In this paper, we provide techniques for handling the effect of discrete transitions on Taylor model flow pipe construction. We explore various solutions based on two ideas: domain contraction and range over-approximation. Instead of explicitly computing the intersection of a Taylor model with a guard set, domain contraction makes the domain of a Taylor model smaller by cutting away parts for which the intersection is empty. It is complemented by range over-approximation that translates Taylor models into commonly used representations such as template polyhedra or zonotopes, on which intersections with guard sets have been previously studied. We provide an implementation of the techniques described in the paper and evaluate the various design choices over a set of challenging benchmarks.},
urldate = {2026-03-18},
booktitle = {2012 {IEEE} 33rd {Real}-{Time} {Systems} {Symposium}},
author = {Chen, Xin and Ábrahám, Erika and Sankaranarayanan, Sriram},
month = dec,
year = {2012},
note = {ISSN: 1052-8725},
keywords = {Approximation methods, Computational modeling, Mathematical model, Polynomials, Safety, Taylor series, Trajectory},
pages = {183--192},
file = {Snapshot:/Users/danesabo/Zotero/storage/7HBF3VMT/6424802.html:text/html},
}
@inproceedings{chen_flow_2013,
address = {Berlin, Heidelberg},
title = {Flow*: {An} {Analyzer} for {Non}-linear {Hybrid} {Systems}},
isbn = {978-3-642-39799-8},
shorttitle = {Flow*},
doi = {10.1007/978-3-642-39799-8_18},
abstract = {The tool Flow* performs Taylor model-based flowpipe construction for non-linear (polynomial) hybrid systems. Flow* combines well-known Taylor model arithmetic techniques for guaranteed approximations of the continuous dynamics in each mode with a combination of approaches for handling mode invariants and discrete transitions. Flow* supports a wide variety of optimizations including adaptive step sizes, adaptive selection of approximation orders and the heuristic selection of template directions for aggregating flowpipes. This paper describes Flow* and demonstrates its performance on a series of non-linear continuous and hybrid system benchmarks. Our comparisons show that Flow* is competitive with other tools.},
language = {en},
booktitle = {Computer {Aided} {Verification}},
publisher = {Springer},
author = {Chen, Xin and Ábrahám, Erika and Sankaranarayanan, Sriram},
editor = {Sharygina, Natasha and Veith, Helmut},
year = {2013},
keywords = {Adaptive Step, Adaptive Step Size, Discrete Transition, Hybrid System, Taylor Model},
pages = {258--263},
file = {Full Text PDF:/Users/danesabo/Zotero/storage/6QV2XCVF/Chen et al. - 2013 - Flow An Analyzer for Non-linear Hybrid Systems.pdf:application/pdf},
}
@inproceedings{althoff_introduction_nodate,
title = {An {Introduction} to {CORA} 2015},
url = {https://easychair.org/publications/paper/xMm},
doi = {10.29007/zbkv},
abstract = {The philosophy, architecture, and capabilities of the COntinuous Reachability Analyzer (CORA) are presented. CORA is a toolbox that integrates various vector and matrix set representations and operations on them as well as reachability algorithms of various dynamic system classes. The software is designed such that set representations can be exchanged without having to modify the code for reachability analysis. CORA has a modular design, making it possible to use the capabilities of the various set representations for other purposes besides reachability analysis. The toolbox is designed using the object oriented paradigm, such that users can safely use methods without concerning themselves with detailed information hidden inside the object. Since the toolbox is written in MATLAB, the installation and use is platform independent.},
urldate = {2026-03-18},
author = {Althoff, Matthias},
pages = {120--87},
file = {Full Text:/Users/danesabo/Zotero/storage/BIGJMRCV/Althoff - An Introduction to CORA 2015.pdf:application/pdf},
}
@article{bogomolov_reachability_2020,
title = {Reachability {Analysis} of {Linear} {Hybrid} {Systems} via {Block} {Decomposition}},
volume = {39},
issn = {1937-4151},
url = {https://ieeexplore.ieee.org/document/9211556},
doi = {10.1109/TCAD.2020.3012859},
abstract = {Reachability analysis aims at identifying states reachable by a system within a given time horizon. This task is known to be computationally expensive for linear hybrid systems. Reachability analysis works by iteratively applying continuous and discrete post operators to compute states reachable according to continuous and discrete dynamics, respectively. In this article, we enhance both of these operators and make sure that most of the involved computations are performed in low-dimensional state space. In particular, we improve the continuous-post operator by performing computations in high-dimensional state space only for time intervals relevant for the subsequent application of the discrete-post operator. Furthermore, the new discrete-post operator performs low-dimensional computations by leveraging the structure of the guard and assignment of a considered transition. We illustrate the potential of our approach on a number of challenging benchmarks.},
number = {11},
urldate = {2026-03-18},
journal = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},
author = {Bogomolov, Sergiy and Forets, Marcelo and Frehse, Goran and Potomkin, Kostiantyn and Schilling, Christian},
month = nov,
year = {2020},
keywords = {Approximation algorithms, Decomposition, Design automation, Heuristic algorithms, hybrid systems, Integrated circuits, Linear systems, reachability, Reachability analysis, Tools},
pages = {4018--4029},
file = {Snapshot:/Users/danesabo/Zotero/storage/D7FYXW7T/9211556.html:text/html;Submitted Version:/Users/danesabo/Zotero/storage/I3HNBQ65/Bogomolov et al. - 2020 - Reachability Analysis of Linear Hybrid Systems via Block Decomposition.pdf:application/pdf},
}