Auto sync: 2025-09-03 11:28:31 (11 files changed)

A  Writing/ERLM/GOv1.pdf

A  Writing/ERLM/goals-and-outcomes/v1.tex

A  Writing/ERLM/goals-and-outcomes/v2.tex

M  Writing/ERLM/main.aux

M  Writing/ERLM/main.fdb_latexmk

M  Writing/ERLM/main.fls

M  Writing/ERLM/main.log

M  Writing/ERLM/main.pdf

Writing/ERLM/goals-and-outcomes/v1.tex

@@ -0,0 +1,66 @@
+\section{Goals and Outcomes}
+
+The goal of this research is to use formal methods to create control systems
+that can switch between operating modes with a high assurance of correct
+construction. Modern control systems today often exist as hybrid control
+systems. Hybrid systems are those that have both continuous and discrete
+dynamics. Because of this, hybrid systems cannot be fully analyzed using only
+tools from continuous or discrete methods. Today, hybrid control systems are
+unable to be completely verified, that is to say we do not currently have ways
+of being building hybrid control systems that we can be certain meet high level
+strategic objectives, or who's behavior is totally understood.
+
+The ambiguity on hybrid system behavior is problematic when one of the most
+useful cases of hybrid system control is for improved autonomy of critical
+systems. Nuclear power is a salient example. For a nuclear reactor during
+start-up, every mode of power from initially cold-start, to controlled core
+heating, and eventually  full operating power is well understood dynamically.
+For each of these modes, significant portions of the control are optimized using
+automated controllers for each stage. The problem that remains for human
+operators is choosing when to switch from control law to the next, and ensuring
+that the proper conditions are met to do so--but these conditions are also
+clearly defined in regulation and operating procedures a priori.
+
+We can use the fact that these transition points are well understood in
+combination with formal methods to synthesize the discrete part of a hybrid
+system. From that point, we can have a robust chain of proof that our discrete
+jumps will happen only at the correct times. Once that is established, we can
+use reachability analysis and traditional control theory to ensure that each
+operation 'mode' satisfies liveness, stability, or performance requirements.
+With the combination of these two methods, we can be sure of correct behavior
+switching between modes, and that strategic goals remain met while transitioning
+from one mode switch to the next.
+
+If this research is successful, we will be able to do the following:
+
+\begin{enumerate}
+
+  \item
+    \textbf{Formalize} mode switching requirements as logical statements that
+    can then be translated into a controller implementation. This piece will
+    address the correct-by-construction generation of the mode switching
+    controller.
+
+  \item 
+    \textbf{Categorize} different continuous modes by their strategic relevance.
+    Certain modes exist as control laws from one mode to the next, such as a
+    controlled heating rate on reactor start-up before reaching operational
+    conditions. Other modes exist as stable regions, such as full-power
+    operation. 
+
+  \item
+    \textbf{Verify} continuous modes and accompanying continuous control laws
+    satisfy strategic requirements. This can be done with reachability analysis,
+    and ensuring that each mode transition as allowed from the requirements
+    synthesis squares up against the reachability analysis and the continuous
+    dynamics.
+
+  \item
+    \textbf{Prove} that a given hybrid system achieves strategic goals across
+    hybrid control modes. By seperately formalizing and analyzing continuous
+    dyanmics and discrete dynamics, we can come back to say the whole hybrid
+    system has met a strong guarantee of requirement adherence.
+
+\end{enumerate}
+
+

Writing/ERLM/goals-and-outcomes/v2.tex

@@ -0,0 +1,75 @@
+\section{Goals and Outcomes}
+
+The goal of this research is to use formal methods to create high-assurance
+hybrid control systems. Hybrid control systems have great potential for
+implementation in autonomous control as they are able to change control laws
+based on discrete triggers in the operating range of the controller. This allows
+the autonomous controller to use several easily tractable control laws for different
+regions in the state space, instead of using one controller over the entire
+systems operating range. But, the discrete jumps between control laws in a
+hybrid controller present challenges in proving stability and liveness
+properties of the whole system. While tools from control theory can prove
+properties for each individual control mode, they do not generalize when
+switching between control laws is introduced.
+
+This research will take a different approach to hybrid controller synthesis and
+verification. Using tools from the formal methods community, we will create
+controllers that are correct-by-construction and allow guarantees to be made
+about the whole system's behavior. To demonstrate this, an autonomous controller
+for a nuclear power plant start-up procedure will be created. Nuclear power is
+an excellent test case for this work as the continuous piece of reactor dynamics
+is well studied, while the discrete component of mode switching is explicitly
+stated in regulatory requirements and operating procedures. Nuclear reactor
+control today \textit{is} a hybrid control system--many functions in the control
+room use automated controllers for basic tasks, but the engagement and selection
+of these controllers is done by human operators referencing procedures to make
+decisions.
+
+The capability to create high-assurance hybrid control systems has the potential
+to reduce the labor required to operate critical systems by removing the human
+operator from the loop. Nuclear power stands to greatly benefit from greater
+controller autonomy as the largest expense for reactors today is operations and
+maintenance. Technologies such as microreactors and modular reactors will
+improve the maintenance costs required through the use of factory-made
+replacement components, but will suffer increased operating costs per megawatt
+produced if they are required to staff the same way reactors today are staffed.
+But, if increased autonomy can be introduced, these costs will be ameliorated.
+
+If this research is successful, we will be able to do the following:
+
+\begin{enumerate}
+
+  \item
+    \textbf{Formalize mode switching requirements as logical specifications that
+    can be translated into discrete controller implementations.} The discrete
+    transitions between continuous controller modes is often explicitly defined
+    for critical systems in operating procedures and regulatory requirements.
+    These statements will be translated into a temporal logic, which will then
+    be synthesized into a discrete controller implementation for continuous
+    controller mode switching.
+
+  \item
+    \textbf{Categorize different continuous controller modes by their strategic
+    relavance.} Different control modes serve one of two purposes: they may be
+    transitory or stabilizing. Knowing when to switch from one control mode to
+    another is handled by the discrete component of the hybrid system, but this
+    outcome will identify the properties the continuous components must satisfy
+    for each controller mode.
+
+  \item
+    \textbf{Verify that continuous controller modes satisfy dynamic
+    requirements.} For the discrete transitions between control modes to be
+    useful, we must ensure that the continuous control modes will actually move
+    the system to the transition, or if stabilizing, keep the system from
+    leaving the control mode.
+
+  \item
+    \textbf{Prove that a hybrid system implementation achieve strategic goals
+    across the entire controller operating range.} By creating discrete
+    controller transitions from logical specifications that are
+    correct-by-construction and validating that continuous components perform
+    appropriately between discrete transitions, we can be confident that the
+    hybrid system is free from defect and can be utilized as a critical
+    autonomous controller.
+  
+\end{enumerate}

Writing/ERLM/main.aux

@@ -1,6 +1,6 @@
 \relax 
 \bibstyle{unsrt}
 \providecommand \oddpage@label [2]{}
-\bibdata{references}
 \@writefile{toc}{\contentsline {section}{\numberline {1}Goals and Outcomes}{1}{}\protected@file@percent }
-\gdef \@abspage@last{2}
+\bibdata{references}
+\gdef \@abspage@last{3}

Writing/ERLM/main.fdb_latexmk

@@ -1,5 +1,5 @@
 # Fdb version 4
-["bibtex main"] 0 "main.aux" "main.bbl" "main" 1756866345.56251 0
+["bibtex main"] 0 "main.aux" "main.bbl" "main" 1756913150.42547 0
   "/usr/share/texlive/texmf-dist/bibtex/bst/base/unsrt.bst" 1292289607 18030 1376b4b231b50c66211e47e42eda2875 ""
   "main.aux" 0 -1 0 "pdflatex"
   "references.bib" 0 -1 0 ""
@@ -7,14 +7,16 @@
   "main.bbl"
   "main.blg"
   (rewritten before read)
-["pdflatex"] 1756866345.1432 "main.tex" "main.pdf" "main" 1756866345.56276 0
+["pdflatex"] 1756913149.4861 "main.tex" "main.pdf" "main" 1756913150.42571 0
-  "/etc/texmf/web2c/texmf.cnf" 1726065852.27662 475 c0e671620eb5563b2130f56340a5fde8 ""
+  "/etc/texmf/web2c/texmf.cnf" 1722610814.59577 475 c0e671620eb5563b2130f56340a5fde8 ""
   "/usr/share/texlive/texmf-dist/fonts/enc/dvips/base/8r.enc" 1165713224 4850 80dc9bab7f31fb78a000ccfed0e27cab ""
   "/usr/share/texlive/texmf-dist/fonts/map/fontname/texfonts.map" 1577235249 3524 cb3e574dea2d1052e39280babc910dc8 ""
   "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvb7t.tfm" 1136768653 2240 eb56c13537f4d8a0bd3fafc25572b1bd ""
   "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvb8r.tfm" 1136768653 4484 b828043cbd581d289d955903c1339981 ""
   "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvr7t.tfm" 1136768653 2520 53e01eef820ca829e42c1333c3fd02b9 ""
   "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvr8r.tfm" 1136768653 4712 9ef4d7d106579d4b136e1529e1a4533c ""
+  "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvro7t.tfm" 1136768653 2772 ab6561c8ff5ee69ff6d5961b9356db5a ""
+  "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvro8r.tfm" 1136768653 4964 f223217e5e1f85fa3742fb0480aba9e8 ""
   "/usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/cmextra/cmex7.tfm" 1246382020 1004 54797486969f23fa377b128694d548df ""
   "/usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm" 1246382020 916 f87d7c45f9c908e672703b83b72241a3 ""
   "/usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam7.tfm" 1246382020 928 2dc8d444221b7a635bb58038579b861a ""
@@ -26,8 +28,10 @@
   "/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmsy10.tfm" 1136768653 1124 6c73e740cf17375f03eec0ee63599741 ""
   "/usr/share/texlive/texmf-dist/fonts/type1/urw/helvetic/uhvb8a.pfb" 1136849748 35941 f27169cc74234d5bd5e4cca5abafaabb ""
   "/usr/share/texlive/texmf-dist/fonts/type1/urw/helvetic/uhvr8a.pfb" 1136849748 44648 23115b2a545ebfe2c526c3ca99db8b95 ""
+  "/usr/share/texlive/texmf-dist/fonts/type1/urw/helvetic/uhvro8a.pfb" 1136849748 48169 b4fd9d908b9ee8c65d4305ad39071c5e ""
   "/usr/share/texlive/texmf-dist/fonts/vf/adobe/helvetic/phvb7t.vf" 1136768653 1372 1c26b449eb4a1a0bcf6ac7cfe376d450 ""
   "/usr/share/texlive/texmf-dist/fonts/vf/adobe/helvetic/phvr7t.vf" 1136768653 1372 dc841a9f00a1a11b1443367ae6c5588e ""
+  "/usr/share/texlive/texmf-dist/fonts/vf/adobe/helvetic/phvro7t.vf" 1136768653 1372 9948cedecdb0445a3b5cf1b8a8082ab8 ""
   "/usr/share/texlive/texmf-dist/tex/context/base/mkii/supp-pdf.mkii" 1461363279 71627 94eb9990bed73c364d7f53f960cc8c5b ""
   "/usr/share/texlive/texmf-dist/tex/generic/iftex/iftex.sty" 1644112042 7237 bdd120a32c8fdb4b433cf9ca2e7cd98a ""
   "/usr/share/texlive/texmf-dist/tex/generic/iftex/ifvtex.sty" 1572645307 1057 525c2192b5febbd8c1f662c9468335bb ""
@@ -207,12 +211,13 @@
   "/usr/share/texlive/texmf-dist/tex/latex/xkeyval/xkeyval.sty" 1655411236 4937 4ce600ce9bd4ec84d0250eb6892fcf4f ""
   "/usr/share/texlive/texmf-dist/web2c/texmf.cnf" 1707919699 40399 f2c302f7d2af602abb742093540a5834 ""
   "/usr/share/texmf/web2c/texmf.cnf" 1707919699 40399 f2c302f7d2af602abb742093540a5834 ""
-  "/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map" 1726065856.46263 128028 f533b797fba58d231669ea19e894e23e ""
+  "/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map" 1722610820.43889 128028 f533b797fba58d231669ea19e894e23e ""
-  "/var/lib/texmf/web2c/pdftex/pdflatex.fmt" 1726065868 6800790 607442c924ed54405961d2b8ac2a25ae ""
+  "/var/lib/texmf/web2c/pdftex/pdflatex.fmt" 1726005817 6800784 2b63e5a224c5ad740802d8f9921962c1 ""
-  "dane_proposal_format.cls" 1756866343.25274 2551 deee3ebc77bdfb5d08546fb19b3bdd53 ""
+  "dane_proposal_format.cls" 1756902979.42453 2551 deee3ebc77bdfb5d08546fb19b3bdd53 ""
-  "main.aux" 1756866345.49569 213 8bec41973e7f8a0e3c5820f1e8e33fe1 "pdflatex"
+  "goals-and-outcomes/v2.tex" 1756913147.34838 3929 81698d2601ffbfc97dd16c2553a8806b ""
+  "main.aux" 1756913150.28919 213 c6307743402c02a0530961857d9d1a69 "pdflatex"
   "main.bbl" 0 -1 0 "bibtex main"
-  "main.tex" 1756865478.72503 3553 735c6dfea3f38b408b7239e8aa1a4ada ""
+  "main.tex" 1756910438.79598 141 c588c1bc2f6a6f85c912c3842ff6c482 ""
   (generated)
   "main.aux"
   "main.log"

Writing/ERLM/main.fls

@@ -382,14 +382,23 @@ INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/helvetic/phvr7t.vf
 INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvr8r.tfm
 INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/helvetic/phvr7t.vf
 INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvr8r.tfm
+INPUT ./goals-and-outcomes/v2.tex
+INPUT ./goals-and-outcomes/v2.tex
+INPUT ./goals-and-outcomes/v2.tex
+INPUT ./goals-and-outcomes/v2.tex
+INPUT goals-and-outcomes/v2.tex
 INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvb7t.tfm
 INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvb7t.tfm
+INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvro7t.tfm
 INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/helvetic/phvb7t.vf
 INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvb8r.tfm
 INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/helvetic/phvr7t.vf
 INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvr8r.tfm
+INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/helvetic/phvro7t.vf
+INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvro8r.tfm
 INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/helvetic/phvb7t.vf
 INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvb8r.tfm
 INPUT main.aux
 INPUT /usr/share/texlive/texmf-dist/fonts/type1/urw/helvetic/uhvb8a.pfb
 INPUT /usr/share/texlive/texmf-dist/fonts/type1/urw/helvetic/uhvr8a.pfb
+INPUT /usr/share/texlive/texmf-dist/fonts/type1/urw/helvetic/uhvro8a.pfb

Writing/ERLM/main.log

@@ -1,4 +1,4 @@
-This is pdfTeX, Version 3.141592653-2.6-1.40.25 (TeX Live 2023/Debian) (preloaded format=pdflatex 2024.9.11)  2 SEP 2025 22:25
+This is pdfTeX, Version 3.141592653-2.6-1.40.25 (TeX Live 2023/Debian) (preloaded format=pdflatex 2024.9.10)  3 SEP 2025 11:25
 entering extended mode
  restricted \write18 enabled.
  file:line:error style messages enabled.
@@ -829,31 +829,30 @@ LaTeX Font Info:    Trying to load font information for U+msb on input line 5.
 File: umsb.fd 2013/01/14 v3.01 AMS symbols B
 ) [1
 
-{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}{/usr/share/texlive/texmf-dist/fonts/enc/dvips/base/8r.enc}]
+{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}{/usr/share/texlive/texmf-dist/fonts/enc/dvips/base/8r.enc}] (./goals-and-outcomes/v2.tex
-Overfull \hbox (0.67523pt too wide) in paragraph at lines 57--62
+LaTeX Font Info:    Font shape `OT1/phv/m/it' in size <12> not available
-\OT1/phv/m/n/12 each mode tran-si-tion as al-lowed from the re-quire-ments syn-the-sis squares up against
+(Font)              Font shape `OT1/phv/m/sl' tried instead on input line 23.
- []
+ [1])
-
 No file main.bbl.
-[1] (./main.aux)
+[2] (./main.aux)
  ***********
 LaTeX2e <2023-11-01> patch level 1
 L3 programming layer <2024-01-22>
  ***********
  ) 
 Here is how much of TeX's memory you used:
- 25245 strings out of 476182
+ 25258 strings out of 476182
- 524777 string characters out of 5795595
+ 525061 string characters out of 5795595
- 1933975 words of memory out of 5000000
+ 1934975 words of memory out of 5000000
- 46726 multiletter control sequences out of 15000+600000
+ 46733 multiletter control sequences out of 15000+600000
- 571272 words of font info for 60 fonts, out of 8000000 for 9000
+ 573158 words of font info for 62 fonts, out of 8000000 for 9000
  14 hyphenation exceptions out of 8191
  110i,6n,107p,1008b,285s stack positions out of 10000i,1000n,20000p,200000b,200000s
-</usr/share/texlive/texmf-dist/fonts/type1/urw/helvetic/uhvb8a.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/helvetic/uhvr8a.pfb>
+</usr/share/texlive/texmf-dist/fonts/type1/urw/helvetic/uhvb8a.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/helvetic/uhvr8a.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/helvetic/uhvro8a.pfb>
-Output written on main.pdf (2 pages, 24992 bytes).
+Output written on main.pdf (3 pages, 30389 bytes).
 PDF statistics:
- 49 PDF objects out of 1000 (max. 8388607)
+ 57 PDF objects out of 1000 (max. 8388607)
- 24 compressed objects within 1 object stream
+ 29 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)
 

Writing/ERLM/main.tex

@@ -3,72 +3,9 @@
 \begin{document}
 
 \maketitle
-\section{Goals and Outcomes}
 
-The goal of this research is to use formal methods to create control systems
+\input{goals-and-outcomes/v2}
-that can switch between operating modes with a high assurance of correct
-construction. Modern control systems today often exist as hybrid control
-systems. Hybrid systems are those that have both continuous and discrete
-dynamics. Because of this, hybrid systems cannot be fully analyzed using only
-tools from continuous or discrete methods. Today, hybrid control systems are
-unable to be completely verified, that is to say we do not currently have ways
-of being building hybrid control systems that we can be certain meet high level
-strategic objectives, or who's behavior is totally understood.
-
-The ambiguity on hybrid system behavior is problematic when one of the most
-useful cases of hybrid system control is for improved autonomy of critical
-systems. Nuclear power is a salient example. For a nuclear reactor during
-start-up, every mode of power from initially cold-start, to controlled core
-heating, and eventually  full operating power is well understood dynamically.
-For each of these modes, significant portions of the control are optimized using
-automated controllers for each stage. The problem that remains for human
-operators is choosing when to switch from control law to the next, and ensuring
-that the proper conditions are met to do so--but these conditions are also
-clearly defined in regulation and operating procedures a priori.
-
-We can use the fact that these transition points are well understood in
-combination with formal methods to synthesize the discrete part of a hybrid
-system. From that point, we can have a robust chain of proof that our discrete
-jumps will happen only at the correct times. Once that is established, we can
-use reachability analysis and traditional control theory to ensure that each
-operation 'mode' satisfies liveness, stability, or performance requirements.
-With the combination of these two methods, we can be sure of correct behavior
-switching between modes, and that strategic goals remain met while transitioning
-from one mode switch to the next.
-
-If this research is successful, we will be able to do the following:
-
-\begin{enumerate}
-
-  \item
-    \textbf{Formalize} mode switching requirements as logical statements that
-    can then be translated into a controller implementation. This piece will
-    address the correct-by-construction generation of the mode switching
-    controller.
-
-  \item 
-    \textbf{Categorize} different continuous modes by their strategic relevance.
-    Certain modes exist as control laws from one mode to the next, such as a
-    controlled heating rate on reactor start-up before reaching operational
-    conditions. Other modes exist as stable regions, such as full-power
-    operation. 
-
-  \item
-    \textbf{Verify} continuous modes and accompanying continuous control laws
-    satisfy strategic requirements. This can be done with reachability analysis,
-    and ensuring that each mode transition as allowed from the requirements
-    synthesis squares up against the reachability analysis and the continuous
-    dynamics.
-
-  \item
-    \textbf{Prove} that a given hybrid system achieves strategic goals across
-    hybrid control modes. By seperately formalizing and analyzing continuous
-    dyanmics and discrete dynamics, we can come back to say the whole hybrid
-    system has met a strong guarantee of requirement adherence.
-
-\end{enumerate}
 
 \bibliography{references}
 
 \end{document}
-