diff --git a/.DS_Store b/.DS_Store index ac024b1..2835636 100644 Binary files a/.DS_Store and b/.DS_Store differ diff --git a/3-research-approach/v2.tex b/3-research-approach/v2.tex index 16a89c1..9fc9cba 100644 --- a/3-research-approach/v2.tex +++ b/3-research-approach/v2.tex @@ -319,6 +319,15 @@ complex but deterministic behavior. % talk a bit about tools here like FRET. Talk about previous attempts. +\begin{figure}[htbp] + \centering + \framebox[0.8\textwidth]{\rule{0pt}{3cm}\textit{Strategic, operational, +tactical placeholder}} + \caption{Breakdown of control scope} + \label{fig:strat_op_tact} +\end{figure} + + Human control of nuclear power can be divided into three different scopes: strategic, operational, and tactical. Strategic control is the high-level and long term decision making for the plant. This level has objectives that are @@ -401,10 +410,32 @@ interpretation is a weakness that must be addressed. %export, or naturlly support reactive synth solver ltlsynt, a sota react synth %solver +Once system requirements we defined as temporal logic specifications we will use +the specifications to build the discrete control system. To do this, reactive +synthesis tools will be utilized. Reactive synthesis is a field in computer +science that deals with the automated creation of reactive programs from +temporal logic specifications. A reactive program is one that for a given state +takes an input, and produces an output. Our systems, such as the discrete +portion of the controller, fit exactly this this mold. The current discrete +state, and status of guard conditions are the input to the system, while the +output is the next discrete state. The output of a reactive synthesis algorithim +is a discrete automata. + +Reactive synthesis' main advantage is the fact that at no point in the +production of a discrete automata of the program is human engineering required. +The resultant automata is correct by construction. This method of construction +eliminates the possibility of human error outright at the implementation state. +Instead, the effort on the human designer is directed at the specification of +the system behavior itself. + % talk about what the benefits of reactive synth are. Proof chain, machine % checkable, blah blah blah +%%%%% I NEED TO WRITE ABOUT HOW REQUIREMENTS ARE EXTRACTED AND WHAT BECOME +CONTINUOUS CONTROLLER TRANSITIONS VS DISCRETE GUARD CONDITIONS + %%%%%%%%%%%% Building continuous controllers +\subsection{Continuous Controllers} % The whole point of a hybrid system is that there are continuous components % underneath the digital system. We built the discrete like the physical doesn't @@ -424,6 +455,39 @@ interpretation is a weakness that must be addressed. % Q: Who designs the continuous controllers and how? This methodology verifies % them, but doesn't synthesize them. Is this a scope problem? +The synthesis of the discrete operational controller is only half of an +autonomous controller. These control systems are hybrid, with both discrete and +continuous components. In this section, we will talk about the continuous +control modes that are the transitions between discrete modes, how they may be +synthesized, and how we plan to verify them. + +The operational control scope defines go/no-go decisions that themselves are +deciding what kind of continuous control to implement. To this end, the entry or +exit of a discrete state triggers are themselves the guard conditions \(G\) that +define the barriers of the continuous controller. These continuous controllers +all share a large state space, but each individual continuous control mode +operates within it's own partition defined by the discrete state \(q_i\) and +guard conditions \(G\). This partitioning of the continuous state space amongst +several discrete vector fields controlled by the given \(q_i\) has traditionally +been a difficult problem for validation and verification of systems properties. +Typically, the discontinuity of the vector fields at discrete state interfaces +make things like reachability analysis computationally expensive, and analytic +solutions become intractable. + +We circumnavigate these issues by designing our hybrid system from the bottom up +with this verification in mind. Each continuous control mode has an input and +output set clearly defined by our discrete transitions \textit{a priori}. +Consider that we define the continuous state space as \(X\). Whenever we create +guard functions from our design requirements for a given system, we are +effectively creating subsets \(X_{entry,i}\) and \(X_{exit,i}\) for each +discrete mode \(q_i\). These subsets define when the state transitions occur +between discrete modes, but more importantly when building continuous control +modes, they become control objectives. + +% Start talking about what it means to build controlelrs to the objectives +% rahter than the other why around. ALso why it makes things much easier to +% verify and validate + %%%%%% Transitory modes % entry and exit conditions diff --git a/main.aux b/main.aux index 11237d0..6dfad88 100644 --- a/main.aux +++ b/main.aux @@ -21,25 +21,28 @@ \citation{HANDBOOK ON HYBRID SYSTEMS CONTROL} \@writefile{toc}{\contentsline {section}{\numberline {3}Research Approach}{6}{}\protected@file@percent } \@writefile{toc}{\contentsline {subsection}{\numberline {3.1}System Requirement and Specifications}{6}{}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {4}Metrics for Success}{7}{}\protected@file@percent } -\@writefile{toc}{\contentsline {paragraph}{TRL 3 \textit {Critical Function and Proof of Concept}}{7}{}\protected@file@percent } -\@writefile{toc}{\contentsline {paragraph}{TRL 4 \textit {Laboratory Testing of Integrated Components}}{7}{}\protected@file@percent } -\@writefile{toc}{\contentsline {paragraph}{TRL 5 \textit {Laboratory Testing in Relevant Environment}}{7}{}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {5}Risks and Contingencies}{9}{}\protected@file@percent } -\@writefile{toc}{\contentsline {subsection}{\numberline {5.1}Computational Tractability of Synthesis}{9}{}\protected@file@percent } -\@writefile{toc}{\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{9}{}\protected@file@percent } -\@writefile{toc}{\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{10}{}\protected@file@percent } +\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Breakdown of control scope}}{7}{}\protected@file@percent } +\newlabel{fig:strat_op_tact}{{1}{7}{System Requirement and Specifications}{figure.1}{}} +\@writefile{toc}{\contentsline {subsection}{\numberline {3.2}Continuous Controllers}{8}{}\protected@file@percent } +\@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}}{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}}{10}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {5}Risks and Contingencies}{12}{}\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}{12}{}\protected@file@percent } +\@writefile{toc}{\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{13}{}\protected@file@percent } \citation{eia_lcoe_2022} \citation{eesi_datacenter_2024} \citation{eia_lcoe_2022} -\@writefile{toc}{\contentsline {section}{\numberline {6}Broader Impacts}{12}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {6}Broader Impacts}{15}{}\protected@file@percent } \bibstyle{ieeetr} \bibdata{references} -\@writefile{toc}{\contentsline {section}{\numberline {7}Schedule, Milestones, and Deliverables}{14}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {7}Schedule, Milestones, and Deliverables}{17}{}\protected@file@percent } \gtt@chartextrasize{0}{164.1287pt} -\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Project schedule showing major research thrusts, milestones (orange row), and publications (green row). Red diamonds indicate completion points. Overlapping bars indicate parallel work where appropriate.}}{14}{}\protected@file@percent } -\newlabel{fig:gantt}{{1}{14}{Schedule, Milestones, and Deliverables}{figure.1}{}} -\@writefile{toc}{\contentsline {subsection}{\numberline {7.1}Milestones and Deliverables}{14}{}\protected@file@percent } +\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Project schedule showing major research thrusts, milestones (orange row), and publications (green row). Red diamonds indicate completion points. Overlapping bars indicate parallel work where appropriate.}}{17}{}\protected@file@percent } +\newlabel{fig:gantt}{{2}{17}{Schedule, Milestones, and Deliverables}{figure.2}{}} +\@writefile{toc}{\contentsline {subsection}{\numberline {7.1}Milestones and Deliverables}{17}{}\protected@file@percent } \bibcite{NUREG-0899}{1} \bibcite{10CFR50.34}{2} \bibcite{10CFR55.59}{3} @@ -55,5 +58,5 @@ \bibcite{Kiniry2024}{13} \bibcite{eia_lcoe_2022}{14} \bibcite{eesi_datacenter_2024}{15} -\@writefile{toc}{\contentsline {section}{References}{15}{}\protected@file@percent } -\gdef \@abspage@last{19} +\@writefile{toc}{\contentsline {section}{References}{18}{}\protected@file@percent } +\gdef \@abspage@last{22} diff --git a/main.fdb_latexmk b/main.fdb_latexmk index 64b3ab5..ec8b7c9 100644 --- a/main.fdb_latexmk +++ b/main.fdb_latexmk @@ -1,13 +1,13 @@ # Fdb version 4 -["bibtex main"] 1769715964.87129 "main.aux" "main.bbl" "main" 1770062339.7998 2 +["bibtex main"] 1769715964.87129 "main.aux" "main.bbl" "main" 1771877557.20826 2 "./references.bib" 1765591319.20023 14069 2a4f74c587187a8a71049043171eb0fe "" "/usr/local/texlive/2025/texmf-dist/bibtex/bst/base/ieeetr.bst" 1292289607 18361 1a00e58565e7f19bf2b3e1bfb82254ae "" - "main.aux" 1770062339.59974 3798 3e4f846d5a63c369ad994a87de4a30be "pdflatex" + "main.aux" 1771877556.99413 4137 a363a1372d71f342ae80c94ef1212f2b "pdflatex" (generated) "main.bbl" "main.blg" (rewritten before read) -["pdflatex"] 1770062338.22246 "main.tex" "main.pdf" "main" 1770062339.79991 2 +["pdflatex"] 1771877555.38007 "main.tex" "main.pdf" "main" 1771877557.20836 2 "/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/v1.tex" 1765591319.1898 10609 44863eb08e23052a1623ef3ebcb1e3ae "" - "3-research-approach/v2.tex" 1770062336.52686 22203 b3b90c4fbb94cd85cdcce085ec1b2a8a "" + "3-research-approach/v2.tex" 1771877553.94196 31543 e385dfd70efe1c4c683a84812df9adf3 "" "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" 1770062339.59974 3798 3e4f846d5a63c369ad994a87de4a30be "pdflatex" + "main.aux" 1771877556.99413 4137 a363a1372d71f342ae80c94ef1212f2b "pdflatex" "main.bbl" 1769715964.93568 2919 0ea026a17b15c1ad2ed657bdbf26dfdc "bibtex main" - "main.tex" 1769453692.01808 954 ea089365572626745e262fed177e4fa3 "" - "main.toc" 1770062339.60048 1565 b9f0d6ea3d8646810f16fc895e4d44da "pdflatex" + "main.tex" 1771522075.784 954 ea089365572626745e262fed177e4fa3 "" + "main.toc" 1771877556.99812 1646 15fa619dbe6b9510750511d8a9cb0d43 "pdflatex" (generated) "main.aux" "main.log" diff --git a/main.fls b/main.fls index 248e23f..aafd63e 100644 --- a/main.fls +++ b/main.fls @@ -1,4 +1,4 @@ -PWD /Users/danesabo/Documents/Dane's Vault/Writing/THESIS_PROPOSAL +PWD /Users/danesabo/Documents/Writing/Thesis INPUT /usr/local/texlive/2025/texmf.cnf INPUT /usr/local/texlive/2025/texmf-dist/web2c/texmf.cnf INPUT /usr/local/texlive/2025/texmf-var/web2c/pdftex/pdflatex.fmt diff --git a/main.log b/main.log index 5bdba60..731cb5a 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) 2 FEB 2026 14:58 +This is pdfTeX, Version 3.141592653-2.6-1.40.27 (TeX Live 2025) (preloaded format=pdflatex 2025.3.8) 23 FEB 2026 15:12 entering extended mode restricted \write18 enabled. file:line:error style messages enabled. @@ -918,61 +918,67 @@ LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <7> not available [5] (./3-research-approach/v2.tex LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <10> not available -(Font) Font shape `OT1/ptm/b/n' tried instead on input line 255. +(Font) Font shape `OT1/ptm/b/n' tried instead on input line 259. LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <7.4> not available -(Font) Font shape `OT1/ptm/b/n' tried instead on input line 255. +(Font) Font shape `OT1/ptm/b/n' tried instead on input line 259. 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 255. +(Font) Font shape `OT1/ptm/b/n' tried instead on input line 259. -LaTeX Warning: Citation `HANDBOOK ON HYBRID SYSTEMS CONTROL' on page 6 undefined on input line 258. +LaTeX Warning: Citation `HANDBOOK ON HYBRID SYSTEMS CONTROL' on page 6 undefined on input line 262. -LaTeX Font Info: Trying to load font information for TS1+ptm on input line 268. +LaTeX Font Info: Trying to load font information for TS1+ptm on input line 272. (/usr/local/texlive/2025/texmf-dist/tex/latex/psnfss/ts1ptm.fd File: ts1ptm.fd 2001/06/04 font definitions for TS1/ptm. ) -./3-research-approach/v2.tex:278: LaTeX Error: \mathcal allowed only in math mode. +./3-research-approach/v2.tex:282: LaTeX Error: \mathcal allowed only in math mode. See the LaTeX manual or LaTeX Companion for explanation. Type H for immediate help. ... -l.278 \item \mathcal +l.282 \item \mathcal {R}: Reset maps that define state 'jumps' You're in trouble here. Try typing to proceed. If that doesn't work, type X to quit. -) -[6] (./4-metrics-of-success/v1.tex -[7]) +[6] -[8] (./5-risks-and-contingencies/v1.tex +[7] -[9] +[8]) + +[9] (./4-metrics-of-success/v1.tex [10]) -[11] (./6-broader-impacts/v1.tex) +[11] (./5-risks-and-contingencies/v1.tex [12] -[13] (./8-schedule/v1.tex +[13]) + +[14] (./6-broader-impacts/v1.tex) + +[15] + +[16] (./8-schedule/v1.tex Missing character: There is no , in font nullfont! ) (./main.bbl -[14] +[17] Underfull \hbox (badness 10000) in paragraph at lines 32--33 \OT1/cmtt/m/n/12 nuclear . org / information -[] library / safety -[] and -[] security / safety -[] of -[] [] -[15]) +[18]) -[16] (./main.aux) +[19] (./main.aux) *********** LaTeX2e <2024-11-01> patch level 2 L3 programming layer <2025-01-18> @@ -983,18 +989,18 @@ LaTeX Warning: There were undefined references. ) Here is how much of TeX's memory you used: - 26141 strings out of 473190 - 544988 string characters out of 5715801 - 963880 words of memory out of 5000000 - 48799 multiletter control sequences out of 15000+600000 + 26142 strings out of 473190 + 545007 string characters out of 5715801 + 963939 words of memory out of 5000000 + 48800 multiletter control sequences out of 15000+600000 608553 words of font info for 146 fonts, out of 8000000 for 9000 1141 hyphenation exceptions out of 8191 110i,9n,107p,1062b,952s stack positions out of 10000i,1000n,20000p,200000b,200000s -Output written on main.pdf (19 pages, 153240 bytes). +Output written on main.pdf (22 pages, 161253 bytes). PDF statistics: - 149 PDF objects out of 1000 (max. 8388607) - 89 compressed objects within 1 object stream + 158 PDF objects out of 1000 (max. 8388607) + 95 compressed objects within 1 object stream 0 named destinations out of 1000 (max. 500000) 109 words of extra memory for PDF output out of 10000 (max. 10000000) diff --git a/main.pdf b/main.pdf index aa5ddf7..8a317e2 100644 Binary files a/main.pdf and b/main.pdf differ diff --git a/main.synctex.gz b/main.synctex.gz index 2ae458c..8ff493f 100644 Binary files a/main.synctex.gz and b/main.synctex.gz differ diff --git a/main.toc b/main.toc index a40a59b..fd1dea7 100644 --- a/main.toc +++ b/main.toc @@ -6,15 +6,16 @@ \contentsline {subsection}{\numberline {2.3}HARDENS and Formal Methods}{4}{}% \contentsline {section}{\numberline {3}Research Approach}{6}{}% \contentsline {subsection}{\numberline {3.1}System Requirement and Specifications}{6}{}% -\contentsline {section}{\numberline {4}Metrics for Success}{7}{}% -\contentsline {paragraph}{TRL 3 \textit {Critical Function and Proof of Concept}}{7}{}% -\contentsline {paragraph}{TRL 4 \textit {Laboratory Testing of Integrated Components}}{7}{}% -\contentsline {paragraph}{TRL 5 \textit {Laboratory Testing in Relevant Environment}}{7}{}% -\contentsline {section}{\numberline {5}Risks and Contingencies}{9}{}% -\contentsline {subsection}{\numberline {5.1}Computational Tractability of Synthesis}{9}{}% -\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{9}{}% -\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{10}{}% -\contentsline {section}{\numberline {6}Broader Impacts}{12}{}% -\contentsline {section}{\numberline {7}Schedule, Milestones, and Deliverables}{14}{}% -\contentsline {subsection}{\numberline {7.1}Milestones and Deliverables}{14}{}% -\contentsline {section}{References}{15}{}% +\contentsline {subsection}{\numberline {3.2}Continuous Controllers}{8}{}% +\contentsline {section}{\numberline {4}Metrics for Success}{10}{}% +\contentsline {paragraph}{TRL 3 \textit {Critical Function and Proof of Concept}}{10}{}% +\contentsline {paragraph}{TRL 4 \textit {Laboratory Testing of Integrated Components}}{10}{}% +\contentsline {paragraph}{TRL 5 \textit {Laboratory Testing in Relevant Environment}}{10}{}% +\contentsline {section}{\numberline {5}Risks and Contingencies}{12}{}% +\contentsline {subsection}{\numberline {5.1}Computational Tractability of Synthesis}{12}{}% +\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{12}{}% +\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{13}{}% +\contentsline {section}{\numberline {6}Broader Impacts}{15}{}% +\contentsline {section}{\numberline {7}Schedule, Milestones, and Deliverables}{17}{}% +\contentsline {subsection}{\numberline {7.1}Milestones and Deliverables}{17}{}% +\contentsline {section}{References}{18}{}% diff --git a/pdflatex88984.fls b/pdflatex88984.fls new file mode 100644 index 0000000..4f172c6 --- /dev/null +++ b/pdflatex88984.fls @@ -0,0 +1,3 @@ +PWD /Users/danesabo/Documents/Writing/Thesis +INPUT /usr/local/texlive/2025/texmf.cnf +INPUT /usr/local/texlive/2025/texmf-dist/web2c/texmf.cnf