Auto sync: 2025-12-05 19:50:41 (47 files changed)

M  .task/backlog.data

M  .task/completed.data

M  .task/pending.data

M  .task/undo.data

R  Writing/ERLM/goals-and-outcomes/research_statement.tex -> Writing/ERLM/1-goals-and-outcomes/research_statement.tex

R  Writing/ERLM/goals-and-outcomes/v1.tex -> Writing/ERLM/1-goals-and-outcomes/v1.tex

R  Writing/ERLM/goals-and-outcomes/v2.tex -> Writing/ERLM/1-goals-and-outcomes/v2.tex

R  Writing/ERLM/goals-and-outcomes/v3.tex -> Writing/ERLM/1-goals-and-outcomes/v3.tex
This commit is contained in:
Dane Sabo 2025-12-05 19:50:41 -05:00
parent 9e01a8e6a1
commit 4980358ea4
47 changed files with 494 additions and 1100 deletions

View File

@ -357,3 +357,8 @@
{"description":"ERLM proposal due","due":"20251206T050000Z","entry":"20251202T131547Z","modified":"20251202T132329Z","project":"ERLM","status":"pending","uuid":"f6968367-96f1-4ce2-8691-e45423e27456","tags":["writing"],"depends":["0888fdb8-f5cd-4374-a589-b7b3c1bbd472","0d921ea2-6211-4cd8-bbc4-4f9bf36794d3","14fee599-fe0f-4773-90fc-c5f78291f425","29cc8c63-1fb7-4523-9953-603467b929ee","2a8e9294-aecc-434a-b5dd-a468baf8f4a8","5ba3929b-5ec3-4c9d-b30e-30fd8fe20b54","689420d6-7191-42b6-b691-94ad39c8e0dd","9ce7d23c-0f56-49af-b97d-a684966cfbae","a4c027fa-f50d-4efc-ab61-5b8054810a80","d1fa2409-2f2f-4855-81be-14ee617df5d2","e354ab0c-cef7-41e2-bfb4-d98886e512b7"]}
{"description":"Review and edit Goals and Outcomes section","due":"20251205T050000Z","entry":"20251202T132235Z","modified":"20251202T152712Z","project":"ERLM","start":"20251202T152712Z","status":"pending","uuid":"0888fdb8-f5cd-4374-a589-b7b3c1bbd472","tags":["editing"]}
{"description":"Review and edit State of the Art section","due":"20251205T050000Z","entry":"20251202T132235Z","modified":"20251203T211706Z","project":"ERLM","start":"20251203T211706Z","status":"pending","uuid":"0d921ea2-6211-4cd8-bbc4-4f9bf36794d3","tags":["editing"]}
{"description":"Review and edit State of the Art section","due":"20251205T050000Z","end":"20251205T225952Z","entry":"20251202T132235Z","modified":"20251205T225952Z","project":"ERLM","status":"completed","uuid":"0d921ea2-6211-4cd8-bbc4-4f9bf36794d3","tags":["editing"]}
{"description":"Review and edit Research Approach section","due":"20251205T050000Z","entry":"20251202T132235Z","modified":"20251205T230823Z","project":"ERLM","start":"20251205T230823Z","status":"pending","uuid":"9ce7d23c-0f56-49af-b97d-a684966cfbae","tags":["editing"]}
{"description":"Review and edit Goals and Outcomes section","due":"20251205T050000Z","end":"20251206T004937Z","entry":"20251202T132235Z","modified":"20251206T004937Z","project":"ERLM","status":"completed","uuid":"0888fdb8-f5cd-4374-a589-b7b3c1bbd472","tags":["editing"]}
{"description":"Review and edit Research Approach section","due":"20251205T050000Z","end":"20251206T004937Z","entry":"20251202T132235Z","modified":"20251206T004937Z","project":"ERLM","status":"completed","uuid":"9ce7d23c-0f56-49af-b97d-a684966cfbae","tags":["editing"]}
{"description":"Review and edit Metrics of Success section","due":"20251205T050000Z","entry":"20251202T132235Z","modified":"20251206T004956Z","project":"ERLM","start":"20251206T004956Z","status":"pending","uuid":"29cc8c63-1fb7-4523-9953-603467b929ee","tags":["editing"]}

View File

@ -1,3 +1,6 @@
[description:"Review and edit Goals and Outcomes section" due:"1764910800" end:"1764982177" entry:"1764681755" modified:"1764982177" project:"ERLM" status:"completed" tags:"editing" tags_editing:"x" uuid:"0888fdb8-f5cd-4374-a589-b7b3c1bbd472"]
[description:"Review and edit Research Approach section" due:"1764910800" end:"1764982177" entry:"1764681755" modified:"1764982177" project:"ERLM" status:"completed" tags:"editing" tags_editing:"x" uuid:"9ce7d23c-0f56-49af-b97d-a684966cfbae"]
[description:"Review and edit State of the Art section" due:"1764910800" end:"1764975592" entry:"1764681755" modified:"1764975592" project:"ERLM" status:"completed" tags:"editing" tags_editing:"x" uuid:"0d921ea2-6211-4cd8-bbc4-4f9bf36794d3"]
[description:"Get information from FSAE about job placements and a couple sentences about their value for the website" due:"1764738000" end:"1764681587" entry:"1763750758" modified:"1764681590" project:"Chair-Search" status:"deleted" uuid:"fb997f7c-c3d8-4f3c-b02c-f6d55cc9b1c8"]
[description:"Make list of tasks for contact about student groups" due:"1764133200" end:"1764681551" entry:"1763750783" modified:"1764681551" project:"Chair-Search" status:"completed" uuid:"0addf099-132c-41af-90d8-19f5f9a9c832"]
[description:"Draft Presentations" due:"1763787540" end:"1764681215" entry:"1762886561" modified:"1764681215" project:"ERLM" status:"completed" uuid:"aa7dde10-50d7-4e92-8732-e9f97e049fd9"]

View File

@ -67,10 +67,7 @@
[description:"Reach out to SOAR for job placement info and website content" due:"1764824400" entry:"1764681551" modified:"1764681551" project:"Chair-Search" status:"pending" uuid:"535c2ffc-f233-46f0-ac33-a93cbfd12f81"]
[description:"Reach out to Material Advantage for job placement info and website content" due:"1764824400" entry:"1764681551" modified:"1764681551" project:"Chair-Search" status:"pending" uuid:"00072514-5622-4a44-9826-49690be83767"]
[description:"Reach out to FSAE for job placement info and website content" due:"1764824400" entry:"1764681551" modified:"1764681551" project:"Chair-Search" status:"pending" uuid:"ca5f0450-483f-4a93-aba1-d06e71b4df5c"]
[description:"Review and edit Goals and Outcomes section" due:"1764910800" entry:"1764681755" modified:"1764689232" project:"ERLM" start:"1764689232" status:"pending" tags:"editing" tags_editing:"x" uuid:"0888fdb8-f5cd-4374-a589-b7b3c1bbd472"]
[description:"Review and edit State of the Art section" due:"1764910800" entry:"1764681755" modified:"1764796626" project:"ERLM" start:"1764796626" status:"pending" tags:"editing" tags_editing:"x" uuid:"0d921ea2-6211-4cd8-bbc4-4f9bf36794d3"]
[description:"Review and edit Research Approach section" due:"1764910800" entry:"1764681755" modified:"1764681755" project:"ERLM" status:"pending" tags:"editing" tags_editing:"x" uuid:"9ce7d23c-0f56-49af-b97d-a684966cfbae"]
[description:"Review and edit Metrics of Success section" due:"1764910800" entry:"1764681755" modified:"1764681755" project:"ERLM" status:"pending" tags:"editing" tags_editing:"x" uuid:"29cc8c63-1fb7-4523-9953-603467b929ee"]
[description:"Review and edit Metrics of Success section" due:"1764910800" entry:"1764681755" modified:"1764982196" project:"ERLM" start:"1764982196" status:"pending" tags:"editing" tags_editing:"x" uuid:"29cc8c63-1fb7-4523-9953-603467b929ee"]
[description:"Review and edit Risks and Contingencies section" due:"1764910800" entry:"1764681755" modified:"1764681755" project:"ERLM" status:"pending" tags:"editing" tags_editing:"x" uuid:"e354ab0c-cef7-41e2-bfb4-d98886e512b7"]
[description:"Review and edit Broader Impacts section" due:"1764910800" entry:"1764681756" modified:"1764681756" project:"ERLM" status:"pending" tags:"editing" tags_editing:"x" uuid:"d1fa2409-2f2f-4855-81be-14ee617df5d2"]
[description:"Review and edit Budget section" due:"1764910800" entry:"1764681756" modified:"1764681756" project:"ERLM" status:"pending" tags:"editing" tags_editing:"x" uuid:"689420d6-7191-42b6-b691-94ad39c8e0dd"]

View File

@ -1274,3 +1274,23 @@ time 1764796626
old [description:"Review and edit State of the Art section" due:"1764910800" entry:"1764681755" modified:"1764681755" project:"ERLM" status:"pending" tags:"editing" tags_editing:"x" uuid:"0d921ea2-6211-4cd8-bbc4-4f9bf36794d3"]
new [description:"Review and edit State of the Art section" due:"1764910800" entry:"1764681755" modified:"1764796626" project:"ERLM" start:"1764796626" status:"pending" tags:"editing" tags_editing:"x" uuid:"0d921ea2-6211-4cd8-bbc4-4f9bf36794d3"]
---
time 1764975592
old [description:"Review and edit State of the Art section" due:"1764910800" entry:"1764681755" modified:"1764796626" project:"ERLM" start:"1764796626" status:"pending" tags:"editing" tags_editing:"x" uuid:"0d921ea2-6211-4cd8-bbc4-4f9bf36794d3"]
new [description:"Review and edit State of the Art section" due:"1764910800" end:"1764975592" entry:"1764681755" modified:"1764975592" project:"ERLM" status:"completed" tags:"editing" tags_editing:"x" uuid:"0d921ea2-6211-4cd8-bbc4-4f9bf36794d3"]
---
time 1764976103
old [description:"Review and edit Research Approach section" due:"1764910800" entry:"1764681755" modified:"1764681755" project:"ERLM" status:"pending" tags:"editing" tags_editing:"x" uuid:"9ce7d23c-0f56-49af-b97d-a684966cfbae"]
new [description:"Review and edit Research Approach section" due:"1764910800" entry:"1764681755" modified:"1764976103" project:"ERLM" start:"1764976103" status:"pending" tags:"editing" tags_editing:"x" uuid:"9ce7d23c-0f56-49af-b97d-a684966cfbae"]
---
time 1764982177
old [description:"Review and edit Goals and Outcomes section" due:"1764910800" entry:"1764681755" modified:"1764689232" project:"ERLM" start:"1764689232" status:"pending" tags:"editing" tags_editing:"x" uuid:"0888fdb8-f5cd-4374-a589-b7b3c1bbd472"]
new [description:"Review and edit Goals and Outcomes section" due:"1764910800" end:"1764982177" entry:"1764681755" modified:"1764982177" project:"ERLM" status:"completed" tags:"editing" tags_editing:"x" uuid:"0888fdb8-f5cd-4374-a589-b7b3c1bbd472"]
---
time 1764982177
old [description:"Review and edit Research Approach section" due:"1764910800" entry:"1764681755" modified:"1764976103" project:"ERLM" start:"1764976103" status:"pending" tags:"editing" tags_editing:"x" uuid:"9ce7d23c-0f56-49af-b97d-a684966cfbae"]
new [description:"Review and edit Research Approach section" due:"1764910800" end:"1764982177" entry:"1764681755" modified:"1764982177" project:"ERLM" status:"completed" tags:"editing" tags_editing:"x" uuid:"9ce7d23c-0f56-49af-b97d-a684966cfbae"]
---
time 1764982196
old [description:"Review and edit Metrics of Success section" due:"1764910800" entry:"1764681755" modified:"1764681755" project:"ERLM" status:"pending" tags:"editing" tags_editing:"x" uuid:"29cc8c63-1fb7-4523-9953-603467b929ee"]
new [description:"Review and edit Metrics of Success section" due:"1764910800" entry:"1764681755" modified:"1764982196" project:"ERLM" start:"1764982196" status:"pending" tags:"editing" tags_editing:"x" uuid:"29cc8c63-1fb7-4523-9953-603467b929ee"]
---

View File

@ -1,4 +1,3 @@
\newpage
\section{State of the Art and Limits of Current Practice}
The principal aim of this research is to create autonomous reactor control

View File

@ -1,30 +1,7 @@
\newpage
\section{Research Approach}
This research will overcome the limitations of current practice to build
high-assurance hybrid control systems for critical infrastructure. Hybrid
systems combine continuous dynamics (flows) with discrete transitions (jumps),
which can be formally expressed as:
\begin{equation}
\dot{x}(t) = f(x(t),q(t),u(t))
\end{equation}
\begin{equation}
q(k+1) = \nu(x(k),q(k),u(k))
\end{equation}
Here, $f(\cdot)$ defines the continuous dynamics while $\nu(\cdot)$ governs
discrete transitions. The continuous states $x$, discrete state $q$, and
control input $u$ interact to produce hybrid behavior. The discrete state $q$
defines which continuous dynamics mode is currently active. Our focus centers
on continuous autonomous hybrid systems, where continuous states remain
unchanged during jumps—a property naturally exhibited by physical systems. For
example, a nuclear reactor switching from warm-up to load-following control
cannot instantaneously change its temperature or control rod position, but can
instantaneously change control laws.
To build these systems with formal correctness guarantees, we must accomplish
high-assurance hybrid control systems for critical infrastructure. To build these systems with formal correctness guarantees, we must accomplish
three main thrusts:
\begin{enumerate}
@ -34,50 +11,25 @@ three main thrusts:
\item Create the discrete half of a hybrid controller using reactive synthesis
\item Develop continuous controllers to operate between modes, and verify
their correctness using reachability analysis
their correctness
\end{enumerate}
The following sections discuss how these thrusts will be accomplished.
\subsection{$(Procedures \wedge FRET) \rightarrow Temporal Specifications$}
The motivation behind this work stems from the fact that commercial nuclear
power operations remain manually controlled by human operators, despite
significant advances in control systems sophistication. The key insight is that
procedures performed by human operators are highly prescriptive and
well-documented. This suggests that human operators in nuclear power plants may
not be entirely necessary given today's available technology.
power operations remain manually controlled by human operators, but procedures
performed by human operators are highly prescriptive and well-documented. This
suggests that human operators in nuclear power plants may not be entirely
necessary given today's available technology. Written procedures and
requirements in nuclear power are sufficiently detailed that we may be able to
translate them into logical formulae with minimal effort. If successful, this
approach would enable automation of existing procedures without requiring system
reengineering. To formalize these procedures, we will use temporal logic, which
captures system behaviors through temporal relations.
Written procedures and requirements in nuclear power are sufficiently detailed
that we may be able to translate them into logical formulae with minimal effort.
If successful, this approach would enable automation of existing procedures
without requiring system reengineering. To formalize these procedures, we will
use temporal logic, which captures system behaviors through temporal relations.
Linear Temporal Logic (LTL) provides four fundamental operators: next ($X$),
eventually ($F$), globally ($G$), and until ($U$). These operators enable
precise specification of time-dependent requirements.
Consider a nuclear reactor SCRAM requirement expressed in natural language:
\textit{``If a high temperature alarm triggers, control rods must immediately
insert and remain inserted until operator reset.''} This plain language
requirement can be translated into a rigorous logical specification:
\begin{equation}
G(HighTemp \rightarrow X(RodsInserted \wedge (\neg RodsWithdrawn\ U\
OperatorReset)))
\end{equation}
This specification precisely captures the temporal relationship between the
alarm condition, the required response, and the persistence requirement. The
global operator $G$ ensures this property holds throughout system operation,
while the next operator $X$ enforces immediate response. The until operator
$U$ maintains the state constraint until the reset condition occurs.
The most efficient path to accomplish this translation is through NASA's
Formal Requirements Elicitation Tool (FRET). FRET employs a specialized
requirements language called FRETish that restricts requirements to easily
understood components while eliminating ambiguity. FRETish bridges natural
The most efficient path to accomplish this translation is through NASA's Formal
Requirements Elicitation Tool (FRET). FRET employs a specialized requirements
language called FRETish that restricts requirements to easily understood
components while eliminating ambiguity~\cite{katis_capture_2022}. FRETish bridges natural
language and mathematical specifications through a structured English-like
syntax that is automatically translatable to temporal logic.
@ -111,12 +63,35 @@ during autonomous controller development, we can deliver controllers free from
these vulnerabilities.
FRET provides the capability to export requirements in temporal logic format
compatible with reactive synthesis tools. This export functionality enables
progression to the next step of our approach: synthesizing discrete mode
switching behavior from the formalized requirements.
compatible with reactive synthesis tools. Linear Temporal Logic (LTL) builds
upon modal logic's foundational operators for necessity ($\Box$, ``box'') and
possibility ($\Diamond$, ``diamond''), extending them to reason about temporal
behavior~\cite{baier_principles_2008}. The box operator $\Box$ expresses that a
property holds at all future times (necessarily always), while the diamond
operator $\Diamond$ expresses that a property holds at some future time
(possibly eventually). These are complemented by the next operator ($X$) for the
immediate successor state and the until operator ($U$) for expressing
persistence conditions.
\subsection{$(TemporalLogic \wedge ReactiveSynthesis) \rightarrow
DiscreteAutomata$}
Consider a nuclear reactor SCRAM requirement expressed in natural language:
\textit{``If a high temperature alarm triggers, control rods must immediately
insert and remain inserted until operator reset.''} This plain language
requirement can be translated into a rigorous logical specification:
\begin{equation}
\Box(HighTemp \rightarrow X(RodsInserted \wedge (\neg
RodsWithdrawn\ U\ OperatorReset)))
\end{equation}
This specification precisely captures the temporal relationship between the
alarm condition, the required response, and the persistence requirement. The
necessity operator $\Box$ ensures this safety property holds throughout all
possible future system executions, while the next operator $X$ enforces
immediate response. The until operator $U$ maintains the state constraint until
the reset condition occurs. There is no ambiguity on the control in this
scenario because all decisions are represented by discrete variables.
Formulating operating rules using this logic enforces a finite and correct way
of operating.
Reactive synthesis is an active research field in computer science focused on
generating discrete controllers from temporal logic specifications. The term
@ -135,8 +110,9 @@ finite state representations.
We will employ state-of-the-art reactive synthesis tools, particularly Strix,
which has demonstrated superior performance in the Reactive Synthesis
Competition (SYNTCOMP) through efficient parity game solving algorithms. Strix
translates linear temporal logic specifications into deterministic automata
Competition (SYNTCOMP) through efficient parity game solving
algorithms~\cite{meyer_strix_2018,jacobs_reactive_2024}. Strix
translates linear temporal logic specifications into deterministic autom\cite
automatically while maximizing generated automata quality. Once constructed, the
automaton can be straightforwardly implemented using standard programming
control flow constructs. The graphical representation provided by the automaton
@ -158,15 +134,30 @@ will not make switching errors between continuous modes. By synthesizing
controllers from logical specifications with guaranteed correctness, we
eliminate the possibility of switching errors.
\subsection{$(DiscreteAutomata \wedge ControlTheory \wedge Reachability)
\rightarrow ContinuousModes$}
While discrete system components will be synthesized with correctness
guarantees, they represent only half of the complete system. Autonomous
controllers like those we are developing exhibit continuous dynamics within
discrete states, as described by $f(\cdot)$ in Equation 1. This section
describes how we will develop continuous control modes, verify their
correctness, and address the unique verification challenges of hybrid systems.
discrete states. These systems, called hybrid systems, combine continuous
dynamics (flows) with discrete transitions (jumps). These dynamics can be
formally expressed as~\cite{branicky_multiple_1998}:
\begin{equation}
\dot{x}(t) = f(x(t),q(t),u(t))
\end{equation}
\begin{equation}
q(k+1) = \nu(x(k),q(k),u(k))
\end{equation}
Here, $f(\cdot)$ defines the continuous dynamics while $\nu(\cdot)$ governs
discrete transitions. The continuous states $x$, discrete state $q$, and
control input $u$ interact to produce hybrid behavior. The discrete state $q$
defines which continuous dynamics mode is currently active. Our focus centers
on continuous autonomous hybrid systems, where continuous states remain
unchanged during jumps—a property naturally exhibited by physical systems. For
example, a nuclear reactor switching from warm-up to load-following control
cannot instantaneously change its temperature or control rod position, but can
instantaneously change control laws.
The approach described for producing discrete automata yields physics-agnostic
specifications that represent only half of a complete hybrid autonomous
@ -211,67 +202,70 @@ on discrete mode transitions:
Building continuous modes after constructing discrete automata enables local
controller design focused on satisfying discrete transitions. The primary
challenge in hybrid system verification is ensuring global stability across
transitions. Current techniques struggle with this problem because dynamic
discontinuities complicate verification. This work alleviates these problems by
designing continuous controllers specifically with transitions in mind. By
decomposing continuous modes according to their required behavior at transition
points, we avoid solving trajectories through the entire hybrid system. Instead,
we can use local behavior information at transition boundaries. To ensure
continuous modes satisfy their requirements, we will employ three main
techniques: reachability analysis, assume-guarantee contracts, and barrier
certificates.
transitions~\cite{branicky_multiple_1998}. Current techniques struggle with this
problem because dynamic discontinuities complicate
verification~\cite{bansal_hamilton-jacobi_2017,guernic_reachability_2009}. This work
alleviates these problems by designing continuous controllers specifically with
transitions in mind. By decomposing continuous modes according to their required
behavior at transition points, we avoid solving trajectories through the entire
hybrid system. Instead, we can use local behavior information at transition
boundaries. To ensure continuous modes satisfy their requirements, we will
employ three main techniques: reachability analysis, assume-guarantee contracts,
and barrier certificates.
\textbf{Reachability Analysis:} Reachability analysis computes the reachable set
of states for a given input set. While trivial for linear continuous systems,
recent advances have extended reachability to complex nonlinear systems. We will
use reachability to define continuous state ranges at discrete transition
boundaries and verify that requirements are satisfied within continuous modes.
Recent advances using neural network approximations of Hamilton-Jacobi equations
have demonstrated significant speedups while maintaining safety guarantees for
high-dimensional systems, expanding the practical applicability of these
methods.
\textbf{Assume-Guarantee Contracts:} Assume-guarantee contracts will be
employed when continuous state boundaries are not explicitly defined. For any
given mode, the input range for reachability analysis is defined by the output
ranges of discrete modes that transition to it. This compositional approach
ensures each continuous controller is prepared for its possible input range,
enabling subsequent reachability analysis without requiring global system
analysis.
\textbf{Barrier Certificates:} Finally, we will use barrier certificates to
Reachability analysis computes the reachable set of states for a given input
set. While trivial for linear continuous systems, recent advances have extended
reachability to complex nonlinear
systems~\cite{frehse_spaceex_2011,mitchell_time-dependent_2005}. We will use
reachability to define continuous state ranges at discrete transition boundaries
and verify that requirements are satisfied within continuous modes.
Assume-guarantee contracts will be employed when continuous state boundaries are
not explicitly defined. For any given mode, the input range for reachability
analysis is defined by the output ranges of discrete modes that transition to
it. This compositional approach ensures each continuous controller is prepared
for its possible input range, enabling subsequent reachability analysis without
requiring global system analysis. Finally, we will use barrier certificates to
prove that mode transitions are satisfied. Barrier certificates ensure that
continuous modes on either side of a transition behave appropriately. Control
barrier functions provide a method to certify safety by establishing
differential inequality conditions that guarantee forward invariance of safe
sets. For example, a barrier certificate can guarantee that a transitory mode
transferring control to a stabilizing mode will always move away from the
transition boundary, rather than destabilizing the target stabilizing mode.
continuous modes on either side of a transition behave appropriately by ensuring
no system trajectories cross a given barrier. Control barrier functions provide
a method to certify safety by establishing differential inequality conditions
that guarantee forward invariance of safe sets~\cite{prajna_safety_2004}. For
example, a barrier certificate can guarantee that a transitory mode transferring
control to a stabilizing mode will always move away from the transition
boundary, rather than destabilizing the target stabilizing mode.
Combining these three techniques will enable us to prove that continuous
components of our hybrid controller satisfy discrete requirements, and thus,
complete system behavior. To demonstrate this methodology, we will develop an
This compositional approach has several advantages. First, this research
approach breaks down the autonomous controller design into smaller chunks. For
designers of future autonomous control systems, the barrier to entry is small,
while milestones in design are clear by the procedural nature of this research
plan. Second, the ability to measure design progress also enables the
measurement of regulatory adherence. Each step in this development procedure
generates an artifact that can be independently evaluated as proof of safety and
performance. Finally, the compositional component of this development plan
enables incremental refinement between control system layers. For example,
difficulty in developing a continuous mode may reflect a discrete automata that
is too restrictive, which in turn may result in refinement of system design
requirements. This synthesis between levels will promote broader understanding
of the autonomous controller.
To demonstrate this methodology, we will develop an
autonomous startup controller for a Small Modular Advanced High Temperature
Reactor (SmAHTR). SmAHTR represents an ideal test case as a liquid-salt cooled
reactor design with well-documented startup procedures that must transition
through multiple distinct operational modes: initial cold conditions, controlled
heating to operating temperature, approach to criticality, low-power physics
testing, and power ascension to full operating capacity. We have already
developed a high-fidelity SmAHTR model in Simulink that captures the
thermal-hydraulic and neutron kinetics behavior essential for verifying
continuous controller performance under realistic plant dynamics. The
synthesized hybrid controller will be implemented on an Emerson Ovation control
system platform, which is representative of industry-standard control hardware
deployed in modern nuclear facilities. The Advanced Reactor Cyber Analysis and
Development Environment (ARCADE) suite will serve as the integration layer,
managing real-time communication between the Simulink simulation and the Ovation
controller. This hardware-in-the-loop configuration enables validation of the
controller implementation on actual industrial control equipment interfacing
with a realistic reactor simulation, providing assessment of computational
performance, real-time execution constraints, and communication latency effects.
By demonstrating autonomous startup control on this representative platform, we
will establish both the theoretical validity and practical feasibility of the
synthesis methodology for deployment in actual small modular reactor systems.
Reactor (SmAHTR). We have already developed a high-fidelity SmAHTR model in
Simulink that captures the thermal-hydraulic and neutron kinetics behavior
essential for verifying continuous controller performance under realistic plant
dynamics. The synthesized hybrid controller will be implemented on an Emerson
Ovation control system platform, which is representative of industry-standard
control hardware deployed in modern nuclear facilities. The Advanced Reactor
Cyber Analysis and Development Environment (ARCADE) suite will serve as the
integration layer, managing real-time communication between the Simulink
simulation and the Ovation controller. This hardware-in-the-loop configuration
enables validation of the controller implementation on actual industrial control
equipment interfacing with a realistic reactor simulation, providing assessment
of computational performance, real-time execution constraints, and communication
latency effects. By demonstrating autonomous startup control on this
representative platform, we will establish both the theoretical validity and
practical feasibility of the synthesis methodology for deployment in actual
small modular reactor systems.
This unified approach addresses a fundamental gap in hybrid system design by
bridging formal methods and control theory through a systematic, tool-supported

View File

@ -1,10 +1,10 @@
\section{Supplemental Sections}
\subsection{Biosketch}
\includepdf[pages=-]{supplemental-sections/cv-1786798.pdf}
\includepdf[pages=-]{9-supplemental-sections/cv-1786798.pdf}
\subsection{Data Management Plan}
\includepdf[pages=-]{supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf}
\includepdf[pages=-]{9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf}
\subsection{Facilities}

View File

@ -3,9 +3,9 @@
\@writefile{toc}{\contentsline {section}{\numberline {1}Goals and Outcomes}{1}{}\protected@file@percent }
\citation{NUREG-0899,10CFR50.34}
\citation{10CFR55.59}
\@writefile{toc}{\contentsline {section}{\numberline {2}State of the Art and Limits of Current Practice}{2}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}Current Reactor Procedures and Operation}{2}{}\protected@file@percent }
\citation{WRPS.Description,gentillon_westinghouse_1999}
\@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 }
\citation{operator_statistics}
\citation{10CFR55}
\citation{10CFR50.54}
@ -13,27 +13,33 @@
\citation{WNA2020}
\citation{hogberg_root_2013}
\citation{zhang_analysis_2025}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Human Factors in Nuclear Accidents}{3}{}\protected@file@percent }
\citation{Kiniry2024}
\citation{Kiniry2024}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Human Factors in Nuclear Accidents}{4}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {2.3}HARDENS and Formal Methods}{4}{}\protected@file@percent }
\citation{Kiniry2024}
\@writefile{toc}{\contentsline {section}{\numberline {3}Research Approach}{6}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}$(Procedures \wedge FRET) \rightarrow Temporal Specifications$}{6}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {3.2}$(TemporalLogic \wedge ReactiveSynthesis) \rightarrow DiscreteAutomata$}{7}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {3.3}$(DiscreteAutomata \wedge ControlTheory \wedge Reachability) \rightarrow ContinuousModes$}{8}{}\protected@file@percent }
\citation{katis_capture_2022}
\@writefile{toc}{\contentsline {section}{\numberline {3}Research Approach}{5}{}\protected@file@percent }
\citation{baier_principles_2008}
\citation{meyer_strix_2018,jacobs_reactive_2024}
\citation{a}
\citation{branicky_multiple_1998}
\citation{branicky_multiple_1998}
\citation{bansal_hamilton-jacobi_2017,guernic_reachability_2009}
\citation{frehse_spaceex_2011,mitchell_time-dependent_2005}
\citation{prajna_safety_2004}
\@writefile{toc}{\contentsline {section}{\numberline {4}Metrics for Success}{10}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{TRL 3 \textit {Critical Function and Proof of Concept}}{11}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{TRL 4 \textit {Laboratory Testing of Integrated Components}}{11}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{TRL 3 \textit {Critical Function and Proof of Concept}}{10}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{TRL 4 \textit {Laboratory Testing of Integrated Components}}{10}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{TRL 5 \textit {Laboratory Testing in Relevant Environment}}{11}{}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {5}Risks and Contingencies}{12}{}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {5}Risks and Contingencies}{11}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {5.1}Computational Tractability of Synthesis}{12}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{13}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{14}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {5.4}Hardware-in-the-Loop Integration Complexity}{15}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{12}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{13}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {5.4}Hardware-in-the-Loop Integration Complexity}{14}{}\protected@file@percent }
\citation{eia_lcoe_2022}
\citation{eesi_datacenter_2024}
\citation{eia_lcoe_2022}
\@writefile{toc}{\contentsline {section}{\numberline {6}Broader Impacts}{16}{}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {6}Broader Impacts}{15}{}\protected@file@percent }
\bibstyle{ieeetr}
\bibdata{references}
\bibcite{NUREG-0899}{1}
@ -49,7 +55,19 @@
\bibcite{hogberg_root_2013}{11}
\bibcite{zhang_analysis_2025}{12}
\bibcite{Kiniry2024}{13}
\@writefile{toc}{\contentsline {section}{References}{18}{}\protected@file@percent }
\bibcite{katis_capture_2022}{14}
\bibcite{baier_principles_2008}{15}
\bibcite{meyer_strix_2018}{16}
\bibcite{jacobs_reactive_2024}{17}
\@writefile{toc}{\contentsline {section}{References}{17}{}\protected@file@percent }
\bibcite{branicky_multiple_1998}{18}
\bibcite{bansal_hamilton-jacobi_2017}{19}
\bibcite{guernic_reachability_2009}{20}
\bibcite{frehse_spaceex_2011}{21}
\bibcite{mitchell_time-dependent_2005}{22}
\bibcite{prajna_safety_2004}{23}
\bibcite{eia_lcoe_2022}{24}
\bibcite{eesi_datacenter_2024}{25}
\@writefile{toc}{\contentsline {section}{\numberline {7}Budget and Budget Justification}{19}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {7.1}Budget Summary}{19}{}\protected@file@percent }
\@writefile{lot}{\contentsline {table}{\numberline {1}{\ignorespaces Proposed Budget by Year and Category}}{19}{}\protected@file@percent }

View File

@ -41,4 +41,43 @@ M.~Zhang, L.~Dai, W.~Chen, and E.~Pang, ``Analysis of human errors in nuclear po
J.~Kiniry, A.~Bakst, S.~Hansen, M.~Podhradsky, and A.~Bivin, ``High assurance rigorous digital engineering for nuclear safety (hardens) final technical report,'' Tech. Rep. TLR-RES-RES/DE-2024-005, Galois, Inc. / U.S. Nuclear Regulatory Commission, 2024.
\newblock NRC Contract 31310021C0014.
\bibitem{katis_capture_2022}
A.~Katis, A.~Mavridou, D.~Giannakopoulou, T.~Pressburger, and J.~Schumann, ``Capture, analyze, diagnose: Realizability checking of requirements in {FRET},'' in {\em Computer Aided Verification} (S.~Shoham and Y.~Vizel, eds.), pp.~490--504, Springer International Publishing.
\bibitem{baier_principles_2008}
C.~Baier and J.-P. Katoen, {\em Principles of Model Checking}.
\newblock {MIT} Press.
\bibitem{meyer_strix_2018}
P.~J. Meyer, S.~Sickert, and M.~Luttenberger, ``Strix: Explicit reactive synthesis strikes back!,'' in {\em Computer Aided Verification} (H.~Chockler and G.~Weissenbacher, eds.), pp.~578--586, Springer International Publishing.
\bibitem{jacobs_reactive_2024}
S.~Jacobs {\em et~al.}, ``The reactive synthesis competition ({SYNTCOMP}): 2018-2021.''
\bibitem{branicky_multiple_1998}
M.~Branicky, ``Multiple lyapunov functions and other analysis tools for switched and hybrid systems,'' vol.~43, no.~4, pp.~475--482.
\bibitem{bansal_hamilton-jacobi_2017}
S.~Bansal, M.~Chen, S.~Herbert, and C.~J. Tomlin, ``Hamilton-jacobi reachability: A brief overview and recent advances,'' in {\em 2017 {IEEE} 56th Annual Conference on Decision and Control ({CDC})}, pp.~2242--2253.
\bibitem{guernic_reachability_2009}
C.~L. Guernic, ``Reachability analysis of hybrid systems with linear continuous dynamics.''
\bibitem{frehse_spaceex_2011}
G.~Frehse, C.~Le~Guernic, A.~Donzé, S.~Cotton, R.~Ray, O.~Lebeltel, R.~Ripado, A.~Girard, T.~Dang, and O.~Maler, ``{SpaceEx}: Scalable verification of hybrid systems,'' in {\em Computer Aided Verification} (G.~Gopalakrishnan and S.~Qadeer, eds.), pp.~379--395, Springer.
\bibitem{mitchell_time-dependent_2005}
I.~Mitchell, A.~Bayen, and C.~Tomlin, ``A time-dependent hamilton-jacobi formulation of reachable sets for continuous dynamic games,'' vol.~50, no.~7, pp.~947--957.
\bibitem{prajna_safety_2004}
S.~Prajna and A.~Jadbabaie, ``Safety verification of hybrid systems using barrier certificates,'' in {\em Hybrid Systems: Computation and Control} (R.~Alur and G.~J. Pappas, eds.), pp.~477--492, Springer.
\bibitem{eia_lcoe_2022}
{U.S. Energy Information Administration}, ``Levelized costs of new generation resources in the annual energy outlook 2022,'' report, U.S. Energy Information Administration, March 2022.
\newblock See Table 1b, page 9.
\bibitem{eesi_datacenter_2024}
{Environmental and Energy Study Institute}, ``Data center energy needs are upending power grids and threatening the climate.'' Web article, 2024.
\newblock Accessed: 2025-09-29.
\end{thebibliography}

View File

@ -9,53 +9,64 @@ 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 "eia_lcoe_2022"
Warning--I didn't find a database entry for "eesi_datacenter_2024"
Warning--entry type for "guernic_reachability_2009" isn't style-file defined
--line 221 of file references.bib
Warning--I didn't find a database entry for "a"
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 13 entries,
Warning--empty year in katis_capture_2022
Warning--empty year in baier_principles_2008
Warning--empty year in meyer_strix_2018
Warning--empty journal in branicky_multiple_1998
Warning--empty year in branicky_multiple_1998
Warning--empty year in bansal_hamilton-jacobi_2017
Warning--empty year in frehse_spaceex_2011
Warning--empty journal in mitchell_time-dependent_2005
Warning--empty year in mitchell_time-dependent_2005
Warning--empty year in prajna_safety_2004
You've used 25 entries,
1876 wiz_defined-function locations,
544 strings with 5480 characters,
and the built_in function-call counts, 2138 in all, are:
= -- 192
> -- 92
609 strings with 7729 characters,
and the built_in function-call counts, 5612 in all, are:
= -- 511
> -- 249
< -- 2
+ -- 38
- -- 25
* -- 130
:= -- 326
add.period$ -- 14
call.type$ -- 13
change.case$ -- 15
+ -- 93
- -- 68
* -- 382
:= -- 798
add.period$ -- 27
call.type$ -- 25
change.case$ -- 27
chr.to.int$ -- 0
cite$ -- 19
duplicate$ -- 92
empty$ -- 229
format.name$ -- 25
if$ -- 511
cite$ -- 41
duplicate$ -- 260
empty$ -- 567
format.name$ -- 68
if$ -- 1343
int.to.chr$ -- 0
int.to.str$ -- 13
missing$ -- 2
newline$ -- 44
num.names$ -- 12
pop$ -- 57
int.to.str$ -- 25
missing$ -- 11
newline$ -- 83
num.names$ -- 32
pop$ -- 125
preamble$ -- 1
purify$ -- 0
quote$ -- 0
skip$ -- 74
skip$ -- 204
stack$ -- 0
substring$ -- 44
swap$ -- 22
substring$ -- 276
swap$ -- 86
text.length$ -- 2
text.prefix$ -- 0
top$ -- 0
type$ -- 0
warning$ -- 6
while$ -- 16
width$ -- 15
write$ -- 107
(There were 11 warnings)
warning$ -- 16
while$ -- 53
width$ -- 27
write$ -- 210
(There were 21 warnings)

View File

@ -1,13 +1,13 @@
# Fdb version 4
["bibtex main"] 1764974760.71217 "main.aux" "main.bbl" "main" 1764975051.10496 0
"./references.bib" 1764974759.12837 5129 de2dc116e7908a86456f09f33e7d7ac7 ""
["bibtex main"] 1764980933.98858 "main.aux" "main.bbl" "main" 1764982133.83346 0
"./references.bib" 1764980611.90841 14069 2a4f74c587187a8a71049043171eb0fe ""
"/usr/share/texlive/texmf-dist/bibtex/bst/base/ieeetr.bst" 1292289607 18361 1a00e58565e7f19bf2b3e1bfb82254ae ""
"main.aux" 1764975050.94085 7608 f4f0b295bef52d13062032206cc95973 "pdflatex"
"main.aux" 1764982133.67597 7881 be02d2f847fcfd08f6011a189f2fc9cf "pdflatex"
(generated)
"main.bbl"
"main.blg"
(rewritten before read)
["pdflatex"] 1764975050.20677 "main.tex" "main.pdf" "main" 1764975051.10514 0
["pdflatex"] 1764982132.94482 "main.tex" "main.pdf" "main" 1764982133.83364 0
"/etc/texmf/web2c/texmf.cnf" 1726065852.27662 475 c0e671620eb5563b2130f56340a5fde8 ""
"/usr/share/texlive/texmf-dist/fonts/enc/dvips/base/8r.enc" 1165713224 4850 80dc9bab7f31fb78a000ccfed0e27cab ""
"/usr/share/texlive/texmf-dist/fonts/map/fontname/texfonts.map" 1577235249 3524 cb3e574dea2d1052e39280babc910dc8 ""
@ -40,6 +40,7 @@
"/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb" 1248133631 35752 024fb6c41858982481f6968b5fc26508 ""
"/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb" 1248133631 32569 5e5ddc8df908dea60932f3c484a54c0d ""
"/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt12.pfb" 1248133631 24252 1e4e051947e12dfb50fee0b7f4e26e3a ""
"/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/symbols/msam10.pfb" 1248133631 31764 459c573c03a4949a528c2cc7f557e217 ""
"/usr/share/texlive/texmf-dist/fonts/type1/urw/symbol/usyr.pfb" 1136849748 33709 b09d2e140b7e807d3a97058263ab6693 ""
"/usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmb8a.pfb" 1136849748 44729 811d6c62865936705a31c797a1d5dada ""
"/usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmbi8a.pfb" 1136849748 44656 0cbca70e0534538582128f6b54593cca ""
@ -241,21 +242,21 @@
"/usr/share/texmf/web2c/texmf.cnf" 1707919699 40399 f2c302f7d2af602abb742093540a5834 ""
"/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map" 1760105440.02229 5312232 f3296911be9cc021788f3f879cf0a47d ""
"/var/lib/texmf/web2c/pdftex/pdflatex.fmt" 1726065868 6800790 607442c924ed54405961d2b8ac2a25ae ""
"broader-impacts/v1.tex" 1762446356.88898 4913 f040011f0dbfa050cad013bb8737b473 ""
"budget/v1.tex" 1762446356.88898 12864 1341c4cfdaf82dc649f2f47f3cc8ecd7 ""
"1-goals-and-outcomes/v6.tex" 1760575541.11104 6070 286ca847b1aac31431e0658cd2989ea2 ""
"2-state-of-the-art/v6.tex" 1764975691.95583 13373 7b26a8331e52f6fdbd3c6203283d61a8 ""
"3-research-approach/v4.tex" 1764982131.29739 17588 1f9490df80ab110e8accd0d34a67ef15 ""
"4-metrics-of-success/v1.tex" 1760575541.11204 6867 9f08b3208bb158042e2fc9bbfeecae68 ""
"5-risks-and-contingencies/v1.tex" 1762446356.89155 15209 c8ff47d0cfbf72d9c457463c5114f2a8 ""
"6-broader-impacts/v1.tex" 1762446356.88898 4913 f040011f0dbfa050cad013bb8737b473 ""
"7-budget/v1.tex" 1762446356.88898 12864 1341c4cfdaf82dc649f2f47f3cc8ecd7 ""
"8-schedule/v1.tex" 1764192995.54631 8440 1c6c59ab8379c2aee45e5ad9b447e61d ""
"9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf" 1764192995.54731 76839 d12cfa78304f51e96ce0e12460ece1e3 ""
"9-supplemental-sections/cv-1786798.pdf" 1764192995.54731 31602 224112b9f507ae1e989c0341a7eb3f42 ""
"9-supplemental-sections/v1.tex" 1764975820.90587 2306 2e5bf084cf72f93d80cf9138d1569d6f ""
"dane_proposal_format.cls" 1764974397.2375 2570 f29186d8a9397205c58fccc0fcffb76c ""
"goals-and-outcomes/v6.tex" 1760575541.11104 6070 286ca847b1aac31431e0658cd2989ea2 ""
"main.aux" 1764975050.94085 7608 f4f0b295bef52d13062032206cc95973 "pdflatex"
"main.bbl" 1764974760.75697 2467 75ddd8bc744ac1d7c685bc124699a008 "bibtex main"
"main.tex" 1764974466.74023 804 d25a45e5732ab0e63adac220a8893f96 ""
"metrics-of-success/v1.tex" 1760575541.11204 6867 9f08b3208bb158042e2fc9bbfeecae68 ""
"research-approach/v3.tex" 1760575541.11304 17351 6ed3e4ff3c33dd86d80597dbdb0cf36f ""
"risks-and-contingencies/v1.tex" 1762446356.89155 15209 c8ff47d0cfbf72d9c457463c5114f2a8 ""
"schedule/v1.tex" 1764192995.54631 8440 1c6c59ab8379c2aee45e5ad9b447e61d ""
"state-of-the-art/v6.tex" 1764975048.60283 13382 c10ff226a1b21f79fbc41b5ad41d2e48 ""
"supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf" 1764192995.54731 76839 d12cfa78304f51e96ce0e12460ece1e3 ""
"supplemental-sections/cv-1786798.pdf" 1764192995.54731 31602 224112b9f507ae1e989c0341a7eb3f42 ""
"supplemental-sections/v1.tex" 1764192995.54731 2302 accf9c1dd3b7c2f35a3a051140113d63 ""
"main.aux" 1764982133.67597 7881 be02d2f847fcfd08f6011a189f2fc9cf "pdflatex"
"main.bbl" 1764980934.02731 5012 668a266823d48f68a9ac1ddb0c83466e "bibtex main"
"main.tex" 1764979384.78263 822 20061a5e271518c18336f9c3c88b120c ""
(generated)
"main.aux"
"main.log"

View File

@ -260,311 +260,3 @@ INPUT /usr/share/texlive/texmf-dist/tex/latex/gincltex/gincltex.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/gincltex/gincltex.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/gincltex/gincltex.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/svn-prov/svn-prov.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/svn-prov/svn-prov.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/adjustbox/adjustbox.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/adjustbox/adjustbox.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/adjustbox/adjcalc.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/adjustbox/adjcalc.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/adjustbox/trimclip.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/adjustbox/trimclip.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/collectbox/collectbox.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/collectbox/collectbox.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/adjustbox/tc-pdftex.def
INPUT /usr/share/texlive/texmf-dist/tex/latex/adjustbox/tc-pdftex.def
INPUT /usr/share/texlive/texmf-dist/tex/latex/adjustbox/tc-pdftex.def
INPUT /usr/share/texlive/texmf-dist/tex/latex/ifoddpage/ifoddpage.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/ifoddpage/ifoddpage.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/ifoddpage/ifoddpage.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/varwidth/varwidth.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/varwidth/varwidth.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/varwidth/varwidth.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/filemod/filemod-expmin.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/filemod/filemod-expmin.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/booktabs/booktabs.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/booktabs/booktabs.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/tools/tabularx.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/tools/tabularx.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/tools/array.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/tools/array.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/makecell/makecell.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/makecell/makecell.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/tools/dcolumn.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/tools/dcolumn.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/multirow/multirow.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/multirow/multirow.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/graphics/lscape.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/graphics/lscape.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/enumitem/enumitem.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/enumitem/enumitem.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/listings/listings.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/listings/listings.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/listings/lstmisc.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/listings/lstmisc.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/listings/lstmisc.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/listings/listings.cfg
INPUT /usr/share/texlive/texmf-dist/tex/latex/listings/listings.cfg
INPUT /usr/share/texlive/texmf-dist/tex/latex/listings/listings.cfg
INPUT /usr/share/texlive/texmf-dist/tex/latex/pgfgantt/pgfgantt.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/pgfgantt/pgfgantt.sty
INPUT /usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarybackgrounds.code.tex
INPUT /usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarybackgrounds.code.tex
INPUT /usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarypatterns.code.tex
INPUT /usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarypatterns.code.tex
INPUT /usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/pgflibrarypatterns.code.tex
INPUT /usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/pgflibrarypatterns.code.tex
INPUT /usr/share/texlive/texmf-dist/tex/latex/pgf/utilities/pgfcalendar.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/pgf/utilities/pgfcalendar.sty
INPUT /usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfcalendar.code.tex
INPUT /usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfcalendar.code.tex
INPUT /usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfcalendar.code.tex
INPUT /usr/share/texlive/texmf-dist/tex/latex/colortbl/colortbl.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/colortbl/colortbl.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/graphics/color.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/ot1ptm.fd
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/ot1ptm.fd
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/ot1ptm.fd
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm
INPUT /usr/share/texlive/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def
INPUT /usr/share/texlive/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def
INPUT ./main.aux
INPUT ./main.aux
INPUT main.aux
OUTPUT main.aux
INPUT /usr/share/texlive/texmf-dist/tex/latex/fmtcount/fc-english.def
INPUT /usr/share/texlive/texmf-dist/tex/latex/fmtcount/fc-english.def
INPUT /usr/share/texlive/texmf-dist/tex/latex/fmtcount/fc-english.def
INPUT /usr/share/texlive/texmf-dist/tex/context/base/mkii/supp-pdf.mkii
INPUT /usr/share/texlive/texmf-dist/tex/context/base/mkii/supp-pdf.mkii
INPUT /usr/share/texlive/texmf-dist/tex/context/base/mkii/supp-pdf.mkii
INPUT /usr/share/texlive/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg
INPUT /usr/share/texlive/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg
INPUT /usr/share/texlive/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg
INPUT /usr/share/texlive/texmf-dist/tex/latex/pdflscape/pdflscape.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/pdflscape/pdflscape.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/pdflscape/pdflscape-nometadata.sty
INPUT /usr/share/texlive/texmf-dist/tex/latex/pdflscape/pdflscape-nometadata.sty
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/ot1ztmcm.fd
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/ot1ztmcm.fd
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/ot1ztmcm.fd
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7t.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7t.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7t.tfm
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/omlztmcm.fd
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/omlztmcm.fd
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/omlztmcm.fd
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/omsztmcm.fd
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/omsztmcm.fd
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/omsztmcm.fd
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/omxztmcm.fd
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/omxztmcm.fd
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/omxztmcm.fd
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmr7t.vf
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm
INPUT /var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map
INPUT /usr/share/texlive/texmf-dist/fonts/enc/dvips/base/8r.enc
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmr7t.vf
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmr7t.vf
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm
INPUT ./goals-and-outcomes/v6.tex
INPUT ./goals-and-outcomes/v6.tex
INPUT ./goals-and-outcomes/v6.tex
INPUT ./goals-and-outcomes/v6.tex
INPUT goals-and-outcomes/v6.tex
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmb7t.vf
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb8r.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmr7t.vf
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmb7t.vf
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb8r.tfm
INPUT ./state-of-the-art/v6.tex
INPUT ./state-of-the-art/v6.tex
INPUT ./state-of-the-art/v6.tex
INPUT ./state-of-the-art/v6.tex
INPUT state-of-the-art/v6.tex
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmri7t.vf
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri8r.tfm
INPUT ./research-approach/v3.tex
INPUT ./research-approach/v3.tex
INPUT ./research-approach/v3.tex
INPUT ./research-approach/v3.tex
INPUT research-approach/v3.tex
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7t.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7t.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7t.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/zptmcm7t.vf
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmr10.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/zptmcm7m.vf
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/psyro.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmmi10.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/zptmcm7y.vf
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmsy10.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/rsfs/rsfs10.tfm
INPUT ./metrics-of-success/v1.tex
INPUT ./metrics-of-success/v1.tex
INPUT ./metrics-of-success/v1.tex
INPUT ./metrics-of-success/v1.tex
INPUT metrics-of-success/v1.tex
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmbi7t.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmbi7t.vf
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmbi8r.tfm
INPUT ./risks-and-contingencies/v1.tex
INPUT ./risks-and-contingencies/v1.tex
INPUT ./risks-and-contingencies/v1.tex
INPUT ./risks-and-contingencies/v1.tex
INPUT risks-and-contingencies/v1.tex
INPUT ./broader-impacts/v1.tex
INPUT ./broader-impacts/v1.tex
INPUT ./broader-impacts/v1.tex
INPUT ./broader-impacts/v1.tex
INPUT broader-impacts/v1.tex
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/ts1ptm.fd
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/ts1ptm.fd
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/ts1ptm.fd
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr8c.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmr8c.vf
INPUT ./main.bbl
INPUT ./main.bbl
INPUT main.bbl
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmtt12.tfm
INPUT ./budget/v1.tex
INPUT ./budget/v1.tex
INPUT ./budget/v1.tex
INPUT ./budget/v1.tex
INPUT budget/v1.tex
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7t.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr8c.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmb7t.vf
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb8r.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmr8c.vf
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmri7t.vf
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri8r.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb8c.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmb8c.vf
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri8c.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmri8c.vf
INPUT ./schedule/v1.tex
INPUT ./schedule/v1.tex
INPUT ./schedule/v1.tex
INPUT ./schedule/v1.tex
INPUT schedule/v1.tex
INPUT ./supplemental-sections/v1.tex
INPUT ./supplemental-sections/v1.tex
INPUT ./supplemental-sections/v1.tex
INPUT ./supplemental-sections/v1.tex
INPUT supplemental-sections/v1.tex
INPUT ./supplemental-sections/cv-1786798.pdf
INPUT ./supplemental-sections/cv-1786798.pdf
INPUT ./supplemental-sections/cv-1786798.pdf
INPUT ./supplemental-sections/cv-1786798.pdf
INPUT ./supplemental-sections/cv-1786798.pdf
INPUT ./supplemental-sections/cv-1786798.pdf
INPUT ./supplemental-sections/cv-1786798.pdf
INPUT ./supplemental-sections/cv-1786798.pdf
INPUT ./supplemental-sections/cv-1786798.pdf
INPUT ./supplemental-sections/cv-1786798.pdf
INPUT ./supplemental-sections/cv-1786798.pdf
INPUT ./supplemental-sections/cv-1786798.pdf
INPUT ./supplemental-sections/cv-1786798.pdf
INPUT ./supplemental-sections/cv-1786798.pdf
INPUT ./supplemental-sections/cv-1786798.pdf
INPUT ./supplemental-sections/cv-1786798.pdf
INPUT ./supplemental-sections/cv-1786798.pdf
INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf
INPUT main.aux
INPUT /usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb
INPUT /usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb
INPUT /usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb
INPUT /usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt12.pfb
INPUT /usr/share/texlive/texmf-dist/fonts/type1/urw/symbol/usyr.pfb
INPUT /usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmb8a.pfb
INPUT /usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmbi8a.pfb
INPUT /usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmr8a.pfb
INPUT /usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmri8a.pfb

View File

@ -1,4 +1,4 @@
This is pdfTeX, Version 3.141592653-2.6-1.40.25 (TeX Live 2023/Debian) (preloaded format=pdflatex 2024.9.11) 5 DEC 2025 17:50
This is pdfTeX, Version 3.141592653-2.6-1.40.25 (TeX Live 2023/Debian) (preloaded format=pdflatex 2024.9.11) 5 DEC 2025 19:50
entering extended mode
restricted \write18 enabled.
file:line:error style messages enabled.
@ -491,576 +491,4 @@ File: tikzlibrarychains.code.tex 2023-01-15 v3.1.10 (3.1.10)
\pgfdecoratedinputsegmentremainingdistance=\dimen274
\pgf@decorate@distancetomove=\dimen275
\pgf@decorate@repeatstate=\count321
\pgfdecorationsegmentamplitude=\dimen276
\pgfdecorationsegmentlength=\dimen277
)
\tikz@lib@dec@box=\box86
) (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/decorations/pgflibrarydecorations.markings.code.tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshadows.code.tex
File: tikzlibraryshadows.code.tex 2023-01-15 v3.1.10 (3.1.10)
(/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryfadings.code.tex
File: tikzlibraryfadings.code.tex 2023-01-15 v3.1.10 (3.1.10)
(/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/pgflibraryfadings.code.tex
File: pgflibraryfadings.code.tex 2023-01-15 v3.1.10 (3.1.10)
))) (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/pgflibraryarrows.meta.code.tex
File: pgflibraryarrows.meta.code.tex 2023-01-15 v3.1.10 (3.1.10)
\pgfarrowinset=\dimen278
\pgfarrowlength=\dimen279
\pgfarrowwidth=\dimen280
\pgfarrowlinewidth=\dimen281
) (/usr/share/texlive/texmf-dist/tex/latex/standalone/standalone.sty
Package: standalone 2022/10/10 v1.3b Package to include TeX sub-files with preambles
(/usr/share/texlive/texmf-dist/tex/latex/tools/shellesc.sty
Package: shellesc 2023/07/08 v1.0d unified shell escape interface for LaTeX
Package shellesc Info: Restricted shell escape enabled on input line 77.
) (/usr/share/texlive/texmf-dist/tex/latex/currfile/currfile.sty
Package: currfile 2022/10/10 v0.8 Provides the file path elements of the current input file
(/usr/share/texlive/texmf-dist/tex/latex/kvoptions/kvoptions.sty
Package: kvoptions 2022-06-15 v3.15 Key value format for package options (HO)
(/usr/share/texlive/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty
Package: ltxcmds 2023-12-04 v1.26 LaTeX kernel commands for general use (HO)
) (/usr/share/texlive/texmf-dist/tex/latex/kvsetkeys/kvsetkeys.sty
Package: kvsetkeys 2022-10-05 v1.19 Key value parser (HO)
)) (/usr/share/texlive/texmf-dist/tex/latex/filehook/filehook.sty
Package: filehook 2022/10/25 v0.8b Hooks for input files
(/usr/share/texlive/texmf-dist/tex/latex/filehook/filehook-2020.sty
Package: filehook-2020 2022/10/25 v0.8b Hooks for input files
))
\c@currfiledepth=\count322
) (/usr/share/texlive/texmf-dist/tex/latex/gincltex/gincltex.sty (/usr/share/texlive/texmf-dist/tex/latex/svn-prov/svn-prov.sty
Package: svn-prov 2010/04/24 v3.1862 Package Date/Version from SVN Keywords
)
Package: gincltex 2011/09/04 v0.3 Include external LaTeX files like graphics
(/usr/share/texlive/texmf-dist/tex/latex/adjustbox/adjustbox.sty
Package: adjustbox 2022/10/17 v1.3a Adjusting TeX boxes (trim, clip, ...)
(/usr/share/texlive/texmf-dist/tex/latex/adjustbox/adjcalc.sty
Package: adjcalc 2012/05/16 v1.1 Provides advanced setlength with multiple back-ends (calc, etex, pgfmath)
) (/usr/share/texlive/texmf-dist/tex/latex/adjustbox/trimclip.sty
Package: trimclip 2020/08/19 v1.2 Trim and clip general TeX material
(/usr/share/texlive/texmf-dist/tex/latex/collectbox/collectbox.sty
Package: collectbox 2022/10/17 v0.4c Collect macro arguments as boxes
\collectedbox=\box87
)
\tc@llx=\dimen282
\tc@lly=\dimen283
\tc@urx=\dimen284
\tc@ury=\dimen285
Package trimclip Info: Using driver 'tc-pdftex.def'.
(/usr/share/texlive/texmf-dist/tex/latex/adjustbox/tc-pdftex.def
File: tc-pdftex.def 2019/01/04 v2.2 Clipping driver for pdftex
))
\adjbox@Width=\dimen286
\adjbox@Height=\dimen287
\adjbox@Depth=\dimen288
\adjbox@Totalheight=\dimen289
\adjbox@pwidth=\dimen290
\adjbox@pheight=\dimen291
\adjbox@pdepth=\dimen292
\adjbox@ptotalheight=\dimen293
(/usr/share/texlive/texmf-dist/tex/latex/ifoddpage/ifoddpage.sty
Package: ifoddpage 2022/10/18 v1.2 Conditionals for odd/even page detection
\c@checkoddpage=\count323
)
(/usr/share/texlive/texmf-dist/tex/latex/varwidth/varwidth.sty
Package: varwidth 2009/03/30 ver 0.92; Variable-width minipages
\@vwid@box=\box88
\sift@deathcycles=\count324
\@vwid@loff=\dimen294
\@vwid@roff=\dimen295
))
\gincltex@box=\box89
) (/usr/share/texlive/texmf-dist/tex/latex/filemod/filemod-expmin.sty
Package: filemod-expmin 2011/09/19 v1.2 Get and compare file modification times (expandable; minimal)
)) (/usr/share/texlive/texmf-dist/tex/latex/booktabs/booktabs.sty
Package: booktabs 2020/01/12 v1.61803398 Publication quality tables
\heavyrulewidth=\dimen296
\lightrulewidth=\dimen297
\cmidrulewidth=\dimen298
\belowrulesep=\dimen299
\belowbottomsep=\dimen300
\aboverulesep=\dimen301
\abovetopsep=\dimen302
\cmidrulesep=\dimen303
\cmidrulekern=\dimen304
\defaultaddspace=\dimen305
\@cmidla=\count325
\@cmidlb=\count326
\@aboverulesep=\dimen306
\@belowrulesep=\dimen307
\@thisruleclass=\count327
\@lastruleclass=\count328
\@thisrulewidth=\dimen308
) (/usr/share/texlive/texmf-dist/tex/latex/tools/tabularx.sty
Package: tabularx 2023/07/08 v2.11c `tabularx' package (DPC)
(/usr/share/texlive/texmf-dist/tex/latex/tools/array.sty
Package: array 2023/10/16 v2.5g Tabular extension package (FMi)
\col@sep=\dimen309
\ar@mcellbox=\box90
\extrarowheight=\dimen310
\NC@list=\toks43
\extratabsurround=\skip57
\backup@length=\skip58
\ar@cellbox=\box91
)
\TX@col@width=\dimen311
\TX@old@table=\dimen312
\TX@old@col=\dimen313
\TX@target=\dimen314
\TX@delta=\dimen315
\TX@cols=\count329
\TX@ftn=\toks44
) (/usr/share/texlive/texmf-dist/tex/latex/makecell/makecell.sty
Package: makecell 2009/08/03 V0.1e Managing of Tab Column Heads and Cells
\rotheadsize=\dimen316
\c@nlinenum=\count330
\TeXr@lab=\toks45
) (/usr/share/texlive/texmf-dist/tex/latex/tools/dcolumn.sty
Package: dcolumn 2023/07/08 v1.06 decimal alignment package (DPC)
) (/usr/share/texlive/texmf-dist/tex/latex/multirow/multirow.sty
Package: multirow 2021/03/15 v2.8 Span multiple rows of a table
\multirow@colwidth=\skip59
\multirow@cntb=\count331
\multirow@dima=\skip60
\bigstrutjot=\dimen317
) (/usr/share/texlive/texmf-dist/tex/latex/graphics/lscape.sty
Package: lscape 2020/05/28 v3.02 Landscape Pages (DPC)
) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty
Package: amsmath 2023/05/13 v2.17o AMS math features
\@mathmargin=\skip61
For additional information on amsmath, use the `?' option.
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty
Package: amstext 2021/08/26 v2.01 AMS text
) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty
Package: amsbsy 1999/11/29 v1.2d Bold Symbols
\pmbraise@=\dimen318
) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty
Package: amsopn 2022/04/08 v2.04 operator names
)
\inf@bad=\count332
LaTeX Info: Redefining \frac on input line 234.
\uproot@=\count333
\leftroot@=\count334
LaTeX Info: Redefining \overline on input line 399.
LaTeX Info: Redefining \colon on input line 410.
\classnum@=\count335
\DOTSCASE@=\count336
LaTeX Info: Redefining \ldots on input line 496.
LaTeX Info: Redefining \dots on input line 499.
LaTeX Info: Redefining \cdots on input line 620.
\Mathstrutbox@=\box92
\strutbox@=\box93
LaTeX Info: Redefining \big on input line 722.
LaTeX Info: Redefining \Big on input line 723.
LaTeX Info: Redefining \bigg on input line 724.
LaTeX Info: Redefining \Bigg on input line 725.
\big@size=\dimen319
LaTeX Font Info: Redeclaring font encoding OML on input line 743.
LaTeX Font Info: Redeclaring font encoding OMS on input line 744.
\macc@depth=\count337
LaTeX Info: Redefining \bmod on input line 905.
LaTeX Info: Redefining \pmod on input line 910.
LaTeX Info: Redefining \smash on input line 940.
LaTeX Info: Redefining \relbar on input line 970.
LaTeX Info: Redefining \Relbar on input line 971.
\c@MaxMatrixCols=\count338
\dotsspace@=\muskip17
\c@parentequation=\count339
\dspbrk@lvl=\count340
\tag@help=\toks46
\row@=\count341
\column@=\count342
\maxfields@=\count343
\andhelp@=\toks47
\eqnshift@=\dimen320
\alignsep@=\dimen321
\tagshift@=\dimen322
\tagwidth@=\dimen323
\totwidth@=\dimen324
\lineht@=\dimen325
\@envbody=\toks48
\multlinegap=\skip62
\multlinetaggap=\skip63
\mathdisplay@stack=\toks49
LaTeX Info: Redefining \[ on input line 2953.
LaTeX Info: Redefining \] on input line 2954.
) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty
Package: amssymb 2013/01/14 v3.01 AMS font symbols
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty
Package: amsfonts 2013/01/14 v3.01 Basic AMSFonts support
\symAMSa=\mathgroup6
\symAMSb=\mathgroup7
LaTeX Font Info: Overwriting math alphabet `\mathfrak' in version `bold'
(Font) U/euf/m/n --> U/euf/b/n on input line 106.
)) (/usr/share/texlive/texmf-dist/tex/latex/enumitem/enumitem.sty
Package: enumitem 2019/06/20 v3.9 Customized lists
\labelindent=\skip64
\enit@outerparindent=\dimen326
\enit@toks=\toks50
\enit@inbox=\box94
\enit@count@id=\count344
\enitdp@description=\count345
) (/usr/share/texlive/texmf-dist/tex/latex/listings/listings.sty
\lst@mode=\count346
\lst@gtempboxa=\box95
\lst@token=\toks51
\lst@length=\count347
\lst@currlwidth=\dimen327
\lst@column=\count348
\lst@pos=\count349
\lst@lostspace=\dimen328
\lst@width=\dimen329
\lst@newlines=\count350
\lst@lineno=\count351
\lst@maxwidth=\dimen330
(/usr/share/texlive/texmf-dist/tex/latex/listings/lstmisc.sty
File: lstmisc.sty 2023/02/27 1.9 (Carsten Heinz)
\c@lstnumber=\count352
\lst@skipnumbers=\count353
\lst@framebox=\box96
) (/usr/share/texlive/texmf-dist/tex/latex/listings/listings.cfg
File: listings.cfg 2023/02/27 1.9 listings configuration
))
Package: listings 2023/02/27 1.9 (Carsten Heinz)
(/usr/share/texlive/texmf-dist/tex/latex/pgfgantt/pgfgantt.sty
Package: pgfgantt 2018/01/10 v5.0 Draw Gantt diagrams with TikZ
(/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarybackgrounds.code.tex
File: tikzlibrarybackgrounds.code.tex 2023-01-15 v3.1.10 (3.1.10)
\pgf@layerbox@background=\box97
\pgf@layerboxsaved@background=\box98
) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarypatterns.code.tex
File: tikzlibrarypatterns.code.tex 2023-01-15 v3.1.10 (3.1.10)
(/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/pgflibrarypatterns.code.tex
File: pgflibrarypatterns.code.tex 2023-01-15 v3.1.10 (3.1.10)
)) (/usr/share/texlive/texmf-dist/tex/latex/pgf/utilities/pgfcalendar.sty (/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfcalendar.code.tex
File: pgfcalendar.code.tex 2023-01-15 v3.1.10 (3.1.10)
\pgfcalendarcurrentjulian=\count354
\pgf@cal@easter@Y=\count355
\pgf@cal@easter@G=\count356
\pgf@cal@easter@C=\count357
\pgf@cal@easter@X=\count358
\pgf@cal@easter@Z=\count359
\pgf@cal@easter@D=\count360
\pgf@cal@easter@E=\count361
\pgf@cal@easter@N=\count362
\pgf@cal@easter@M=\count363
\pgf@cal@easter@julianday=\count364
))
\gtt@currentline=\count365
\gtt@lasttitleline=\count366
\gtt@currgrid=\count367
\gtt@chartwidth=\count368
\gtt@lasttitleslot=\count369
\gtt@elementid=\count370
\gtt@today@slot=\count371
\gtt@startjulian=\count372
\gtt@endjulian=\count373
\gtt@chartid=\count374
\gtt@vrule@slot=\count375
\gtt@calendar@slots=\count376
\gtt@calendar@weeknumber=\count377
\gtt@calendar@startofweek=\count378
\gtt@left@slot=\count379
\gtt@right@slot=\count380
)
\figurewidth=\skip65
\figureheight=\skip66
\c@task=\count381
) (/usr/share/texlive/texmf-dist/tex/latex/colortbl/colortbl.sty
Package: colortbl 2022/06/20 v1.0f Color table columns (DPC)
\everycr=\toks52
\minrowclearance=\skip67
\rownum=\count382
)
LaTeX Font Info: Trying to load font information for OT1+ptm on input line 10.
(/usr/share/texlive/texmf-dist/tex/latex/psnfss/ot1ptm.fd
File: ot1ptm.fd 2001/06/04 font definitions for OT1/ptm.
) (/usr/share/texlive/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def
File: l3backend-pdftex.def 2024-01-04 L3 backend support: PDF output (pdfTeX)
\l__color_backend_stack_int=\count383
\l__pdf_internal_box=\box99
) (./main.aux)
\openout1 = `main.aux'.
LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 10.
LaTeX Font Info: ... okay on input line 10.
LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 10.
LaTeX Font Info: ... okay on input line 10.
LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 10.
LaTeX Font Info: ... okay on input line 10.
LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 10.
LaTeX Font Info: ... okay on input line 10.
LaTeX Font Info: Checking defaults for TS1/cmr/m/n on input line 10.
LaTeX Font Info: ... okay on input line 10.
LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 10.
LaTeX Font Info: ... okay on input line 10.
LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 10.
LaTeX Font Info: ... okay on input line 10.
*geometry* driver: auto-detecting
*geometry* detected driver: pdftex
*geometry* verbose mode - [ preamble ] result:
* driver: pdftex
* paper: <default>
* layout: <same size as paper>
* layoutoffset:(h,v)=(0.0pt,0.0pt)
* modes:
* h-part:(L,W,R)=(72.26999pt, 469.75502pt, 72.26999pt)
* v-part:(T,H,B)=(72.26999pt, 650.43001pt, 72.26999pt)
* \paperwidth=614.295pt
* \paperheight=794.96999pt
* \textwidth=469.75502pt
* \textheight=650.43001pt
* \oddsidemargin=0.0pt
* \evensidemargin=0.0pt
* \topmargin=-37.0pt
* \headheight=12.0pt
* \headsep=25.0pt
* \topskip=12.0pt
* \footskip=30.0pt
* \marginparwidth=44.0pt
* \marginparsep=10.0pt
* \columnsep=10.0pt
* \skip\footins=10.8pt plus 4.0pt minus 2.0pt
* \hoffset=0.0pt
* \voffset=0.0pt
* \mag=1000
* \@twocolumnfalse
* \@twosidefalse
* \@mparswitchfalse
* \@reversemarginfalse
* (1in=72.27pt=25.4mm, 1cm=28.453pt)
(/usr/share/texlive/texmf-dist/tex/latex/fmtcount/fc-english.def
File: fc-english.def 2016/01/12
) (/usr/share/texlive/texmf-dist/tex/context/base/mkii/supp-pdf.mkii
[Loading MPS to PDF converter (version 2006.09.02).]
\scratchcounter=\count384
\scratchdimen=\dimen331
\scratchbox=\box100
\nofMPsegments=\count385
\nofMParguments=\count386
\everyMPshowfont=\toks53
\MPscratchCnt=\count387
\MPscratchDim=\dimen332
\MPnumerator=\count388
\makeMPintoPDFobject=\count389
\everyMPtoPDFconversion=\toks54
) (/usr/share/texlive/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty
Package: epstopdf-base 2020-01-24 v2.11 Base part for package epstopdf
Package epstopdf-base Info: Redefining graphics rule for `.eps' on input line 485.
(/usr/share/texlive/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg
File: epstopdf-sys.cfg 2010/07/13 v1.3 Configuration of (r)epstopdf for TeX Live
)) (/usr/share/texlive/texmf-dist/tex/latex/pdflscape/pdflscape.sty
Package: pdflscape 2022-10-27 v0.13 Display of landscape pages in PDF
(/usr/share/texlive/texmf-dist/tex/latex/pdflscape/pdflscape-nometadata.sty
Package: pdflscape-nometadata 2022-10-28 v0.13 Display of landscape pages in PDF (HO)
Package pdflscape Info: Auto-detected driver: pdftex on input line 81.
))
\c@lstlisting=\count390
LaTeX Font Info: Trying to load font information for OT1+ztmcm on input line 12.
(/usr/share/texlive/texmf-dist/tex/latex/psnfss/ot1ztmcm.fd
File: ot1ztmcm.fd 2000/01/03 Fontinst v1.801 font definitions for OT1/ztmcm.
)
LaTeX Font Info: Trying to load font information for OML+ztmcm on input line 12.
(/usr/share/texlive/texmf-dist/tex/latex/psnfss/omlztmcm.fd
File: omlztmcm.fd 2000/01/03 Fontinst v1.801 font definitions for OML/ztmcm.
)
LaTeX Font Info: Trying to load font information for OMS+ztmcm on input line 12.
(/usr/share/texlive/texmf-dist/tex/latex/psnfss/omsztmcm.fd
File: omsztmcm.fd 2000/01/03 Fontinst v1.801 font definitions for OMS/ztmcm.
)
LaTeX Font Info: Trying to load font information for OMX+ztmcm on input line 12.
(/usr/share/texlive/texmf-dist/tex/latex/psnfss/omxztmcm.fd
File: omxztmcm.fd 2000/01/03 Fontinst v1.801 font definitions for OMX/ztmcm.
)
LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <14.4> not available
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 12.
LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <10.95> not available
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 12.
LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <8> not available
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 12.
[1
{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}{/usr/share/texlive/texmf-dist/fonts/enc/dvips/base/8r.enc}] (./goals-and-outcomes/v6.tex [1]) (./state-of-the-art/v6.tex [2] [3] [4]) (./research-approach/v3.tex [5]
LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <12> not available
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 8.
LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <9> not available
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 8.
LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <7> not available
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 8.
[6] [7] [8] [9]) (./metrics-of-success/v1.tex [10] [11]) (./risks-and-contingencies/v1.tex [12] [13] [14]) (./broader-impacts/v1.tex [15]
LaTeX Font Info: Trying to load font information for TS1+ptm on input line 14.
(/usr/share/texlive/texmf-dist/tex/latex/psnfss/ts1ptm.fd
File: ts1ptm.fd 2001/06/04 font definitions for TS1/ptm.
)
LaTeX Warning: Citation `eia_lcoe_2022' on page 16 undefined on input line 14.
LaTeX Warning: Citation `eesi_datacenter_2024' on page 16 undefined on input line 16.
LaTeX Warning: Citation `eia_lcoe_2022' on page 16 undefined on input line 21.
[16]) [17] (./main.bbl
Underfull \hbox (badness 10000) in paragraph at lines 32--33
\OT1/cmtt/m/n/12 nuclear . org / information -[] library / safety -[] and -[] security / safety -[] of -[]
[]
) [18] (./budget/v1.tex
LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <6> not available
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 22.
[19] [20] [21]
Overfull \hbox (22.53047pt too wide) in paragraph at lines 264--271
[] []\OT1/ptm/b/n/12 Uni-ver-sity In-fras-truc-ture[] \OT1/ptm/m/n/12 The Uni-ver-sity of Pitts-burgh pro-vides com-pre-hen-sive MAT-LAB/Simulink
[]
) (./schedule/v1.tex [22]
Missing character: There is no , in font nullfont!
Overfull \hbox (35.80641pt too wide) in paragraph at lines 61--62
[][]
[]
[23]) (./supplemental-sections/v1.tex [24]
<supplemental-sections/cv-1786798.pdf, id=118, 614.295pt x 794.97pt>
File: supplemental-sections/cv-1786798.pdf Graphic file (type pdf)
<use supplemental-sections/cv-1786798.pdf>
Package pdftex.def Info: supplemental-sections/cv-1786798.pdf used on input line 4.
(pdftex.def) Requested size: 614.29349pt x 794.96806pt.
File: supplemental-sections/cv-1786798.pdf Graphic file (type pdf)
<use supplemental-sections/cv-1786798.pdf>
Package pdftex.def Info: supplemental-sections/cv-1786798.pdf used on input line 4.
(pdftex.def) Requested size: 614.29349pt x 794.96806pt.
<supplemental-sections/cv-1786798.pdf, id=121, page=1, 614.295pt x 794.97pt>
File: supplemental-sections/cv-1786798.pdf Graphic file (type pdf)
<use supplemental-sections/cv-1786798.pdf, page 1>
Package pdftex.def Info: supplemental-sections/cv-1786798.pdf , page1 used on input line 4.
(pdftex.def) Requested size: 614.29349pt x 794.96806pt.
File: supplemental-sections/cv-1786798.pdf Graphic file (type pdf)
<use supplemental-sections/cv-1786798.pdf, page 1>
Package pdftex.def Info: supplemental-sections/cv-1786798.pdf , page1 used on input line 4.
(pdftex.def) Requested size: 614.58406pt x 795.3441pt.
[25]
File: supplemental-sections/cv-1786798.pdf Graphic file (type pdf)
<use supplemental-sections/cv-1786798.pdf, page 1>
Package pdftex.def Info: supplemental-sections/cv-1786798.pdf , page1 used on input line 4.
(pdftex.def) Requested size: 614.58406pt x 795.3441pt.
File: supplemental-sections/cv-1786798.pdf Graphic file (type pdf)
<use supplemental-sections/cv-1786798.pdf, page 1>
Package pdftex.def Info: supplemental-sections/cv-1786798.pdf , page1 used on input line 4.
(pdftex.def) Requested size: 614.58406pt x 795.3441pt.
File: supplemental-sections/cv-1786798.pdf Graphic file (type pdf)
<use supplemental-sections/cv-1786798.pdf, page 1>
Package pdftex.def Info: supplemental-sections/cv-1786798.pdf , page1 used on input line 4.
(pdftex.def) Requested size: 614.58406pt x 795.3441pt.
[26
<./supplemental-sections/cv-1786798.pdf>]
<supplemental-sections/cv-1786798.pdf, id=141, page=2, 614.295pt x 794.97pt>
File: supplemental-sections/cv-1786798.pdf Graphic file (type pdf)
<use supplemental-sections/cv-1786798.pdf, page 2>
Package pdftex.def Info: supplemental-sections/cv-1786798.pdf , page2 used on input line 4.
(pdftex.def) Requested size: 614.58406pt x 795.3441pt.
File: supplemental-sections/cv-1786798.pdf Graphic file (type pdf)
<use supplemental-sections/cv-1786798.pdf, page 2>
Package pdftex.def Info: supplemental-sections/cv-1786798.pdf , page2 used on input line 4.
(pdftex.def) Requested size: 614.58406pt x 795.3441pt.
File: supplemental-sections/cv-1786798.pdf Graphic file (type pdf)
<use supplemental-sections/cv-1786798.pdf, page 2>
Package pdftex.def Info: supplemental-sections/cv-1786798.pdf , page2 used on input line 4.
(pdftex.def) Requested size: 614.58406pt x 795.3441pt.
[27
<./supplemental-sections/cv-1786798.pdf>]
<supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf, id=145, 614.295pt x 794.97pt>
File: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf Graphic file (type pdf)
<use supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf>
Package pdftex.def Info: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf used on input line 7.
(pdftex.def) Requested size: 614.29349pt x 794.96806pt.
File: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf Graphic file (type pdf)
<use supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf>
Package pdftex.def Info: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf used on input line 7.
(pdftex.def) Requested size: 614.29349pt x 794.96806pt.
<supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf, id=148, page=1, 614.295pt x 794.97pt>
File: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf Graphic file (type pdf)
<use supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf, page 1>
Package pdftex.def Info: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf , page1 used on input line 7.
(pdftex.def) Requested size: 614.29349pt x 794.96806pt.
File: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf Graphic file (type pdf)
<use supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf, page 1>
Package pdftex.def Info: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf , page1 used on input line 7.
(pdftex.def) Requested size: 614.58406pt x 795.3441pt.
[28]
File: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf Graphic file (type pdf)
<use supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf, page 1>
Package pdftex.def Info: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf , page1 used on input line 7.
(pdftex.def) Requested size: 614.58406pt x 795.3441pt.
File: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf Graphic file (type pdf)
<use supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf, page 1>
Package pdftex.def Info: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf , page1 used on input line 7.
(pdftex.def) Requested size: 614.58406pt x 795.3441pt.
File: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf Graphic file (type pdf)
<use supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf, page 1>
Package pdftex.def Info: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf , page1 used on input line 7.
(pdftex.def) Requested size: 614.58406pt x 795.3441pt.
[29
<./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf>]
<supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf, id=172, page=2, 614.295pt x 794.97pt>
File: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf Graphic file (type pdf)
<use supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf, page 2>
Package pdftex.def Info: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf , page2 used on input line 7.
(pdftex.def) Requested size: 614.58406pt x 795.3441pt.
File: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf Graphic file (type pdf)
<use supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf, page 2>
Package pdftex.def Info: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf , page2 used on input line 7.
(pdftex.def) Requested size: 614.58406pt x 795.3441pt.
File: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf Graphic file (type pdf)
<use supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf, page 2>
Package pdftex.def Info: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf , page2 used on input line 7.
(pdftex.def) Requested size: 614.58406pt x 795.3441pt.
[30
<./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf>]
<supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf, id=177, page=3, 614.295pt x 794.97pt>
File: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf Graphic file (type pdf)
<use supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf, page 3>
Package pdftex.def Info: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf , page3 used on input line 7.
(pdftex.def) Requested size: 614.58406pt x 795.3441pt.
File: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf Graphic file (type pdf)
<use supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf, page 3>
Package pdftex.def Info: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf , page3 used on input line 7.
(pdftex.def) Requested size: 614.58406pt x 795.3441pt.
File: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf Graphic file (type pdf)
<use supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf, page 3>
Package pdftex.def Info: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf , page3 used on input line 7.
(pdftex.def) Requested size: 614.58406pt x 795.3441pt.
[31
<./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf>]) [32] (./main.aux)
***********
LaTeX2e <2023-11-01> patch level 1
L3 programming layer <2024-01-22>
***********
LaTeX Warning: There were undefined references.
)
Here is how much of TeX's memory you used:
26056 strings out of 476182
542834 string characters out of 5795595
1947975 words of memory out of 5000000
47475 multiletter control sequences out of 15000+600000
596976 words of font info for 119 fonts, out of 8000000 for 9000
14 hyphenation exceptions out of 8191
110i,17n,107p,1062b,952s stack positions out of 10000i,1000n,20000p,200000b,200000s
</usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt12.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/symbol/usyr.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmb8a.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmbi8a.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmr8a.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmri8a.pfb>
Output written on main.pdf (33 pages, 254858 bytes).
PDF statistics:
225 PDF objects out of 1000 (max. 8388607)
133 compressed objects within 2 object streams
0 named destinations out of 1000 (max. 500000)
164 words of extra memory for PDF output out of 10000 (max. 10000000)
\pgfdecorationsegmentamplitude=\

Binary file not shown.

View File

Binary file not shown.

View File

@ -10,19 +10,19 @@
\begin{document}
\maketitle
\input{goals-and-outcomes/v6}
\input{state-of-the-art/v6}
\input{research-approach/v3}
\input{metrics-of-success/v1}
\input{risks-and-contingencies/v1}
\input{broader-impacts/v1}
\input{1-goals-and-outcomes/v7}
\input{2-state-of-the-art/v6}
\input{3-research-approach/v4}
\input{4-metrics-of-success/v2}
\input{5-risks-and-contingencies/v1}
\input{6-broader-impacts/v1}
\newpage
\bibliographystyle{ieeetr}
\bibliography{references}
\newpage
\input{budget/v1}
\input{schedule/v1}
\input{supplemental-sections/v1}
\input{7-budget/v1}
\input{8-schedule/v1}
\input{9-supplemental-sections/v1}
% White Paper

View File

@ -122,3 +122,190 @@ Publisher: Idaho National Engineering and Environmental Laboratory},
number = {TLR-RES-RES/DE-2024-005},
note = {NRC Contract 31310021C0014}
}
@techreport{eia_lcoe_2022,
author = {{U.S. Energy Information Administration}},
title = {Levelized Costs of New Generation Resources in the Annual Energy Outlook 2022},
institution = {U.S. Energy Information Administration},
year = {2022},
month = {March},
type = {Report},
url = {https://www.eia.gov/outlooks/aeo/pdf/electricity_generation.pdf},
note = {See Table 1b, page 9}
}
@misc{eesi_datacenter_2024,
author = {{Environmental and Energy Study Institute}},
title = {Data Center Energy Needs Are Upending Power Grids and Threatening the Climate},
howpublished = {Web article},
year = {2024},
url = {https://www.eesi.org/articles/view/data-center-energy-needs-are-upending-power-grids-and-threatening-the-climate},
note = {Accessed: 2025-09-29}
}
@book{baier_principles_2008,
location = {Cambridge, {MA}, {USA}},
title = {Principles of Model Checking},
isbn = {978-0-262-02649-9},
abstract = {A comprehensive introduction to the foundations of model checking, a fully automated technique for finding flaws in hardware and software; with extensive examples and both practical and theoretical exercises.},
pagetotal = {984},
publisher = {{MIT} Press},
author = {Baier, Christel and Katoen, Joost-Pieter},
date = {2008-04-25},
langid = {english},
}
@inproceedings{katis_capture_2022,
location = {Cham},
title = {Capture, Analyze, Diagnose: Realizability Checking Of Requirements in {FRET}},
isbn = {978-3-031-13188-2},
doi = {10.1007/978-3-031-13188-2_24},
shorttitle = {Capture, Analyze, Diagnose},
pages = {490--504},
booktitle = {Computer Aided Verification},
publisher = {Springer International Publishing},
author = {Katis, Andreas and Mavridou, Anastasia and Giannakopoulou, Dimitra and Pressburger, Thomas and Schumann, Johann},
editor = {Shoham, Sharon and Vizel, Yakir},
date = {2022},
langid = {english},
file = {Full Text PDF:/home/danesabo/Zotero/storage/3JPVH8U2/Katis et al. - 2022 - Capture, Analyze, Diagnose Realizability Checking Of Requirements in FRET.pdf:application/pdf},
}
@inproceedings{meyer_strix_2018,
location = {Cham},
title = {Strix: Explicit Reactive Synthesis Strikes Back!},
isbn = {978-3-319-96145-3},
doi = {10.1007/978-3-319-96145-3_31},
shorttitle = {Strix},
pages = {578--586},
booktitle = {Computer Aided Verification},
publisher = {Springer International Publishing},
author = {Meyer, Philipp J. and Sickert, Salomon and Luttenberger, Michael},
editor = {Chockler, Hana and Weissenbacher, Georg},
date = {2018},
langid = {english},
}
@misc{jacobs_reactive_2024,
title = {The Reactive Synthesis Competition ({SYNTCOMP}): 2018-2021},
url = {http://arxiv.org/abs/2206.00251},
doi = {10.48550/arXiv.2206.00251},
shorttitle = {The Reactive Synthesis Competition ({SYNTCOMP})},
number = {{arXiv}:2206.00251},
publisher = {{arXiv}},
author = {Jacobs, Swen and others},
urldate = {2025-12-06},
date = {2024-05-06},
eprinttype = {arxiv},
eprint = {2206.00251 [cs]},
keywords = {Computer Science - Logic in Computer Science},
file = {Preprint PDF:/home/danesabo/Zotero/storage/GU6W5UH4/Jacobs et al. - 2024 - The Reactive Synthesis Competition (SYNTCOMP) 2018-2021.pdf:application/pdf;Snapshot:/home/danesabo/Zotero/storage/57UPK6A5/2206.html:text/html},
}
@article{branicky_multiple_1998,
title = {Multiple Lyapunov functions and other analysis tools for switched and hybrid systems},
volume = {43},
issn = {1558-2523},
url = {https://ieeexplore.ieee.org/document/664150},
doi = {10.1109/9.664150},
pages = {475--482},
number = {4},
journaltitle = {{IEEE} Transactions on Automatic Control},
author = {Branicky, M.S.},
urldate = {2025-09-10},
date = {1998-04},
keywords = {Automata, Control systems, Difference equations, Differential equations, Lagrangian functions, Limit-cycles, Lyapunov method, Stability analysis, Switched systems, Switches},
file = {PDF:/home/danesabo/Zotero/storage/5AQWDPAA/Branicky - 1998 - Multiple Lyapunov functions and other analysis tools for switched and hybrid systems.pdf:application/pdf},
}
@thesis{guernic_reachability_2009,
title = {Reachability Analysis of Hybrid Systems with Linear Continuous Dynamics},
url = {https://theses.hal.science/tel-00422569},
institution = {Université Joseph-Fourier - Grenoble I},
type = {phdthesis},
author = {Guernic, Colas Le},
urldate = {2025-09-14},
date = {2009-10-28},
langid = {english},
file = {Full Text PDF:/home/danesabo/Zotero/storage/A5XNTDZ9/Guernic - 2009 - Reachability Analysis of Hybrid Systems with Linear Continuous Dynamics.pdf:application/pdf},
}
@inproceedings{alur_hybrid_1993,
location = {Berlin, Heidelberg},
title = {Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems},
isbn = {978-3-540-48060-0},
doi = {10.1007/3-540-57318-6_30},
shorttitle = {Hybrid automata},
pages = {209--229},
booktitle = {Hybrid Systems},
publisher = {Springer},
author = {Alur, Rajeev and Courcoubetis, Costas and Henzinger, Thomas A. and Ho, Pei -Hsin},
editor = {Grossman, Robert L. and Nerode, Anil and Ravn, Anders P. and Rischel, Hans},
date = {1993},
langid = {english},
keywords = {Acceptance Condition, Hybrid Automaton, Hybrid System, Mutual Exclusion, Reachability Problem},
file = {Full Text PDF:/home/danesabo/Zotero/storage/WBXYUC86/Alur et al. - 1993 - Hybrid automata An algorithmic approach to the specification and verification of hybrid systems.pdf:application/pdf},
}
@article{mitchell_time-dependent_2005,
title = {A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games},
volume = {50},
issn = {1558-2523},
url = {https://ieeexplore.ieee.org/abstract/document/1463302},
doi = {10.1109/TAC.2005.851439},
pages = {947--957},
number = {7},
journaltitle = {{IEEE} Transactions on Automatic Control},
author = {Mitchell, I.M. and Bayen, A.M. and Tomlin, C.J.},
urldate = {2025-09-15},
date = {2005-07},
keywords = {Aircraft, Collaborative software, Collision avoidance, Computational modeling, Differential games, 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,
title = {Hamilton-Jacobi reachability: A brief overview and recent advances},
url = {https://ieeexplore.ieee.org/abstract/document/8263977},
doi = {10.1109/CDC.2017.8263977},
shorttitle = {Hamilton-Jacobi reachability},
eventtitle = {2017 {IEEE} 56th Annual Conference on Decision and Control ({CDC})},
pages = {2242--2253},
booktitle = {2017 {IEEE} 56th Annual Conference on Decision and Control ({CDC})},
author = {Bansal, Somil and Chen, Mo and Herbert, Sylvia and Tomlin, Claire J.},
urldate = {2025-09-15},
date = {2017-12},
keywords = {Aircraft, Games, Level set, Safety, Tools, Trajectory, Tutorials},
file = {Snapshot:/home/danesabo/Zotero/storage/EEK5IE93/8263977.html:text/html;Submitted Version:/home/danesabo/Zotero/storage/BMNLZ9DW/Bansal et al. - 2017 - Hamilton-Jacobi reachability A brief overview and recent advances.pdf:application/pdf},
}
@inproceedings{prajna_safety_2004,
location = {Berlin, Heidelberg},
title = {Safety Verification of Hybrid Systems Using Barrier Certificates},
isbn = {978-3-540-24743-2},
doi = {10.1007/978-3-540-24743-2_32},
pages = {477--492},
booktitle = {Hybrid Systems: Computation and Control},
publisher = {Springer},
author = {Prajna, Stephen and Jadbabaie, Ali},
editor = {Alur, Rajeev and Pappas, George J.},
date = {2004},
langid = {english},
keywords = {Continuous State, Discrete Transition, Hybrid System, Integral Constraint, Reachability Analysis},
}