From afa43d28141c9afdb7c8054b8f82e281671ed613 Mon Sep 17 00:00:00 2001
From: Dane Sabo <dane.sabo@pitt.edu>
Date: Mon, 11 Aug 2025 15:38:02 -0400
Subject: [PATCH] vault backup: 2025-08-11 15:38:02

---
 .obsidian/app.json                           |  3 +-
 .sessions/Journal.vim                        | 11 +++--
 Zettelkasten/Permanent Notes/thesis-ideas.md | 50 +++++++++++++++-----
 3 files changed, 47 insertions(+), 17 deletions(-)

diff --git a/.obsidian/app.json b/.obsidian/app.json
index 0c2168b7..dc63047c 100755
--- a/.obsidian/app.json
+++ b/.obsidian/app.json
@@ -16,5 +16,6 @@
   "strictLineBreaks": true,
   "defaultViewMode": "preview",
   "livePreview": false,
-  "showInlineTitle": false
+  "showInlineTitle": false,
+  "uriCallbacks": false
 }
\ No newline at end of file
diff --git a/.sessions/Journal.vim b/.sessions/Journal.vim
index 49a256c3..4e8ed134 100644
--- a/.sessions/Journal.vim
+++ b/.sessions/Journal.vim
@@ -14,12 +14,13 @@ else
   set shortmess=aoO
 endif
 badd +22 Journal/2025_07_30.md
-badd +17 Zettelkasten/Literature\ Notes/Nonlinear\ Identification\ and\ Control.md
+badd +72 ~/Documents/Dane\'s\ Vault/Zettelkasten/Literature\ Notes/albertiAutomationLevelsNuclear2023.md
+badd +16 ~/Documents/Dane\'s\ Vault/Zettelkasten/Literature\ Notes/agarwalSystematicClassificationNeuralnetworkbased1997.md
 argglobal
 %argdel
-edit Journal/2025_07_30.md
+edit ~/Documents/Dane\'s\ Vault/Zettelkasten/Literature\ Notes/albertiAutomationLevelsNuclear2023.md
 argglobal
-balt Zettelkasten/Literature\ Notes/Nonlinear\ Identification\ and\ Control.md
+balt Journal/2025_07_30.md
 setlocal foldmethod=manual
 setlocal foldexpr=0
 setlocal foldmarker={{{,}}}
@@ -30,11 +31,11 @@ setlocal foldnestmax=20
 setlocal foldenable
 silent! normal! zE
 let &fdl = &fdl
-let s:l = 22 - ((21 * winheight(0) + 27) / 55)
+let s:l = 78 - ((5 * winheight(0) + 10) / 21)
 if s:l < 1 | let s:l = 1 | endif
 keepjumps exe s:l
 normal! zt
-keepjumps 22
+keepjumps 78
 normal! 0
 tabnext 1
 if exists('s:wipebuf') && len(win_findbuf(s:wipebuf)) == 0 && getbufvar(s:wipebuf, '&buftype') isnot# 'terminal'
diff --git a/Zettelkasten/Permanent Notes/thesis-ideas.md b/Zettelkasten/Permanent Notes/thesis-ideas.md
index 80ca420b..5d265605 100644
--- a/Zettelkasten/Permanent Notes/thesis-ideas.md	
+++ b/Zettelkasten/Permanent Notes/thesis-ideas.md	
@@ -133,27 +133,55 @@ ___________________________________________________________
 
 ### Goals:
 
-The goal of this program is to use temporal logic
-specifications to procedurally generate autonomous
-supervisory controllers for a reactor system.
+The goal of this research is to develop a framework for
+generating autonomous supervisory controllers for reactor
+control systems directly from high-level temporal logic
+specifications. In high-assurance systems such as nuclear
+power, building control logic that is verified to adhere to
+regulatory requirements is an arduous error-prone task. To
+mitigate this problem this work will use formal
+specification languages, such as TLA+ and FRET, to encode
+safety and operational requirements. Once encoded, these
+requirements will be automatically be synthesized into a
+realizable automata.
 
 ### Outcomes:
 
-If this research is successful, I will have accomplished the
+For this research to be successful, I will accomplish the
 following:
 
-- Captured high level safety and operating requirements in a
-  temporal logic language such as TLA+ or FRET
+1. Captured high level safety and operating reactor control
+   requirements in a temporal logic language 
 
-- Synthesize a supervisory controller from the temporal
-logic specification that can be implemented on a real
-control system with minimal user effort.
+2. Synthesize a supervisory controller from the temporal
+   logic specification using a tool like Strix
 
-- Verify the supervisory controller generated adheres to
-safety specifications using exhaustive model checking.
+3. Verify the supervisory controller generated adheres to
+   safety specifications using exhaustive model checking.
+
+4. Generate proof artifacts of controller adherence to
+   formal requirements
 
 ### Impact:
 
+Safety-critical systems require controllers that have a high
+assurance that they adhere to safety and operational
+requirements. Building these controllers, however, is not an
+easy task. To build a high assurance controller today
+requires a great deal of labor as the controller and
+requirements must be iteratively checked against one another
+until an acceptable controller is found. This work seeks to
+eliminate this labor cost, and instead offload the
+controller synthesis to an automated computational solution. 
+
+While the nuclear industry is the motivating industry for
+this work, applications in other high assurance systems are
+possible. This work closes a gap between regulatory
+adherence and controller synthesis that is easily
+translatable to industries such as aerospace, autonomous
+manufacturing and other critical infrastructure.
+
+
 ### Related Papers:
 ___________________________________________________________