Obsidian/Zettelkasten/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:
[[enhancing-cyber-physical-system-dependability-via-synthesis-challenges-and-future-directions]]
___________________________________________________________

## **Formally Verified Runtime Monitoring and Fallback**

### Goals:

The goal of this research is to create a methodology for
automatically generating runtime monitoring and fallback
switching components from formal specifications in FRET for
a reactor control system. Runtime monitoring with automatic
switchover is a proven approach to ensuring safety in
critical control systems: a primary controller operates
under normal conditions, while a fallback safety controller
is engaged if safety limits are approached or violated.
These fallback mechanisms lend themselves naturally to
linear temporal logic (LTL) specifications that can be
elicited from high-level safety and operational requirements
using automated tools. If the creation of these runtime
monitors and switchovers can be automated from formal
requirements, the engineering effort to implement robust
fallback logic will be greatly reduced, while maintaining
provable adherence to safety constraints. 

### Outcomes:

1. Implement reactor control safety and operational
   requirements as requirements in FRET, and extract
temporal logic definitions of allowable system behaviors.

2. Synthesize the switching component from LTL specification
   using an automated tool such as Strix.

2. Develop a new endpoint for the Advanced Reactor Cyber
   Analysis and Development Environment (ARCADE) that
utilizes a shielding mechanism to switch between control
trains.

3. Create an example learning-based controller to
   demonstrate the application of the machine generated
shield.

4. Provide proof artifacts that automatically generated
   shield components will not allow an arbitrary controller
to reach an unsafe state.

### Impact:

This approach addresses a persistent challenge in
high-assurance systems: stringent safety requirements often
force engineers to trade innovation and adaptability for
proven but rigid safety mechanisms. The proposed method
maintains safety guarantees while allowing more flexible or
advanced primary control strategies. Moreover, automating
the translation from formal safety requirements into
executable monitoring and switchover logic creates a
repeatable, transparent, and verifiable process. This
reduces engineering effort, improves traceability to
regulatory requirements, and may enable faster deployment of
safety-critical control architectures in nuclear power and
other critical infrastructure systems.

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

### Goals:

The goal of this research is to develop a high-assurance,
digital twin–based fault detection and mitigation framework
for a reactor control system. A physics-based digital twin
will be run in parallel with plant measurements to detect
anomalies such as coolant losses, sensor and actuator
faults, and abnormal component degradation. Discrepancies
between the digital twin and plant data will be analyzed
using residual0based and physics-informed machine learning
models to diagnose the underlying fault and trigger
appropriate graded autonomous control actions ranging from
control adjustments to safe shutdown.

### Outcomes:

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

1. Create a simulation suite for the Small Modular Advanced
   High Temperature Reactor (SmAHTR) to simulate high-impact
fault types such as secondary loop coolant losses, heat
exchanger fouling, and sensor drifting.

2. Implement a residual-based physics-informed neural
   network (PINN) to estimate key plant parameters, detect
discrepancies between predicted and measured signals, and
identify probable fault condition and severity.

3. Integrate the fault detection developed with a
   proof-of-concept autonomous supervisory controller
capable of implementing graded responses to fault conditions
aligned with NRC safety protocols.

### 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. Large reactors are able to spread these O&M
costs over large power outputs, but small modular reactors
(SMR) and microreactors (MR) do not have the same capacity
to dissipate O&M costs. Instead, SMRs and MRs must innovate
in O&M to be economically competitve. As SMRs and MRs become
more common, the cost of repair and maintenance will reduce
dramatically as nuclear power components become modular,
replaceable parts instead of the bespoke reactor designs
currently operating in large reactors. Operator wages,
however, can be expected to increase without introducing
greater controller autonomy. SMRs and MRs have much smaller
power output 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 cost.

(I think something can be said about safety here too (time
to respond, human factors removed, etc.), but I'm chewing on
how to word that.)

### Related Papers:
___________________________________________________________

## **Verified Adaptive Control** 

### Goals:

The goal of this research is to create an adaptive
controller for a reactor control system that can adjust to
system dynamics changes from component degredation or
post-maintenance effects to maintain an optimal control,
while using formal methods to provide strong safety
guarantees that all adaptations remain within verified
safety limits.

### Outcomes:

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

1. Create a simulation suite for the Small Modular Advanced
   High Temperature Reactor (SmAHTR) to simulate component
degradation such as heat exchanger fouling or chemistry
changes following maintenance.

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

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

### Impact:

Many reactor control systems already automate steady-state
operation and basic load-following, but their performance
degrades over time as plant equipment wears or is replaced.
Without retuning, controllers may become less efficient,
leading to suboptimal thermal efficiency, reduced grid
responsiveness, and unnecessary operational margins that can
lead to unnecessary shutdowns. Adaptive control can address
these challenges by continuously tuning control parameters
to match the evolving plant dynamics. However, without
provable safety guarantees, such adaptation is unlikely to
be accepted in high-assurance domains without proof of
controller safety. By embedding formal, contract-based
verification into the adaptation process, this work will
enable the use of responsive and efficient control
strategies that maintain regulatory compliance while
improving plant performance and availability.

### Related Papers: