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.

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

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

5. 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: