vault backup: 2025-12-17 15:52:19

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":[]
+}

Writing/THESIS_PROPOSAL/ERLM-Proposal-Review-Summary.md

@@ -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!

Writing/THESIS_PROPOSAL/references_old.bib

@@ -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}
-}

Writing/THESIS_PROPOSAL/whitepaper/v1.tex

@@ -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}
-