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

Auto sync: 2026-03-04 13:00:34 (8 files changed)

Browse Source 
M  3-research-approach/v3.tex

M  main.aux

M  main.blg

M  main.fdb_latexmk

M  main.log

M  main.pdf

M  main.synctex.gz

M  main.toc
This commit is contained in:
Dane Sabo 2026-03-04 13:00:34 -05:00
parent c3309cf4a4
commit f1b43da96f
8 changed files with 125 additions and 142 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

202
3-research-approach/v3.tex
View File

@ -144,7 +144,7 @@ complex reactor operations.
% 2. SYSTEM REQUIREMENTS AND SPECIFICATIONS % 2. SYSTEM REQUIREMENTS AND SPECIFICATIONS
% ---------------------------------------------------------------------------- % ----------------------------------------------------------------------------
\subsection{System Requirements and Specifications} \subsection{System Requirements, Specifications, and Discrete Controllers}
Human control of nuclear power can be divided into three different scopes: Human control of nuclear power can be divided into three different scopes:
strategic, operational, and tactical. Strategic control is high-level and strategic, operational, and tactical. Strategic control is high-level and
long-term decision making for the plant. This level has objectives that are long-term decision making for the plant. This level has objectives that are
@ -175,15 +175,6 @@ which tactical control law to apply.
%Say something about autonomous control systems near here? %Say something about autonomous control systems near here?
Before constructing a HAHACS, we must completely describe its
intended behavior. The behavior of any control system originates in
requirements: statements about what the system must do, must not do, and under
what conditions. For nuclear systems, these requirements derive from multiple
sources including regulatory mandates, design basis analyses, and operating
procedures. The challenge is formalizing these requirements with sufficient
precision that they can serve as the foundation for autonomous control system
synthesis and verification.
\begin{figure} \begin{figure}
\centering \centering
@ -232,24 +223,15 @@ control scope.
The method of constructing a HAHACS in this proposal leverages two key The method of constructing a HAHACS in this proposal leverages two key
observations about current practice. First, the operational scope control is observations about current practice. First, the operational scope control is
effectively discrete control. Second, the rules for implementing this control effectively discrete control. Second, the rules for implementing this control
are described prior to their implementation in operating procedures. We can are described prior to their implementation in operating procedures. Before
exploit these facts by formalizing the rules for transitioning between discrete constructing a HAHACS, we must completely describe its intended behavior. The
states using temporal logic. behavior of any control system originates in requirements: statements about what
the system must do, must not do, and under what conditions. For nuclear systems,
\textcolor{blue}{The discrete predicates that trigger mode transitions are these requirements derive from multiple sources including regulatory mandates,
Boolean functions over the continuous state space: $p_i: \mathcal{X} design basis analyses, and operating procedures. The challenge is formalizing
\rightarrow \{\text{true}, \text{false}\}$. These predicates formalize these requirements with sufficient precision that they can serve as the
conditions like ``coolant temperature exceeds 315°C'' or ``pressurizer level foundation for autonomous control system synthesis and verification. We can
is between 30\% and 60\%.'' Critically, we do not impose this discrete build these requirements using temporal logic.
abstraction artificially. Operating procedures for nuclear systems already
define go/no-go conditions as discrete predicates. These thresholds come from
design basis safety analysis and have been validated over decades of
operational experience. Our methodology assumes this domain knowledge exists
and provides a framework to formalize it. This is why the approach is
feasible for nuclear applications specifically: the hard work of defining
safe operating boundaries has already been done by generations of nuclear
engineers. We are formalizing existing practice, not inventing new
abstractions.}
Temporal logic is a powerful set of semantics for building systems with complex Temporal logic is a powerful set of semantics for building systems with complex
but deterministic behavior. Temporal logic extends classical propositional logic but deterministic behavior. Temporal logic extends classical propositional logic
@ -262,7 +244,20 @@ logic statements. These specifications form the basis of any proofs about a
HAHACS and constitute the fundamental truth statements about what the behavior HAHACS and constitute the fundamental truth statements about what the behavior
of the system is designed to be. of the system is designed to be.
\textcolor{blue}{Linear temporal logic (LTL) is particularly well-suited for Discrete mode transitions include predicates that are Boolean functions over the
continuous state space: $p_i: \mathcal{X} \rightarrow \{\text{true},
\text{false}\}$. These predicates formalize conditions like ``coolant
temperature exceeds 315°C'' or ``pressurizer level is between 30\% and 60\%.''
Critically, we do not impose this discrete abstraction artificially. Operating
procedures for nuclear systems already define go/no-go conditions as discrete
predicates. These thresholds come from design basis safety analysis and have
been validated over decades of operational experience. Our methodology assumes
this domain knowledge exists and provides a framework to formalize it. This is
why the approach is feasible for nuclear applications specifically: the hard
work of defining safe operating boundaries has already been done by generations
of nuclear engineers.
Linear temporal logic (LTL) is particularly well-suited for
specifying reactive systems. LTL formulas are built from atomic propositions specifying reactive systems. LTL formulas are built from atomic propositions
(our discrete predicates) using Boolean connectives and temporal operators. (our discrete predicates) using Boolean connectives and temporal operators.
The key temporal operators are: The key temporal operators are:
@ -275,7 +270,8 @@ The key temporal operators are:
These operators allow us to express safety properties (``the reactor never These operators allow us to express safety properties (``the reactor never
enters an unsafe configuration''), liveness properties (``the system enters an unsafe configuration''), liveness properties (``the system
eventually reaches operating temperature''), and response properties (``if eventually reaches operating temperature''), and response properties (``if
coolant pressure drops, the system initiates shutdown within bounded time'').} coolant pressure drops, the system initiates shutdown within bounded time'').
To build these temporal logic statements, an intermediary tool called FRET is To build these temporal logic statements, an intermediary tool called FRET is
planned to be used. FRET stands for Formal Requirements Elicitation Tool, and planned to be used. FRET stands for Formal Requirements Elicitation Tool, and
@ -297,6 +293,7 @@ implementation. Second, it clearly demonstrates where natural language documents
are insufficient. These procedures may still be used by human operators, so any are insufficient. These procedures may still be used by human operators, so any
room for interpretation is a weakness that must be addressed. room for interpretation is a weakness that must be addressed.
(Some examples of where FRET has been used and why it will be successful here)
%%% NOTES (Section 2): %%% NOTES (Section 2):
% - Add concrete FRET example showing requirement → FRETish → LTL % - Add concrete FRET example showing requirement → FRETish → LTL
% - Discuss hysteresis and how to prevent mode chattering near boundaries % - Discuss hysteresis and how to prevent mode chattering near boundaries
@ -307,8 +304,6 @@ room for interpretation is a weakness that must be addressed.
% 3. DISCRETE CONTROLLER SYNTHESIS % 3. DISCRETE CONTROLLER SYNTHESIS
% ---------------------------------------------------------------------------- % ----------------------------------------------------------------------------
\subsection{Discrete Controller Synthesis}
Once system requirements are defined as temporal logic specifications, we use Once system requirements are defined as temporal logic specifications, we use
them to build the discrete control system. To do this, reactive synthesis tools them to build the discrete control system. To do this, reactive synthesis tools
are employed. Reactive synthesis is a field in computer science that deals with are employed. Reactive synthesis is a field in computer science that deals with
@ -316,50 +311,37 @@ the automated creation of reactive programs from temporal logic specifications.
A reactive program is one that, for a given state, takes an input and produces A reactive program is one that, for a given state, takes an input and produces
an output. Our systems fit exactly this mold: the current discrete state and an output. Our systems fit exactly this mold: the current discrete state and
status of guard conditions are the input, while the output is the next discrete status of guard conditions are the input, while the output is the next discrete
state. The output of a reactive synthesis algorithm is a discrete automaton. state.
\textcolor{blue}{Reactive synthesis solves the following problem: given an LTL Reactive synthesis solves the following problem: given an LTL formula $\varphi$
formula $\varphi$ that specifies desired system behavior, automatically that specifies desired system behavior, automatically construct a finite-state
construct a finite-state machine (strategy) that produces outputs in response machine (strategy) that produces outputs in response to environment inputs such
to environment inputs such that all resulting execution traces satisfy that all resulting execution traces satisfy $\varphi$. If such a strategy
$\varphi$. If such a strategy exists, the specification is called exists, the specification is called \emph{realizable}. The synthesis algorithm
\emph{realizable}. The synthesis algorithm either produces a correct-by-construction either produces a correct-by-construction controller or reports that no such
controller or reports that no such controller can exist. This realizability controller can exist. This realizability check is itself valuable: an
check is itself valuable: an unrealizable specification indicates conflicting unrealizable specification indicates conflicting or impossible requirements in
or impossible requirements in the original procedures.} the original procedures.
The main advantage of reactive synthesis is that at no point in the production The main advantage of reactive synthesis is that at no point in the production
of the discrete automaton is human engineering of the implementation required. of the discrete automaton is human engineering of the implementation required.
The resultant automaton is correct by construction. This method of construction The resultant automaton is correct by construction. This method of construction
eliminates the possibility of human error at the implementation stage entirely. eliminates the possibility of human error at the implementation stage entirely.
Instead, the effort on the human designer is directed at the specification of Instead, the effort on the human designer is directed at the specification of
system behavior itself. system behavior itself. This has two critical implications. First, it makes the
creation of the discrete controller tractable. The reasons the controller
changes between modes can be traced back to the specification and thus to any
requirements, which provides a trace for liability and justification of system
behavior. Second, discrete control decisions made by humans are reliant on the
human operator operating correctly. Humans are intrinsically probabilistic
creatures who cannot eliminate human error. By defining the behavior of this
system using temporal logics and synthesizing the controller using deterministic
algorithms, we are assured that strategic decisions will always be made
according to operating procedures.
This has two critical implications. First, it makes the creation of the (Talk about how one would go from a discrete automaton to actual code)
controller tractable. The reasons the controller changes between modes can be
traced back to the specification and thus to any requirements, which provides a
trace for liability and justification of system behavior. Second, discrete
control decisions made by humans are reliant on the human operator operating
correctly. Humans are intrinsically probabilistic creatures who cannot eliminate
human error. By defining the behavior of this system using temporal logics and
synthesizing the controller using deterministic algorithms, we are assured that
strategic decisions will always be made according to operating procedures.
\textcolor{blue}{FRET can export specifications directly to formats compatible (Examples of reactive synthesis in the wild)
with reactive synthesis solvers such as Strix, a state-of-the-art LTL
synthesis tool. The synthesis pipeline proceeds as follows:
\begin{enumerate}
\item Operating procedures are formalized in FRET's structured English
\item FRET translates requirements to past-time or future-time LTL
\item Realizability analysis checks for specification conflicts
\item If realizable, synthesis produces a Mealy machine implementing the
discrete controller
\item The Mealy machine is compiled to executable code for the target
platform
\end{enumerate}
This pipeline provides complete traceability from natural language procedures
to verified implementation, with each step producing artifacts that can be
independently reviewed and validated.}
%%% NOTES (Section 3): %%% NOTES (Section 3):
% - Mention computational complexity of synthesis (doubly exponential worst case) % - Mention computational complexity of synthesis (doubly exponential worst case)
@ -371,60 +353,55 @@ independently reviewed and validated.}
% 4. CONTINUOUS CONTROLLERS % 4. CONTINUOUS CONTROLLERS
% ---------------------------------------------------------------------------- % ----------------------------------------------------------------------------
\subsection{Continuous Controllers} \subsection{Continuous Control Modes}
The synthesis of the discrete operational controller is only half of an The synthesis of the discrete operational controller is only half of an
autonomous controller. These control systems are hybrid, with both discrete and autonomous controller. These control systems are hybrid, with both discrete and
continuous components. This section describes the continuous control modes that continuous components. This section describes the continuous control modes that
execute within each discrete state, and how we verify that they satisfy execute within each discrete state, and how we verify that they satisfy the
the requirements imposed by the discrete layer. requirements imposed by the discrete layer. It is important to clarify the scope
of this methodology with respect to continuous controller design. This work
\textcolor{blue}{It is important to clarify the scope of this methodology with verifies continuous controllers; it does not synthesize them. The distinction
respect to continuous controller design. This work verifies continuous parallels model checking in software verification: model checking does not tell
controllers; it does not synthesize them. The distinction parallels model engineers how to write correct software, but it verifies whether a given
checking in software verification: model checking does not tell engineers how implementation satisfies its specification. Similarly, we assume that continuous
to write correct software, but it verifies whether a given implementation controllers can be designed using standard control theory techniques. Our
satisfies its specification. Similarly, we assume that continuous controllers contribution is a verification framework that confirms candidate controllers
can be designed using standard control theory techniques. Our contribution is compose correctly with the discrete layer to produce a safe hybrid system.
a verification framework that confirms candidate controllers compose correctly
with the discrete layer to produce a safe hybrid system.}
The operational control scope defines go/no-go decisions that determine what The operational control scope defines go/no-go decisions that determine what
kind of continuous control to implement. The entry or exit conditions of a kind of continuous control to implement. The entry or exit conditions of a
discrete state are themselves the guard conditions $\mathcal{G}$ that define the discrete state are themselves the guard conditions $\mathcal{G}$ that define the
boundaries for each continuous controller. These continuous controllers all boundaries for each continuous controller's allowed state-space region. These
share a common state space, but each individual continuous control mode operates continuous controllers all share a common state space, but each individual
within its own partition defined by the discrete state $q_i$ and the associated continuous control mode operates within its own partition defined by the
guards. This partitioning of the continuous state space among several discrete discrete state $q_i$ and the associated guards. This partitioning of the
vector fields has traditionally been a difficult problem for validation and continuous state space among several discrete vector fields has traditionally
verification. The discontinuity of the vector fields at discrete state been a difficult problem for validation and verification. The discontinuity of
interfaces makes reachability analysis computationally expensive, and analytic the vector fields at discrete state interfaces makes reachability analysis
solutions often become intractable. computationally expensive, and analytic solutions often become intractable
\cite{MANYUS THESIS}.
We circumvent these issues by designing our hybrid system from the bottom up We circumvent these issues by designing our hybrid system from the bottom up
with verification in mind. Each continuous control mode has an input set and with verification in mind. Each continuous control mode has an input set and
output set clearly defined by our discrete transitions \textit{a priori}. output set clearly defined by our discrete transitions \textit{a priori}.
Consider that we define the continuous state space as $\mathcal{X}$. Whenever we Consider that we define the continuous state space as $\mathcal{X}$. Each
create guard conditions from our design requirements, we are effectively discrete mode $q_i$ then provides three key pieces of information for continuous
creating subsets $\mathcal{X}_{entry,i}$ and $\mathcal{X}_{exit,i}$ for each controller design:
discrete mode $q_i$. These subsets define when state transitions occur between
discrete modes. More importantly, when building continuous control modes, they
become control objectives.
\textcolor{blue}{Mathematically, each discrete mode $q_i$ provides three key
pieces of information for continuous controller design:
\begin{enumerate} \begin{enumerate}
\item \textbf{Entry conditions:} $\mathcal{X}_{entry,i} \subseteq \mathcal{X}$, \item \textbf{Entry conditions:} $\mathcal{X}_{entry,i} \subseteq \mathcal{X}$,
the set of possible initial states when entering this mode the set of possible initial states when entering this mode
\item \textbf{Exit conditions:} $\mathcal{X}_{exit,i} \subseteq \mathcal{X}$, \item \textbf{Exit conditions:} $\mathcal{X}_{exit,i} \subseteq \mathcal{X}$,
the target states that trigger transition to the next mode the target states that trigger transition to the next mode, or is the region
in the state space a stabilizing mode remains within.
\item \textbf{Safety invariants:} $\mathcal{X}_{safe,i} \subseteq \mathcal{X}$, \item \textbf{Safety invariants:} $\mathcal{X}_{safe,i} \subseteq \mathcal{X}$,
the envelope of safe states during operation in this mode the envelope of safe states during operation in this mode. These are derived
from invariants \(Inv\).
\end{enumerate} \end{enumerate}
These sets come directly from the discrete controller synthesis and define These sets come directly from the discrete controller synthesis and define
precise objectives for continuous control. The continuous controller for mode precise objectives for continuous control. The continuous controller for mode
$q_i$ must drive the system from any state in $\mathcal{X}_{entry,i}$ to some $q_i$ must drive the system from any state in $\mathcal{X}_{entry,i}$ to some
state in $\mathcal{X}_{exit,i}$ while remaining within $\mathcal{X}_{safe,i}$.} state in $\mathcal{X}_{exit,i}$ while remaining within $\mathcal{X}_{safe,i}$.
We classify continuous controllers into three types based on their objectives: We classify continuous controllers into three types based on their objectives:
transitory, stabilizing, and expulsory. Each type has distinct verification transitory, stabilizing, and expulsory. Each type has distinct verification
@ -441,13 +418,13 @@ requirements that determine which formal methods tools are appropriate.
\subsubsection{Transitory Modes} \subsubsection{Transitory Modes}
\textcolor{blue}{Transitory modes are continuous controllers designed to move Transitory modes are continuous controllers designed to move
the plant from one discrete operating condition to another. Their purpose is to the plant from one discrete operating condition to another. Their purpose is to
execute transitions: starting from entry conditions, reaching exit conditions, execute transitions: starting from entry conditions, reach exit conditions,
while maintaining safety throughout. Examples include power ramp-up sequences, and maintain safety invariants throughout. Examples include power ramp-up sequences,
cooldown procedures, and load-following maneuvers.} cooldown procedures, and load-following maneuvers.
\textcolor{blue}{The control objective for a transitory mode can be stated The control objective for a transitory mode can be stated
formally. Given entry conditions $\mathcal{X}_{entry}$, exit conditions formally. Given entry conditions $\mathcal{X}_{entry}$, exit conditions
$\mathcal{X}_{exit}$, safety invariant $\mathcal{X}_{safe}$, and closed-loop $\mathcal{X}_{exit}$, safety invariant $\mathcal{X}_{safe}$, and closed-loop
dynamics $\dot{x} = f(x, u(x))$, the controller must satisfy: dynamics $\dot{x} = f(x, u(x))$, the controller must satisfy:
@ -456,9 +433,9 @@ dynamics $\dot{x} = f(x, u(x))$, the controller must satisfy:
\land \forall t \in [0,T]: x(t) \in \mathcal{X}_{safe} \land \forall t \in [0,T]: x(t) \in \mathcal{X}_{safe}
\] \]
That is, from any valid entry state, the trajectory must eventually reach the That is, from any valid entry state, the trajectory must eventually reach the
exit condition without ever leaving the safe region.} exit condition without ever leaving the safe region.
\textcolor{blue}{Verification of transitory modes uses reachability analysis. Verification of transitory modes uses reachability analysis.
Reachability analysis computes the set of all states reachable from a given Reachability analysis computes the set of all states reachable from a given
initial set under the system dynamics. For a transitory mode to be valid, the initial set under the system dynamics. For a transitory mode to be valid, the
reachable set from $\mathcal{X}_{entry}$ must satisfy two conditions: reachable set from $\mathcal{X}_{entry}$ must satisfy two conditions:
@ -471,9 +448,9 @@ reachable set from $\mathcal{X}_{entry}$ must satisfy two conditions:
Formally, if $\text{Reach}(\mathcal{X}_{entry}, f, [0,T])$ denotes the states Formally, if $\text{Reach}(\mathcal{X}_{entry}, f, [0,T])$ denotes the states
reachable within time horizon $T$: reachable within time horizon $T$:
\[ \[
\text{Reach}(\mathcal{X}_{entry}, f, [0,T]) \subseteq \mathcal{X}_{safe} \land \text{Reach}(\mathcal{X}_{entry}, f_i, [0,T]) \subseteq \mathcal{X}_{safe} \land
\text{Reach}(\mathcal{X}_{entry}, f, [0,T]) \cap \mathcal{X}_{exit} \neq \emptyset \text{Reach}(\mathcal{X}_{entry}, f_i, [0,T]) \cap \mathcal{X}_{exit} \neq \emptyset
\]} \]
Because the discrete controller defines clear boundaries in continuous state Because the discrete controller defines clear boundaries in continuous state
space, the verification problem for each transitory mode is well-posed. We know space, the verification problem for each transitory mode is well-posed. We know
@ -481,14 +458,13 @@ the possible initial conditions, we know the target conditions, and we know the
safety envelope. The verification task is to confirm that the candidate safety envelope. The verification task is to confirm that the candidate
continuous controller achieves the objective from all possible starting points. continuous controller achieves the objective from all possible starting points.
\textcolor{blue}{Several tools exist for computing reachable sets of hybrid Several tools exist for computing reachable sets of hybrid
systems, including CORA, Flow*, SpaceEx, and JuliaReach. The choice of tool systems, including CORA, Flow*, SpaceEx, and JuliaReach. The choice of tool
depends on the structure of the continuous dynamics. Linear systems admit depends on the structure of the continuous dynamics. Linear systems admit
efficient polyhedral or ellipsoidal reachability computations. Nonlinear efficient polyhedral or ellipsoidal reachability computations. Nonlinear
systems require more conservative over-approximations using techniques such as systems require more conservative over-approximations using techniques such as
Taylor models or polynomial zonotopes. For this work, we will select tools Taylor models or polynomial zonotopes. For this work, we will select tools
appropriate to the fidelity of the reactor models available through the appropriate to the fidelity of the reactor models available.
Emerson partnership.}
%%% NOTES (Section 4.1): %%% NOTES (Section 4.1):
% - Add timing constraints discussion: what if the transition takes too long? % - Add timing constraints discussion: what if the transition takes too long?

16
main.aux
View File

@ -24,15 +24,15 @@
\@writefile{toc}{\contentsline {section}{\numberline {3}Research Approach}{7}{}\protected@file@percent } \@writefile{toc}{\contentsline {section}{\numberline {3}Research Approach}{7}{}\protected@file@percent }
\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Simplified hybrid automaton for reactor startup. Each discrete state $q_i$ has associated continuous dynamics $f_i$. Guard conditions on transitions (e.g., $T_{avg} > T_{min}$) are predicates over continuous state. Invariant violations ($\neg Inv_i$) trigger transitions to the SCRAM state. The operational level manages discrete transitions; the tactical level executes continuous control within each mode.}}{8}{}\protected@file@percent } \@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Simplified hybrid automaton for reactor startup. Each discrete state $q_i$ has associated continuous dynamics $f_i$. Guard conditions on transitions (e.g., $T_{avg} > T_{min}$) are predicates over continuous state. Invariant violations ($\neg Inv_i$) trigger transitions to the SCRAM state. The operational level manages discrete transitions; the tactical level executes continuous control within each mode.}}{8}{}\protected@file@percent }
\newlabel{fig:hybrid_automaton}{{1}{8}{Research Approach}{figure.1}{}} \newlabel{fig:hybrid_automaton}{{1}{8}{Research Approach}{figure.1}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}System Requirements and Specifications}{8}{}\protected@file@percent } \@writefile{toc}{\contentsline {subsection}{\numberline {3.1}System Requirements, Specifications, and Discrete Controllers}{8}{}\protected@file@percent }
\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Control scope hierarchy in nuclear power operations. Strategic control (long-term planning) remains with human management. HAHACS addresses the operational level (discrete mode switching) and tactical level (continuous control within modes), which together form a hybrid control system.}}{9}{}\protected@file@percent } \@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Control scope hierarchy in nuclear power operations. Strategic control (long-term planning) remains with human management. HAHACS addresses the operational level (discrete mode switching) and tactical level (continuous control within modes), which together form a hybrid control system.}}{9}{}\protected@file@percent }
\newlabel{fig:strat_op_tact}{{2}{9}{System Requirements and Specifications}{figure.2}{}} \newlabel{fig:strat_op_tact}{{2}{9}{System Requirements, Specifications, and Discrete Controllers}{figure.2}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.2}Discrete Controller Synthesis}{10}{}\protected@file@percent } \citation{MANYUS THESIS}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.3}Continuous Controllers}{11}{}\protected@file@percent } \@writefile{toc}{\contentsline {subsection}{\numberline {3.2}Continuous Control Modes}{11}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.3.1}Transitory Modes}{12}{}\protected@file@percent } \@writefile{toc}{\contentsline {subsubsection}{\numberline {3.2.1}Transitory Modes}{12}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.3.2}Stabilizing Modes}{13}{}\protected@file@percent } \@writefile{toc}{\contentsline {subsubsection}{\numberline {3.2.2}Stabilizing Modes}{12}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.3.3}Expulsory Modes}{14}{}\protected@file@percent } \@writefile{toc}{\contentsline {subsubsection}{\numberline {3.2.3}Expulsory Modes}{13}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {3.4}Industrial Implementation}{14}{}\protected@file@percent } \@writefile{toc}{\contentsline {subsection}{\numberline {3.3}Industrial Implementation}{14}{}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {4}Metrics for Success}{16}{}\protected@file@percent } \@writefile{toc}{\contentsline {section}{\numberline {4}Metrics for Success}{16}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{TRL 3 \textit {Critical Function and Proof of Concept}}{16}{}\protected@file@percent } \@writefile{toc}{\contentsline {paragraph}{TRL 3 \textit {Critical Function and Proof of Concept}}{16}{}\protected@file@percent }
\@writefile{toc}{\contentsline {paragraph}{TRL 4 \textit {Laboratory Testing of Integrated Components}}{16}{}\protected@file@percent } \@writefile{toc}{\contentsline {paragraph}{TRL 4 \textit {Laboratory Testing of Integrated Components}}{16}{}\protected@file@percent }

6
main.blg
View File

@ -5,6 +5,10 @@ White space in argument---line 23 of file main.aux
: \citation{HANDBOOK : \citation{HANDBOOK
: ON HYBRID SYSTEMS} : ON HYBRID SYSTEMS}
I'm skipping whatever remains of this command I'm skipping whatever remains of this command
White space in argument---line 30 of file main.aux
: \citation{MANYUS
: THESIS}
I'm skipping whatever remains of this command
The style file: ieeetr.bst The style file: ieeetr.bst
Database file #1: references.bib Database file #1: references.bib
Warning--entry type for "gentillon_westinghouse_1999" isn't style-file defined Warning--entry type for "gentillon_westinghouse_1999" isn't style-file defined
@ -60,4 +64,4 @@ warning$ -- 6
while$ -- 18 while$ -- 18
width$ -- 17 width$ -- 17
write$ -- 128 write$ -- 128
(There was 1 error message) (There were 2 error messages)

14
main.fdb_latexmk
View File

@ -1,13 +1,13 @@
# Fdb version 4 # Fdb version 4
["bibtex main"] 1772569109.73094 "main.aux" "main.bbl" "main" 1772569786.73648 2 ["bibtex main"] 1772647153.79833 "main.aux" "main.bbl" "main" 1772647228.17025 2
"./references.bib" 1765591319.20023 14069 2a4f74c587187a8a71049043171eb0fe "" "./references.bib" 1765591319.20023 14069 2a4f74c587187a8a71049043171eb0fe ""
"/usr/local/texlive/2025/texmf-dist/bibtex/bst/base/ieeetr.bst" 1292289607 18361 1a00e58565e7f19bf2b3e1bfb82254ae "" "/usr/local/texlive/2025/texmf-dist/bibtex/bst/base/ieeetr.bst" 1292289607 18361 1a00e58565e7f19bf2b3e1bfb82254ae ""
"main.aux" 1772569786.52811 5798 63f8b414cf301c83251584a9871955c0 "pdflatex" "main.aux" 1772647227.95816 5748 e33be58dd60b44046113ddb8b0d9bf30 "pdflatex"
(generated) (generated)
"main.bbl" "main.bbl"
"main.blg" "main.blg"
(rewritten before read) (rewritten before read)
["pdflatex"] 1772569785.36118 "main.tex" "main.pdf" "main" 1772569786.73657 0 ["pdflatex"] 1772647226.2456 "main.tex" "main.pdf" "main" 1772647228.17034 0
"/usr/local/texlive/2025/texmf-dist/fonts/enc/dvips/base/8r.enc" 1165713224 4850 80dc9bab7f31fb78a000ccfed0e27cab "" "/usr/local/texlive/2025/texmf-dist/fonts/enc/dvips/base/8r.enc" 1165713224 4850 80dc9bab7f31fb78a000ccfed0e27cab ""
"/usr/local/texlive/2025/texmf-dist/fonts/map/fontname/texfonts.map" 1577235249 3524 cb3e574dea2d1052e39280babc910dc8 "" "/usr/local/texlive/2025/texmf-dist/fonts/map/fontname/texfonts.map" 1577235249 3524 cb3e574dea2d1052e39280babc910dc8 ""
"/usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm" 1136768653 1408 5937f58aa508ea2cea4901c07d10f5fe "" "/usr/local/texlive/2025/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm" 1136768653 1408 5937f58aa508ea2cea4901c07d10f5fe ""
@ -246,16 +246,16 @@
"1-goals-and-outcomes/research_statement_v1.tex" 1765591319.18896 4450 070caee751214eaddffa6b3403f8ed43 "" "1-goals-and-outcomes/research_statement_v1.tex" 1765591319.18896 4450 070caee751214eaddffa6b3403f8ed43 ""
"1-goals-and-outcomes/v1.tex" 1765591319.1893 5825 07f6fba24cfa050a3b2b00c416f0f45f "" "1-goals-and-outcomes/v1.tex" 1765591319.1893 5825 07f6fba24cfa050a3b2b00c416f0f45f ""
"2-state-of-the-art/v2.tex" 1772219521.82345 12622 8fd5435154f6a45bb3e558ffebacbf58 "" "2-state-of-the-art/v2.tex" 1772219521.82345 12622 8fd5435154f6a45bb3e558ffebacbf58 ""
"3-research-approach/v3.tex" 1772569783.90542 37777 147d095e6b46494cc02aea8c3fe2b0c2 "" "3-research-approach/v3.tex" 1772647226.05037 36560 f9231e331bb93290a2a1d788c915c945 ""
"4-metrics-of-success/v1.tex" 1765591319.19036 5586 e5fb80ced00bcdc318ffe3861b0064bc "" "4-metrics-of-success/v1.tex" 1765591319.19036 5586 e5fb80ced00bcdc318ffe3861b0064bc ""
"5-risks-and-contingencies/v1.tex" 1765591319.19058 10412 17e755aa8451c45198372af7afe3c500 "" "5-risks-and-contingencies/v1.tex" 1765591319.19058 10412 17e755aa8451c45198372af7afe3c500 ""
"6-broader-impacts/v1.tex" 1765591319.19072 4834 418aae223b778759691eaf9124a5360c "" "6-broader-impacts/v1.tex" 1765591319.19072 4834 418aae223b778759691eaf9124a5360c ""
"8-schedule/v1.tex" 1765591319.19095 4473 8ad96bbf9cedf2ea09298ecbd4e01b83 "" "8-schedule/v1.tex" 1765591319.19095 4473 8ad96bbf9cedf2ea09298ecbd4e01b83 ""
"dane_proposal_format.cls" 1769715785.9835 2883 ea175794171aa0291ef71716b2190bf0 "" "dane_proposal_format.cls" 1769715785.9835 2883 ea175794171aa0291ef71716b2190bf0 ""
"main.aux" 1772569786.52811 5798 63f8b414cf301c83251584a9871955c0 "pdflatex" "main.aux" 1772647227.95816 5748 e33be58dd60b44046113ddb8b0d9bf30 "pdflatex"
"main.bbl" 1772569109.7887 2919 0ea026a17b15c1ad2ed657bdbf26dfdc "bibtex main" "main.bbl" 1772647153.8597 2919 0ea026a17b15c1ad2ed657bdbf26dfdc "bibtex main"
"main.tex" 1772218582.98667 954 b43a8fa32e5ebbd5cc6319a366737c39 "" "main.tex" 1772218582.98667 954 b43a8fa32e5ebbd5cc6319a366737c39 ""
"main.toc" 1772569786.53217 2186 052b3bee753c55d6c7b2587731bc12e5 "pdflatex" "main.toc" 1772647227.96211 2129 5b96f286c13251cf15256102f6fd6b8f "pdflatex"
(generated) (generated)
"main.aux" "main.aux"
"main.log" "main.log"

16
main.log
View File

@ -1,4 +1,4 @@
This is pdfTeX, Version 3.141592653-2.6-1.40.27 (TeX Live 2025) (preloaded format=pdflatex 2025.3.8) 3 MAR 2026 15:29 This is pdfTeX, Version 3.141592653-2.6-1.40.27 (TeX Live 2025) (preloaded format=pdflatex 2025.3.8) 4 MAR 2026 13:00
entering extended mode entering extended mode
restricted \write18 enabled. restricted \write18 enabled.
file:line:error style messages enabled. file:line:error style messages enabled.
@ -940,6 +940,10 @@ LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <5> not available
[10] [10]
LaTeX Warning: Citation `MANYUS THESIS' on page 11 undefined on input line 383.
[11] [11]
[12] [12]
@ -986,15 +990,15 @@ LaTeX Warning: There were undefined references.
) )
Here is how much of TeX's memory you used: Here is how much of TeX's memory you used:
26266 strings out of 473190 26267 strings out of 473190
547137 string characters out of 5715801 547152 string characters out of 5715801
963979 words of memory out of 5000000 964002 words of memory out of 5000000
48906 multiletter control sequences out of 15000+600000 48907 multiletter control sequences out of 15000+600000
614280 words of font info for 155 fonts, out of 8000000 for 9000 614280 words of font info for 155 fonts, out of 8000000 for 9000
1141 hyphenation exceptions out of 8191 1141 hyphenation exceptions out of 8191
110i,9n,107p,1062b,965s stack positions out of 10000i,1000n,20000p,200000b,200000s 110i,9n,107p,1062b,965s stack positions out of 10000i,1000n,20000p,200000b,200000s
</usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt12.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/symbols/msbm10.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/rsfs/rsfs10.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/urw/symbol/usyr.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/urw/symbol/usyr.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/urw/times/utmb8a.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/urw/times/utmbi8a.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/urw/times/utmr8a.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/urw/times/utmri8a.pfb> </usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt12.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/symbols/msbm10.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/rsfs/rsfs10.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/urw/symbol/usyr.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/urw/symbol/usyr.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/urw/times/utmb8a.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/urw/times/utmbi8a.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/urw/times/utmr8a.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/urw/times/utmri8a.pfb>
Output written on main.pdf (28 pages, 190643 bytes). Output written on main.pdf (28 pages, 189916 bytes).
PDF statistics: PDF statistics:
183 PDF objects out of 1000 (max. 8388607) 183 PDF objects out of 1000 (max. 8388607)
111 compressed objects within 2 object streams 111 compressed objects within 2 object streams

BIN
main.pdf
View File

Binary file not shown.

BIN
main.synctex.gz
View File

Binary file not shown.

13
main.toc
View File

@ -7,13 +7,12 @@
\contentsline {subsubsection}{\numberline {2.3.1}HARDENS}{4}{}% \contentsline {subsubsection}{\numberline {2.3.1}HARDENS}{4}{}%
\contentsline {subsubsection}{\numberline {2.3.2}Sequent Calculus and Differential Dynamic Logic}{5}{}% \contentsline {subsubsection}{\numberline {2.3.2}Sequent Calculus and Differential Dynamic Logic}{5}{}%
\contentsline {section}{\numberline {3}Research Approach}{7}{}% \contentsline {section}{\numberline {3}Research Approach}{7}{}%
\contentsline {subsection}{\numberline {3.1}System Requirements and Specifications}{8}{}% \contentsline {subsection}{\numberline {3.1}System Requirements, Specifications, and Discrete Controllers}{8}{}%
\contentsline {subsection}{\numberline {3.2}Discrete Controller Synthesis}{10}{}% \contentsline {subsection}{\numberline {3.2}Continuous Control Modes}{11}{}%
\contentsline {subsection}{\numberline {3.3}Continuous Controllers}{11}{}% \contentsline {subsubsection}{\numberline {3.2.1}Transitory Modes}{12}{}%
\contentsline {subsubsection}{\numberline {3.3.1}Transitory Modes}{12}{}% \contentsline {subsubsection}{\numberline {3.2.2}Stabilizing Modes}{12}{}%
\contentsline {subsubsection}{\numberline {3.3.2}Stabilizing Modes}{13}{}% \contentsline {subsubsection}{\numberline {3.2.3}Expulsory Modes}{13}{}%
\contentsline {subsubsection}{\numberline {3.3.3}Expulsory Modes}{14}{}% \contentsline {subsection}{\numberline {3.3}Industrial Implementation}{14}{}%
\contentsline {subsection}{\numberline {3.4}Industrial Implementation}{14}{}%
\contentsline {section}{\numberline {4}Metrics for Success}{16}{}% \contentsline {section}{\numberline {4}Metrics for Success}{16}{}%
\contentsline {paragraph}{TRL 3 \textit {Critical Function and Proof of Concept}}{16}{}% \contentsline {paragraph}{TRL 3 \textit {Critical Function and Proof of Concept}}{16}{}%
\contentsline {paragraph}{TRL 4 \textit {Laboratory Testing of Integrated Components}}{16}{}% \contentsline {paragraph}{TRL 4 \textit {Laboratory Testing of Integrated Components}}{16}{}%