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.

___________________________________________________________

## **Integrating Shielding into Nuclear Power Control** 

### Goal:

The goal of this research is to use temporal logic shielding
to do online safety assurance of a machine learning (ML)
based controller for a reactor control system (RCS). While
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. Translate regulatory and system level requirements into a
   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. Design a verified fallback controller against the same
   verification requirements that can either return the
reactor to the safe state space or safely shut down the
reactor.

3. Evaluate performance of the ML controller with attached
   shield, while assessing shield intervention frequency for
different operating scenarios (power up, shut down, regular
load following).

### Impact: 

Machine learning controllers can outperform PID and
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 prevents ML based controllers from
being used in high-assurance usecases such as nuclear power.
Shielding can address this issue, by providing a formal
runtime assurance, alleviating the burden of explainability
away from the machine learning algorithm. This work would
further bring regulatory requiremnts into the formal design
of control systems and high

### 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 resarch is to use formal methods to verify
safety properties of neural network controller for a reactor
control system. Neural network based controllers are able to
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:

For this research to be successful, I will accomplish the
following:

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

2. Encode shutdown margin safety requirements into a SMT or
   MILP framework.

3. Formally verify that the neural network based controller
   will not violate any shutdown margin restrictions while
still meeting operational goals.

### Impact:

SMT and MILP methods of verifying neural networks have been
previously applied to classification problems, but have not
been utilized to check neural network controllers for
adherence to cyber-physical system requirements. Critical
infrastructure control such as nuclear power is an ideal
candidate for these methods to be utilized, however, because
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 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:

For this research to be successful, I will accomplish the
following:

1. Captured high level safety and operating reactor control
   requirements in a temporal logic language 

2. Synthesize a supervisory controller from the temporal
   logic specification using a tool like Strix

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

## **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)?

- 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 Fault Detection Using High-Assurance Digital Twins** 
(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
from a real plant to identify issues such as coolant losses,
sensor and actuator failures, or component degredation so
that safety strategic decisions about the plant can be made
autonomously.

### Outcomes:

For this research to be successful, I will accomplish the
following:

- Create a simulation suite for the Small Modular Advanced
  High Temperature Reactor (SmAHTR) to simulate fault
  conditions of sensors, actuators, and component degradation.

- Develop a physics informed neural network (PINN) approach
  to evaluate physics discrepancies in measured signals and
  to estimate physically relevant parameters to determine
  real system divergence from the nominal plant. 

- Realize a proof of concept autonomous controller than can
  react to fault conditions by switching to different
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
maintenance, and finally the labor involved in operating the
reactor itself. Currently the largest of these O&M expenses
is the labor and part cost used in maintenance, while large
nuclear reactor facilities require a modest reactor operator
budget per megawatt of energy produced. The advent of small
modular reactors (SMRs) and microreactors (MRs) will change
these economics significantly. 

As SMRs and MRs become more common, the cost of repair and
maintenance should reduce dramatically as nuclear power
components will become modular, replaceable parts instead of
the bespoke reactor designs currently operating. Operator
wages, however, can be expected to increase without
introducing greater controller autonomy. SMRs and MRs are
much smaller output designs per reactor core, and if they
are required to employ the same size reactor operator team
as a conventional large reactor, will suffer from much
larger operator expense per megawatt. Greater controller
autonomy can solve this problem by unloading some reactor
control responsibilities from the operator, and therein
reduce labor consumption.

<# TO DO #>
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:

- Create a simulation suite for the Small Modular Advanced High
Temperature Reactor (SmAHTR) to simulate component degradation
such as heat exchanger blockages and fuel concentration burn-up.*

- Create an adaptive control rod controller to maximize load following
precision for a simulated power grid demand.

- Use contract based verification at runtime to ensure that
learned parameters for the adaptive controller remain within
safety specification limits

*Is this actually even a problem for SmAHTR? Figuring the fuel is
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
changes from the power grid on their own, but over will lose
efficiency as the underlying plant mechanics become less
efficient, or maintenance is performed and components are
refreshed. For nuclear power contexts, fine control is ideal to
maximize profits and to minimize energy wasteage. This is not an
easy problem to solve, however, as the dynamics of the underlying
plant are constantly changing. Adaptive control can help address
this issue, but learnable controllers must come with guarantees
of safety in order to be attractive to the nuclear industry.

### Related Papers: