Auto sync: 2025-09-05 11:32:34 (11 files changed)

M .sessions/Journal.vim M .sessions/nvim_config.vim A Writing/ERLM/goals-and-outcomes/v3.tex M Writing/ERLM/main.fdb_latexmk M Writing/ERLM/main.fls M Writing/ERLM/main.log M Writing/ERLM/main.pdf M Writing/ERLM/main.synctex.gz
2025-09-05 11:32:34 -04:00 · 2025-09-05 11:32:34 -04:00 · 1be3b7420c
commit 1be3b7420c
parent a9632a264e
11 changed files with 207 additions and 28 deletions
--- a/.sessions/Journal.vim
+++ b/.sessions/Journal.vim
@ -3,7 +3,7 @@ let s:so_save = &g:so | let s:siso_save = &g:siso | setg so=0 siso=0 | setl so=-
 let v:this_session=expand("<sfile>:p")
 silent only
 silent tabonly
-cd ~/Documents/Dane\'s\ Vault
+cd ~/Documents/Dane\'s\ Vault/Writing/Journal
 if expand('%') == '' && !&modified && line('$') <= 1 && getline(1) == ''
  let s:wipebuf = bufnr('%')
 endif
@ -13,14 +13,13 @@ if &shortmess =~ 'A'
 else
  set shortmess=aoO
 endif
-badd +22 Journal/2025_07_30.md
-badd +1 ~/Documents/Dane\'s\ Vault/Zettelkasten/Literature\ Notes/albertiAutomationLevelsNuclear2023.md
-badd +16 ~/Documents/Dane\'s\ Vault/Zettelkasten/Literature\ Notes/agarwalSystematicClassificationNeuralnetworkbased1997.md
+badd +1 ~/Documents/Dane\'s\ Vault/Journal/2025_07_30.md
+badd +22 ~/Documents/Dane\'s\ Vault/Writing/Journal//JRNL-20250904-135850.md
 argglobal
 %argdel
-edit ~/Documents/Dane\'s\ Vault/Zettelkasten/Literature\ Notes/albertiAutomationLevelsNuclear2023.md
+edit ~/Documents/Dane\'s\ Vault/Writing/Journal//JRNL-20250904-135850.md
 argglobal
-balt Journal/2025_07_30.md
+balt ~/Documents/Dane\'s\ Vault/Journal/2025_07_30.md
 setlocal foldmethod=manual
 setlocal foldexpr=0
 setlocal foldmarker={{{,}}}
@ -31,12 +30,12 @@ setlocal foldnestmax=20
 setlocal foldenable
 silent! normal! zE
 let &fdl = &fdl
-let s:l = 1 - ((0 * winheight(0) + 32) / 64)
+let s:l = 22 - ((12 * winheight(0) + 30) / 60)
 if s:l < 1 | let s:l = 1 | endif
 keepjumps exe s:l
 normal! zt
-keepjumps 1
-normal! 0
+keepjumps 22
+normal! 010|
 tabnext 1
 if exists('s:wipebuf') && len(win_findbuf(s:wipebuf)) == 0 && getbufvar(s:wipebuf, '&buftype') isnot# 'terminal'
  silent exe 'bwipe ' . s:wipebuf
--- a/.sessions/nvim_config.vim
+++ b/.sessions/nvim_config.vim
@ -15,7 +15,7 @@ else
 endif
 badd +12 ~/.config/nvim/lua/custom/plugins.lua
 badd +44 custom/configs/lspconfig.lua
-badd +106 custom/journal.lua
+badd +89 custom/journal.lua
 argglobal
 %argdel
 edit custom/journal.lua
@ -31,12 +31,12 @@ setlocal foldnestmax=20
 setlocal foldenable
 silent! normal! zE
 let &fdl = &fdl
-let s:l = 1 - ((0 * winheight(0) + 32) / 64)
+let s:l = 89 - ((11 * winheight(0) + 23) / 47)
 if s:l < 1 | let s:l = 1 | endif
 keepjumps exe s:l
 normal! zt
-keepjumps 1
-normal! 0
+keepjumps 89
+normal! 016|
 tabnext 1
 if exists('s:wipebuf') && len(win_findbuf(s:wipebuf)) == 0 && getbufvar(s:wipebuf, '&buftype') isnot# 'terminal'
  silent exe 'bwipe ' . s:wipebuf
--- a/Writing/ERLM/goals-and-outcomes/v3.tex
+++ b/Writing/ERLM/goals-and-outcomes/v3.tex
@ -0,0 +1,84 @@
+\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
+autonomous control applications because they can switch between different
+control laws based on discrete triggers in the system's operating range. This
+approach allows autonomous controllers to use several tractable control laws
+optimized for different regions in the state space, rather than relying on a
+single controller across the entire operating range. However, the discrete
+transitions between control laws in hybrid controllers present significant
+challenges in proving stability and liveness properties for the complete system.
+While tools from control theory can establish properties for individual control
+modes, these guarantees do not generalize when mode switching is introduced.
+Existing temporal logic synthesis tools like Strix can generate discrete
+controllers from logical specifications, but they assume instantaneous mode
+transitions. In hybrid systems, transitions occur along continuous trajectories
+governed by differential equations, creating a verification gap that neither
+purely discrete synthesis nor traditional control theory can address alone.
+
+This research takes a novel approach to hybrid controller synthesis and
+verification by bridging this gap. We will leverage formal methods to create
+controllers that are correct-by-construction, enabling guarantees about the
+complete system's behavior. To demonstrate this approach, we will develop an
+autonomous controller for nuclear power plant start-up procedures. Nuclear power
+represents an excellent test case because the continuous reactor dynamics are
+well-studied, while the discrete mode switching requirements are explicitly
+defined in regulatory procedures and operating guidelines. Current nuclear
+reactor control \textit{is} already a hybrid system---many control room
+functions employ automated controllers for basic tasks, but the engagement and
+selection of these controllers relies on human operators following procedural
+decision-making.
+
+The capability to create high-assurance hybrid control systems has significant
+potential to reduce labor costs in operating critical systems by removing human
+operators from routine control loops. Nuclear power stands to benefit
+substantially from increased controller autonomy, as operations and maintenance
+represent the largest expense for current reactor designs. While emerging
+technologies such as microreactors and small modular reactors will reduce
+maintenance costs through factory-manufactured replacement components, they face
+increased per-megawatt operating costs if required to maintain traditional
+staffing levels. However, if increased autonomy can be safely introduced, these
+economic challenges can be addressed while maintaining safety standards.
+
+If this research is successful, we will achieve the following outcomes:
+
+\begin{enumerate}
+
+  \item
+    \textbf{Formalize mode switching requirements as logical specifications that
+    can be synthesized into discrete controller implementations.} The discrete
+    transitions between continuous controller modes are often explicitly defined
+    in operating procedures and regulatory requirements for critical systems.
+    These natural language requirements will be translated into temporal logic
+    specifications, which will then be synthesized into provably correct
+    discrete controllers for continuous mode switching.
+
+  \item
+    \textbf{Categorize continuous controller modes by their strategic
+    relevance.} Different control modes serve distinct purposes: they may be
+    transitory (guiding the system toward a target state) or stabilizing
+    (maintaining the system within desired operating bounds). While the discrete
+    component handles mode switching decisions, this outcome will identify the
+    dynamic properties that continuous components must satisfy for each
+    controller mode.
+
+  \item
+    \textbf{Verify that continuous controller modes satisfy dynamic
+    requirements using appropriate analysis methods.} For linear dynamics, we
+    will apply classical control theory to establish stability and performance
+    within each mode. For nonlinear systems, reachability analysis will verify
+    that transitory modes drive the system toward intended transitions while
+    maintaining safety constraints, and that stabilizing modes maintain the
+    system within designated operating regions.
+
+  \item
+    \textbf{Prove that hybrid system implementations achieve strategic goals
+    across the complete operating range.} By synthesizing discrete controller
+    transitions from logical specifications using correct-by-construction
+    methods and verifying that continuous components perform appropriately
+    between discrete transitions, we can establish confidence that the hybrid
+    system is defect-free and suitable for deployment as a critical autonomous
+    controller.
+  
+\end{enumerate}
--- a/Writing/ERLM/main.fdb_latexmk
+++ b/Writing/ERLM/main.fdb_latexmk
@ -1,5 +1,5 @@
 # Fdb version 4
-["bibtex main"] 0 "main.aux" "main.bbl" "main" 1756913150.42547 0
+["bibtex main"] 0 "main.aux" "main.bbl" "main" 1756914815.67803 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,7 +7,7 @@
  "main.bbl"
  "main.blg"
  (rewritten before read)
-["pdflatex"] 1756913149.4861 "main.tex" "main.pdf" "main" 1756913150.42571 0
+["pdflatex"] 1756914814.87506 "main.tex" "main.pdf" "main" 1756914815.67825 0
  "/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 ""
@ -214,10 +214,10 @@
  "/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map" 1722610820.43889 128028 f533b797fba58d231669ea19e894e23e ""
  "/var/lib/texmf/web2c/pdftex/pdflatex.fmt" 1726005817 6800784 2b63e5a224c5ad740802d8f9921962c1 ""
  "dane_proposal_format.cls" 1756902979.42453 2551 deee3ebc77bdfb5d08546fb19b3bdd53 ""
-  "goals-and-outcomes/v2.tex" 1756913147.34838 3929 81698d2601ffbfc97dd16c2553a8806b ""
-  "main.aux" 1756913150.28919 213 c6307743402c02a0530961857d9d1a69 "pdflatex"
+  "goals-and-outcomes/v3.tex" 1756914813.48011 5009 e6fec2f2a28458203dc7d8364359d335 ""
+  "main.aux" 1756914815.55804 213 c6307743402c02a0530961857d9d1a69 "pdflatex"
  "main.bbl" 0 -1 0 "bibtex main"
-  "main.tex" 1756910438.79598 141 c588c1bc2f6a6f85c912c3842ff6c482 ""
+  "main.tex" 1756914785.75852 141 3cd602a79ef89e3739fb95feacd0ad80 ""
  (generated)
  "main.aux"
  "main.log"
--- a/Writing/ERLM/main.fls
+++ b/Writing/ERLM/main.fls
@ -382,11 +382,11 @@ 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 ./goals-and-outcomes/v3.tex
+INPUT ./goals-and-outcomes/v3.tex
+INPUT ./goals-and-outcomes/v3.tex
+INPUT ./goals-and-outcomes/v3.tex
+INPUT goals-and-outcomes/v3.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
--- a/Writing/ERLM/main.log
+++ b/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.10)  3 SEP 2025 11: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:53
 entering extended mode
 restricted \write18 enabled.
 file:line:error style messages enabled.
@ -829,9 +829,9 @@ 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}] (./goals-and-outcomes/v2.tex
+{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}{/usr/share/texlive/texmf-dist/fonts/enc/dvips/base/8r.enc}] (./goals-and-outcomes/v3.tex
 LaTeX Font Info:    Font shape `OT1/phv/m/it' in size <12> not available
-(Font)              Font shape `OT1/phv/m/sl' tried instead on input line 23.
+(Font)              Font shape `OT1/phv/m/sl' tried instead on input line 28.
 [1])
 No file main.bbl.
 [2] (./main.aux)
@ -849,7 +849,7 @@ Here is how much of TeX's memory you used:
 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/uhvro8a.pfb>
-Output written on main.pdf (3 pages, 30389 bytes).
+Output written on main.pdf (3 pages, 31255 bytes).
 PDF statistics:
 57 PDF objects out of 1000 (max. 8388607)
 29 compressed objects within 1 object stream
--- a/Writing/ERLM/main.pdf
+++ b/Writing/ERLM/main.pdf
--- a/Writing/ERLM/main.synctex.gz
+++ b/Writing/ERLM/main.synctex.gz
--- a/Writing/ERLM/main.tex
+++ b/Writing/ERLM/main.tex
@ -4,7 +4,7 @@

 \maketitle

-\input{goals-and-outcomes/v2}
+\input{goals-and-outcomes/v3}

 \bibliography{references}

--- a/Writing/Journal/JRNL-20250904-135850.md
+++ b/Writing/Journal/JRNL-20250904-135850.md
@ -0,0 +1,69 @@
+---
+id: JRNL-20250904-135850
+title: Thursday, September 04, 2025 - 01:58 PM
+type: journal
+created: 2025-09-04T17:58:50Z
+modified: 2025-09-04T17:58:50Z
+tags: [journal]
+---
+
+# Thursday, September 04, 2025 - 01:58 PM
+
+So today is actually a late journal for yesterday... I got
+sschleepy and went to bed.
+
+Yesterday significantly less happened. I finished my first
+draft of the goals and outcomes section, I went to class,
+and then I got food at Totopo with Devyn and Erik
+(Juengling).
+
+The first draft of my goals and outcomes section was pretty
+good I think, but there's still issues. For one, I've got to
+tighten up my goal. It's just not good enough but it must
+straddle a line between being too long and being jargony.
+There's also problems with intellectual merit. I feel like
+there's not one single issue that is being addressed.
+
+We discussed this somewhat in the group meeting we had right
+after class. Dan started talking about how for hybrid
+systems the proving of stability is still very difficult. I
+feel like I could have some good ideas on how to solve that
+problem, because the answer has to exist in examining
+boundary behavior. I should get a move on trying some things
+out for that. I watched a lecture by Andre Platzer about
+verifying hybrid systems, and while his system of
+differential dynamic logic does seem to capture hybrid
+system behavior, it feels way too complicated.
+
+ERLM was fun. Dan went over some goals and outcomes
+submissions and offered comments. I think mine would've been
+one of the best but I've had a head start on this whole
+proposal thing. Also, I feel like my writing experience
+lets me get ideas across easily.
+
+The rest of the day was pretty chill. I retooled my dating
+profiles with some better pictures of me. One of me from the
+last Yinz Run Club, and one again from Jonathan's wedding.
+Claude thinks I need a picture that is a proof of
+sociability. It might be right. The results though have been
+dramatic. I'm certainly getting more matches and have a
+couple new threads going.
+
+Then, Devyn, Erik, and I caught up at Totopo. That was a lot
+of fun :). Devyn is not having the best time out in King of
+Prussia and is interviewing for jobs out here (As well as
+around the country). He thinks Philadelphia Gear is a boring
+company to work for, and for someone with his skillset, is
+probably a waste of his talents. He and his girlfriend have
+a debt mountain that they're trying to work down too--she is
+having a really hard time finding a job with a biostatistics
+degree. They're going on 27. It was really nice to see Devyn
+again. I forgot how much I actually missed that guy. Erik
+was good too, he's working full time at Siemens now and is
+living in Lawrenceville with his girlfriend.
+
+That's pretty much it from Wednesday. Today (Thursday) I
+woke up and  didn't really get moving until close to noon.
+That's problematic but I do feel refreshed. Today I have the
+union meeting, and I'm watching the Eagles game and
+Andrew's.
--- a/Notes/Weekly/2025_36.md
+++ b/Notes/Weekly/2025_36.md
@ -0,0 +1,27 @@
+---
+id: 2025-36
+title: Weekly — 2025-09-02
+type: Weekly
+created: 2025-08-20T13:54:13Z
+modified: 2025-09-03T18:59:44Z
+tags: [weekly]
+---
+
+# Weekly - 2025 CW 36 (Aug 25 - Aug 30)
+
+## Accomplishments
+- Wrote the goals and outcomes, went up to V4.
+- Goal was flubbed but have new content
+- started thinking about how continuous dynamics need to be
+  included. 
+- Tried to watch a video about hybrid system verification.
+Made fun of 'trajectories' nomenclature instead of
+executions and then shit really went off the rails fast.
+Lots of pretty figures but I have to be honest I have no
+idea what the fuck he was talking about.
+- Had crises about intellectual mert
+
+## To Do
+- Rewrite GO
+- SOTA. Start writing. 
+- look up cones for math