update
This commit is contained in:
parent
5964dc8fbd
commit
5031f1c679
@ -1,132 +0,0 @@
|
||||
# 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
|
||||
|
||||
- [X] Review and edit 3
|
||||
- [X] Write an impact section
|
||||
|
||||
- [X] Review and edit 4
|
||||
- [X] Needs more goal
|
||||
|
||||
- [X] Review and edit 5
|
||||
|
||||
- [X] Review and edit 6
|
||||
|
||||
## Discussion Cheat Sheet
|
||||
|
||||
Chat helped with this
|
||||
|
||||
### Temporal Logic Specifications for Autonomous Controller
|
||||
Synthesis
|
||||
- **Feasibility:** ★★★★★
|
||||
- **Impact:** ★★★★☆
|
||||
- **Merit:** ★★★★★
|
||||
|
||||
**Scope Boundaries:** Focus on one subsystem (e.g., rod
|
||||
supervisory control), one specification language, and
|
||||
existing synthesis tools (TLA+, FRET, Strix).
|
||||
|
||||
**Key Risk:** State space explosion during synthesis could
|
||||
make controller generation intractable.
|
||||
|
||||
**Mitigation Strategy:** Use bounded abstractions,
|
||||
compositional synthesis, and validate the synthesized
|
||||
controller on a high-fidelity simulation before scaling up.
|
||||
|
||||
---
|
||||
|
||||
### Formally Verified Runtime Monitoring and Fallback
|
||||
- **Feasibility:** ★★★★★
|
||||
- **Impact:** ★★★★☆
|
||||
- **Merit:** ★★★★☆
|
||||
|
||||
**Scope Boundaries:** Single primary controller with one
|
||||
fallback controller, one LTL specification set, and
|
||||
integration with ARCADE.
|
||||
|
||||
**Key Risk:** Limited novelty if scoped too narrowly or
|
||||
perceived as a straightforward engineering integration.
|
||||
|
||||
**Mitigation Strategy:** Emphasize automation of
|
||||
specification-to-monitor translation, nuclear-specific
|
||||
verification, and proof artifact generation to show novelty.
|
||||
|
||||
---
|
||||
|
||||
### Verified Adaptive Control
|
||||
- **Feasibility:** ★★★★☆
|
||||
- **Impact:** ★★★★☆
|
||||
- **Merit:** ★★★★☆
|
||||
|
||||
**Scope Boundaries:** One subsystem (rod control), one
|
||||
adaptation method, runtime contract monitoring only.
|
||||
|
||||
**Key Risk:** Over-scoping to multiple adaptation targets
|
||||
or attempting plant-wide adaptive control.
|
||||
|
||||
**Mitigation Strategy:** Pick representative degradation
|
||||
types (e.g., HX fouling, pump efficiency drop); limit
|
||||
adaptation to parameter tuning inside pre-verified safe
|
||||
envelopes.
|
||||
|
||||
---
|
||||
|
||||
### Integrating Shielding into Nuclear Power Control
|
||||
- **Feasibility:** ★★★★☆
|
||||
- **Impact:** ★★★★☆
|
||||
- **Merit:** ★★★★☆
|
||||
|
||||
**Scope Boundaries:** One ML control task (e.g., startup or
|
||||
load-following), one shield synthesis approach from temporal
|
||||
logic.
|
||||
|
||||
**Key Risk:** Regulatory and industry reluctance toward ML
|
||||
in safety-critical nuclear applications.
|
||||
|
||||
**Mitigation Strategy:** Demonstrate shielding benefits for
|
||||
both ML and conventional controllers to broaden acceptance.
|
||||
|
||||
---
|
||||
|
||||
### Improved: Data-Driven Fault Detection Using
|
||||
High-Assurance Digital Twins
|
||||
- **Feasibility:** ★★★★☆
|
||||
- **Impact:** ★★★★☆
|
||||
- **Merit:** ★★★★☆
|
||||
|
||||
**Scope Boundaries:** Limit to 3–4 high-impact fault types
|
||||
(e.g., secondary coolant loss, HX fouling, sensor drift),
|
||||
residual-based detection with physics-informed models.
|
||||
|
||||
**Key Risk:** Scope creep into too many fault scenarios or
|
||||
overly complex ML methods.
|
||||
|
||||
**Mitigation Strategy:** Focus on explainable,
|
||||
physics-informed detection; tie mitigation responses
|
||||
directly to NRC-aligned safety procedures.
|
||||
|
||||
---
|
||||
|
||||
### Formally Verified Neural Network Control of Control Rod
|
||||
System
|
||||
- **Feasibility:** ★★★☆☆
|
||||
- **Impact:** ★★★★☆
|
||||
- **Merit:** ★★★☆☆
|
||||
|
||||
**Scope Boundaries:** Small, well-structured NN
|
||||
architecture; bounded state space; one primary safety
|
||||
property (shutdown margin).
|
||||
|
||||
**Key Risk:** Scalability issues in SMT/MILP verification
|
||||
for larger or more complex networks.
|
||||
|
||||
**Mitigation Strategy:** Constrain network size and
|
||||
complexity; limit verification domain to tractable operating
|
||||
regions; focus on proof-of-concept that shows
|
||||
nuclear-specific applicability.
|
||||
@ -5,6 +5,74 @@
|
||||
|
||||
## Work
|
||||
|
||||
Yesterday Dan and I had our meeting about
|
||||
[[thesis-ideas-2025-07-30 | topic ideas]]. The results were
|
||||
as follows:
|
||||
|
||||
5. Integrating Shielding in Nuclear Power
|
||||
3. Formally Verified NN CTRL of CRS
|
||||
1. Temporal Logic Specifications for Autonomous Control
|
||||
Synthesis.
|
||||
1. Formally Verified Runtime Monitoring and Fallback
|
||||
6. High Assurance Fault Detection with Digital Twins
|
||||
4. Verified Adaptive Control.
|
||||
|
||||
The final topic result?
|
||||
|
||||
*Hybrid Controller Synthesis from Temporal Logic
|
||||
Specifications*
|
||||
|
||||
The research will be basically a mix of the third and fourth
|
||||
idea. More work to come on this one.
|
||||
|
||||
I also got roped into making a presentation about Strix for
|
||||
next week's meeting. So I must learn about that!
|
||||
|
||||
## Reading
|
||||
|
||||
Yesterday I read more of *The Power of Habit* and I learned
|
||||
about the **craving**. A craving is what actually makes the
|
||||
habit loop work. It was explained to me that the brain
|
||||
releases a spike in activity at first when it recognizes the
|
||||
reward. Once the cue and routine are associated with the
|
||||
reward, the brain over time will deliver the activity spike
|
||||
as an anticipation of the reward *earlier and earlier*. The
|
||||
result is that the brain gets the activity spike as soon as
|
||||
it sees the cue, anticipates the reward, and is thus
|
||||
motivated to do the routine. The craving is what makes
|
||||
habits easy.
|
||||
|
||||
|
||||
## Personal
|
||||
|
||||
Finally my personal info. I feel pretty good today. I didn't
|
||||
get a lot done this morning but I'm steady cooking now that
|
||||
I'm working in a Starbucks on campus. I've been
|
||||
peoplewatching as people slowly move in for the fall
|
||||
semester. It's fun to see all the different kinds of people
|
||||
walking around and to see the connection between kids and
|
||||
parents. The kids definitely look more nervous on average
|
||||
than the parents. And I get it, the parents know what to
|
||||
expect, but for the kids, this is the transition to the deep
|
||||
end. They'll be fine.
|
||||
|
||||
On the lady front, here's today's update:
|
||||
|
||||
**Miranda:**
|
||||
Honestly I'm getting a little bored. I think it might just
|
||||
be a texting issue, or perhaps the infatuation wearing off.
|
||||
That's okay though, she's really busy this week som maybe
|
||||
that has something to do with it.
|
||||
|
||||
**Abby:**
|
||||
No update!
|
||||
|
||||
**Katarina:**
|
||||
Also no update, but I'm excited for our date tonight. We'll
|
||||
see how it goes.
|
||||
|
||||
I made some updates to my hinge profile to make things sound
|
||||
more serious and better indicate what I want / who I am.
|
||||
Maybe this'll stand out more. Honestly, I tried to write the
|
||||
profile like one I'd be looking for.
|
||||
|
||||
|
||||
@ -1,39 +0,0 @@
|
||||
# A random thesis idea I had
|
||||
|
||||
This is kind of connected to the high assurance digital twin
|
||||
idea, but I am currently in the middle of reading and needed
|
||||
to get this out of my head.
|
||||
|
||||
Here's the situation:
|
||||
|
||||
Manyu's work made a lot of progress to apply contract based
|
||||
formal methods to nuclear power. To do this, an assumption
|
||||
of a certain components output is fed into the input of the
|
||||
next component. Math is done, and then the output of that
|
||||
component becomes a guarantee, which is then the assumption
|
||||
for the next component in line after that.
|
||||
|
||||
But here's a question: how do you know that your assumptions
|
||||
and guarantee's are valid on a real system, in real time?
|
||||
These contracts are based on having a model of the system
|
||||
with which you can evaluate the assumptions/guarantee pairs.
|
||||
But, real systems never will line up perfectly with a model,
|
||||
and over time or different conditions, will absolutely have
|
||||
different physical behaviors. Knowing if the contracts still
|
||||
hold for the real system is a significant problem.
|
||||
|
||||
Here's where some online modeling in simulation can come in.
|
||||
Perhaps, we can use a digital twin to estimate what the
|
||||
critical model parameters for the contract methods are in
|
||||
the real system. This is probably most easily accomplished
|
||||
with either a physics informed neural network (PINN) or some
|
||||
sort of particle filter bayesian nonsense. Once those
|
||||
parameters are identified, we can reevaluate the contracts
|
||||
to know a) if our system is safe, b) what our new
|
||||
assumptions and safe operating range are, and c) make
|
||||
strategic decisions about the plant control if necessary.
|
||||
|
||||
This relates to the [autonomous framework paper](/Zettelkasten/Literature%20Notes/albertiAutomationLevelsNuclear2023.md)
|
||||
that talks about getting to higher levels of automation.
|
||||
Level 3 is exactly this, the automated reactor operation
|
||||
system being able to detect and diagnose what an error is.
|
||||
@ -1,4 +0,0 @@
|
||||
# Therapy Log for CW31 and CW32
|
||||
|
||||
- So my crush is not gay (yay!), she has a boyfriend
|
||||
(despair!)
|
||||
Some files were not shown because too many files have changed in this diff Show More
Loading…
x
Reference in New Issue
Block a user