hehe

Zettelkasten/Fleeting Notes/Editing/thesis_ideas_notes.md

@@ -1,3 +1,19 @@
 # Notes on [[thesis-ideas-2025-07-30]]
 
+What needs done:
 
+- [X] 1 needs edited and reviewed
+    - [X] Review outcomes. I really don't like outcome
+    number 1.
+
+- [X] Review and edit 2
+
+- [ ] Review and edit 3
+    - [ ] Write an impact section
+
+- [ ] Review and edit 4
+    - [ ] Needs more goal 
+
+- [ ] Review and edit 5
+
+- [ ] Review and edit 6

Zettelkasten/Fleeting Notes/Journal/2025_08_07.md

@@ -1,7 +1,7 @@
 ---
 ---
 
-# 2025-08-06
+# 2025-08-07
 Today I have not gotten too much done, but I did get here
 early today. Today, I'll sell the truck and work on Sam's
 car. I saw Patrick today too, which was nice. Robert's stuff

Zettelkasten/Fleeting Notes/Journal/2025_08_10.md

@@ -0,0 +1,8 @@
+---
+---
+
+# 2025-08-10
+Today I'm finishing the thesis ideas, for real this time.
+
+I'm also going to get a model of a heat exchanger working.
+

Zettelkasten/Permanent Notes/thesis-ideas.md

@@ -5,38 +5,49 @@ suggested I write down 6 ideas, and from them we shall
 figure out a possible topic idea that I can really start
 working on.
 
-I used ChatGPT to do some of the heavy lifting based on the
-papers I've been reading, and leveraged the 'deep research'
-feature. Here are some of my favorite ideas, broken down
-into goals, outcomes, impact, and related papers.
-
 ___________________________________________________________
 
 ## **Integrating Shielding into Nuclear Power Control** 
 
 ### Goal:
-The goal of this research is develop machine learning
+
-enabled control algorithims for nuclear power applications
+The goal of this research is to use temporal logic shielding
-that incoporate shielding: a formal guarantee of adherence
+to do online safety assurance of a machine learning (ML)
-to system specifications without augmenting the machine
+based controller for a reactor control system (RCS). While
-learning process.
+ML-based controllers can outperform traditional rule-based
+or PID control systems, their lack of provable safety
+guarantees has prevented their deployment in nuclear control
+applications. This work proposes to integrate shielding into
+a ML-based RCS to provide a strong safety guarntee.
+Shielding uses temporal logic specifications to define an
+area in the state space that is safe. If the ML controller's
+predicted actions leave this space or violate a
+specification, the shield intervenes and engage a
+safety-oriented fallback controller. This way, safety
+guarantees are still provided by the fallback controller,
+but the ML controller is free to operate within the verified
+safe region..
 
 ### Outcomes:
+
 For this research to be successful, I will accomplish the
 following: 
 
-1. Identify key controllers in a nuclear power context with
+1. Translate regulatory and system level requirements into a
-   the most benefit from using an ML-based controller
+   temporal logic specification to synthesize a controller
+'shield'. This shield monitors the ML controller and
+intervenes whenever a requirement is predicted to be
+violated.
 
-2. Translate regulatory and system level requirements into a
+2. Design a verified fallback controller against the same
-   formal specification to synthesize a controller 'shield'.
+   verification requirements that can either return the
-   This shield monitors the ML controller and intervenes 
+reactor to the safe state space or safely shut down the
-   whenever a requirement is predicted to be violated.
+reactor.
 
 3. Evaluate performance of the ML controller with attached
-   shield, while assessing the amount of shield useage for
+   shield, while assessing shield intervention frequency for
-   different operating scenarios (power up, shut down, regular
+different operating scenarios (power up, shut down, regular
-   load following)
+load following).
 
 ### Impact: 
 
@@ -45,17 +56,16 @@ rule-based controllers by adapting to nonlinear dynamics,
 optimizing over multi-objective cost functions, and changing
 plant conditions. But, these ML controllers are often
 *unexplainable*, meaning that their global behavior is not
-easily understood.This unexplainability prevents ML based
+easily understood. This prevents ML based controllers from
-controllers from being used in high-assurance usecases such
+being used in high-assurance usecases such as nuclear power.
-as nuclear power. Shielding can address this issue, by
+Shielding can address this issue, by providing a formal
-providing a formal runtime assurance, allieviating the
+runtime assurance, alleviating the burden of explainability
-burden of explainability away from the machine learning
+away from the machine learning algorithm. This work would
-algorithm. This work would further bring regulatory
+further bring regulatory requiremnts into the formal design
-requiremnts into the formal design of control systems and
+of control systems and high
-help bridge the gap between high assurance systems and the
-start of the art in control.
 
 ### Relevant Papers
+
 [[safe-reinforcement-learning-via-shielding]]
 [[evaluating-robustness-of-neural-networks-with-mixed-integer-programming]]
 
@@ -64,50 +74,71 @@ ___________________________________________________________
 ## **Formally Verified Neural Network Control of Control Rod System** 
 
 ### Goals:
-The goal of this research is to use formal methods to ensure that
+
-a neural network based control rod controller will never violate
+The goal of this resarch is to use formal methods to verify
-safety guarantees of a reactor trip system. To do this, a
+safety properties of neural network controller for a reactor
-satisfiability modulo theory method will be applied to
+control system. Neural network based controllers are able to
-exhaustively search the network for potential failure modes.
+efficiently control nonlinear systems with complex
+objectives, but by their nature are are opaque systems whose
+behavior is not easily analyzed. That being said, once a
+neural network is trained, it is an entirely deterministic
+system. Recent techniques using satisfiability modulo theory
+(SMT) or mixed integer linear programming (MILP) encodings
+of neural networks have been used to verify neural network
+controller behavior adheres to constraints for fixed input
+spaces. This work will adapt these methods to be used with
+nuclear-specific safety constraints and enable provably safe
+neural network control for the nuclear industry.
 
 ### Outcomes:
-If this research is successful, I will have accomplished the
+
+For this research to be successful, I will accomplish the
 following:
 
-- Build a neural network controller for real time control of a
+1. Build a neural network controller for real time control
-control rod system.
+   of a control rod system.
 
-- Formalize safety guarantees of shutdown margin in a
+2. Encode shutdown margin safety requirements into a SMT or
-satisfiability modulo theory embedding
+   MILP framework.
 
-- Formally verify that the neural network based controller will
+3. Formally verify that the neural network based controller
-not violate any shutdown margin restrictions 
+   will not violate any shutdown margin restrictions while
+still meeting operational goals.
 
 ### Impact:
-SMT solvers and MILP formulations have been applied to neural
+
-networks to ensure that the network is resilient to input
+SMT and MILP methods of verifying neural networks have been
-perturbations. I think we can expand this to more general
+previously applied to classification problems, but have not
-considerations of the state space, especially when there are a
+been utilized to check neural network controllers for
-relatively small number of states such as in power contexts. The
+adherence to cyber-physical system requirements. Critical
-benefit of this system is that we would get closer to saying
+infrastructure control such as nuclear power is an ideal
-neural network based systems can be high assurance for physical
+candidate for these methods to be utilized, however, because
-systems.
+the systems being controlled have a bounded and
+well-characterized state space compared to other neural
+network controller usecases (autonomous flight, autonomous
+driving, image classification, etc.). This work, if
+successful, will help ease tensions about neural network
+controllers' safety for critical infrastructure, and allow a
+new class of provably safe control architectures to be used
+in high assurance systems.
 
 ### Related Papers:
+
 [[reluplex-an-efficient-smt-solver-for-verifying-deep-neural-networks]]
 [[evaluating-robustness-of-neural-networks-with-mixed-integer-programming]]
 [[formal-verification-of-neural-network-controlled-autonomous-systems]]
-
 ___________________________________________________________
 
 ## **Temporal Logic Specifications for Autonomous Controller Synthesis**
 
 ### Goals:
+
 The goal of this program is to use temporal logic
 specifications to procedurally generate autonomous
 supervisory controllers for a reactor system.
 
 ### Outcomes:
+
 If this research is successful, I will have accomplished the
 following:
 
@@ -129,11 +160,13 @@ ___________________________________________________________
 ## **Formally Verified Runtime Monitoring and Fallback**
 
 ### Goals:
+
 If this research is successful, we will be able to generate
 autonomous controller shields that provably adhere to specifications
 written with temporal logic.
 
 ### Outcomes:
+
 - Create an intermediary shield that mediates signals between an
   optimal control system and the physical plant (MODBUS)?
 
@@ -145,6 +178,7 @@ 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
@@ -162,6 +196,7 @@ 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]]
@@ -172,6 +207,7 @@ ___________________________________________________________
 (8)
 
 ### Goals:
+
 The goal of this research is to use machine learning to
 identify system faults of a reactor control system during
 runtime. A digital twin will be compared to measurements
@@ -181,6 +217,7 @@ that safety strategic decisions about the plant can be made
 autonomously.
 
 ### Outcomes:
+
 For this research to be successful, I will accomplish the
 following:
 
@@ -199,6 +236,7 @@ control modes rather than only responding with reactor
 shutdown.
 
 ### Impact:
+
 The nuclear energy industry's largest expense is operations
 and maintenance (O&M). These costs include typical reactor repair
 and refueling, the labor involved to complete such
@@ -229,17 +267,19 @@ Finally reactor safety can be improved by greater autonomy
 yada yada find some reasons to back this up.
 
 ### Related Papers:
-
 ___________________________________________________________
 
 ## **Verified Adaptive Control** 
+
 ### Goals:
+
 The goal of this research is to create an adaptive controller
 that can adjust to system dynamics changes over time to maintain
 an optimal control, while using formal methods to provide strong
 safety guarantees about the malleable control law.
 
 ### Outcomes:
+
 For this research to be successful, I will accomplish the
 following:
 
@@ -259,6 +299,7 @@ suspended in the salt I'd assume chemistry is pretty strictly
 controlled. I'm sure I can find other examples.
 
 ### Impact:
+
 Certain reactor control systems are already automatic systems,
 such as constant temperature or pressure controls for operating
 at steady state. These simple controllers are able to follow load
@@ -274,5 +315,3 @@ of safety in order to be attractive to the nuclear industry.
 
 ### Related Papers:
 
-
-