vault backup: 2025-07-31 10:18:54

.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
 }

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

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

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:
 
 ___________________________________________________________