Obsidian/Zettelkasten/Permanent Notes/thesis-ideas.md

# Thesis Ideas 2025-07-30

Following our group meeting from Monday, July 28th, Dan
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 to develop machine learning
control algorithms for nuclear power applications with
strict safety guarantees.

### Outcomes:
If this research is successful, I will have accomplished the
following:

1. Develop controller shielding methods for nuclear power
   contexts

2. Provide concrete safety guarantees for autonomous control
   of a nuclear asset.

3. ??? <!TODO!>

### Impact: 
Machine learning based systems have been shown to be more
efficient than typical PID based controllers, and are able to
learn more complex objective functions than a typical controller
can. The problem with these controllers though is that they are
often unexplainable. This is not acceptable for high assurance
applications, where slight perturbations on inputs can yield
wildly different outputs. Shielding can solve this problem,
helping ensure safety of ML based controllers while not limiting
their development or construction. 

### Relevant Papers
[[safe-reinforcement-learning-via-shielding]]
[[evaluating-robustness-of-neural-networks-with-mixed-integer-programming]]

___________________________________________________________

## **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
safety guarantees of a reactor trip system. To do this, a
satisfiability modulo theory method will be applied to
exhaustively search the network for potential failure modes.

### Outcomes:
If this research is successful, I will have accomplished the
following:

- Build a neural network controller for real time control of a
control rod system.

- Formalize safety guarantees of shutdown margin in a
satisfiability modulo theory embedding

- Formally verify that the neural network based controller will
not violate any shutdown margin restrictions 

### Impact:
SMT solvers and MILP formulations have been applied to neural
networks to ensure that the network is resilient to input
perturbations. I think we can expand this to more general
considerations of the state space, especially when there are a
relatively small number of states such as in power contexts. The
benefit of this system is that we would get closer to saying
neural network based systems can be high assurance for physical
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:

- Captured high level safety and operating requirements in a
  temporal logic language such as TLA+ or FRET

- Synthesize a supervisory controller from the temporal
logic specification that can be implemented on a real
control system with minimal user effort.

- Verify the supervisory controller generated adheres to
safety specifications using exhaustive model checking.

### Impact:

### Related Papers:
___________________________________________________________

## **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 automatically.

### Outcomes:
- Create an intermediary shield that mediates signals between an
  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]]

___________________________________________________________

## **Data-Driven Model Verification for High-Assurance Digital Twins** 
(8)

### Goals:

### Outcomes:

### Impact:

### Related Papers:

___________________________________________________________

## **Verified Adaptive Control** 
(10)

### Goals:

### Outcomes:

### Impact:

### Related Papers: