diff --git a/.sessions/Journal.vim b/.sessions/Journal.vim index d5343b719..f0cf63abf 100644 --- 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(":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 diff --git a/.sessions/nvim_config.vim b/.sessions/nvim_config.vim index dbf694aed..f65f9e7dd 100644 --- 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 diff --git a/Writing/ERLM/goals-and-outcomes/v3.tex b/Writing/ERLM/goals-and-outcomes/v3.tex new file mode 100644 index 000000000..347a721c8 --- /dev/null +++ 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} diff --git a/Writing/ERLM/main.fdb_latexmk b/Writing/ERLM/main.fdb_latexmk index c9e6964ee..887f1e9cc 100644 --- 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" diff --git a/Writing/ERLM/main.fls b/Writing/ERLM/main.fls index 0746a54b0..acda58820 100644 --- 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 diff --git a/Writing/ERLM/main.log b/Writing/ERLM/main.log index 23d5e696b..c28f949ec 100644 --- 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 -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 diff --git a/Writing/ERLM/main.pdf b/Writing/ERLM/main.pdf index 99477d251..84cb66680 100644 Binary files a/Writing/ERLM/main.pdf and b/Writing/ERLM/main.pdf differ diff --git a/Writing/ERLM/main.synctex.gz b/Writing/ERLM/main.synctex.gz index a51db1e95..8e85ccb67 100644 Binary files a/Writing/ERLM/main.synctex.gz and b/Writing/ERLM/main.synctex.gz differ diff --git a/Writing/ERLM/main.tex b/Writing/ERLM/main.tex index d88fd0a92..0151cecd2 100644 --- 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} diff --git a/Writing/Journal/JRNL-20250904-135850.md b/Writing/Journal/JRNL-20250904-135850.md new file mode 100644 index 000000000..55da3a326 --- /dev/null +++ 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. diff --git a/Zettelkasten/Fleeting Notes/Weekly/2025_36.md b/Zettelkasten/Fleeting Notes/Weekly/2025_36.md new file mode 100644 index 000000000..f83eb99ff --- /dev/null +++ b/Zettelkasten/Fleeting 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