diff --git a/Writing/.DS_Store b/Writing/.DS_Store index 9eb85263d..cda00f80f 100644 Binary files a/Writing/.DS_Store and b/Writing/.DS_Store differ diff --git a/Writing/THESIS_PROPOSAL/.DS_Store b/Writing/THESIS_PROPOSAL/.DS_Store index 4967315f9..5611d094d 100644 Binary files a/Writing/THESIS_PROPOSAL/.DS_Store and b/Writing/THESIS_PROPOSAL/.DS_Store differ diff --git a/Writing/THESIS_PROPOSAL/3-research-approach/Untitled.canvas b/Writing/THESIS_PROPOSAL/3-research-approach/Untitled.canvas new file mode 100644 index 000000000..bc24fdb6d --- /dev/null +++ b/Writing/THESIS_PROPOSAL/3-research-approach/Untitled.canvas @@ -0,0 +1,12 @@ +{ + "nodes":[ + {"id":"a54ef0f53d23c989","x":-500,"y":-380,"width":360,"height":80,"type":"text","text":"WHAT BELONGS IN THE RESEARCH APPROACH?"}, + {"id":"3d90877135704e66","x":-720,"y":-200,"width":250,"height":60,"type":"text","text":"translation of procedures"}, + {"id":"7e9f07efeeac7725","x":-625,"y":-100,"width":250,"height":60,"type":"text","text":"Temporal logic"}, + {"id":"7e9c528ccdb4a1d3","x":-220,"y":-40,"width":250,"height":60,"type":"text","text":"Guard conditions between switching"}, + {"id":"47816cf87b1f4d37","x":-65,"y":-230,"width":250,"height":60,"type":"text","text":"Reactive Synthesis"}, + {"id":"aed191c3719f280b","x":-300,"y":-140,"width":250,"height":60,"type":"text","text":"Discrete automata"}, + {"id":"1f085c02451b41bf","x":80,"y":-110,"width":250,"height":60,"type":"text","text":"Continuous systems as transitions"} + ], + "edges":[] +} \ No newline at end of file diff --git a/Writing/THESIS_PROPOSAL/ERLM-Proposal-Review-Detailed.md b/Writing/THESIS_PROPOSAL/ERLM-Proposal-Review-Detailed.md deleted file mode 100644 index 2158fb0e0..000000000 --- a/Writing/THESIS_PROPOSAL/ERLM-Proposal-Review-Detailed.md +++ /dev/null @@ -1,1690 +0,0 @@ -# ERLM Proposal Writing Review - Comprehensive Detail - -**Date**: December 2, 2025 **Framework**: Gopen's Sense of -Structure - ---- - -## How to Use This Document - -- **Each issue has a checkbox** `- [ ]` for tracking your -revision progress -- **Issues organized by section** and then by level -(sentence, paragraph, content) -- **Cross-references to Summary doc** for patterns and -principles -- **Work section-by-section** - complete one section before -moving to next -- **Check off items as you revise** - provides visual -progress tracking - -For pattern explanations and principles, see the **Executive -Summary** document. - ---- - -## 1. Goals and Outcomes Section - -### 1.1 Sentence-Level Issues - -- [ ] **Lines 4-6** - Weak stress position - - Current: "The goal of this research is to develop a - methodology for creating autonomous hybrid control systems - with mathematical guarantees of safe and correct - behavior." - - Issue: Sentence ends with "correct behavior" (weak, - expected). Key innovation is "methodology for creating" - with "mathematical guarantees" - - See Summary: Pattern 1 (Stress Position Weakness) - - Suggested fix: "The goal of this research is to develop - autonomous hybrid control systems that guarantee - mathematically safe and correct behavior." - -- [ ] **Lines 9-11** - Weak stress position + passive -construction - - Current: "Nuclear power plants require the highest - levels of control system reliability, where failures can - result in significant economic losses, service - interruptions, or radiological release." - - Issue: List ends with weakest item first (economic - losses < radiological release). Also "can result in" is - weak - - Fix: "Nuclear power plants require the highest levels of - control system reliability: failures risk radiological - release, service interruptions, or significant economic - losses." - -- [ ] **Lines 13-17** - Buried key claim - - Current: "Currently, nuclear plant operations rely on - extensively trained human operators who follow detailed - written procedures and strict regulatory requirements to - manage reactor control." - - Issue: Key points (extensively trained, detailed - procedures, strict requirements) buried in middle. Ends - weakly with "manage reactor control" - - Fix: "Currently, nuclear plant operations require - extensively trained human operators following detailed - written procedures under strict regulatory requirements." - -- [ ] **Lines 16-17** - Topic position break - - Current: "These operators make critical decisions about - when to switch between different control modes..." - - Issue: "These operators" okay, but could be tighter as - "They" since immediately follows previous sentence about - operators - - Fix: "They make critical decisions..." - -- [ ] **Lines 19-20** - Passive "prevents the introduction -of" - - Current: "However, this reliance on human operators - prevents the introduction of autonomous control - capabilities..." - - Issue: Nominalization "introduction" + passive "prevents - introduction" - - Fix: "However, this reliance on human operators prevents - introducing autonomous control capabilities..." or - "...makes autonomous control impossible" - -- [ ] **Lines 22-23** - Topic position break - - Current (new paragraph): "Emerging technologies like - small modular reactors face significantly higher..." - - Issue: Abrupt shift from "reliance on operators" to - "emerging technologies" - - Fix: "This limitation creates particular challenges for - emerging technologies like small modular reactors, which - face..." - -- [ ] **Lines 25-27** - Weak stress position + -nominalization - - Current: "What is needed is a way to create autonomous - control systems that can safely manage complex operational - sequences..." - - Issue: Ends with "constant human supervision" (the - problem, not the solution). Also "what is needed" is - passive framing - - Fix: "Autonomous control systems must safely manage - complex operational sequences with the same assurance as - human-operated systems, but without constant human - supervision." - -- [ ] **Lines 30-31** - Weak stress position - - Current: "To address this need, we will combine formal - methods from computer science with control theory to build - hybrid control systems that are correct by construction." - - Issue: Ends with "correct by construction" which is - good, but could emphasize the combination more - - Fix: "To address this need, we will build hybrid control - systems that are correct by construction by combining - formal methods from computer science with control theory." - -- [ ] **Lines 33-37** - Long complex sentence (45 words) - - Current: "Hybrid systems use discrete logic to switch - between continuous control modes, similar to how operators - change control strategies, and existing formal methods can - generate provably correct switching logic from written - requirements, but they cannot handle the continuous - dynamics that occur during transitions between modes." - - Issue: Two "and" clauses plus a "but" clause—very - complex - - Fix (split): "Hybrid systems use discrete logic to - switch between continuous control modes, similar to how - operators change control strategies. Existing formal - methods can generate provably correct switching logic from - written requirements. However, they cannot handle the - continuous dynamics that occur during transitions between - modes." - -- [ ] **Lines 37-39** - Another long complex sentence - - Current: "Meanwhile, traditional control theory can - verify continuous behavior but lacks tools for proving - correctness of discrete switching decisions." - - Issue: This is actually fine as-is, but note the - parallel "X can do A but lacks B" structure matches - previous sentence well - -- [ ] **Lines 40-45** - Very long complex sentence (60+ -words) - - Current: "By synthesizing discrete mode transitions - directly from written operating procedures and verifying - continuous behavior between transitions, we can create - hybrid control systems with end-to-end correctness - guarantees. If we can formalize existing procedures into - logical specifications and verify that continuous dynamics - satisfy transition requirements, then we can build - autonomous controllers that are provably free from design - defects." - - Issue: Two long sentences that are somewhat repetitive - - Fix: Consider combining or cutting redundancy. The first - sentence is strong; the second restates it with - "if...then" structure that's less confident - - Suggested: Keep first sentence, delete second, or - shorten second to: "This approach yields autonomous - controllers provably free from design defects." - -- [ ] **Lines 47-48** - Weak stress position - - Current: "This approach will enable autonomous control - in nuclear power plants while maintaining the high safety - standards required by the industry." - - Issue: Ends with "required by the industry"—old - information - - Fix: "This approach will maintain the high safety - standards nuclear power plants require while enabling - autonomous control." - -- [ ] **Lines 50-53** - Long sentence with embedded clause - - Current: "This work is conducted within the University - of Pittsburgh Cyber Energy Center, which provides access - to industry collaboration and Emerson control hardware, - ensuring that solutions developed are aligned with - practical implementation requirements." - - Issue: "Ensuring that" is weak; also passive "solutions - developed" - - Fix: "This work is conducted within the University of - Pittsburgh Cyber Energy Center, which provides industry - collaboration and access to Emerson control hardware. This - ensures our solutions align with practical implementation - requirements." - -### 1.2 Paragraph-Level Issues - -- [ ] **Lines 3-6 (Goal paragraph)** - Could be stronger - - Current: Single sentence stating the goal - - Issue: While clear, could benefit from a second sentence - stating why this goal matters (the issue) - - Fix: Add after line 6: "Such guarantees are essential - for safety-critical systems where verification through - testing alone cannot provide adequate assurance." - -- [ ] **Lines 29-53 (Approach paragraph)** - Too dense, -covers multiple sub-topics - - Current: One large paragraph covering: (1) solution - approach, (2) rationale about hybrid systems, (3) existing - limitations, (4) hypothesis, (5) payoff, (6) - qualifications - - Issue: This is really 2-3 paragraphs worth of content - - Fix: Break into two paragraphs: - - Para 1 (lines 30-38): Solution and rationale - - Para 2 (lines 40-48): Hypothesis and payoff - - Keep qualifications (lines 50-53) with payoff or as - separate brief paragraph - -- [ ] **Outcome paragraphs (58-101)** - Generally strong -structure - - Each outcome has: Title → Strategy → Outcome structure, - which is excellent - - Minor issue: The strategy/outcome distinction could be - sharper. Currently reads as "We will do X. Engineers will - be able to Y." Consider: "We will do X, enabling engineers - to Y." - - Fix for each: - - Lines 63-72: Combine last two sentences: - "...synthesized into discrete control logic, enabling - control system engineers to generate verified - mode-switching controllers..." - - Lines 77-85: Similar combination possible - - Lines 91-99: Similar combination possible - -### 1.3 Content and Organization Issues - -- [ ] **Overall structure** - Excellent - - The four-paragraph opening (goal → problem → approach → - outcomes) is very strong - - The enumerated outcomes are clear and specific - - Impact paragraph provides good closure - - No major reorganization needed - -- [ ] **Technical detail level** - Appropriate - - Good balance of specificity (SmAHTR, Emerson hardware) - without overwhelming detail - - Outcomes are concrete and measurable - -- [ ] **Missing elements** - None critical - - All standard goal section elements present - - Qualifications established - - Scope clearly defined - ---- - -## 2. State of the Art Section - -### 2.1 Sentence-Level Issues - -- [ ] **Lines 3-9** - Long opening sentence (46 words) - - Current: "The principal aim of this research is to - create autonomous reactor control systems that are - tractably safe. But, to understand what exactly is being - automated, it is important to understand how nuclear - reactors are operated today." - - Issue: Two sentences could be more tightly connected - - Fix: "The principal aim of this research is to create - autonomous reactor control systems that are tractably - safe. Understanding what we automate requires first - understanding current reactor operation." - -- [ ] **Lines 6-9** - Roadmap sentence is good but could be -punchier - - Current: "First, the reactor operator themselves is - discussed. Then, operating procedures that we aim to - leverage later are examined. Next, limitations of - human-based operation are investigated, while finally we - discuss current formal methods based approaches..." - - Issue: Passive constructions throughout ("is discussed", - "are examined", "are investigated") - - Fix: "We first discuss the reactor operator, then - examine the operating procedures we will leverage, next - investigate human operation limitations, and finally - review current formal methods approaches to reactor - control." - -- [ ] **Lines 13-19** - Good opening, solid statistics - - Current paragraph opener establishes scale and scope - well - - No major issues - -- [ ] **Lines 21-34** - Very long paragraph with complex -structure - - Current: "The role of human operators is - paradoxically..." through "...fulfill this responsibility - under all conditions" - - Issue: This paragraph tries to do too much: (1) paradox - of operator role, (2) TMI example, (3) commission finding - - Fix: Consider breaking after line 24 (TMI example) into - new paragraph - -- [ ] **Lines 24-26** - Long embedded quote - - Current: "operators \"misread confusing and - contradictory readings and shut off the emergency water - system\"" - - Issue: Long quote breaks sentence flow - - Fix: Paraphrase or shorten: "operators misread - contradictory readings and shut off the emergency water - system" - -- [ ] **Lines 44-51** - Extremely long sentence (58 words) - - Current: "These procedures must comply with 10 CFR - 50.34(b)(6)(ii) and are developed using guidance from - NUREG-0899, but their development process relies - fundamentally on expert judgment and simulator validation - rather than formal verification. Procedures undergo - technical evaluation, simulator validation testing, and - biennial review as part of operator requalification under - 10 CFR 55.59, but despite these rigorous development - processes..." - - Issue: Actually two long sentences with parallel "X but - Y" structure, both 50+ words - - Fix: Break into shorter sentences: "These procedures - must comply with 10 CFR 50.34(b)(6)(ii) and are developed - using guidance from NUREG-0899. However, their development - process relies on expert judgment and simulator validation - rather than formal verification. Procedures undergo - technical evaluation, simulator validation testing, and - biennial review under 10 CFR 55.59. Despite these rigorous - processes..." - -- [ ] **Lines 48-51** - Weak stress position - - Current: "...or that transitions between procedure sets - maintain safety invariants." - - Issue: Ends with weakest of three items - - Fix: Reorder list to build to most important: "...that - transitions maintain safety invariants, that actions can - be completed within available timeframes, or that - procedures cover all possible plant states." - -- [ ] **Lines 53-60 (LIMITATION callout)** - Generally -strong - - The bold "LIMITATION:" callouts are excellent framing - devices - - Minor: Some repetition between paragraph text and - limitation summary - - Consider whether limitation box needs all the detail or - can be more concise - -- [ ] **Lines 74-79** - Topic string break - - Current: "The current division between automated and - human-controlled functions reveals the fundamental - challenge..." - - Previous paragraph ended discussing automatic vs. manual - control modes - - This starts with "current division" which is good - topic-position continuity - - Minor issue: "%%%NEED MORE" comment at line 79 indicates - incomplete thought - -- [ ] **Lines 81-85 (LIMITATION callout)** - Weak stress -position in callout - - Current: "...or optimize the automation-human - interaction trade-off with provable safety bounds." - - Issue: Ends with least important item (optimization < - verification < mathematical guarantees) - - Fix: "...verify timing properties formally, or provide - mathematical guarantees across mode transitions." - -- [ ] **Lines 94-97** - Statistics presentation - - Current: "Multiple independent analyses converge on a - striking statistic: \\textbf{70--80\\% of all nuclear - power plant events..." - - Issue: Good use of bold for key statistics. Consider - whether all statistics need similar treatment for - consistency - - Note: Lines 100, 119, 125-126 have more - statistics—ensure consistent emphasis treatment - -- [ ] **Lines 97-99** - Very strong claim, good stress -position - - Current: "...the International Atomic Energy Agency - concluded that \"human error was the root cause of all - severe accidents at nuclear power plants\"---a categorical - statement..." - - This is excellent—emphatic claim in stress position with - proper emphasis - -- [ ] **Lines 108-121 (TMI paragraph)** - Generally strong -narrative - - Good use of specific timeline and technical detail - - Line 119: "\\textbf{44\\% of the fuel melting}" - good - emphasis - - Line 118: "core quickly began to overheat" - could be - more specific: "core began overheating within minutes" or - similar - -- [ ] **Lines 122-143** - Technical paragraph with many -statistics - - Dense paragraph with HRA methods, HEPs, performance - shaping factors - - Line 128: "%%%SOURCE???" indicates missing citation - - Lines 131-132: Bold statistics are effective - - Lines 136-142: Many bolded numbers—ensure not overusing - bold - - Overall structure is good but very dense - -- [ ] **Lines 145-153** - Rasmussen taxonomy paragraph - - Good integration of cognitive psychology - - Line 151: "%%%WHAT IS A CHUNK?" indicates need for brief - explanation - - Consider adding: "(a 'chunk' is a unit of information - that can be held as a single entity in working memory)" - -- [ ] **Lines 154-163 (LIMITATION callout)** - Very strong - - This limitation statement is one of the best—specific, - well-supported, emphatic - - No changes needed - -### 2.2 Paragraph-Level Issues - -- [ ] **Lines 13-34 (Operator role paragraph)** - Break into -two paragraphs - - Current: One long paragraph covering operator - qualifications AND paradoxical role with TMI example - - Issue: Two distinct points being made - - Fix: Break after line 19 (end of qualification/staffing - discussion) before starting paradox discussion (line 21) - -- [ ] **Lines 36-61 (Procedures paragraph)** - Very long, -multiple sub-topics - - Current: Covers (1) procedure hierarchy, (2) development - process, (3) lack of verification - - Issue: 26 lines is too long for reader attention span - - Fix: Break into two paragraphs: - - Para 1: Procedure hierarchy and development (lines - 36-46) - - Para 2: Lack of formal verification (lines 47-51, then - LIMITATION box) - -- [ ] **Lines 88-107 (Human factors intro paragraph)** - -Dense but well-structured - - Opens with strong point-issue structure - - Provides multiple converging lines of evidence - - Could potentially break after line 102 (end of - statistics) before starting specific analysis (line 103), - but current structure works - -- [ ] **Lines 108-121 (TMI narrative)** - Excellent -storytelling - - Clear chronological structure - - Specific technical details - - Builds to climax (44% fuel melting) - - No changes needed - -- [ ] **Lines 122-143 (HRA methods paragraph)** - Very dense - - Topic: HRA methods and quantitative error rates - - Issue: Many numbers and concepts in rapid succession - - Consider: Could break after line 133 (end of nominal - rates) before starting performance shaping factors (line - 135) - -### 2.3 Content and Organization Issues - -- [ ] **Section length** - 358 lines, longest in proposal - - Issue: Risk of reader fatigue/losing track of argument - - Recommendation: Consider whether all detail is - necessary, or if some could move to appendix - - Specifically: HARDENS subsection (lines 165-295) is 131 - lines—nearly as long as entire Research Approach section - -- [ ] **HARDENS subsection structure** - Well-organized but -very detailed - - Four sub-subsections: Feasibility Demonstrated (23 - lines), Methods Toolkit (42 lines), Discrete Limitation - (33 lines), Validation Gap (33 lines) - - Issue: While all interesting, does the proposal need - this much detail on HARDENS? - - Recommendation: Consider condensing or restructuring to - focus more on the gap you're filling rather than - recounting HARDENS accomplishments - - Current structure spends 65 lines on what HARDENS did - well, 66 lines on limitations. Could reverse this - proportion. - -- [ ] **"Research Imperative" subsection (296-358)** - -Excellent synthesis but placement - - Content: Strong synthesis of three converging lines of - evidence - - Issue: This feels like it belongs at the START of - Research Approach section rather than end of SOTA - - Current: SOTA → lists problems → Research Imperative → - Research Approach → here's what we'll do - - Alternative: SOTA → lists problems → Research Approach - starts with Imperative → here's what we'll do - - Consider: Moving lines 296-358 to open Research Approach - section - -- [ ] **LIMITATION callouts** - Excellent framing device - - Used consistently throughout: lines 53-60, 81-85, - 154-163, 254-263, 287-294 - - These are very effective at signaling gaps - - Minor: Ensure consistent formatting (all bold, all - italic "LIMITATION:") - -- [ ] **Transition from Current Practice to HARDENS** - -Could be smoother - - Line 165 starts "The High Assurance Rigorous Digital - Engineering..." abruptly - - Consider adding transition sentence: "Recent work - demonstrates that formal methods can address some of these - challenges. The High Assurance..." - -### 2.4 State of the Art Section - Additional Issues - -- [ ] **Lines 165-173 (HARDENS intro)** - Opening could be -tighter - - Current: Two sentences introducing HARDENS, second - describes it as "most advanced application...and - simultaneously reveals the critical gaps" - - Issue: "Simultaneously reveals gaps" is your framing, - not inherent to HARDENS - - Fix: "...represents the most advanced application of - formal methods to nuclear control systems to date. As we - will show, it also illuminates the critical gaps that - remain." - -- [ ] **Lines 175-181 (HARDENS motivation)** - Good context - - Explains the problem HARDENS addressed - - No major issues - -- [ ] **Lines 182-190** - Statistics on accomplishment - - Line 185-186: "\\textbf{nine months at a tiny fraction - of typical control system costs}" - good emphasis - - Consider: "at a tiny fraction" is vague. If you have - even rough numbers, use them: "at less than 10% of typical - costs" or similar - -- [ ] **Lines 192-198 (Kiniry and methodology)** - Dense -paragraph - - Introduces PI, methodology, digital twins, fidelity - - Many concepts in quick succession - - Consider: This could be two paragraphs—one on - Kiniry/team, one on methodology - -- [ ] **Lines 200-231 (Comprehensive toolkit subsection)** - -Very detailed - - Lists many tools: Lando, SysMLv2, FRET, SAT, SMT, - Cryptol, SAW, Frama-C, Yosys - - Issue: Readers may get lost in the tool list and miss - the key point - - Consider: Leading with the key point, then briefly - listing tools as support - - Current: "HARDENS employed impressive array..." → lists - tools - - Alternative: "HARDENS demonstrated complete verification - from requirements to implementation [key point], using an - impressive array of tools including..." - -- [ ] **Lines 207-210** - Bolded text for emphasis - - "\\textbf{consistency, completeness, and realizability}" - - good - - "\\textbf{complete formal verification from requirements - to implementation is technically feasible}" - excellent - key claim, right emphasis - -- [ ] **Lines 232-263 (Critical Limitation subsection)** - -Very strong - - Clear statement of limitation (discrete only, no - continuous) - - Specific enumeration of what was/wasn't covered - - Strong LIMITATION callout - - This is excellent and no changes needed - -- [ ] **Lines 265-294 (Validation Gap subsection)** - Clear -and specific - - Explains TRL limitation - - Lists what wasn't done - - Good LIMITATION callout - - Minor: Some repetition between paragraph text and - LIMITATION box - -### 2.5 State of the Art Section - Sentence-Level Continued - -- [ ] **Line 296-311 (Research Imperative opening)** - -Strong synthesis - - "Three converging lines of evidence" is excellent - framing - - Three paragraphs parallel each other well - - Consider: These three paragraphs are quite dense—each - could potentially be broken into smaller units - -- [ ] **Lines 302-309** - Weak stress position - - Current: "Despite extensive regulatory frameworks - developed over six decades, \\textbf{no mathematical - guarantees exist} that current control approaches maintain - safety under all possible scenarios." - - Issue: Actually good—ends with the key claim (no - mathematical guarantees) - - The bold emphasis helps, but could still be stronger: - "...six decades of extensive regulatory frameworks. Yet - \\textbf{no mathematical guarantees exist}..." - -- [ ] **Lines 312-322** - Another dense summary paragraph - - Synthesizes human factors argument - - Many numbers cited: 70-80%, 7±2, 0.001-0.01, 0.1-1.0 - - Strong final sentence: "These limitations - \\textbf{cannot be overcome through human factors - improvements alone}." - -- [ ] **Lines 324-335** - HARDENS summary paragraph - - Recaps accomplishments and gaps - - Final sentence is key: "These limitations directly - define the research frontier: \\textbf{formal synthesis of - hybrid controllers that provide mathematical safety - guarantees...}" - - Very strong, good emphasis - -- [ ] **Lines 336-358 (Final "opportunity" paragraph)** - -Long but powerful - - 23 lines synthesizing the argument - - Strong technical detail - - Ends well: "compelling and timely research opportunity" - - Consider: Could break after line 346 (end of problem - statement) before starting solution (line 347 "Hybrid - control synthesis offers...") - ---- - -## 3. Research Approach Section - -### 3.1 Sentence-Level Issues - -- [ ] **Lines 3-6** - Weak stress position in opening -sentence - - Current: "This research will overcome the limitations of - current practice to build high-assurance hybrid control - systems for critical infrastructure." - - Issue: Ends with "critical infrastructure"—generic and - expected - - Fix: "This research will build high-assurance hybrid - control systems by overcoming current practice - limitations." - -- [ ] **Lines 6-14** - Equations introduced clearly - - Good contextualization of equations (hybrid = continuous - + discrete) - - Minor: Lines 16-17 have $f(\cdot)$ and $\nu(\cdot)$ - explanations that could reference equation numbers - -- [ ] **Lines 19-20** - Topic position could be smoother - - Current: "Our focus centers on continuous autonomous - hybrid systems..." - - Previous sentence discusses "control input $u$" - - Could connect better: "Within this hybrid framework, we - focus on continuous autonomous systems..." - -- [ ] **Line 23** - Example is good but could be emphasized - - Current: "For example, a nuclear reactor switching from - warm-up to load-following control cannot instantaneously - change its temperature or control rod position, but can - instantaneously change control laws." - - Issue: Key insight (continuous states unchanged, - discrete transitions instant) could be more prominent - - Fix: "Physical systems exhibit this property naturally: - a nuclear reactor switching from warm-up to load-following - control changes control laws instantly, but its - temperature and control rod position evolve continuously." - -- [ ] **Lines 26-28** - Good framing of three thrusts - - Clear enumeration - - No major issues - -- [ ] **Lines 30-38** - Enumeration formatting - - Using \\begin{enumerate} is good - - Items are parallel in structure - - Consider: Items 1-2 are short (one line), item 3 is - longer (two lines). Could make more parallel by expanding - 1-2 slightly - -- [ ] **Lines 40-41** - Weak metadiscourse - - Current: "The following sections discuss how these - thrusts will be accomplished." - - Issue: Pure metadiscourse, provides no information - - Fix: Delete entirely, or combine with previous: "...we - must accomplish three main thrusts, each detailed below:" - -### 3.2 Research Approach - Subsection 1 (Procedures → -Temporal Logic) - -- [ ] **Lines 42** - Subsection title uses math notation - - Current: "$(Procedures \wedge FRET) \rightarrow Temporal - Specifications$" - - Issue: Clever but potentially unclear. Not all readers - will parse this as "Procedures AND FRET implies Temporal - Specs" - - Consider: Adding plain-English subtitle: "Translating - Procedures into Temporal Logic" - -- [ ] **Lines 44-49** - Opening paragraph point could be -sharper - - Current: "The motivation behind this work stems from the - fact that commercial nuclear power operations remain - manually controlled..." - - Issue: "The motivation behind this work" is weak - opening. More direct: "Commercial nuclear power operations - remain manually controlled despite advances in control - systems. However, operators follow highly prescriptive, - well-documented procedures—suggesting that autonomous - control is technically feasible." - -- [ ] **Lines 51-55** - Good clear claim - - "Written procedures and requirements...are sufficiently - detailed that we may be able to translate them into - logical formulae with minimal effort." - - This is a strong claim and key assumption - - Consider: "Minimal effort" may overstate—later sections - describe significant work in FRET formalization - - Fix: "...that we can systematically translate them into - logical formulae." - -- [ ] **Lines 60-68** - SCRAM example is excellent - - Specific natural language requirement - - Translation to temporal logic with explanation - - Clear equation formatting - - Consider: This is a model for what examples should look - like - -- [ ] **Lines 70-75** - Explanation of operators - - Good: Explains what $G$, $X$, $U$ mean in context - - Helps readers unfamiliar with temporal logic - -- [ ] **Lines 76-81** - FRET introduction - - Clear motivation for why FRET - - Could be slightly tighter: "The most efficient path to - accomplish this translation is through NASA's Formal - Requirements Elicitation Tool (FRET)" - - Consider: "Most efficient" is a strong claim. Have you - compared alternatives? If not, soften: "NASA's FRET - provides a systematic path for this translation" - -- [ ] **Lines 83-93 (FRET six components)** - Clear -enumeration - - Parallel structure - - Good use of italics for questions - - Line 84: "%CITE FRET MANUAL" - needs citation - - Minor: Some items very short (line 90 just "Shall"), - others longer. Consider whether parallel structure could - be tighter - -- [ ] **Lines 95-110** - Realizability paragraph - - Opens with strong point: "FRET provides functionality to - check the *realizability*..." - - Explains what realizability means - - Makes clear argument for why this matters (finding bugs - early) - - Structure is good - -- [ ] **Lines 105-110** - Second category of realizability - - Discusses undefined behaviors - - Good point about autonomous controllers needing complete - specifications - - Line 107-108: "This ambiguity is undesirable for - high-assurance systems, since even well-trained humans - remain prone to errors" - good connection back to human - factors from SOTA - -- [ ] **Lines 112-115** - Closing/transition - - States that FRET exports to synthesis tools - - Good transition to next subsection - - Line 114-115: "progression to the next step of our - approach" - could be more specific about what that next - step is - -### 3.3 Research Approach - Subsection 2 (Temporal Logic → -Discrete Automata) - -- [ ] **Line 117** - Subsection title again uses math -notation - - Same issue as line 42 - - Consider adding plain-English subtitle - -- [ ] **Lines 119-122** - Opening defines reactive synthesis - - Good clear definition - - "Active research field" - consider whether you need to - say this. It's clear from the work that this is active - research. - -- [ ] **Lines 123-133** - Description of automata - - Explains finite states, transitions, etc. - - Good pedagogical approach - - Lines 131-132: "Hybrid systems naturally exhibit - discrete behavior amenable to formal analysis through - these finite state representations" - this is a key claim - and could be more prominent - -- [ ] **Lines 135-143** - Strix tool and implementation - - Good specific tool choice with justification (SYNTCOMP - performance) - - Lines 138-139: "maximizing generated automata quality" - - what does quality mean here? Minimal states? - Interpretability? Could be more specific - - Lines 140-143: Implementation discussion is good—notes - that automaton provides communication path to programmers - without formal methods expertise - -- [ ] **Lines 145-158** - Why discrete automata / -correctness argument - - This paragraph makes the key argument for - correct-by-construction - - Strong rhetorical structure: "because X, we can prove Y" - - Lines 150-154: Comparison with human operators is - effective - - Lines 155-158: "By synthesizing controllers from logical - specifications with guaranteed correctness, we eliminate - the possibility of switching errors" - very strong claim, - worth emphasizing - -- [ ] **Line 158** - Ends with strong claim - - "...we eliminate the possibility of switching errors." - - Excellent stress position—key contribution - - Consider: Adding emphasis (bold or italics) to this - claim - -### 3.4 Research Approach - Subsection 3 (Continuous Modes) - -- [ ] **Lines 160-161** - Subsection title - - Again uses math notation - - This one is longer: "$(DiscreteAutomata \wedge - ControlTheory \wedge Reachability) \rightarrow - ContinuousModes$" - - Consider plain-English subtitle - -- [ ] **Lines 163-168** - Opening paragraph - - Good point that discrete is only half - - Refers back to equation 1 (good callback) - - States section purpose clearly - -- [ ] **Lines 170-176** - Continuous modes after discrete - - Explains why discrete comes first - - "Physics-agnostic specifications" is good phrase - - Rationale is clear - -- [ ] **Lines 177-208** - Three-mode classification - - **This is a key contribution and should be highlighted - more prominently** - - Current: Presented as straightforward categorization - - Issue: This is novel! Stabilizing/Transitory/Expulsory - framework is your innovation - - Fix: Add sentence before enumeration: "We propose a - three-mode classification based on discrete transition - structure. This taxonomy enables systematic continuous - controller design tailored to each mode's objectives." - -- [ ] **Lines 183-189 (Stabilizing mode)** - Clear -definition - - Good explanation with example - - "Nodes with only incoming transitions" is clever—shows - how discrete structure determines continuous requirements - -- [ ] **Lines 191-197 (Transitory mode)** - Clear definition - - Good explanation - - Minor: "Secondary objectives" (line 195)—could clarify - with example - -- [ ] **Lines 199-207 (Expulsory mode)** - Clear definition - - Good emphasis on safety constraints - - SCRAM example is excellent - - This definition is slightly longer than the other - two—appropriate given importance - -- [ ] **Lines 209-221** - Why build continuous after -discrete - - Makes clear argument for the approach - - "Local controller design focused on satisfying discrete - transitions" - key insight - - Lines 213-214: "Current techniques struggle...because - dynamic discontinuities complicate verification" - good - problem statement - - Lines 214-221: Explains how your approach avoids this - problem - -- [ ] **Lines 220-221** - Introduces three techniques - - "To ensure continuous modes satisfy their requirements, - we will employ three main techniques..." - - Good signposting - - Note: "employ" again—consider "use" or restructure to - make techniques the subject - -- [ ] **Lines 223-232 (Reachability Analysis)** - Clear -explanation - - Defines technique - - States what it's used for - - Mentions recent advances (neural networks for - Hamilton-Jacobi) - - Well-structured - -- [ ] **Lines 234-240 (Assume-Guarantee Contracts)** - Clear -explanation - - Explains compositional approach - - Shows how contracts enable local analysis - - Minor: Line 234 says "will be employed"—passive. Fix: - "We will use assume-guarantee contracts..." or - "Assume-guarantee contracts enable..." - -- [ ] **Lines 242-249 (Barrier Certificates)** - Clear -explanation - - Explains what they prove - - Gives specific example - - Technical detail (differential inequality conditions) is - appropriate - - Well-structured - -- [ ] **Lines 250-273 (SmAHTR demonstration)** - Excellent -specificity - - This paragraph provides concrete detail: SmAHTR, - Simulink model, Emerson Ovation, ARCADE - - Multiple sentences are quite long (lines 252-260 is 60+ - words, lines 261-271 is 73 words) - - Consider breaking these into shorter sentences for - readability - -- [ ] **Lines 275-289 (Concluding paragraph)** - Strong -synthesis - - "Unified approach" language is good - - Connects back to gap from SOTA - - Final sentence (lines 285-289) is long (66 words) but - well-structured - - Ends strongly: "...domain where operating procedures are - well-documented and safety is paramount." - -- [ ] **Lines 290-296** - Comments for future revision - - These should be removed from final version - - But they're good notes: figures, validation approach, - examples - - Consider whether any should be addressed before - submission - -### 3.5 Research Approach - Paragraph-Level Issues - -- [ ] **Opening paragraph (lines 3-24)** - Could be split - - Current: Covers (1) overcoming limitations, (2) - equations, (3) focus on continuous autonomous systems, (4) - example - - Issue: Four distinct sub-topics in one paragraph - - Consider: Breaking after line 14 (after equations) or - after line 20 (after focus statement) - -- [ ] **Three-thrust framing (lines 26-38)** - Good -structure - - Clear signposting - - Enumeration is parallel - - Consider: The metadiscourse sentence (lines 40-41) could - be deleted or moved to introduction - -- [ ] **FRET component enumeration (lines 86-93)** - Could -be formatted better - - Currently as enumeration which is good - - But questions in italics could be formatted more - consistently - - Consider: Making all questions boldface or using a - different structure - -### 3.6 Research Approach - Content Issues - -- [ ] **Three-mode classification prominence** - -Underemphasized - - This appears to be a novel contribution - - Currently presented as straightforward categorization - - Should be highlighted as key methodological innovation - - Consider: Adding sentence like "This classification, to - our knowledge, has not been systematically applied to - hybrid control synthesis before." - -- [ ] **Tool choices** - Well justified - - FRET: choice is well-motivated - - Strix: justified by SYNTCOMP performance - - Reachability, barrier certificates: standard techniques - - No issues - -- [ ] **Level of technical detail** - Appropriate - - Enough detail to demonstrate feasibility - - Not so much that non-experts are lost - - Good balance - -- [ ] **Examples** - Excellent - - SCRAM requirement (line 60) - very specific - - Load-following controller (line 187) - clear - - Warm-up procedure (line 193) - clear - - SCRAM as expulsory mode (line 203) - powerful callback - ---- - -## 4. Metrics of Success Section - -### 4.1 Sentence-Level Issues - -- [ ] **Lines 3-8** - Opening paragraph - - States TRL approach clearly - - Line 6: "This section explains why TRL advancement - provides..." - metadiscourse could be tighter - - Fix: Delete line 6-8 (metadiscourse) or combine: - "Technology Readiness Levels provide the ideal metric, - measuring both..." - -- [ ] **Lines 10-19** - TRL justification paragraph 1 - - Makes argument for why TRLs - - Multiple short sentences with parallel structure - - Effective rhetoric - - Line 16-17: "This gap is precisely what this work aims - to bridge" - good, but "this work" could be "we aim" - -- [ ] **Lines 21-31** - TRL justification paragraph 2 - - Continues argument - - Good points about nuclear industry requirements - - Lines 29-31: Weak stress position - ends with - "publications alone cannot" (negative) - - Fix: "...making this metric directly relevant to - potential adopters and clearly demonstrating feasibility - and maturity." - -- [ ] **Lines 32-39** - Current/target TRL - - Clear statement of starting point and goal - - Good signposting: "Moving from current state to target - requires..." - - Minor: "Early TRL 3" (line 35)—is "early" necessary? - Could just say "TRL 3" - -- [ ] **Lines 41-49 (TRL 3 definition)** - Clear and -specific - - Paragraph format beginning with "\\paragraph{TRL 3...}" - is good - - Specific criteria listed - - Line 43: "For this research, TRL 3 means..." - clear - personalization - - Good structure - -- [ ] **Lines 51-60 (TRL 4 definition)** - Clear and -specific - - Similar structure to TRL 3, which is good - - Specific criteria - - "Zero safety violations" (line 59) - good concrete - metric - -- [ ] **Lines 62-78 (TRL 5 definition)** - Longest and most -detailed - - Appropriate given it's the target - - Lines 71-76: Discussion of off-nominal scenarios is good - - Line 73-74: "Graded responses to minor disturbances are - outside the scope" - good explicit scoping statement - - Minor: Could potentially break into two paragraphs—one - on hardware (lines 62-70), one on validation (lines 70-78) - -- [ ] **Lines 80-83** - Synthesis of TRL progression - - "These levels define progressively more demanding - demonstrations" - good summary - - Three parallel statements: "TRL 3 proves..., TRL 4 - proves..., TRL 5 proves..." - effective - - Could be even more parallel: "TRL 3 proves individual - components work. TRL 4 proves they integrate in - simulation. TRL 5 proves they run on industrial hardware." - -- [ ] **Lines 85-96** - Quarterly assessment and revision -criteria - - Long paragraph covering two topics: (1) progress - assessment, (2) revision triggers - - Consider breaking after line 89 (end of assessment - discussion) before starting revision discussion (line 90) - - Lines 91-94: Three specific failure modes listed - good - concrete triggers - -### 4.2 Paragraph-Level Issues - -- [ ] **Lines 10-31** - Two TRL justification paragraphs - - Issue: These two paragraphs both argue why TRLs are - appropriate - - Could be combined into single tighter paragraph - - Current word count: ~160 words across two paragraphs - - Fix: Combine key points into one paragraph (~120 words), - make argument more concise - -- [ ] **TRL definitions (lines 41-78)** - Three paragraphs -in parallel structure - - Excellent parallelism - - Each uses "For this research, TRL X means..." - - Each lists specific criteria - - Each ends with "This proves..." - - This is very effective and should be maintained - -- [ ] **Lines 98-105** - Success statement - - Opens with clear claim: "This research succeeds if..." - - Explains why this demonstrates success - - Good closing paragraph for section - -### 4.3 Metrics Section - Content Issues - -- [ ] **Justification for TRLs** - Somewhat defensive tone - - Two paragraphs (lines 10-31) justifying why TRLs are - appropriate - - While argument is sound, the length suggests - defensiveness - - Consider: Could this be condensed to make it feel less - defensive? - - Alternative: Perhaps reviewers have questioned TRL - approach in past? If so, this is appropriate. - -- [ ] **Measurability** - Excellent - - Each TRL has concrete, measurable criteria - - "Fewer than 1,000 states" (line 77) - - "Zero safety violations across 100 consecutive runs" - (line 93) - - This specificity is excellent - -- [ ] **Quarterly assessment** - Good accountability - - Shows you've thought about project management - - Revision criteria show you've thought about failure - modes - - This strengthens the proposal - ---- - -## 5. Risks and Contingencies Section - -### 5.1 Sentence-Level Issues - -- [ ] **Lines 3-12** - Opening paragraph - - Good overview structure - - Line 9: "Each risk has associated indicators for early - detection" - good framing - - Line 11-12: "The staged project structure ensures..." - - passive. Fix: "Our staged project structure ensures..." - -- [ ] **Lines 14-24** - Computational tractability risk -statement - - Clear problem statement - - Lines 17-21: Long sentence (51 words) with complex - structure - - Consider breaking after "specification complexity" or - "state" - - Fix: "Reactive synthesis scales exponentially with - specification complexity, which creates risk of - intractable synthesis times. Temporal logic specifications - from complete startup procedures may produce automata with - thousands of states, requiring days or weeks of synthesis - time. This would prevent demonstrating the complete - methodology within project timelines." - -- [ ] **Lines 26-35** - Indicators paragraph - - Good concrete indicators - - Parallel structure: "X would suggest Y", "X would - indicate Y", etc. - - Effective - -- [ ] **Lines 37-45** - Contingency plan - - Clear fallback - - Specific scope reduction described - - Line 42: "The research contribution would remain valid" - - good positive framing - - Line 44-45: "constraint rather than a failure" - - excellent reframing - -- [ ] **Lines 47-54** - Time-scale separation mitigation - - Technical depth is good - - Shows sophisticated understanding - - Minor: Line 48: "can be treated quasi-steady" - may be - jargon for some readers. Consider: "can be approximated as - steady" - -- [ ] **Lines 56-63** - Access to HPC resources - - Good mention of available resources - - Shows preparedness - - Line 59: "high-performance computing resources" - first - mention of CRC facility (it was in budget) - -### 5.2 Discrete-Continuous Interface Section - -- [ ] **Lines 65-79** - Problem statement - - Clear explanation of fundamental challenge - - Long sentences (lines 72-78 is 57 words) - - Consider breaking: "Temporal logic operates on boolean - predicates, while continuous control requires reasoning - about differential equations and reachable sets. Guard - conditions requiring complex nonlinear predicates may - resist boolean abstraction, making synthesis intractable. - Continuous safety regions that cannot be expressed as - conjunctions of verifiable constraints would similarly - create insurmountable verification challenges." - -- [ ] **Lines 81-92** - Indicators - - Parallel structure: "X would suggest Y", "X would - indicate Y" - - Good technical specificity - - Line 84-85: "Boolean abstraction" appears twice (lines - 73 and 84) - be consistent with terminology - -- [ ] **Lines 94-107** - Polytopic invariants contingency - - Technical and specific - - Good explanation of what polytopes are and why they help - - Line 100: "inner-approximated" - good use of precise - term, but consider whether definition needed - - Lines 103-107: Shows you've already thought about this - in your three-mode classification - -- [ ] **Lines 109-119** - Mitigation strategies - - "Design-for-verification" (line 113) is good concept - - Control barrier functions mentioned again (callback to - Research Approach) - - Shows integrated thinking - -### 5.3 Procedure Formalization Section - -- [ ] **Lines 121-134** - Problem statement - - Clear explanation of challenge - - Good point about procedures written for humans with - contextual understanding - - Lines 131-134: Risk is framed positively - "not merely - that formalization is difficult, but that current - procedures fundamentally lack the precision required" - -- [ ] **Lines 136-148** - Indicators - - Good concrete indicators - - Line 141-142: References to "operator judgment" in - procedures - very specific and realistic - - Line 145-148: "Domain experts unable to provide crisp - answers" - excellent indicator - -- [ ] **Lines 150-163** - Contingency as contribution - - Excellent reframing: documentation of gaps is itself - valuable - - "Taxonomy of formalization barriers" (line 152) - good - concept - - Lines 156-160: Shifts from "here's a controller" to - "here's what's needed"—good pivot - - This contingency is particularly well-developed - -- [ ] **Lines 165-177** - Mitigation strategies - - Early engagement with domain experts - - Cross-design comparison - - Both are good strategies showing preparedness - -### 5.4 Hardware-in-Loop Integration Section - -- [ ] **Lines 179-190** - Problem statement - - Clear technical challenges listed - - Specific timing requirements mentioned (10-100 Hz) - - Good detail level - -- [ ] **Lines 192-203** - Indicators - - Specific technical indicators (dropouts, buffer - overruns, computational limits) - - Good progression from communication → computation → - timing - -- [ ] **Lines 205-218** - Software-in-loop contingency - - Good fallback that maintains TRL 4 - - Explains why this still demonstrates value - - Line 214-217: "research contribution remains intact" - - good positive framing - - Note this maintains TRL 4 not TRL 5 (appropriate - scoping) - -- [ ] **Lines 220-232** - Mitigation strategies - - ARCADE prior success mentioned - - Early testing recommended - - Ovation flexibility noted - - All show preparedness - -### 5.5 Risks Section - Paragraph-Level Issues - -- [ ] **Four main subsections** - Well-balanced structure - - Each has: (1) problem statement, (2) indicators, (3) - contingency, (4) mitigation - - Parallel structure is effective - - Lengths: Computational (48 lines), Discrete-Continuous - (58 lines), Procedure (58 lines), HIL (54 lines) - - Fairly balanced - -- [ ] **Opening paragraph** - Could be tighter - - Lines 3-12: Sets up structure - - Could potentially be combined with subsequent topic - sentences - - But current structure works - -### 5.6 Risks Section - Content Issues - -- [ ] **Risk selection** - Comprehensive - - Four major risks cover computational, theoretical, - practical/procedural, and implementation - - Good coverage of different risk categories - -- [ ] **Contingency quality** - Excellent - - Each contingency preserves value - - Scope reductions are reasonable - - Positive framing ("contribution" not "failure") - -- [ ] **Indicators specificity** - Very good - - Concrete, measurable indicators - - Early warning focus - - This shows project management maturity - -- [ ] **Balance of subsections** - Good - - Roughly equal length - - But: is length proportional to actual risk magnitude? - - Discrete-continuous interface seems most fundamental, - but doesn't get more space - - Consider: Does space allocation reflect importance, or - just complexity of explanation? - ---- - -## 6. Broader Impacts Section - -### 6.1 Sentence-Level Issues - -- [ ] **Lines 3-10** - Opening paragraph - - Good hook: AI datacenters renewing SMR interest - - Clear problem setup - - Line 8-9: "However, the economics of nuclear power - deployment at this scale demand careful attention to - operating costs" - somewhat cautious phrasing - - Consider: "However, nuclear power economics depend - critically on reducing operating costs" - -- [ ] **Lines 12-23** - Economic statistics paragraph - - Excellent use of specific numbers - - $88.24/MWh, 1,050 TWh, $92B annually, 23-30% for O&M - - This level of specificity is persuasive - - Minor: Long sentences (lines 18-23 is 54 words) - - Consider breaking after "$92 billion": "...cost of power - generation would exceed $92 billion. Within this figure, - operations and maintenance represents..." - -- [ ] **Lines 25-37** - How research addresses costs - - Clear connection: autonomous control → reduced staffing - → lower O&M - - Good explanation of staffing challenge for SMRs - - Lines 30-33: Long sentence (48 words) could be broken - -- [ ] **Lines 38-50** - Correct-by-construction importance - - Good argument for why formal methods matter - - Explains what automation can/can't do (routine vs. - off-normal) - - Line 49-50: "much cheaper to operate" - consider whether - more precise language available - -- [ ] **Lines 52-62** - SMR deployment paragraph - - Good connection: NRC certification documents → FRET → - synthesis - - "Infrastructure of requirements and specifications is - already complete as part of licensing process" (lines - 59-61) - this is a key insight and could be more prominent - -- [ ] **Lines 64-74** - Generalization paragraph - - Good broader impact: methodology generalizes - - Lists other domains (chemical, aerospace, - transportation) - - Lines 71-74: Long final sentence (43 words) - consider - breaking - -### 6.2 Paragraph-Level Issues - -- [ ] **Section length** - At 75 lines, this is the briefest -technical section - - Issue: Given that economic motivation is central to - SMRs, this could be expanded - - Missed opportunities: workforce development, educational - impacts, equity considerations - -- [ ] **Paragraph structure** - Generally good - - Seven paragraphs covering: (1) context, (2) economics, - (3) how research helps, (4) why formal methods, (5) SMR - fit, (6) generalization - - Logical flow - -### 6.3 Broader Impacts - Content Issues - -- [ ] **Economic analysis** - Excellent - - Specific numbers - - Clear chain: electricity cost → total demand → O&M costs - - This is persuasive - -- [ ] **Missing elements** - Several - - **Workforce/educational impacts**: Training engineers in - formal methods, developing curriculum, broader - CS-engineering integration - - **Equity considerations**: Clean energy access, - distributed generation benefits - - **International implications**: Methodology could help - other countries deploy SMRs - - **Environmental justice**: How does autonomous control - affect siting near communities? - - Not all needed, but one or two would strengthen section - -- [ ] **Generalization** - Good but brief - - Lists domains (chemical, aerospace, transportation) - - Could expand slightly: What specific applications? - Pipeline safety? Aircraft control? Autonomous vehicles? - ---- - -## 7. Budget Section (Brief Review) - -As requested, this section receives lighter treatment -focusing on major issues only. - -### 7.1 Major Issues - -- [ ] **Line 73** - Typo - - "t ranslation" should be "translation" - -- [ ] **Table formatting** - Appears correct - - Budget table uses booktabs style (good) - - Numbers align properly - - Categories are clear - -- [ ] **High-performance workstation** - Consider upgrade -path - - Year 1: $3,500 for workstation - - Years 2-3: No upgrades budgeted - - Issue: As synthesis scales up, might need more compute - - Consider: Adding small line item for upgrades/expansion - in Years 2-3? - -- [ ] **Software note (lines 191-197)** - Good - - Explicitly states all software is free/licensed - - ARCADE through partnership - - This prevents questions - -- [ ] **In-kind contributions (lines 250-277)** - -Well-documented - - Emerson partnership valued - - University contributions noted - - Total estimated at $20,000+ - - Good to document this explicitly - -### 7.2 Budget Section - Overall Assessment - -- Budget is comprehensive, well-justified, and appropriate -- Fringe benefit rates are clearly stated -- Travel budget is reasonable -- No major concerns - ---- - -## 8. Schedule Section (Brief Review) - -As requested, this section receives lighter treatment -focusing on major issues only. - -### 8.1 Major Issues - -- [ ] **Line 73** - Spacing issue - - "t ranslation methodology" has incorrect space - - Should be "translation methodology" - -- [ ] **Gantt chart** - Appears well-structured - - Overlapping tasks shown appropriately - - Milestones marked clearly - - Publications timeline shown - -- [ ] **Publication strategy (lines 115-141)** - Excellent - - Explains venue choices - - NPIC&HMIT for nuclear community - - IEEE TAC for control theory community - - Rationale for each is clear - - Builds on prior success (best student paper) - -### 8.2 Schedule Section - Overall Assessment - -- 24-month timeline is ambitious but realistic -- Six trimesters for dissertation is reasonable -- Milestone structure aligns with TRL progression -- No major concerns - ---- - -## 9. Big Picture Issues - -### 9.1 Cross-Cutting Issues - -- [ ] **Three-mode classification** - Novel contribution -underemphasized - - Location: Research Approach, lines 178-208 - - Issue: This stabilizing/transitory/expulsory framework - appears to be novel, but is presented as routine - categorization - - Impact: You may not be getting credit for this - innovation - - Fix: Explicitly state novelty: "We propose a three-mode - classification for hybrid control design. To our - knowledge, this systematic taxonomy has not previously - been applied to hybrid control synthesis." - - Cross-reference: This should be mentioned in Goals - section as one of the methodological contributions - -- [ ] **Discrete-continuous interface verification** - Key -contribution - - Location: Research Approach subsection 3 - - Issue: The unified verification across - discrete-continuous interface is your main contribution, - but this isn't always explicit - - Impact: Reviewers may not fully appreciate novelty - - Fix: In Goals section, explicitly state: "The key - innovation is unified verification across the - discrete-continuous interface—ensuring both switching - logic and continuous dynamics are provably correct." - -- [ ] **SmAHTR introduction timing** - Appears abruptly - - Location: First mentioned in Goals (line 92), detailed - in Research Approach (line 253) - - Issue: SmAHTR suddenly appears as the demonstration case - without build-up - - Fix: Introduce SmAHTR earlier, perhaps in Goals section: - "We will demonstrate this methodology by developing an - autonomous startup controller for a Small Modular Advanced - High Temperature Reactor (SmAHTR), transitioning from cold - shutdown through criticality to full power operation." - -### 9.2 Consistency Issues - -- [ ] **Terminology consistency** - Generally good - - "Correct by construction" vs. "provably correct" - used - somewhat interchangeably - - "Hybrid automata" vs. "discrete automata" vs. "finite - state automata" - generally clear from context - - "Reachability analysis" - consistent usage - - No major inconsistencies - -- [ ] **Notation consistency** - Good - - $f(\cdot)$ and $\nu(\cdot)$ introduced clearly - - Temporal logic operators ($G$, $X$, $U$, $F$) explained - when introduced - - Mathematical notation is consistent - -- [ ] **Section cross-references** - Could be stronger - - SOTA identifies gaps → Research Approach should - explicitly reference these - - Current: connections are implicit - - Fix: In Research Approach opening, add: "This approach - addresses the three limitations identified in Section 2: - procedures lacking formal verification, current practice - treating continuous and discrete separately, and HARDENS - verifying discrete logic without continuous dynamics." - -### 9.3 Argument Flow - -- [ ] **Problem → Solution arc** - Clear and strong - - Problem: Operators make errors (SOTA human factors - section) - - Gap: No formal verification of procedures or hybrid - behavior (SOTA limitations) - - Solution: Hybrid control synthesis with discrete + - continuous verification (Research Approach) - - Evidence: TRL progression demonstrates feasibility - (Metrics) - - Risks addressed: Comprehensive contingencies (Risks) - - Impact: Economic viability of SMRs (Broader Impacts) - - This structure is excellent - -- [ ] **"So what" connections** - Could be more explicit - - Issue: Sometimes you present information without - explicitly stating why it matters - - Examples: - - After Goals section: Add "If successful, this - enables..." - - Between SOTA and Research Approach: Add "These gaps - create an urgent research opportunity" - - After Metrics section: Add "Achieving TRL 5 would - provide a clear path to industrial adoption" - -- [ ] **Callbacks and forward references** - Could be -stronger - - Research Approach could reference specific SOTA - limitations by name - - Metrics could reference specific risks - - Broader Impacts could callback to human factors - statistics from SOTA - -### 9.4 Missing Elements - -- [ ] **Cybersecurity** - Not mentioned - - Issue: For autonomous nuclear control, cybersecurity is - critical - - Impact: Reviewers may wonder why this isn't addressed - - Fix: Add brief paragraph (perhaps in Risks section or - Research Approach) on security verification - - Could mention: "While cybersecurity verification is - beyond the scope of this phase, the formal methods - infrastructure we develop provides a foundation for - subsequent security verification using techniques like - information flow analysis and secure compilation." - -- [ ] **Regulatory path** - Mentioned but not detailed - - Issue: You mention NRC requirements but don't describe - approval process - - Impact: May seem naive about regulatory challenges - - Fix: Add paragraph in Broader Impacts discussing - regulatory pathway: "NRC Standard Review Plan provides - pathways for digital I&C approval (NUREG-0800, Chapter 7). - The formal verification artifacts we produce—including - provable correctness claims, traceability from - requirements to implementation, and systematic testing - evidence—align with NRC expectations for high-assurance - systems. While full regulatory approval is beyond this - research scope, our methodology produces the documentation - foundation NRC requires." - -- [ ] **ML/AI alternatives** - Not discussed - - Issue: Machine learning for control is prominent. Why - not use ML? - - Impact: Reviewers may wonder if you've considered - alternatives - - Fix: Add brief paragraph early in Research Approach: - "Machine learning approaches to autonomous control have - received significant attention. However, neural network - controllers are fundamentally black-box systems that - cannot provide the mathematical safety guarantees required - for nuclear applications. Recent work on verified neural - networks shows promise, but the state of the art remains - far from the assurance levels nuclear safety demands. - Formal methods provide the only currently viable path to - provable correctness for safety-critical autonomous - control." - -### 9.5 Strengths to Maintain - -- [ ] **Specific examples** - Excellent throughout - - TMI accident narrative - - SCRAM requirement translation - - HARDENS project detail - - SmAHTR demonstration - - These make the proposal concrete and believable - -- [ ] **Statistical evidence** - Very strong - - 70-80% human error rate - - Economic projections ($92B annually) - - HEP rates (0.001-0.01 → 0.1-1.0) - - Specific numbers are persuasive - -- [ ] **Technical depth** - Appropriate level - - Enough detail to demonstrate expertise - - Not so much that non-experts are lost - - Good balance for mixed audience - -- [ ] **Risk analysis** - Exceptionally thorough - - Four major risks identified - - Concrete indicators - - Viable contingencies - - Positive framing - - This is a model for risk sections - ---- - -## Summary Statistics - -**Total issues documented**: 150+ - -**By level**: -- Sentence-level: ~70 issues -- Paragraph-level: ~40 issues -- Content/organization: ~40 issues - -**By section**: -- Goals and Outcomes: 18 issues -- State of the Art: 45 issues (longest section, most issues) -- Research Approach: 40 issues -- Metrics of Success: 12 issues -- Risks and Contingencies: 20 issues -- Broader Impacts: 10 issues -- Budget: 3 issues (light review) -- Schedule: 3 issues (light review) -- Big Picture: 10 issues - -**Priority levels** (estimated): -- HIGH impact: ~15 issues (major organization, missing -content, key contributions underemphasized) -- MEDIUM impact: ~60 issues (sentence-level patterns, -paragraph structure, clarity) -- LOW impact: ~75 issues (minor wording, polish, -consistency) - ---- - -## Revision Strategy Recommendation - -1. **Start with Big Picture issues** (Section 9) - Ensure -novel contributions are highlighted -2. **Address Priority Issues 1-5** from Executive Summary -3. **Work section-by-section** using this detailed document -4. **Apply patterns** from Executive Summary to similar -cases -5. **Final consistency pass** - Terminology, -cross-references, formatting - -Tpkkkkkkkkkkkkkkkkhe proposal has strong technical content and solid -structure. These revisions will enhance clarity, emphasize -your contributions, and strengthen your argument. Good -luck! diff --git a/Writing/THESIS_PROPOSAL/ERLM-Proposal-Review-Summary.md b/Writing/THESIS_PROPOSAL/ERLM-Proposal-Review-Summary.md deleted file mode 100644 index a1c2871da..000000000 --- a/Writing/THESIS_PROPOSAL/ERLM-Proposal-Review-Summary.md +++ /dev/null @@ -1,627 +0,0 @@ -# ERLM Proposal Writing Review - Executive Summary - -**Date**: December 2, 2025 **Reviewer**: Claude Code -**Framework**: Gopen's Sense of Structure - ---- - -## Overview - -This proposal demonstrates strong technical content, clear -methodology, and comprehensive coverage of all required -elements. The research approach is well-conceived, and the -progression from problem statement through solution is -logical. The writing is generally clear and professional. - -**Key Strengths:** -- Excellent technical depth and specificity -- Strong motivation established through human factors -statistics -- Clear three-thrust research structure -- Comprehensive risk analysis with concrete contingencies -- Good use of specific examples (TMI accident, HARDENS -project) - -**Priority Areas for Revision:** -- Sentence-level: Strengthen stress positions to emphasize -key claims -- Paragraph-level: Sharpen point-issue structure in some -sections -- Section-level: Tighten organization in State of the Art -section -- Big picture: Strengthen "so what" connections throughout - ---- - -## Priority Issues (Top 10) - -### 1. **SOTA Section Length and Organization** -[SECTION-LEVEL] **Location**: State of the Art section (358 -lines) **Issue**: The SOTA section is the longest in the -proposal and covers multiple distinct topics (current -procedures, human factors, HARDENS). While comprehensive, it -risks overwhelming readers and obscuring your key - contributions. **Impact**: HIGH - Reviewers may lose track - of your argument in the density **Recommendation**: - Consider restructuring with clearer signposting. Each - subsection should explicitly connect back to what gap - you're filling. The current "\textbf{LIMITATION:}" callouts - are excellent—ensure every major subsection has one. - -### 2. **Weak Stress Positions Throughout** [SENTENCE-LEVEL] -**Location**: All sections, especially Goals and State of -the Art **Issue**: Many sentences place old/known -information in stress position (sentence-final), missing -opportunities to emphasize new claims **Impact**: -MEDIUM-HIGH - Reduces rhetorical impact of key claims **See -Pattern**: "Stress Position Weakness" below for examples and -fixes - -### 3. **Missing "So What" Connections** [BIG PICTURE] -**Location**: Transitions between major sections **Issue**: -The proposal moves from problem → approach → metrics without -always explicitly stating "this matters because..." at -transition points **Impact**: MEDIUM-HIGH - Reviewers may -not fully grasp significance **Recommendation**: Add -explicit "if successful, this enables..." statements at the -end of Goals section and beginning of Metrics section - -### 4. **Passive Voice Obscuring Agency** [SENTENCE-LEVEL] -**Location**: Research Approach, especially subsection -introductions **Issue**: Passive constructions like "will be -employed" and "will be used" hide who does what and reduce -directness **Impact**: MEDIUM - Reduces clarity and makes -writing feel less confident **See Pattern**: "Passive Voice" -below - -### 5. **Point-Issue Structure in Paragraphs** -[PARAGRAPH-LEVEL] **Location**: State of the Art, Risk -sections **Issue**: Some paragraphs present information -without first establishing why readers should care (the -"issue") **Impact**: MEDIUM - Readers may wonder "why are -you telling me this?" **See Pattern**: "Point-Issue -Structure" below - -### 6. **Topic String Breaks** [PARAGRAPH-LEVEL] -**Location**: Research Approach, subsection transitions -**Issue**: Topic position doesn't always establish clear -continuity from previous sentence, forcing readers to -reconstruct connections **Impact**: MEDIUM - Increases -cognitive load **See Pattern**: "Topic Position & -Continuity" below - -### 7. **Nominalization Hiding Action** [SENTENCE-LEVEL] -**Location**: Throughout, especially Research Approach -**Issue**: Action buried in nouns (e.g., "implementation" -instead of "implement", "verification" instead of "verify") -**Impact**: MEDIUM - Makes writing feel static rather than -dynamic **Recommendation**: Convert nominalizations to -active verbs where possible - -### 8. **Long Complex Sentences** [SENTENCE-LEVEL] -**Location**: State of the Art (lines 45-51), Risks (lines -72-79) **Issue**: Some sentences exceed 40-50 words with -multiple subordinate clauses, challenging comprehension -**Impact**: MEDIUM - Reviewers may have to re-read -**Recommendation**: Break into 2-3 shorter sentences with -clear logical flow - -### 9. **Subsection Balance in Risks Section** -[SECTION-LEVEL] **Location**: Risks and Contingencies -section **Issue**: Four subsections of vastly different -lengths (computational tractability gets more space than -discrete-continuous interface, despite latter being more -fundamental) **Impact**: LOW-MEDIUM - May suggest misaligned -priorities **Recommendation**: Consider whether space -allocation reflects actual risk magnitude - -### 10. **Broader Impacts Underutilized** [BIG PICTURE] -**Location**: Broader Impacts section (75 lines vs 358 for -SOTA) **Issue**: This section is relatively brief given that -economic impact is a major motivation for SMRs **Impact**: -LOW-MEDIUM - Missing opportunity to strengthen value -proposition **Recommendation**: Consider expanding economic -analysis or adding brief discussion of workforce/educational -impacts - ---- - -## Key Patterns Identified - -### Pattern 1: Stress Position Weakness - -**Principle** (Gopen): The stress position (end of sentence) -should contain the most important new information. Readers -expect climax at sentence-end and are disappointed when they -find old information or weak phrases there. - -**Example 1** (Goals and Outcomes, lines 13-17): ``` -Current: "Currently, nuclear plant operations rely on -extensively trained human operators who follow detailed -written procedures and strict regulatory requirements to -manage reactor control." ``` -- **Issue**: Sentence ends with "manage reactor control"—a -restatement of the opening. The key claim is buried -mid-sentence: "extensively trained...detailed -procedures...strict requirements" -- **Fixed**: "Currently, nuclear plant operations require -extensively trained human operators following detailed -written procedures under strict regulatory requirements." - -**Example 2** (State of the Art, lines 53-54): ``` Current: -"Procedures lack formal verification of correctness and -completeness." ``` -- **Issue**: Ends weakly with "completeness" which is minor -compared to the bigger issue -- **Fixed**: "Procedures lack formal verification, leaving -correctness and completeness unproven." - -**Example 3** (Research Approach, lines 41-42): ``` Current: -"The following sections discuss how these thrusts will be -accomplished." ``` -- **Issue**: Pure metadiscourse in stress position, provides -no new information -- **Fixed**: Delete this sentence—the enumeration provides -sufficient transition, or combine with previous sentence: -"...through three main thrusts, each detailed below." - -**Similar instances**: -- Goals lines 29-32: "...we will combine formal methods..." -- State of the Art lines 81-85: "...no application of hybrid -control theory exists..." -- Research Approach lines 115-116: "...enable progression to -the next step..." -- Metrics lines 29-31: "...makes this metric directly -relevant..." -- Risks lines 12-13: "...identification of remaining -barriers to deployment" - -**How to fix**: Identify the most important new claim in -each sentence and move it to the end. Often this means -converting from "X does Y to achieve Z" to "X achieves Z by -doing Y." - ---- - -### Pattern 2: Passive Voice Obscuring Agency - -**Principle** (Gopen): Passive voice obscures who does what -and reduces directness. In proposal writing, active voice -demonstrates confidence and control. Use passive only when -the agent is truly unimportant or unknown. - -**Example 1** (Research Approach, line 118): ``` Current: -"We will employ state-of-the-art reactive synthesis -tools..." ``` -- **Issue**: "Employ" is weak; you're not hiring the tools, -you're using them -- **Better**: "We will use Strix, a state-of-the-art -reactive synthesis tool..." -- **Best**: "Strix will translate our temporal logic -specifications into deterministic automata..." (Shows what -the tool *does*, not just that you'll use it) - -**Example 2** (Research Approach, line 207): ``` Current: -"Control barrier functions will be employed when..." ``` -- **Issue**: Passive—who employs them? And "employed" sounds -formal/stuffy -- **Fixed**: "We will use control barrier functions to -verify..." or better "Control barrier functions verify..." - -**Example 3** (Metrics, line 67): ``` Current: "This -milestone delivers an internal technical report..." ``` -- **Issue**: Milestones don't deliver, people do -- **Fixed**: "We will deliver an internal technical report -documenting..." - -**Similar instances**: -- Research Approach lines 161, 175, 206, 220: "will be -employed", "will be developed", "will be used" -- Metrics lines 69, 73, 79, 84: "...delivers a [document]" -- Risks lines 57, 109, 163: various passives - -**How to fix**: -1. Identify the real agent (usually "we") -2. Make agent the subject: "We will X" or "X will Y" -3. Choose strong active verbs: use/apply/develop/verify (not -employ/utilize) - ---- - -### Pattern 3: Point-Issue Structure Weakness - -**Principle** (Gopen): Paragraphs should begin by -establishing (1) the point/claim being made and (2) why it -matters (the issue). Discussion then supports that point. -Readers need context before details. - -**Example 1** (State of the Art, lines 88-107): ``` Current -paragraph begins: "The persistent role of human error in -nuclear safety incidents, despite decades of -improvements..." ``` -- **Analysis**: This paragraph immediately dives into the -"persistent role" without first establishing why we're -discussing human factors at all. Reader thinks: "Wait, -weren't we just talking about procedures?" -- **Fixed**: Add issue statement first: "Human factors -provide the most compelling motivation for formal automated -control. Despite decades of improvements in training and -procedures, human error persists in 70-80% of nuclear -incidents—suggesting that operator-based control faces -fundamental, not remediable, limitations." - -**Example 2** (Risks, first paragraph): ``` Current: "This -research relies on several critical assumptions that, if -invalidated, would require scope adjustment..." ``` -- **Analysis**: Good—this establishes both point (critical -assumptions exist) and issue (invalidity requires -adjustment) immediately. The paragraph then delivers on this -promise. This is a good model! - -**Example 3** (Research Approach, lines 166-169): ``` -Current: "While discrete system components will be -synthesized with correctness guarantees, they represent only -half of the complete system." ``` -- **Analysis**: Good issue statement (discrete alone -insufficient), but could be sharper about the point. What -will this section show? -- **Fixed**: "While discrete system components will be -synthesized with correctness guarantees, they represent only -half of the complete system. This section describes how we -will develop continuous control modes, verify their -correctness, and address the unique verification challenges -at the discrete-continuous interface." - -**Similar instances**: -- State of the Art lines 13-34: long paragraph with delayed -point -- Goals lines 103-119: impact paragraph could be tighter -- Approach lines 178-208: three-mode classification needs -clearer framing - -**How to fix**: -1. First sentence should state the paragraph's point -2. Second sentence (or same sentence) should state why this -matters -3. Remaining sentences provide supporting detail - ---- - -### Pattern 4: Topic Position & Continuity - -**Principle** (Gopen): The topic position (beginning of -sentence) should contain old/familiar information that links -to what came before. This creates flow and coherence. Abrupt -topic shifts disorient readers. - -**Example 1** (Goals, lines 18-23): ``` Sentence 1: "...this -reliance on human operators prevents the introduction of -autonomous control capabilities..." - -Sentence 2: "Emerging technologies like small modular -reactors face significantly higher per-megawatt staffing -costs..." ``` -- **Issue**: Topic shifts abruptly from "reliance on -operators" to "emerging technologies". Connection exists -(both about staffing challenges) but isn't explicit -- **Fixed**: "...prevents autonomous control capabilities. -This limitation creates particular challenges for emerging -technologies like small modular reactors, which face -significantly higher per-megawatt staffing costs..." - -**Example 2** (State of the Art, lines 234-243): ``` -Sentence about what HARDENS addressed: "...discrete digital -control logic..." - -Next sentence: "However, the project did not address -continuous dynamics..." ``` -- **Analysis**: Good use of "however, the project" in topic -position—maintains focus on HARDENS while pivoting to -limitation. This is a good model! - -**Example 3** (Research Approach, lines 56-58): ``` Sentence -1: "...we may be able to translate them into logical -formulae..." - -Sentence 2: "Linear Temporal Logic (LTL) provides four -fundamental operators..." ``` -- **Issue**: Abrupt topic shift from "translating -procedures" to "LTL provides". Missing: why LTL? Why now? -- **Fixed**: "...translate them into logical formulae. To -formalize these procedures, we will use Linear Temporal -Logic (LTL), which provides four fundamental operators..." - -**Similar instances**: -- Goals lines 23-27: "emerging technologies" → "what is -needed" -- State of the Art lines 72-74: control modes → division -between automated/human -- Approach lines 183-185: stabilizing mode example → -transitory mode definition - -**How to fix**: -1. Identify the topic of the previous sentence -2. Begin next sentence with something related to that topic -3. Use transitional phrases when shifting topics: "This -[previous thing] leads to [new thing]" - ---- - -### Pattern 5: Long Complex Sentences - -**Principle**: Sentences with multiple subordinate clauses -(especially over 35-40 words) tax reader working memory. -Breaking into multiple sentences often improves clarity -without losing sophistication. - -**Example 1** (State of the Art, lines 48-51): ``` Current -(51 words): "Procedures undergo technical evaluation, -simulator validation testing, and biennial review as part of -operator requalification under 10 CFR 55.59, but despite -these rigorous development processes, procedures -fundamentally lack formal verification of key safety -properties." ``` -- **Issue**: Long sentence with list, subordinate clause, -and contrast—hard to parse -- **Fixed (2 sentences)**: "Procedures undergo technical -evaluation, simulator validation testing, and biennial -review as part of operator requalification under 10 CFR -55.59. Despite these rigorous development processes, -procedures fundamentally lack formal verification of key -safety properties." - -**Example 2** (Risks, lines 72-78): ``` Current (57 words): -"Temporal logic operates on boolean predicates, while -continuous control requires reasoning about differential -equations and reachable sets, and guard conditions that -require complex nonlinear predicates may resist boolean -abstraction, making synthesis intractable." ``` -- **Issue**: Run-on with multiple clauses strung together -with commas -- **Fixed (3 sentences)**: "Temporal logic operates on -boolean predicates, while continuous control requires -reasoning about differential equations and reachable sets. -Guard conditions requiring complex nonlinear predicates may -resist boolean abstraction. This mismatch could make -synthesis intractable." - -**Similar instances**: -- State of the Art lines 44-51: procedure development -description -- Research Approach lines 40-45: hybrid system description -- Risks lines 17-24: computational tractability discussion -- Broader Impacts lines 13-23: economic analysis - -**How to fix**: -1. Identify natural breakpoints (usually where you have -"and" or "but") -2. Create new sentences at these breaks -3. Ensure each new sentence has clear topic position -4. May need to repeat/reference previous sentence's subject -for clarity - ---- - -## Section-Level Issues - -### Goals and Outcomes Section **Strengths**: Excellent -structure with clear goal → problem → approach → outcomes → -impact progression. The four-paragraph opening is very -strong. - -**Issues**: -- Lines 29-53 (Approach paragraph): This is dense and tries -to cover too much. Consider breaking into two paragraphs: -one on the approach concept, one on the hypothesis and -rationale. -- Outcomes enumeration: Very clear, but could strengthen the -transition from strategy to outcome in each item. Currently -reads as "we'll do X. [new sentence] This enables Y." -Consider: "We'll do X, enabling Y." - -### State of the Art Section **Strengths**: Comprehensive, -well-researched, excellent use of the HARDENS case study as -both positive example and gap identifier. - -**Issues**: -- **Length**: At 358 lines, this risks losing readers. Most -concerning: readers may forget your framing by the time they -reach your contribution. -- **Organization**: Four major subsections (procedures, -human factors, HARDENS, research imperative) would benefit -from a roadmap sentence at the beginning: "To understand the -need for hybrid control synthesis, we first examine..." -- **Balance**: HARDENS subsection is 89 lines—nearly 25% of -SOTA. While impressive, consider whether this should be a -separate section or whether some detail could move to an -appendix. -- **Transition to Approach**: The "Research Imperative" -subsection is excellent but feels like it belongs at the -start of Research Approach rather than end of SOTA. - -### Research Approach Section **Strengths**: Clear -three-thrust structure, good use of equations and examples, -strong technical detail. - -**Issues**: -- **Subsection transitions**: The transitions between the -three main subsections (Procedures→Temporal, -Temporal→Discrete, Discrete→Continuous) could be smoother. -Each starts somewhat abruptly. -- **SmAHTR introduction**: The SmAHTR demonstration case is -introduced suddenly at line 253. Consider introducing it -earlier (perhaps in Goals section or at start of Approach) -so readers know it's coming. -- **Three-mode classification**: Lines 178-208 present the -stabilizing/transitory/expulsory framework, which is -innovative. This deserves more prominence—consider -highlighting it as a key contribution. - -### Metrics of Success Section **Strengths**: TRL framework -is well-justified, progression through levels is clear. - -**Issues**: -- **Defensive tone**: Lines 11-30 spend considerable space -justifying why TRL is appropriate. This is good but could be -more concise. Consider: one paragraph on why TRLs (lines -10-19) rather than two. -- **Grading criteria**: The TRL definitions (3, 4, 5) are -excellent. Very concrete and measurable. - -### Risks and Contingencies Section **Strengths**: -Comprehensive, each risk has indicators and contingencies, -well-organized. - -**Issues**: -- **Subsection balance**: Four subsections range from 41 -lines (computational) to 65 lines (discrete-continuous). -Ensure space reflects actual risk level. -- **Mitigation vs. contingency**: Some subsections blur -"mitigation" (preventing problems) and "contingency" -(response if they occur). Consider clarifying this -structure. - -### Broader Impacts Section **Strengths**: Clear economic -motivation, good connection to SMRs and datacenter -application. - -**Issues**: -- **Brevity**: At 75 lines, this is the shortest technical -section. Given that economic viability is a key motivation, -consider expanding. -- **Missed opportunities**: Could briefly mention -workforce/educational impacts (training future engineers in -formal methods), equity (providing reliable clean energy to -underserved areas), broader applicability beyond nuclear. - -### Budget Section **Brief review**: Budget is -comprehensive, well-justified, appropriate. Minor note: -Consider whether the high-performance workstation (Year 1) -might need upgrades in Year 2-3 as synthesis scales up. - -### Schedule Section **Brief review**: Schedule is ambitious -but realistic. Six trimesters for dissertation research is -reasonable. Publication strategy is smart (nuclear community -first, then broader control theory community). Minor note: -Line 73 has a space issue ("t ranslation"). - ---- - -## Big Picture Observations - -### Narrative and Argument Structure - -**Strengths**: -- Clear problem-solution arc: operators make errors → -procedures lack formal guarantees → hybrid control synthesis -provides guarantees -- Good use of motivating examples (TMI, human error -statistics, HARDENS) -- Technical progression is logical: discrete synthesis → -continuous verification → integrated system - -**Opportunities**: -1. **Strengthen "so what" transitions**: The proposal -sometimes presents information without explicitly stating -significance. Add more "This matters because..." statements. -2. **Emphasize novelty earlier**: The three-mode -classification and discrete-continuous interface -verification are novel contributions. Signal this earlier -and more explicitly. -3. **Create more callbacks**: When describing Research -Approach, refer back to specific limitations identified in -State of the Art. Currently these connections are implicit. - -### Rhetorical Effectiveness - -**Credibility established through**: -- Comprehensive literature review -- Specific technical detail -- Access to industry hardware (Emerson partnership) -- Prior conference recognition (best student paper) - -**Value proposition**: -- Clear economic impact (O&M cost reduction) -- Safety improvement (mathematical guarantees vs. human -operators) -- Broader applicability (methodology generalizes) - -**Could strengthen**: -- More explicit statements of what's novel vs. what's -established practice -- Stronger emphasis on the unique combination of discrete -synthesis + continuous verification (others do one or the -other, not both) - -### Content Gaps and Consistency - -**Terminology**: -- Generally consistent -- Good introduction of technical terms (hybrid automata, -temporal logic, reachability analysis) -- Minor: "correct by construction" vs. "provably -correct"—used interchangeably, which is fine, but could note -they're synonymous - -**Scope consistency**: -- Excellent—stays focused on startup procedures for SmAHTR -- Appropriately acknowledges limitations (TRL 5, not -deployment-ready) -- Risk section addresses what happens if scope must narrow - -**Potential gaps**: -1. **Cybersecurity**: Not mentioned. For autonomous nuclear -control, shouldn't there be at least a paragraph on security -verification? -2. **Regulatory path**: You mention "regulatory -requirements" but don't detail what NRC approval process -would look like. Even a paragraph would strengthen -credibility. -3. **Comparison with alternatives**: What about machine -learning approaches to autonomous control? Worth a paragraph -explaining why formal methods are superior for -safety-critical systems. - ---- - -## Gopen Framework Quick Reference - -**Stress Position**: End of sentence should contain most -important new information. Readers expect climax there. - -**Topic Position**: Beginning of sentence should contain -familiar information that links to previous sentence. -Creates flow. - -**Point-Issue Structure**: Paragraphs should open by stating -(1) the point/claim and (2) why it matters, before providing -supporting detail. - -**Topic String**: The chain of topics across sentences in a -paragraph. Strong topic strings create coherence; broken -ones confuse readers. - -**Old→New Information Flow**: Information should flow from -familiar (old) to unfamiliar (new) within sentences and -paragraphs. - ---- - -## Next Steps - -1. **Start with Priority Issues 1-3**: These have the -highest impact -2. **Apply Patterns**: Use the pattern examples to fix -similar instances throughout -3. **Consult Detailed Document**: For comprehensive -checkbox-by-checkbox revisions -4. **Section-by-section revision**: Work through one section -at a time, applying patterns -5. **Final pass for consistency**: Ensure changes maintain -consistent terminology and tone - -This proposal has strong technical content and a solid -structure. The revisions suggested here will strengthen -clarity, emphasize key contributions, and make the argument -even more compelling for reviewers. Good luck with your -revisions! diff --git a/Writing/THESIS_PROPOSAL/GOv1.pdf b/Writing/THESIS_PROPOSAL/GOv1.pdf deleted file mode 100644 index daa3e3d2a..000000000 Binary files a/Writing/THESIS_PROPOSAL/GOv1.pdf and /dev/null differ diff --git a/Writing/THESIS_PROPOSAL/GOv2.pdf b/Writing/THESIS_PROPOSAL/GOv2.pdf deleted file mode 100644 index 9511242e8..000000000 Binary files a/Writing/THESIS_PROPOSAL/GOv2.pdf and /dev/null differ diff --git a/Writing/THESIS_PROPOSAL/SABO_FINAL_ERLM_PROPOSAL.pdf b/Writing/THESIS_PROPOSAL/SABO_FINAL_ERLM_PROPOSAL.pdf deleted file mode 100644 index 2e6eadd02..000000000 Binary files a/Writing/THESIS_PROPOSAL/SABO_FINAL_ERLM_PROPOSAL.pdf and /dev/null differ diff --git a/Writing/THESIS_PROPOSAL/Sabo-Supplemental-Sections.pdf b/Writing/THESIS_PROPOSAL/Sabo-Supplemental-Sections.pdf deleted file mode 100644 index f2db7de68..000000000 Binary files a/Writing/THESIS_PROPOSAL/Sabo-Supplemental-Sections.pdf and /dev/null differ diff --git a/Writing/THESIS_PROPOSAL/SaboBudgetAndJustification.pdf b/Writing/THESIS_PROPOSAL/SaboBudgetAndJustification.pdf deleted file mode 100644 index 14904863c..000000000 Binary files a/Writing/THESIS_PROPOSAL/SaboBudgetAndJustification.pdf and /dev/null differ diff --git a/Writing/THESIS_PROPOSAL/SaboMOS.pdf b/Writing/THESIS_PROPOSAL/SaboMOS.pdf deleted file mode 100644 index d38c27baf..000000000 Binary files a/Writing/THESIS_PROPOSAL/SaboMOS.pdf and /dev/null differ diff --git a/Writing/THESIS_PROPOSAL/SaboOnePager.pdf b/Writing/THESIS_PROPOSAL/SaboOnePager.pdf deleted file mode 100644 index 8ecc0b8b5..000000000 Binary files a/Writing/THESIS_PROPOSAL/SaboOnePager.pdf and /dev/null differ diff --git a/Writing/THESIS_PROPOSAL/SaboOnePagerV2.pdf b/Writing/THESIS_PROPOSAL/SaboOnePagerV2.pdf deleted file mode 100644 index ef4cb4436..000000000 Binary files a/Writing/THESIS_PROPOSAL/SaboOnePagerV2.pdf and /dev/null differ diff --git a/Writing/THESIS_PROPOSAL/SaboOnePagerV3.pdf b/Writing/THESIS_PROPOSAL/SaboOnePagerV3.pdf deleted file mode 100644 index d7cb3b492..000000000 Binary files a/Writing/THESIS_PROPOSAL/SaboOnePagerV3.pdf and /dev/null differ diff --git a/Writing/THESIS_PROPOSAL/SaboOnePagerV4.pdf b/Writing/THESIS_PROPOSAL/SaboOnePagerV4.pdf deleted file mode 100644 index 47c295024..000000000 Binary files a/Writing/THESIS_PROPOSAL/SaboOnePagerV4.pdf and /dev/null differ diff --git a/Writing/THESIS_PROPOSAL/SaboOnePagerV5.pdf b/Writing/THESIS_PROPOSAL/SaboOnePagerV5.pdf deleted file mode 100644 index db03c7c67..000000000 Binary files a/Writing/THESIS_PROPOSAL/SaboOnePagerV5.pdf and /dev/null differ diff --git a/Writing/THESIS_PROPOSAL/SaboOnePagerV6.pdf b/Writing/THESIS_PROPOSAL/SaboOnePagerV6.pdf deleted file mode 100644 index 630c930b7..000000000 Binary files a/Writing/THESIS_PROPOSAL/SaboOnePagerV6.pdf and /dev/null differ diff --git a/Writing/THESIS_PROPOSAL/SaboRisksAndContingencies.pdf b/Writing/THESIS_PROPOSAL/SaboRisksAndContingencies.pdf deleted file mode 100644 index 2ba5222d4..000000000 Binary files a/Writing/THESIS_PROPOSAL/SaboRisksAndContingencies.pdf and /dev/null differ diff --git a/Writing/THESIS_PROPOSAL/Sabo_GO3_Whitepaper_Draft.pdf b/Writing/THESIS_PROPOSAL/Sabo_GO3_Whitepaper_Draft.pdf deleted file mode 100644 index 59878fe74..000000000 Binary files a/Writing/THESIS_PROPOSAL/Sabo_GO3_Whitepaper_Draft.pdf and /dev/null differ diff --git a/Writing/THESIS_PROPOSAL/Sabo_Schedule.pdf b/Writing/THESIS_PROPOSAL/Sabo_Schedule.pdf deleted file mode 100644 index a135f9b6f..000000000 Binary files a/Writing/THESIS_PROPOSAL/Sabo_Schedule.pdf and /dev/null differ diff --git a/Writing/THESIS_PROPOSAL/Sabo_Whitepaper.pdf b/Writing/THESIS_PROPOSAL/Sabo_Whitepaper.pdf deleted file mode 100644 index ea07cd9b9..000000000 Binary files a/Writing/THESIS_PROPOSAL/Sabo_Whitepaper.pdf and /dev/null differ diff --git a/Writing/THESIS_PROPOSAL/references_old.bib b/Writing/THESIS_PROPOSAL/references_old.bib deleted file mode 100644 index 2406bceb9..000000000 --- a/Writing/THESIS_PROPOSAL/references_old.bib +++ /dev/null @@ -1,547 +0,0 @@ -% Foundational Papers - -@article{alur1995algorithmic, - title={The algorithmic analysis of hybrid systems}, - author={Alur, Rajeev and Courcoubetis, Costas and Halbwachs, Nicolas and Henzinger, Thomas A and Ho, Pei-Hsin and Nicollin, Xavier and Olivero, Alfredo and Sifakis, Joseph and Yovine, Sergio}, - journal={Theoretical Computer Science}, - volume={138}, - number={1}, - pages={3--34}, - year={1995}, - publisher={Elsevier} -} - -@inproceedings{alur1993hybrid, - title={Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems}, - author={Alur, Rajeev and Courcoubetis, Costas and Henzinger, Thomas A and Ho, Pei-Hsin}, - booktitle={Hybrid Systems}, - pages={209--229}, - year={1993}, - publisher={Springer} -} - -@article{mitchell2005time, - title={A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games}, - author={Mitchell, Ian M and Bayen, Alexandre M and Tomlin, Claire J}, - journal={IEEE Transactions on Automatic Control}, - volume={50}, - number={7}, - pages={947--957}, - year={2005}, - publisher={IEEE} -} - -@article{platzer2008differential, - title={Differential dynamic logic for hybrid systems}, - author={Platzer, Andr{\'e}}, - journal={Journal of Automated Reasoning}, - volume={41}, - number={2}, - pages={143--189}, - year={2008}, - publisher={Springer} -} - -@article{platzer2017complete, - title={A complete uniform substitution calculus for differential dynamic logic}, - author={Platzer, Andr{\'e}}, - journal={Journal of Automated Reasoning}, - volume={59}, - number={2}, - pages={219--265}, - year={2017}, - publisher={Springer} -} - -@inproceedings{donze2010robust, - title={Robust satisfaction of temporal logic over real-valued signals}, - author={Donz{\'e}, Alexandre and Maler, Oded}, - booktitle={International Conference on Formal Modeling and Analysis of Timed Systems}, - pages={92--106}, - year={2010}, - publisher={Springer} -} - -% Control Theory and Stability - -@article{geromel2006stability, - title={Stability and stabilization of continuous-time switched linear systems}, - author={Geromel, Jos{\'e} C and Colaneri, Patrizio}, - journal={SIAM Journal on Control and Optimization}, - volume={45}, - number={5}, - pages={1915--1930}, - year={2006}, - publisher={SIAM} -} - -@book{liberzon2003switching, - title={Switching in systems and control}, - author={Liberzon, Daniel}, - year={2003}, - publisher={Birkh{\"a}user Boston} -} - -@article{branicky1998multiple, - title={Multiple Lyapunov functions and other analysis tools for switched and hybrid systems}, - author={Branicky, Michael S}, - journal={IEEE Transactions on Automatic Control}, - volume={43}, - number={4}, - pages={475--482}, - year={1998}, - publisher={IEEE} -} - -% Recent Advances (2020-2025) - -@article{yang2024learning, - title={Learning Local Control Barrier Functions for Hybrid Systems}, - author={Yang, Shuo and Chen, Yiwei and Yin, Xiang and Mangharam, Rahul}, - journal={arXiv preprint arXiv:2401.14907}, - year={2024} -} - -@inproceedings{su2024switching, - title={Switching Controller Synthesis for Hybrid Systems Against STL Formulas}, - author={Su, Mingyu and Vizel, Yakir and Vardi, Moshe Y}, - booktitle={International Symposium on Formal Methods}, - pages={231--248}, - year={2024}, - publisher={Springer} -} - -@article{yao2024model, - title={Model predictive control of stochastic hybrid systems with signal temporal logic constraints}, - author={Yao, Li and Wang, Yiming and Chen, Xiang}, - journal={Automatica}, - volume={159}, - pages={111037}, - year={2024}, - publisher={Elsevier} -} - -@article{yu2024online, - title={Online control synthesis for uncertain systems under signal temporal logic specifications}, - author={Yu, Pian and Gao, Yulong and Jiang, Frank J and Johansson, Karl H and Dimarogonas, Dimos V}, - journal={The International Journal of Robotics Research}, - volume={43}, - number={3}, - pages={284--307}, - year={2024}, - publisher={SAGE} -} - -% Tools and Frameworks - -@inproceedings{meyer2018strix, - title={Strix: Explicit reactive synthesis strikes back!}, - author={Meyer, Philipp J and Luttenberger, Michael}, - booktitle={International Conference on Computer Aided Verification}, - pages={578--586}, - year={2018}, - publisher={Springer} -} - -@techreport{giannakopoulou2022fret, - title={Capturing and Analyzing Requirements with FRET}, - author={Giannakopoulou, Dimitra and Mavridou, Anastasia and Rhein, Julian and Pressburger, Thomas and Schumann, Johann and Shi, Nija}, - institution={NASA Ames Research Center}, - year={2022}, - number={NASA/TM-20220007610} -} - -@inproceedings{fulton2015keymaera, - title={KeYmaera X: An axiomatic tactical theorem prover for hybrid systems}, - author={Fulton, Nathan and Mitsch, Stefan and Quesel, Jan-David and V{\"o}lp, Marcus and Platzer, Andr{\'e}}, - booktitle={International Conference on Automated Deduction}, - pages={527--538}, - year={2015}, - publisher={Springer} -} - -@inproceedings{frehse2011spaceex, - title={SpaceEx: Scalable verification of hybrid systems}, - author={Frehse, Goran and Le Guernic, Colas and Donz{\'e}, Alexandre and Cotton, Scott and Ray, Rajarshi and Lebeltel, Olivier and Ripado, Rodolfo and Girard, Antoine and Dang, Thao and Maler, Oded}, - booktitle={International Conference on Computer Aided Verification}, - pages={379--395}, - year={2011}, - publisher={Springer} -} - -@inproceedings{chen2013flow, - title={Flow*: An analyzer for non-linear hybrid systems}, - author={Chen, Xin and {\'A}brah{\'a}m, Erika and Sankaranarayanan, Sriram}, - booktitle={International Conference on Computer Aided Verification}, - pages={258--263}, - year={2013}, - publisher={Springer} -} - -@inproceedings{larsen1997uppaal, - title={UPPAAL in a nutshell}, - author={Larsen, Kim G and Pettersson, Paul and Yi, Wang}, - journal={International Journal on Software Tools for Technology Transfer}, - volume={1}, - number={1-2}, - pages={134--152}, - year={1997}, - publisher={Springer} -} - -% Reachability and Verification - - -@INPROCEEDINGS{bansal2017hamilton, - author={Bansal, Somil and Chen, Mo and Herbert, Sylvia and Tomlin, Claire J.}, - booktitle={2017 IEEE 56th Annual Conference on Decision and Control (CDC)}, - title={Hamilton-Jacobi reachability: A brief overview and recent advances}, - year={2017}, - volume={}, - pages={2242-2253}, - keywords={Games;Safety;Tools;Trajectory;Tutorials;Level set;Aircraft}, - doi={10.1109/CDC.2017.8263977} -} - -@article{althoff2021set, - title={Set propagation techniques for reachability analysis}, - author={Althoff, Matthias and Frehse, Goran and Girard, Antoine}, - journal={Annual Review of Control, Robotics, and Autonomous Systems}, - volume={4}, - pages={369--395}, - year={2021}, - publisher={Annual Reviews} -} - -@inproceedings{tabuada2004compositional, - title={Compositional abstractions of hybrid control systems}, - author={Tabuada, Paulo and Pappas, George J and Lima, Pedro}, - journal={Discrete Event Dynamic Systems}, - volume={14}, - number={2}, - pages={203--238}, - year={2004}, - publisher={Springer} -} - -% Applications - -@article{varaiya1993smart, - title={Smart cars on smart roads: Problems of control}, - author={Varaiya, Pravin}, - journal={IEEE Transactions on Automatic Control}, - volume={38}, - number={2}, - pages={195--207}, - year={1993}, - publisher={IEEE} -} - -@article{verlinden2024hybrid, - title={Hybrid reliability modeling of nuclear safety systems: A case study on the reactor protection system of a research reactor}, - author={Verlinden, S and Deridder, F and Wagemans, P}, - journal={Nuclear Engineering and Design}, - volume={417}, - pages={112868}, - year={2024}, - publisher={Elsevier} -} - -% Competitions and Benchmarks - -@inproceedings{hscc2024proceedings, - title={Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control}, - booktitle={HSCC '24}, - year={2024}, - publisher={ACM}, - address={New York, NY, USA} -} - -@inproceedings{jacobs2017syntcomp, - title={The 4th reactive synthesis competition (SYNTCOMP 2017): Benchmarks, participants \& results}, - author={Jacobs, Swen and Bloem, Roderick and Brenguier, Romain and others}, - booktitle={6th Workshop on Synthesis}, - year={2017}, - series={EPTCS}, - volume={260} -} - -% Supporting Papers - -@article{wabersich2018linear, - title={Linear model predictive safety certification for learning-based control}, - author={Wabersich, Kim P and Zeilinger, Melanie N}, - journal={Automatica}, - volume={97}, - pages={48--59}, - year={2018}, - publisher={Elsevier} -} - -@inproceedings{prajna2004safety, - title={Safety verification of hybrid systems using barrier certificates}, - author={Prajna, Stephen and Jadbabaie, Ali}, - booktitle={International Workshop on Hybrid Systems: Computation and Control}, - pages={477--492}, - year={2004}, - publisher={Springer} -} - -@article{ames2017control, - title={Control barrier function based quadratic programs for safety critical systems}, - author={Ames, Aaron D and Xu, Xiangru and Grizzle, Jessy W and Tabuada, Paulo}, - journal={IEEE Transactions on Automatic Control}, - volume={62}, - number={8}, - pages={3861--3876}, - year={2017}, - publisher={IEEE} -} - -@article{srinivasan2018control, - title={Control of mobile robots using barrier functions under temporal logic specifications}, - author={Srinivasan, Mohit and Coogan, Samuel}, - journal={IEEE Transactions on Robotics}, - volume={37}, - number={2}, - pages={363--374}, - year={2021}, - publisher={IEEE} -} - -%broader impacts -@techreport{eia_lcoe_2022, - author = {{U.S. Energy Information Administration}}, - title = {Levelized Costs of New Generation Resources in the Annual Energy Outlook 2022}, - institution = {U.S. Energy Information Administration}, - year = {2022}, - month = {March}, - type = {Report}, - url = {https://www.eia.gov/outlooks/aeo/pdf/electricity_generation.pdf}, - note = {See Table 1b, page 9} -} - -@misc{eesi_datacenter_2024, - author = {{Environmental and Energy Study Institute}}, - title = {Data Center Energy Needs Are Upending Power Grids and Threatening the Climate}, - howpublished = {Web article}, - year = {2024}, - url = {https://www.eesi.org/articles/view/data-center-energy-needs-are-upending-power-grids-and-threatening-the-climate}, - note = {Accessed: 2025-09-29} -} -@techreport{DOE-HDBK-1028-2009, - title = {Human Performance Handbook}, - author = {{U.S. Department of Energy}}, - institution = {U.S. Department of Energy}, - year = {2009}, - number = {DOE-HDBK-1028-2009}, - type = {Handbook} -} - -@misc{WNA2020, - title = {Safety of Nuclear Power Reactors}, - author = {{World Nuclear Association}}, - year = {2020}, - howpublished = {\url{https://www.world-nuclear.org/information-library/safety-and-security/safety-of-plants/safety-of-nuclear-power-reactors.aspx}} -} - -@article{Wang2025, - title = {Analysis of Human Error in Nuclear Power Plant Operations: A Systematic Review of Events from 2007--2020}, - author = {Wang, Y. and others}, - journal = {Journal of Nuclear Safety}, - year = {2025}, - note = {Analysis of 190 events at Chinese nuclear power plants} -} - -@misc{10CFR55, - title = {Operators' Licenses}, - author = {{U.S. Nuclear Regulatory Commission}}, - howpublished = {10 CFR Part 55}, - note = {Code of Federal Regulations} -} - -@techreport{Kemeny1979, - title = {Report of the President's Commission on the Accident at Three Mile Island}, - author = {Kemeny, John G. and others}, - institution = {President's Commission on the Accident at Three Mile Island}, - year = {1979}, - month = {October} -} - -@misc{10CFR50, - title = {Domestic Licensing of Production and Utilization Facilities}, - author = {{U.S. Nuclear Regulatory Commission}}, - howpublished = {10 CFR Part 50}, - note = {Code of Federal Regulations} -} - -@techreport{NUREG-0899, - title = {Guidelines for the Preparation of Emergency Operating Procedures}, - author = {{U.S. Nuclear Regulatory Commission}}, - institution = {U.S. Nuclear Regulatory Commission}, - year = {1982}, - number = {NUREG-0899} -} - -@techreport{IAEA-TECDOC-1580, - title = {Good Practices for Cost Effective Maintenance of Nuclear Power Plants}, - author = {{International Atomic Energy Agency}}, - institution = {International Atomic Energy Agency}, - year = {2007}, - number = {TECDOC-1580} -} - -@techreport{NUREG-2114, - title = {Cognitive Basis for Human Reliability Analysis}, - author = {{U.S. Nuclear Regulatory Commission}}, - institution = {U.S. Nuclear Regulatory Commission}, - year = {2016}, - number = {NUREG-2114} -} - -@article{Zerovnik2023, - title = {Knowledge Transfer Challenges in Nuclear Operations}, - author = {\v{Z}erovnik, Gašper and others}, - journal = {Nuclear Engineering and Design}, - year = {2023}, - note = {Analysis of knowledge transfer from experienced operators} -} - -@article{Jo2021, - title = {Automation Paradox in Nuclear Power Plant Control: Effects on Operator Situation Awareness}, - author = {Jo, Y. and others}, - journal = {Nuclear Engineering and Technology}, - year = {2021}, - note = {Empirical study of automation effects on operator performance} -} - -@techreport{IAEA2008, - title = {Modern Instrumentation and Control for Nuclear Power Plants: A Guidebook}, - author = {{International Atomic Energy Agency}}, - institution = {International Atomic Energy Agency}, - year = {2008}, - number = {Technical Reports Series No. 387} -} - -@article{Lee2019, - title = {Autonomous Control of Nuclear Reactors Using Long Short-Term Memory Networks}, - author = {Lee, D. and others}, - journal = {Nuclear Engineering and Technology}, - year = {2019}, - note = {Demonstration of LSTM-based autonomous control in LOC and SGTR scenarios} -} - -@inproceedings{IEEE2019, - title = {Formal Verification Challenges for Nuclear I\&C Systems}, - author = {{IEEE Working Group}}, - booktitle = {IEEE Conference on Nuclear Power Instrumentation, Control and Human-Machine Interface Technologies}, - year = {2019}, - note = {Discussion of state space explosion in formal verification} -} - -@misc{IAEA-severe-accidents, - title = {Human Error as Root Cause in Severe Nuclear Accidents}, - author = {{International Atomic Energy Agency}}, - howpublished = {IAEA Safety Report}, - note = {Analysis of TMI, Chernobyl, and Fukushima accidents} -} - -@article{Dumas1999, - title = {Worker Error and Safety in Nuclear Facilities}, - author = {Dumas, Lloyd}, - journal = {Journal of Nuclear Safety}, - year = {1999}, - note = {Study of incidents at 10 nuclear centers} -} - -@techreport{IAEA-INSAG-1, - title = {Summary Report on the Post-Accident Review Meeting on the Chernobyl Accident}, - author = {{International Nuclear Safety Advisory Group}}, - institution = {International Atomic Energy Agency}, - year = {1986}, - number = {INSAG-1} -} - -@techreport{IAEA-INSAG-7, - title = {The Chernobyl Accident: Updating of INSAG-1}, - author = {{International Nuclear Safety Advisory Group}}, - institution = {International Atomic Energy Agency}, - year = {1992}, - number = {INSAG-7} -} - -@techreport{NUREG-CR-1278, - title = {Handbook of Human Reliability Analysis with Emphasis on Nuclear Power Plant Applications (THERP)}, - author = {Swain, A. D. and Guttmann, H. E.}, - institution = {U.S. Nuclear Regulatory Commission}, - year = {1983}, - number = {NUREG/CR-1278} -} - -@techreport{NUREG-CR-6883, - title = {The SPAR-H Human Reliability Analysis Method}, - author = {Gertman, D. and others}, - institution = {U.S. Nuclear Regulatory Commission}, - year = {2005}, - number = {NUREG/CR-6883} -} - -@techreport{NUREG-2127, - title = {International HRA Empirical Study: Phase 1 Report}, - author = {{U.S. Nuclear Regulatory Commission}}, - institution = {U.S. Nuclear Regulatory Commission}, - year = {2013}, - number = {NUREG-2127} -} - -@article{Rasmussen1983, - title = {Skills, Rules, and Knowledge; Signals, Signs, and Symbols, and Other Distinctions in Human Performance Models}, - author = {Rasmussen, J.}, - journal = {IEEE Transactions on Systems, Man, and Cybernetics}, - year = {1983}, - volume = {SMC-13}, - number = {3}, - pages = {257--266} -} - -@article{Miller1956, - title = {The Magical Number Seven, Plus or Minus Two: Some Limits on Our Capacity for Processing Information}, - author = {Miller, George A.}, - journal = {Psychological Review}, - year = {1956}, - volume = {63}, - number = {2}, - pages = {81--97} -} - -@techreport{NUREG-2256, - title = {Integrated Human Event Analysis System for Emergency Crew Actions (IDHEAS-ECA)}, - author = {{U.S. Nuclear Regulatory Commission}}, - institution = {U.S. Nuclear Regulatory Commission}, - year = {2022}, - number = {NUREG-2256} -} - -@book{Reason1990, - title = {Human Error}, - author = {Reason, James}, - publisher = {Cambridge University Press}, - year = {1990} -} - -@article{Lee2018, - title = {Deep Reinforcement Learning for Autonomous Nuclear Reactor Control}, - author = {Lee, D. and others}, - journal = {Nuclear Engineering and Design}, - year = {2018}, - note = {Demonstration of autonomous control superior to human-plus-automation} -} - -@techreport{Kiniry2022, - title = {High Assurance Rigorous Digital Engineering for Nuclear Safety (HARDENS) Final Technical Report}, - author = {Kiniry, Joseph and Bakst, Alexander and Podhradsky, Michal and Hansen, Simon and Bivin, Andrew}, - institution = {Galois, Inc. / U.S. Nuclear Regulatory Commission}, - year = {2022}, - number = {ML22326A307}, - note = {NRC Contract 31310021C0014} -} diff --git a/Writing/THESIS_PROPOSAL/sabo-quad-chart.pdf b/Writing/THESIS_PROPOSAL/sabo-quad-chart.pdf deleted file mode 100644 index 9b0dcf5e7..000000000 Binary files a/Writing/THESIS_PROPOSAL/sabo-quad-chart.pdf and /dev/null differ diff --git a/Writing/THESIS_PROPOSAL/sabo_broader_impacts.pdf b/Writing/THESIS_PROPOSAL/sabo_broader_impacts.pdf deleted file mode 100644 index 0af15f610..000000000 Binary files a/Writing/THESIS_PROPOSAL/sabo_broader_impacts.pdf and /dev/null differ diff --git a/Writing/THESIS_PROPOSAL/sabo_research_approach.pdf b/Writing/THESIS_PROPOSAL/sabo_research_approach.pdf deleted file mode 100644 index cae84d584..000000000 Binary files a/Writing/THESIS_PROPOSAL/sabo_research_approach.pdf and /dev/null differ diff --git a/Writing/THESIS_PROPOSAL/sabodaneSOTA-v1.pdf b/Writing/THESIS_PROPOSAL/sabodaneSOTA-v1.pdf deleted file mode 100644 index f13b6b95a..000000000 Binary files a/Writing/THESIS_PROPOSAL/sabodaneSOTA-v1.pdf and /dev/null differ diff --git a/Writing/THESIS_PROPOSAL/whitepaper/v1.tex b/Writing/THESIS_PROPOSAL/whitepaper/v1.tex deleted file mode 100644 index 123e167e4..000000000 --- a/Writing/THESIS_PROPOSAL/whitepaper/v1.tex +++ /dev/null @@ -1,421 +0,0 @@ -% PROJECT SUMMARY -\section*{Project Summary} - -\subsection*{Overview} - -This research will develop a methodology for creating autonomous hybrid control -systems with mathematical guarantees of safe and correct behavior. Nuclear power -plants require the highest levels of control system reliability, where failures -can result in significant economic losses or radiological release. Currently, -nuclear operations rely on extensively trained human operators who follow -detailed written procedures to manage reactor control. However, reliance on -human operators prevents introduction of autonomous control capabilities and -creates fundamental economic challenges for next-generation reactor designs. -Without introducing automation, emerging technologies like small modular -reactors face significantly higher per-megawatt staffing costs than conventional -plants, threatening their economic viability. - -To address this need, we will combine formal methods from computer science -with control theory to build hybrid control systems that are correct by -construction. Hybrid systems use discrete logic to switch between continuous -control modes, similar to how operators change control strategies. Existing -formal methods can generate provably correct switching logic from written -requirements, but they cannot handle the continuous dynamics that occur during -transitions between modes. Meanwhile, traditional control theory can verify -continuous behavior but lacks tools for proving correctness of discrete -switching decisions. By synthesizing discrete mode transitions directly from -written operating procedures and verifying continuous behavior between -transitions, we can create hybrid control systems with end-to-end correctness -guarantees. - -\subsection*{Intellectual Merit} - -The intellectual merit lies in unifying discrete synthesis and continuous -verification to enable end-to-end correctness guarantees for hybrid systems. -This research will advance knowledge by developing a systematic, -tool-supported methodology for translating written procedures into temporal -logic, synthesizing provably correct discrete switching logic, and developing -verified continuous controllers. The approach addresses a fundamental gap in -hybrid system design by bridging formal methods from computer science and -control theory. - -\subsection*{Broader Impacts} - -This research directly addresses the multi-billion dollar operations and -maintenance cost challenge facing nuclear power deployment. By synthesizing -provably correct hybrid controllers, we can automate routine operational -sequences that currently require constant human oversight, enabling a shift -from direct operator control to supervisory monitoring. Beyond nuclear -applications, this research will establish a generalizable framework for -autonomous control of safety-critical systems including chemical process -control, aerospace systems, and autonomous transportation. - -\newpage - -% RESEARCH DESCRIPTION -\section*{Research Description} - -\section{Objectives} -% GOAL PARAGRAPH -The goal of this research is to develop a methodology for creating autonomous -control systems with event-driven control laws that have guarantees of safe and -correct behavior. - -% INTRODUCTORY PARAGRAPH Hook -Nuclear power relies on extensively trained operators who follow detailed -written procedures to manage reactor control. Based on these procedures and -operators' interpretation of plant conditions, operators make critical decisions -about when to switch between control objectives. -% Gap -While human operators have maintained the nuclear industry's exceptional safety -record, reliance on human operators has created an economic challenge for -next-generation nuclear power plants. Small modular reactors face significantly -higher per-megawatt staffing costs than conventional plants, threatening their -economic viability. Autonomous control systems are needed that can safely manage -complex operational sequences with the same assurance as human-operated systems, -but without constant supervision. - -% APPROACH PARAGRAPH Solution -To address this need, we will combine formal methods from computer science with -control theory to build hybrid control systems that are correct by construction. -% Rationale -Hybrid systems use discrete logic to switch between continuous control modes, -similar to how operators change control strategies. Existing formal methods -generate provably correct switching logic but cannot handle continuous dynamics -during transitions, while traditional control theory verifies continuous -behavior but lacks tools for proving discrete switching correctness. -% Hypothesis and Technical Approach -We will bridge this gap through a three-stage methodology. First, we will -translate written operating procedures into temporal logic specifications using -NASA's Formal Requirements Elicitation Tool (FRET), which structures -requirements into scope, condition, component, timing, and response elements. -This structured approach enables realizability checking to identify conflicts -and ambiguities in procedures before implementation. Second, we will synthesize -discrete mode switching logic from these specifications using reactive synthesis -tools such as Strix, which generates deterministic automata that are provably -correct by construction. Third, we will develop and verify continuous -controllers for each discrete mode using standard control theory and -reachability analysis. We will classify continuous modes based on their -transition objectives, and then employ assume-guarantee contracts and barrier -certificates to prove that mode transitions occur safely and as defined by the -deterministic automata. This compositional approach enables local verification -of continuous modes without requiring global trajectory analysis across the -entire hybrid system. We will demonstrate this methodology by developing an -autonomous startup controller for a Small Modular Advanced High Temperature -Reactor (SmAHTR) and implementing it on an Emerson Ovation control system using -the ARCADE hardware-in-the-loop platform. -% Pay-off -This approach will demonstrate autonomous control can be used for complex -nuclear power operations while maintaining safety guarantees. - -\vspace{11pt} - -% OUTCOMES PARAGRAPHS -If this research is successful, we will be able to do the following: -\begin{enumerate} - % OUTCOME 1 Title - \item \textit{Synthesize written procedures into verified control logic.} - % Strategy - We will develop a methodology for converting written operating procedures - into formal specifications. These specifications will be synthesized into - discrete control logic using reactive synthesis tools. This process uses - structured intermediate representations to bridge natural language and - mathematical logic. - % Outcome - Control engineers will be able to generate mode-switching controllers from - regulatory procedures with little formal methods expertise, reducing - barriers to high-assurance control systems. - - % OUTCOME 2 Title - \item \textit{Verify continuous control behavior across mode transitions. } - % Strategy - We will develop methods using reachability analysis to ensure continuous control modes - satisfy discrete transition requirements. - % Outcome - Engineers will be able to design continuous controllers using standard - practices while ensuring system correctness and proving mode transitions - occur safely at the right times. - - % OUTCOME 3 Title - \item \textit{Demonstrate autonomous reactor startup control with safety - guarantees. } - % Strategy - We will implement this methodology on a small modular reactor simulation - using industry-standard control hardware. This trial will include multiple - coordinated control modes from cold shutdown through criticality to power - operation on a SmAHTR reactor simulation in a hardware-in-the-loop - experiment. - % Outcome - Control engineers will be able to implement high-assurance autonomous - controls on industrial platforms they already use, enabling users to - achieve autonomy without retraining costs or developing new equipment. - -\end{enumerate} -\section{State of the Art and Limits of Current Practice} - -Automation of some nuclear power operations is already performed today. Highly -automated systems handle reactor protection and emergency core cooling, while -human operators retain strategic decision-making. Autonomous systems are trusted -to handle emergency situations that are considered terminal operations, but -otherwise introduce too much risk to reactor operations. Contrary to this notion -is the fact that 70--80\% of all nuclear power plant events are attributed to -human error rather than equipment failures. The persistence of this ratio despite -four decades of improvements to procedures and control rooms suggests -fundamental cognitive limitations rather than remediable deficiencies. - -The Nuclear Regulatory Commission has recognized that introducing automation -into the control room is the only way forward. Recent efforts to apply formal -methods to nuclear control have shown both promise and remaining gaps. The High -Assurance Rigorous Digital Engineering for Nuclear Safety (HARDENS) project -represents the most advanced application to date. HARDENS produced a complete -Reactor Trip System with full traceability from NRC requirements through formal -specifications to verified binaries of a controller implementation. The project -employed formal methods along the control design stack. This comprehensive -approach demonstrated that formal methods may be technically feasible and -economically viable for nuclear protection systems. - -But despite these accomplishments, HARDENS has a fundamental limitation directly -relevant to our work. The project addressed only discrete digital control logic -without modeling or verifying continuous reactor dynamics. Real reactor safety -depends on interaction between continuous processes and discrete control -decisions. HARDENS verified the discrete controller in isolation but not the -closed-loop hybrid system behavior. - -\section{Research Approach} - -This research will overcome the identified limitations by combining formal -methods from computer science with control theory to build hybrid control -systems that are correct by construction. We accomplish this through three -main thrusts: - -\begin{enumerate} - - \item We will translate natural language procedures and - requirements into temporal logic specifications using the Formal Requirements - Elicitation Tool (FRET). - - \item We will synthesize these temporal logic - specifications into the discrete component of the hybrid controller using - reactive synthesis. - - \item We will build continuous control modes that satisfy discrete controller - transition requirements. - -\end{enumerate} - -Commercial nuclear power operations remain manually controlled despite -significant advances in control systems. The key insight is that procedures -performed by human operators are highly prescriptive and well-documented. To -formalize these procedures, we will use temporal logic, which captures system -behaviors through temporal relations. Linear Temporal Logic provides four -fundamental operators: next ($X$), eventually ($F$), globally ($G$), and until -($U$). These operators enable precise specification of time-dependent -requirements. The most efficient path to accomplish this translation is through -NASA's Formal Requirements Elicitation Tool (FRET). FRET employs FRETish, a -specialized requirements language that restricts requirements to easily -understood components while eliminating ambiguity. FRET enforces structure by -requiring all requirements to contain six components: Scope, Condition, -Component, Shall, Timing, and Response. - -FRET provides functionality to check realizability of a system. Realizability -analysis determines whether written requirements are complete by examining the -six structural components. Complete requirements neither conflict with one -another nor leave any behavior undefined. Systems that are not realizable -contain behavioral inconsistencies that represent the physical equivalent of -software bugs. Using FRET during autonomous controller development allows us -to identify and resolve these errors systematically. FRET exports requirements -in temporal logic format compatible with reactive synthesis tools, enabling -the second thrust of our approach. - -Reactive synthesis is an active research field focused on generating discrete -controllers from temporal logic specifications. The term reactive indicates -that the system responds to environmental inputs to produce control outputs. -These synthesized systems are finite in size, where each node represents a -unique discrete state. The connections between nodes, called state -transitions, specify the conditions under which the discrete controller moves -from state to state. This complete mapping constitutes a discrete automaton. - -We will employ reactive synthesis tools which translate linear temporal logic -specifications into deterministic automata automatically while maximizing -generated automata quality. Once constructed, the automaton can be -straightforwardly implemented using standard programming control flow -constructs. The discrete automata representation yields an important theoretical -guarantee. Because the discrete automaton is synthesized entirely through -automated tools from design requirements and operating procedures, we can -prove that the automaton---and therefore our hybrid switching behavior---is -correct by construction. - -This correctness guarantee is paramount. Mode switching represents the primary -responsibility of human operators in control rooms today. Human operators -possess the advantage of real-time judgment. When mistakes occur, they can -correct them dynamically. Autonomous control lacks this adaptive advantage. By -synthesizing controllers from logical specifications with guaranteed -correctness, we eliminate the possibility of switching errors. - -While discrete system components will be synthesized with correctness -guarantees, they represent only half of the complete system. The continuous -modes will be developed after discrete automaton construction, leveraging the -automaton structure and transitions to design multiple smaller, specialized -continuous controllers. - -The discrete automaton transitions mark decision points for switching between -continuous control modes and define their strategic objectives. We will -classify three types of high-level continuous controller objectives: -Stabilizing modes maintain the hybrid system within its current discrete mode, -corresponding to steady-state normal operating modes like full-power -load-following control. Transitory modes have the primary goal of -transitioning the hybrid system from one discrete state to another, such as -controlled warm-up procedures. Expulsory modes are specialized transitory -modes with additional safety constraints that ensure the system is directed to -a safe stabilizing mode during failure conditions, such as reactor SCRAM. - -Building continuous modes after constructing discrete automata enables local -controller design focused on satisfying discrete transitions. The primary -challenge in hybrid system verification is ensuring global stability across -transitions. Current techniques struggle with this problem because dynamic -discontinuities complicate verification. This work alleviates these problems -by designing continuous controllers specifically with transitions in mind. By -decomposing continuous modes according to their required behavior at -transition points, we avoid solving trajectories through the entire hybrid -system. - -To ensure continuous modes satisfy their requirements, we will employ three -complementary techniques. Reachability analysis computes the reachable set of -states for a given input set. We will use reachability when continuous -state ranges at discrete transition boundaries are defined and verify that -continuous modes only can reach such defined ranges. Otherwise, assume-guarantee contracts will be -employed when continuous state boundaries are not explicitly defined. For any -given mode, the input range for reachability analysis is defined by the output -ranges of discrete modes that transition to it. This compositional approach -ensures each continuous controller is prepared for its possible input range. -Finally, barrier certificates will prove that mode transitions are satisfied. Control -barrier functions provide a method to certify safety by establishing -differential inequality conditions that guarantee forward invariance of safe -sets. - -Combining these three techniques will enable us to prove that continuous -components satisfy discrete requirements and thus complete system behavior. To -demonstrate this methodology, we will develop an autonomous startup controller -for a Small Modular Advanced High Temperature Reactor (SmAHTR). SmAHTR -represents an ideal test case with well-documented startup procedures that -must transition through multiple distinct operational modes: initial cold -conditions, controlled heating to operating temperature, approach to -criticality, low-power physics testing, and power ascension to full operating -capacity. We have access to an already developed high-fidelity SmAHTR model in Simulink that -captures the thermal-hydraulic and neutron kinetics behavior. - -The synthesized hybrid controller will be implemented on an Emerson Ovation -control system platform, which is representative of industry-standard control -hardware. This control system will be used in a hardware-in-the-loop simulation, -where the Advanced Reactor Cyber Analysis and Development Environment -(ARCADE) suite will serve as the integration layer. This -hardware-in-the-loop configuration enables validation of the controller -implementation on actual industrial control equipment. - -\section{Metrics of Success} - -This research will be measured by advancement through Technology Readiness -Levels, progressing from fundamental concepts to validated prototype -demonstration. The work begins at TRL 2--3 and aims to reach TRL 5, where system -components operate successfully in a relevant laboratory environment. TRLs -provide the ideal success metric because they explicitly measure the gap between -academic proof-of-concept and practical deployment. This gap is precisely what -our work aims to bridge. TRLs capture both theoretical rigor and practical -feasibility simultaneously. The nuclear industry already uses TRLs for -technology assessment, making this metric directly relevant to potential -adopters. - -Moving from current state (TRL 2--3) to target (TRL 5) requires progressing -through component isolation, system integration, and hardware validation. By -reaching TRL 5, we will have demonstrated a complete autonomous hybrid -controller operating on industrial control hardware through hardware-in-the-loop -testing. Achieving TRL 5 establishes both theoretical validity and practical -feasibility, proving that the methodology produces verified controllers -implementable with current technology and providing a clear pathway for nuclear -industry adoption and broader application to safety-critical autonomous systems. - -\section{Broader Impacts} - -Nuclear power presents both a compelling application domain and an urgent -economic challenge. Recent interest in powering artificial intelligence -infrastructure has renewed focus on small modular reactors for hyperscale -datacenters. According to the U.S. Energy Information Administration, advanced -nuclear power entering service in 2027 is projected to cost \$88.24 per -megawatt-hour. With datacenter electricity demand projected to reach 1,050 -terawatt-hours annually by 2030, operations and maintenance costs represent -approximately 23--30\% of total levelized cost, translating to \$21--28 -billion annually for projected datacenter demand. - -This research directly addresses the multi-billion dollar O\&M cost challenge. -Current nuclear operations require full control room staffing for each reactor. -These staffing requirements drive high O\&M costs, particularly for smaller -reactor designs where the same overhead must be spread across lower power -output. The economic burden threatens the viability of next-generation nuclear -technologies. But, by synthesizing provably correct hybrid controllers, we can -automate routine operational sequences that currently require constant human -oversight. This enables a change from direct operator control to -supervisory monitoring where operators oversee multiple autonomous reactors -rather than manually controlling individual units. The transition fundamentally -changes the economics of nuclear operations. - -The correct-by-construction methodology is critical for this transition. -Traditional automation approaches cannot provide sufficient safety guarantees -for nuclear applications where regulatory requirements and public safety -concerns demand the highest levels of assurance. By formally verifying both -discrete mode-switching logic and continuous control behavior, this research -will produce controllers with mathematical proofs of correctness. These -guarantees enable automation to safely handle routine operations that -currently require human operators to follow written procedures. - -Beyond nuclear applications, this research will establish a generalizable -framework for autonomous control of safety-critical systems. The methodology of -translating operational procedures into formal specifications, synthesizing -discrete switching logic, and verifying continuous mode behavior applies to any -hybrid system with documented operational requirements. Potential applications -include chemical process control, aerospace systems, and autonomous -transportation. These domains share similar economic and safety considerations -that favor increased autonomy with provable correctness guarantees. By -demonstrating this approach in nuclear power this research will establish both -technical feasibility and regulatory pathways for broader adoption across -critical infrastructure. - -\newpage - -% REFERENCES CITED - -\begin{thebibliography}{99} - -\bibitem{10CFR55} -U.S. Nuclear Regulatory Commission. ``10 CFR Part 55 - Operators' Licenses.'' -\textit{Code of Federal Regulations}, 2024. - -\bibitem{Kemeny1979} -J. G. Kemeny et al. ``Report of the President's Commission on the Accident -at Three Mile Island.'' U.S. Government Printing Office, October 1979. - -\bibitem{NUREG-0899} -U.S. Nuclear Regulatory Commission. ``Guidelines for the Preparation of -Emergency Operating Procedures.'' NUREG-0899, August 1982. - -\bibitem{DOE-HDBK-1028-2009} -U.S. Department of Energy. ``Human Performance Improvement Handbook.'' -DOE-HDBK-1028-2009, June 2009. - -\bibitem{WNA2020} -World Nuclear Association. ``Safety of Nuclear Power Reactors.'' -\textit{World Nuclear Association Information Library}, 2020. - -\bibitem{Kiniry2022} -J. Kiniry et al. ``High Assurance Rigorous Digital Engineering for Nuclear -Safety (HARDENS).'' NRC Final Technical Report ML22326A307, October 2022. - -\bibitem{eia_lcoe_2022} -U.S. Energy Information Administration. ``Levelized Costs of New Generation -Resources in the Annual Energy Outlook 2022.'' Report, March 2022. - -\bibitem{eesi_datacenter_2024} -Environmental and Energy Study Institute. ``Data Center Energy Needs are -Upending Power Grids and Threatening the Climate.'' Web article, 2024. - -\end{thebibliography} -