diff --git a/3-research-approach/v3.tex b/3-research-approach/v3.tex index 9543fa1..b98954f 100644 --- a/3-research-approach/v3.tex +++ b/3-research-approach/v3.tex @@ -144,7 +144,7 @@ complex reactor operations. % 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: strategic, operational, and tactical. Strategic control is high-level and 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? -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} \centering @@ -232,24 +223,15 @@ control scope. The method of constructing a HAHACS in this proposal leverages two key observations about current practice. First, the operational scope control is effectively discrete control. Second, the rules for implementing this control -are described prior to their implementation in operating procedures. We can -exploit these facts by formalizing the rules for transitioning between discrete -states using temporal logic. - -\textcolor{blue}{The discrete predicates that trigger mode transitions 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. We are formalizing existing practice, not inventing new -abstractions.} +are described prior to their implementation in operating procedures. Before +constructing a HAHACS, we must completely describe its intended behavior. The +behavior of any control system originates in requirements: statements about what +the system must do, must not do, and under what conditions. For nuclear systems, +these requirements derive from multiple sources including regulatory mandates, +design basis analyses, and operating procedures. The challenge is formalizing +these requirements with sufficient precision that they can serve as the +foundation for autonomous control system synthesis and verification. We can +build these requirements using temporal logic. Temporal logic is a powerful set of semantics for building systems with complex but deterministic behavior. Temporal logic extends classical propositional logic @@ -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 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 (our discrete predicates) using Boolean connectives and temporal operators. 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 enters an unsafe configuration''), liveness properties (``the system eventually reaches operating temperature''), and response properties (``if -coolant pressure drops, the system initiates shutdown within bounded time'').} +coolant pressure drops, the system initiates shutdown within bounded time''). + To build these temporal logic statements, an intermediary tool called FRET is planned to be used. FRET stands for Formal Requirements Elicitation Tool, and @@ -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 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): % - Add concrete FRET example showing requirement → FRETish → LTL % - 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 % ---------------------------------------------------------------------------- -\subsection{Discrete Controller Synthesis} - Once system requirements are defined as temporal logic specifications, we use them to build the discrete control system. To do this, reactive synthesis tools 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 an output. Our systems fit exactly this mold: the current discrete state and status of guard conditions are the input, while the output is the next discrete -state. The output of a reactive synthesis algorithm is a discrete automaton. +state. -\textcolor{blue}{Reactive synthesis solves the following problem: given an LTL -formula $\varphi$ that specifies desired system behavior, automatically -construct a finite-state machine (strategy) that produces outputs in response -to environment inputs such that all resulting execution traces satisfy -$\varphi$. If such a strategy exists, the specification is called -\emph{realizable}. The synthesis algorithm either produces a correct-by-construction -controller or reports that no such controller can exist. This realizability -check is itself valuable: an unrealizable specification indicates conflicting -or impossible requirements in the original procedures.} +Reactive synthesis solves the following problem: given an LTL formula $\varphi$ +that specifies desired system behavior, automatically construct a finite-state +machine (strategy) that produces outputs in response to environment inputs such +that all resulting execution traces satisfy $\varphi$. If such a strategy +exists, the specification is called \emph{realizable}. The synthesis algorithm +either produces a correct-by-construction controller or reports that no such +controller can exist. This realizability check is itself valuable: an +unrealizable specification indicates conflicting or impossible requirements in +the original procedures. The main advantage of reactive synthesis is that at no point in the production of the discrete automaton is human engineering of the implementation required. The resultant automaton is correct by construction. This method of construction eliminates the possibility of human error at the implementation stage entirely. Instead, the effort on the human designer is directed at the specification of -system behavior itself. +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 -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. +(Talk about how one would go from a discrete automaton to actual code) -\textcolor{blue}{FRET can export specifications directly to formats compatible -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.} +(Examples of reactive synthesis in the wild) %%% NOTES (Section 3): % - Mention computational complexity of synthesis (doubly exponential worst case) @@ -371,60 +353,55 @@ independently reviewed and validated.} % 4. CONTINUOUS CONTROLLERS % ---------------------------------------------------------------------------- -\subsection{Continuous Controllers} +\subsection{Continuous Control Modes} The synthesis of the discrete operational controller is only half of an autonomous controller. These control systems are hybrid, with both discrete and continuous components. This section describes the continuous control modes that -execute within each discrete state, and how we verify that they satisfy -the requirements imposed by the discrete layer. - -\textcolor{blue}{It is important to clarify the scope of this methodology with -respect to continuous controller design. This work verifies continuous -controllers; it does not synthesize them. The distinction parallels model -checking in software verification: model checking does not tell engineers how -to write correct software, but it verifies whether a given implementation -satisfies its specification. Similarly, we assume that continuous controllers -can be designed using standard control theory techniques. Our contribution is -a verification framework that confirms candidate controllers compose correctly -with the discrete layer to produce a safe hybrid system.} +execute within each discrete state, and how we verify that they satisfy the +requirements imposed by the discrete layer. It is important to clarify the scope +of this methodology with respect to continuous controller design. This work +verifies continuous controllers; it does not synthesize them. The distinction +parallels model checking in software verification: model checking does not tell +engineers how to write correct software, but it verifies whether a given +implementation satisfies its specification. Similarly, we assume that continuous +controllers can be designed using standard control theory techniques. Our +contribution is a verification framework that confirms candidate controllers +compose correctly with the discrete layer to produce a safe hybrid system. The operational control scope defines go/no-go decisions that determine what kind of continuous control to implement. The entry or exit conditions of a discrete state are themselves the guard conditions $\mathcal{G}$ that define the -boundaries for each continuous controller. These continuous controllers all -share a common state space, but each individual continuous control mode operates -within its own partition defined by the discrete state $q_i$ and the associated -guards. This partitioning of the continuous state space among several discrete -vector fields has traditionally been a difficult problem for validation and -verification. The discontinuity of the vector fields at discrete state -interfaces makes reachability analysis computationally expensive, and analytic -solutions often become intractable. +boundaries for each continuous controller's allowed state-space region. These +continuous controllers all share a common state space, but each individual +continuous control mode operates within its own partition defined by the +discrete state $q_i$ and the associated guards. This partitioning of the +continuous state space among several discrete vector fields has traditionally +been a difficult problem for validation and verification. The discontinuity of +the vector fields at discrete state interfaces makes reachability analysis +computationally expensive, and analytic solutions often become intractable +\cite{MANYUS THESIS}. 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 output set clearly defined by our discrete transitions \textit{a priori}. -Consider that we define the continuous state space as $\mathcal{X}$. Whenever we -create guard conditions from our design requirements, we are effectively -creating subsets $\mathcal{X}_{entry,i}$ and $\mathcal{X}_{exit,i}$ for each -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: +Consider that we define the continuous state space as $\mathcal{X}$. Each +discrete mode $q_i$ then provides three key pieces of information for continuous +controller design: \begin{enumerate} \item \textbf{Entry conditions:} $\mathcal{X}_{entry,i} \subseteq \mathcal{X}$, the set of possible initial states when entering this mode \item \textbf{Exit conditions:} $\mathcal{X}_{exit,i} \subseteq \mathcal{X}$, - the target states that trigger transition to the next mode + the target states that trigger transition to the next mode, or is the region + in the state space a stabilizing mode remains within. \item \textbf{Safety invariants:} $\mathcal{X}_{safe,i} \subseteq \mathcal{X}$, - the envelope of safe states during operation in this mode + the envelope of safe states during operation in this mode. These are derived + from invariants \(Inv\). \end{enumerate} These sets come directly from the discrete controller synthesis and define precise objectives for continuous control. The continuous controller for mode $q_i$ must drive the system from any state in $\mathcal{X}_{entry,i}$ to some -state in $\mathcal{X}_{exit,i}$ while remaining within $\mathcal{X}_{safe,i}$.} +state in $\mathcal{X}_{exit,i}$ while remaining within $\mathcal{X}_{safe,i}$. We classify continuous controllers into three types based on their objectives: transitory, stabilizing, and expulsory. Each type has distinct verification @@ -441,13 +418,13 @@ requirements that determine which formal methods tools are appropriate. \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 -execute transitions: starting from entry conditions, reaching exit conditions, -while maintaining safety throughout. Examples include power ramp-up sequences, -cooldown procedures, and load-following maneuvers.} +execute transitions: starting from entry conditions, reach exit conditions, +and maintain safety invariants throughout. Examples include power ramp-up sequences, +cooldown procedures, and load-following maneuvers. -\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 $\mathcal{X}_{exit}$, safety invariant $\mathcal{X}_{safe}$, and closed-loop 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} \] 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 initial set under the system dynamics. For a transitory mode to be valid, the 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 reachable within time horizon $T$: \[ -\text{Reach}(\mathcal{X}_{entry}, f, [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]) \subseteq \mathcal{X}_{safe} \land +\text{Reach}(\mathcal{X}_{entry}, f_i, [0,T]) \cap \mathcal{X}_{exit} \neq \emptyset +\] Because the discrete controller defines clear boundaries in continuous state space, the verification problem for each transitory mode is well-posed. We know @@ -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 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 depends on the structure of the continuous dynamics. Linear systems admit efficient polyhedral or ellipsoidal reachability computations. Nonlinear systems require more conservative over-approximations using techniques such as Taylor models or polynomial zonotopes. For this work, we will select tools -appropriate to the fidelity of the reactor models available through the -Emerson partnership.} +appropriate to the fidelity of the reactor models available. %%% NOTES (Section 4.1): % - Add timing constraints discussion: what if the transition takes too long? diff --git a/main.aux b/main.aux index 89fdc18..971193e 100644 --- a/main.aux +++ b/main.aux @@ -24,15 +24,15 @@ \@writefile{toc}{\contentsline {section}{\numberline {3}Research Approach}{7}{}\protected@file@percent } \@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Simplified hybrid automaton for reactor startup. Each discrete state $q_i$ has associated continuous dynamics $f_i$. Guard conditions on transitions (e.g., $T_{avg} > T_{min}$) are predicates over continuous state. Invariant violations ($\neg Inv_i$) trigger transitions to the SCRAM state. The operational level manages discrete transitions; the tactical level executes continuous control within each mode.}}{8}{}\protected@file@percent } \newlabel{fig:hybrid_automaton}{{1}{8}{Research Approach}{figure.1}{}} -\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}System Requirements 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 } -\newlabel{fig:strat_op_tact}{{2}{9}{System Requirements and Specifications}{figure.2}{}} -\@writefile{toc}{\contentsline {subsection}{\numberline {3.2}Discrete Controller Synthesis}{10}{}\protected@file@percent } -\@writefile{toc}{\contentsline {subsection}{\numberline {3.3}Continuous Controllers}{11}{}\protected@file@percent } -\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.3.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.3.3}Expulsory Modes}{14}{}\protected@file@percent } -\@writefile{toc}{\contentsline {subsection}{\numberline {3.4}Industrial Implementation}{14}{}\protected@file@percent } +\newlabel{fig:strat_op_tact}{{2}{9}{System Requirements, Specifications, and Discrete Controllers}{figure.2}{}} +\citation{MANYUS THESIS} +\@writefile{toc}{\contentsline {subsection}{\numberline {3.2}Continuous Control Modes}{11}{}\protected@file@percent } +\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.2.1}Transitory Modes}{12}{}\protected@file@percent } +\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.2.2}Stabilizing Modes}{12}{}\protected@file@percent } +\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.2.3}Expulsory Modes}{13}{}\protected@file@percent } +\@writefile{toc}{\contentsline {subsection}{\numberline {3.3}Industrial Implementation}{14}{}\protected@file@percent } \@writefile{toc}{\contentsline {section}{\numberline {4}Metrics for Success}{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 } diff --git a/main.blg b/main.blg index 789f914..5c8f818 100644 --- a/main.blg +++ b/main.blg @@ -5,6 +5,10 @@ White space in argument---line 23 of file main.aux : \citation{HANDBOOK : ON HYBRID SYSTEMS} I'm skipping whatever remains of this command +White space in argument---line 30 of file main.aux + : \citation{MANYUS + : THESIS} +I'm skipping whatever remains of this command The style file: ieeetr.bst Database file #1: references.bib Warning--entry type for "gentillon_westinghouse_1999" isn't style-file defined @@ -60,4 +64,4 @@ warning$ -- 6 while$ -- 18 width$ -- 17 write$ -- 128 -(There was 1 error message) +(There were 2 error messages) diff --git a/main.fdb_latexmk b/main.fdb_latexmk index c01de7a..01a63e5 100644 --- a/main.fdb_latexmk +++ b/main.fdb_latexmk @@ -1,13 +1,13 @@ # 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 "" "/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) "main.bbl" "main.blg" (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/map/fontname/texfonts.map" 1577235249 3524 cb3e574dea2d1052e39280babc910dc8 "" "/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/v1.tex" 1765591319.1893 5825 07f6fba24cfa050a3b2b00c416f0f45f "" "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 "" "5-risks-and-contingencies/v1.tex" 1765591319.19058 10412 17e755aa8451c45198372af7afe3c500 "" "6-broader-impacts/v1.tex" 1765591319.19072 4834 418aae223b778759691eaf9124a5360c "" "8-schedule/v1.tex" 1765591319.19095 4473 8ad96bbf9cedf2ea09298ecbd4e01b83 "" "dane_proposal_format.cls" 1769715785.9835 2883 ea175794171aa0291ef71716b2190bf0 "" - "main.aux" 1772569786.52811 5798 63f8b414cf301c83251584a9871955c0 "pdflatex" - "main.bbl" 1772569109.7887 2919 0ea026a17b15c1ad2ed657bdbf26dfdc "bibtex main" + "main.aux" 1772647227.95816 5748 e33be58dd60b44046113ddb8b0d9bf30 "pdflatex" + "main.bbl" 1772647153.8597 2919 0ea026a17b15c1ad2ed657bdbf26dfdc "bibtex main" "main.tex" 1772218582.98667 954 b43a8fa32e5ebbd5cc6319a366737c39 "" - "main.toc" 1772569786.53217 2186 052b3bee753c55d6c7b2587731bc12e5 "pdflatex" + "main.toc" 1772647227.96211 2129 5b96f286c13251cf15256102f6fd6b8f "pdflatex" (generated) "main.aux" "main.log" diff --git a/main.log b/main.log index f92c2e7..5c8dfc8 100644 --- a/main.log +++ b/main.log @@ -1,4 +1,4 @@ -This is pdfTeX, Version 3.141592653-2.6-1.40.27 (TeX Live 2025) (preloaded format=pdflatex 2025.3.8) 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 restricted \write18 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] +LaTeX Warning: Citation `MANYUS THESIS' on page 11 undefined on input line 383. + + + [11] [12] @@ -986,15 +990,15 @@ LaTeX Warning: There were undefined references. ) Here is how much of TeX's memory you used: - 26266 strings out of 473190 - 547137 string characters out of 5715801 - 963979 words of memory out of 5000000 - 48906 multiletter control sequences out of 15000+600000 + 26267 strings out of 473190 + 547152 string characters out of 5715801 + 964002 words of memory out of 5000000 + 48907 multiletter control sequences out of 15000+600000 614280 words of font info for 155 fonts, out of 8000000 for 9000 1141 hyphenation exceptions out of 8191 110i,9n,107p,1062b,965s stack positions out of 10000i,1000n,20000p,200000b,200000s -Output written on main.pdf (28 pages, 190643 bytes). +Output written on main.pdf (28 pages, 189916 bytes). PDF statistics: 183 PDF objects out of 1000 (max. 8388607) 111 compressed objects within 2 object streams diff --git a/main.pdf b/main.pdf index 6b1c44f..88cad6d 100644 Binary files a/main.pdf and b/main.pdf differ diff --git a/main.synctex.gz b/main.synctex.gz index 25ce9fd..4c72008 100644 Binary files a/main.synctex.gz and b/main.synctex.gz differ diff --git a/main.toc b/main.toc index 88e0011..6817872 100644 --- a/main.toc +++ b/main.toc @@ -7,13 +7,12 @@ \contentsline {subsubsection}{\numberline {2.3.1}HARDENS}{4}{}% \contentsline {subsubsection}{\numberline {2.3.2}Sequent Calculus and Differential Dynamic Logic}{5}{}% \contentsline {section}{\numberline {3}Research Approach}{7}{}% -\contentsline {subsection}{\numberline {3.1}System Requirements and Specifications}{8}{}% -\contentsline {subsection}{\numberline {3.2}Discrete Controller Synthesis}{10}{}% -\contentsline {subsection}{\numberline {3.3}Continuous Controllers}{11}{}% -\contentsline {subsubsection}{\numberline {3.3.1}Transitory Modes}{12}{}% -\contentsline {subsubsection}{\numberline {3.3.2}Stabilizing Modes}{13}{}% -\contentsline {subsubsection}{\numberline {3.3.3}Expulsory Modes}{14}{}% -\contentsline {subsection}{\numberline {3.4}Industrial Implementation}{14}{}% +\contentsline {subsection}{\numberline {3.1}System Requirements, Specifications, and Discrete Controllers}{8}{}% +\contentsline {subsection}{\numberline {3.2}Continuous Control Modes}{11}{}% +\contentsline {subsubsection}{\numberline {3.2.1}Transitory Modes}{12}{}% +\contentsline {subsubsection}{\numberline {3.2.2}Stabilizing Modes}{12}{}% +\contentsline {subsubsection}{\numberline {3.2.3}Expulsory Modes}{13}{}% +\contentsline {subsection}{\numberline {3.3}Industrial Implementation}{14}{}% \contentsline {section}{\numberline {4}Metrics for Success}{16}{}% \contentsline {paragraph}{TRL 3 \textit {Critical Function and Proof of Concept}}{16}{}% \contentsline {paragraph}{TRL 4 \textit {Laboratory Testing of Integrated Components}}{16}{}%