From bf539832c3db45b30a85e54534833a957f806405 Mon Sep 17 00:00:00 2001
From: Dane Sabo <dane.sabo@pitt.edu>
Date: Thu, 31 Jul 2025 10:18:54 -0400
Subject: [PATCH] vault backup: 2025-07-31 10:18:54

---
 .obsidian/plugins/colored-tags/data.json      |  3 +-
 .../Fleeting Notes/Journal/2025_07_30.md      |  2 +-
 .../Fleeting Notes/Journal/2025_07_31.md      | 22 ++++++++
 Zettelkasten/Permanent Notes/thesis-ideas.md  | 51 +++++++++++++------
 4 files changed, 60 insertions(+), 18 deletions(-)
 create mode 100644 Zettelkasten/Fleeting Notes/Journal/2025_07_31.md

diff --git a/.obsidian/plugins/colored-tags/data.json b/.obsidian/plugins/colored-tags/data.json
index 2519fc7d..1f637f8b 100755
--- a/.obsidian/plugins/colored-tags/data.json
+++ b/.obsidian/plugins/colored-tags/data.json
@@ -320,7 +320,8 @@
     "Security": 308,
     "Systematic-mapping-study": 309,
     "InFirstPaks": 310,
-    "Formal-Methods": 311
+    "Formal-Methods": 311,
+    "admin": 312
   },
   "_version": 3
 }
\ No newline at end of file
diff --git a/Zettelkasten/Fleeting Notes/Journal/2025_07_30.md b/Zettelkasten/Fleeting Notes/Journal/2025_07_30.md
index 62834118..2a036ba0 100644
--- a/Zettelkasten/Fleeting Notes/Journal/2025_07_30.md	
+++ b/Zettelkasten/Fleeting Notes/Journal/2025_07_30.md	
@@ -1,7 +1,7 @@
 ---
 ---
 
-# Today's Journal
+# 2025-07-30
 
 ## Morning Brief
 Today's goal is to finish writing up some thesis ideas. I
diff --git a/Zettelkasten/Fleeting Notes/Journal/2025_07_31.md b/Zettelkasten/Fleeting Notes/Journal/2025_07_31.md
new file mode 100644
index 00000000..84b44ecf
--- /dev/null
+++ b/Zettelkasten/Fleeting Notes/Journal/2025_07_31.md	
@@ -0,0 +1,22 @@
+---
+---
+
+# 2025-07-31
+
+## Morning Brief
+Yesterday I wrote 2 thesis ideas and started a third. Today,
+we finish them! I'm struggling to write outcomes but we'll
+get there over time. I can do this.
+
+I started the morning with an hour of doomscrolling. I
+really have to sort that out.
+
+Tasks are the same from [[2025-07-30|yesterday]]. Maybe I
+should make a centralized page for tasks.
+
+- [ ] Make task page #admin
+
+## Lunch Brief
+
+
+## Note for tomorrow
diff --git a/Zettelkasten/Permanent Notes/thesis-ideas.md b/Zettelkasten/Permanent Notes/thesis-ideas.md
index 69485b98..4f5ded65 100644
--- a/Zettelkasten/Permanent Notes/thesis-ideas.md	
+++ b/Zettelkasten/Permanent Notes/thesis-ideas.md	
@@ -88,36 +88,55 @@ systems.
 ___________________________________________________________
 
 ## **Temporal Logic Specifications for Autonomous Controller Shield Synthesis**
-(3)
+
+### Goals:
+
+### Outcomes:
+
+### Impact:
+
+### Related Papers:
+___________________________________________________________
+
+## **Formally Verified Runtime Monitoring and Fallback**
 
 ### Goals:
 If this research is successful, we will be able to generate
-autonomous controllers that provably adhere to specifications
+autonomous controller shields that provably adhere to specifications
 written with temporal logic automatically.
 
 ### Outcomes:
 - Create an intermediary shield that mediates signals between an
-  optimal control system and the physical plant
+  optimal control system and the physical plant (MODBUS)?
 
-- 
+- Translate specifications in a language like TLA+ into an
+executable program 
+
+- Provide proof artifacts that automatically generated
+shield components will not allow an arbitrary controller to
+reach an unsafe state.
 
 ### Impact:
+Shielding is one of the preeminent ways to do safe machine
+learning controllers. Instead of putting the proof burden on
+the machine learning component, shielding creates a safe
+boundary in the state space where a safety controller will
+step in if the machine learning controller endangers the
+system. This technology solves a critical problem with high
+assurance systems: high assurance systems have critical
+safety requirements that make scrutiny on autonomous systems
+safety intense. Shielding can provide a safety barrier for
+the controller, allowing the architecture of the control
+laws to be amenable to more efficient machine learning based
+methods. Finally, utilizing an automatic translation from a
+temporal logic formulation of a speculation will allow the
+engineers of these systems to quickly and clearly implement
+a shield, without all of the cumbersome derivation.
 
 ### Related Papers:
+[[on-using-real-time-reachability-for-the-safety-assurance-of-machine-learning-controllers]]
 [[enhancing-cyber-physical-system-dependability-via-synthesis-challenges-and-future-directions]]
 [[safe-reinforcement-learning-via-shielding]]
-___________________________________________________________
-
-## **Formally Verified Runtime Monitoring and Fallback**
-(4)
-
-### Goals:
-
-### Outcomes:
-
-### Impact:
-
-### Related Papers:
 
 ___________________________________________________________