diff --git a/1-goals-and-outcomes/research_statement_v1.tex b/1-goals-and-outcomes/research_statement_v1.tex index 18d2d6a..b00503d 100644 --- a/1-goals-and-outcomes/research_statement_v1.tex +++ b/1-goals-and-outcomes/research_statement_v1.tex @@ -4,14 +4,14 @@ I develop autonomous control systems with mathematical guarantees of safe and co % INTRODUCTORY PARAGRAPH Hook Nuclear reactors today depend on extensively trained human operators who follow detailed written procedures and switch between control objectives as plant conditions change. % Gap -Small modular reactors face a fundamental economic challenge: their per-megawatt staffing costs significantly exceed those of conventional plants, threatening economic viability. Autonomous control could manage complex operational sequences without constant supervision—but only with safety assurance equal to or exceeding human operators. +Small modular reactors face a fundamental economic challenge: their per-megawatt staffing costs significantly exceed those of conventional plants, threatening economic viability. Autonomous control could manage complex operational sequences without constant supervision—but only if it provides safety assurance equal to or exceeding that of human operators. % APPROACH PARAGRAPH Solution I produce hybrid control systems correct by construction, unifying formal methods from computer science with control theory. % Rationale -Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic but cannot handle continuous dynamics. Control theory verifies continuous behavior but cannot prove discrete switching correctness. Both must work together to achieve end-to-end correctness. +Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic but cannot handle continuous dynamics. Control theory verifies continuous behavior but cannot prove discrete switching correctness. End-to-end correctness requires both working together. % Hypothesis and Technical Approach -Three stages bridge this gap. First, NASA's Formal Requirements Elicitation Tool (FRET) translates written operating procedures into temporal logic specifications, structuring requirements by scope, condition, component, timing, and response. Realizability checking then exposes conflicts and ambiguities before implementation begins. Second, reactive synthesis generates deterministic automata provably correct by construction. Third, reachability analysis verifies that continuous controllers satisfy the requirements each discrete mode imposes. Engineers design these continuous controllers using standard control theory techniques. +Three stages bridge this gap. First, NASA's Formal Requirements Elicitation Tool (FRET) translates written operating procedures into temporal logic specifications, structuring requirements by scope, condition, component, timing, and response. Realizability checking exposes conflicts and ambiguities before implementation begins. Second, reactive synthesis generates deterministic automata provably correct by construction. Third, reachability analysis verifies that continuous controllers satisfy the requirements each discrete mode imposes. Engineers design these continuous controllers using standard control theory techniques. Control objectives classify continuous modes into three types. Transitory modes drive the plant between conditions. Stabilizing modes maintain operation within regions. Expulsory modes ensure safety under failures. Barrier certificates and assume-guarantee contracts prove safe mode transitions, enabling local verification without global trajectory analysis. The methodology demonstrates on an Emerson Ovation control system—the industrial platform nuclear power plants already use. % Pay-off diff --git a/1-goals-and-outcomes/v1.tex b/1-goals-and-outcomes/v1.tex index 62015b9..4642961 100644 --- a/1-goals-and-outcomes/v1.tex +++ b/1-goals-and-outcomes/v1.tex @@ -8,12 +8,12 @@ Nuclear power plants require the highest levels of control system reliability. C % Known information Nuclear plants today depend on extensively trained human operators who follow detailed written procedures and strict regulatory requirements. Operators switch between control modes based on plant conditions and procedural guidance. % Gap -This reliance on human operators prevents autonomous control and creates a fundamental economic challenge for next-generation reactor designs. Small modular reactors face per-megawatt staffing costs far exceeding those of conventional plants, threatening economic viability. Autonomous control could manage complex operational sequences without constant supervision—but only with safety assurance equal to or exceeding human operators. +This reliance on human operators prevents autonomous control and creates a fundamental economic challenge for next-generation reactor designs. Small modular reactors face per-megawatt staffing costs far exceeding those of conventional plants, threatening economic viability. Autonomous control could manage complex operational sequences without constant supervision—but only if it provides safety assurance equal to or exceeding that of human operators. % APPROACH PARAGRAPH Solution I produce hybrid control systems correct by construction, unifying formal methods with control theory. % Rationale -Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic from written requirements but cannot handle the continuous dynamics governing transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. Both approaches must work together to achieve end-to-end correctness. +Human operators already work this way: discrete logic switches between continuous control modes. Formal methods generate provably correct switching logic from written requirements but cannot handle the continuous dynamics governing transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. End-to-end correctness requires both approaches working together. % Hypothesis Two steps close this gap. First, discrete mode transitions synthesize directly from written operating procedures. Second, continuous behavior between transitions verifies against discrete requirements. This formalizes operating procedures into logical specifications that constrain continuous dynamics, producing autonomous controllers provably free from design defects. @@ -64,7 +64,7 @@ If successful, this approach produces three concrete outcomes: % IMPACT PARAGRAPH Innovation These three outcomes—procedure translation, continuous verification, and hardware demonstration—establish a complete methodology from regulatory documents to deployed systems. -\textbf{What makes this research new?} No existing methodology achieves end-to-end correctness guarantees for hybrid systems. This work unifies discrete synthesis with continuous verification through a key innovation: discrete specifications become contracts that continuous controllers must satisfy. Each layer verifies independently while guaranteeing correct composition. Formal methods verify discrete logic. Control theory verifies continuous dynamics. Section 2 examines why prior work fails at this integration and what limits current practice. Section 3 details what is new in this approach and why it will succeed. +\textbf{What makes this research new?} No existing methodology achieves end-to-end correctness guarantees for hybrid systems. This work unifies discrete synthesis with continuous verification through a key innovation: discrete specifications become contracts that continuous controllers must satisfy. Each layer verifies independently while guaranteeing correct composition—formal methods verify discrete logic, control theory verifies continuous dynamics. Section 2 examines why prior work fails at this integration and identifies the limits of current practice. Section 3 details what is new in this approach and why it will succeed. % Outcome Impact If successful, control engineers create autonomous controllers from diff --git a/2-state-of-the-art/v2.tex b/2-state-of-the-art/v2.tex index 03349b8..0318ec5 100644 --- a/2-state-of-the-art/v2.tex +++ b/2-state-of-the-art/v2.tex @@ -4,9 +4,9 @@ This section examines how nuclear reactors operate today. No current approach provides autonomous control with end-to-end correctness guarantees—neither human-centered operation nor formal methods. -Three subsections structure this analysis: first, reactor operators and their operating procedures; second, fundamental limitations of human-based operation; third, formal methods approaches that verify discrete logic or continuous dynamics but not both together. +Three subsections structure this analysis: first, reactor operators and their operating procedures; second, fundamental limitations of human-based operation; third, formal methods approaches that verify discrete logic or continuous dynamics but not both together. -These limits establish the verification gap that Section 3 addresses. +Section 3 addresses the verification gap these limits establish. \subsection{Current Reactor Procedures and Operation} @@ -14,7 +14,7 @@ Understanding the limits of current practice requires examining how nuclear plan Nuclear plant procedures form a strict hierarchy. Normal operating procedures govern routine operations. Abnormal operating procedures handle off-normal conditions. Emergency Operating Procedures (EOPs) manage design-basis accidents. Severe Accident Management Guidelines (SAMGs) address beyond-design-basis events. Extensive Damage Mitigation Guidelines (EDMGs) cover catastrophic damage. All procedures must comply with 10 CFR 50.34(b)(6)(ii); NUREG-0899 provides development guidance~\cite{NUREG-0899, 10CFR50.34}. -Procedure development relies on expert judgment and simulator validation—not formal verification. 10 CFR 55.59~\cite{10CFR55.59} requires rigorous assessment through technical evaluation, simulator validation testing, and biennial review. Yet key safety properties escape formal verification: no mathematical proofs confirm procedures cover all possible plant states, required actions complete within available timeframes, or transitions between procedure sets maintain safety invariants. +Procedure development relies on expert judgment and simulator validation—not formal verification. 10 CFR 55.59~\cite{10CFR55.59} requires rigorous assessment through technical evaluation, simulator validation testing, and biennial review. Yet key safety properties escape formal verification: no mathematical proofs confirm that procedures cover all possible plant states, that required actions complete within available timeframes, or that transitions between procedure sets maintain safety invariants. \textbf{LIMITATION:} \textit{Procedures lack formal verification of correctness and completeness.} Current procedure development relies on expert judgment and @@ -31,7 +31,7 @@ This division between automated and human-controlled functions reveals the funda \subsection{Human Factors in Nuclear Accidents} -The previous subsection established that procedures lack formal verification despite rigorous development. This represents only half the reliability challenge. Perfect procedures cannot guarantee safe operation when humans execute them imperfectly. +The previous subsection established that procedures lack formal verification despite rigorous development—but this represents only half the reliability challenge. Perfect procedures cannot guarantee safe operation when humans execute them imperfectly. Human operators—the second pillar of current practice—introduce reliability limitations independent of procedure quality. Procedures define what to do; operators determine when and how. This introduces persistent failure modes that training alone cannot eliminate. @@ -59,9 +59,9 @@ limitations are fundamental to human-driven control, not remediable defects. \subsection{Formal Methods} -The previous two subsections revealed two critical limitations of current practice. First, procedures lack formal verification despite rigorous development processes. Second, human operators introduce persistent reliability issues that four decades of training improvements have failed to eliminate. +The previous two subsections revealed two critical limitations of current practice. First, procedures lack formal verification despite rigorous development processes. Second, human operators introduce persistent reliability issues that four decades of training improvements have failed to eliminate. -Training and procedural improvements cannot solve these problems. They are fundamental limitations, not remediable defects. Formal methods might offer a solution by providing mathematical guarantees of correctness that eliminate both human error and procedural ambiguity. But can they deliver on this promise for autonomous hybrid control systems? +Training and procedural improvements cannot solve these problems—they are fundamental limitations, not remediable defects. Formal methods might offer a solution by providing mathematical guarantees of correctness that eliminate both human error and procedural ambiguity. But can they deliver on this promise for autonomous hybrid control systems? Even the most advanced formal methods applications in nuclear control leave a critical verification gap. This subsection examines two approaches illustrating this gap. HARDENS verified discrete logic without continuous dynamics. Differential dynamic logic handles hybrid verification only post-hoc. Each demonstrates the current state of formal methods while revealing the verification gap my research addresses. @@ -162,8 +162,8 @@ This section answered two Heilmeier questions: What has been done? What are the \end{itemize} No existing approach addresses both discrete and continuous verification compositionally. -\textbf{What are the limits of current practice?} No existing methodology synthesizes provably correct hybrid controllers from operational procedures with verification integrated into design. Current approaches verify either discrete logic or continuous dynamics—never both compositionally. This verification gap prevents autonomous nuclear control with end-to-end correctness guarantees. Training improvements cannot overcome human reliability limits. Post-hoc verification cannot scale to system design. +\textbf{What are the limits of current practice?} No existing methodology synthesizes provably correct hybrid controllers from operational procedures with verification integrated into design. Current approaches verify either discrete logic or continuous dynamics—never both compositionally. This verification gap prevents autonomous nuclear control with end-to-end correctness guarantees. Training improvements cannot overcome human reliability limits; post-hoc verification cannot scale to system design. -Two imperatives converge: economic necessity demands solutions (small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants), and technical opportunity enables solutions (formal methods tools have matured to enable compositional hybrid verification). +Two imperatives converge: economic necessity demands solutions, and technical opportunity enables them. Small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants. Formal methods tools have matured to enable compositional hybrid verification. Section 3 closes this verification gap by establishing what makes this approach new and why it will succeed. diff --git a/3-research-approach/v3.tex b/3-research-approach/v3.tex index b0a4d39..1145706 100644 --- a/3-research-approach/v3.tex +++ b/3-research-approach/v3.tex @@ -23,13 +23,13 @@ This section presents the complete technical approach for synthesizing provably % ---------------------------------------------------------------------------- % 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION % ---------------------------------------------------------------------------- -Previous approaches verified either discrete switching logic or continuous control behavior—never both simultaneously. Engineers validate continuous controllers through extensive simulation trials. They test discrete switching logic through simulated control room testing and human factors research. Neither method provides rigorous guarantees. Both consume enormous resources. +Previous approaches verified either discrete switching logic or continuous control behavior—never both simultaneously. Engineers validate continuous controllers through extensive simulation trials and test discrete switching logic through simulated control room testing and human factors research. Neither method provides rigorous guarantees; both consume enormous resources. -My approach bridges that gap by composing formal methods from computer science with control-theoretic verification, formalizing reactor operations as hybrid automata. +My approach bridges this gap by composing formal methods from computer science with control-theoretic verification, formalizing reactor operations as hybrid automata. Hybrid system verification faces a fundamental challenge: discrete transitions change the governing vector field, creating discontinuities through the interaction between discrete and continuous dynamics. Traditional verification techniques cannot handle this interaction directly. -This methodology decomposes the problem. It verifies discrete switching logic and continuous mode behavior separately, then composes them to establish guarantees for the complete hybrid system. This two-layer approach mirrors reactor operations: discrete supervisory logic determines which control mode is active; continuous controllers govern plant behavior within each mode. +This methodology decomposes the problem, verifying discrete switching logic and continuous mode behavior separately, then composing them to establish guarantees for the complete hybrid system. This two-layer approach mirrors reactor operations: discrete supervisory logic determines which control mode is active; continuous controllers govern plant behavior within each mode. A high-assurance hybrid autonomous control system requires a mathematical description. This work draws on automata theory, temporal logic, and control theory to provide that description. A hybrid system is a dynamical system with both continuous and discrete states. This proposal addresses continuous autonomous hybrid systems specifically—systems with no external input where continuous states remain continuous when discrete states change, representing physical quantities that remain Lipschitz continuous. This work follows the nomenclature from the Handbook on Hybrid Systems Control~\cite{HANDBOOK ON HYBRID SYSTEMS}, redefined here for convenience: @@ -56,7 +56,7 @@ where: A HAHACS requires this tuple together with proof artifacts demonstrating that the control system's actual implementation satisfies its intended behavior. -\textbf{What is new in this research?} Existing approaches verify either discrete logic or continuous dynamics—never both compositionally. Section 2 established this limitation. Reactive synthesis, reachability analysis, and barrier certificates exist independently. Prior work has not integrated them into a systematic design methodology. No prior work spans from procedures to verified implementation. +\textbf{What is new in this research?} Existing approaches verify either discrete logic or continuous dynamics—never both compositionally. Section 2 established this limitation: reactive synthesis, reachability analysis, and barrier certificates exist independently, but prior work has not integrated them into a systematic design methodology spanning from procedures to verified implementation. Three innovations enable this integration: @@ -140,11 +140,9 @@ These factors combine to demonstrate feasibility on production control systems w \subsection{System Requirements, Specifications, and Discrete Controllers} -The previous subsection established the hybrid automaton formalism—a mathematical framework describing discrete modes, continuous dynamics, guards, and invariants. +The previous subsection established the hybrid automaton formalism—a mathematical framework describing discrete modes, continuous dynamics, guards, and invariants. Where do these formal descriptions originate? -But where do these formal descriptions originate? Nuclear operations already possess a natural hybrid structure that maps directly to the automaton formalism through three control scopes: strategic, operational, and tactical. - -This approach constructs formal hybrid systems from existing operational knowledge rather than imposing artificial abstractions. It leverages decades of domain expertise already encoded in operating procedures. +Nuclear operations already possess a natural hybrid structure that maps directly to the automaton formalism through three control scopes: strategic, operational, and tactical. This approach constructs formal hybrid systems from existing operational knowledge rather than imposing artificial abstractions, leveraging decades of domain expertise already encoded in operating procedures. Human control of nuclear power divides into three scopes: strategic, operational, and tactical. Strategic control represents high-level, long-term decision making spanning months or years, managing labor needs and supply chains to optimize scheduled maintenance and downtime. @@ -260,7 +258,9 @@ FRET has been successfully applied to spacecraft control systems, autonomous veh \subsection{Discrete Controller Synthesis} -Operating procedures translate into temporal logic specifications using FRET. These specifications define what the system must do, but how do we implement those requirements? Reactive synthesis provides the answer by automatically constructing controllers guaranteed to satisfy temporal logic specifications. +Operating procedures translate into temporal logic specifications using FRET. These specifications define what the system must do—but how do we implement those requirements? + +Reactive synthesis provides the answer by automatically constructing controllers guaranteed to satisfy temporal logic specifications. Reactive synthesis automates the creation of reactive programs from temporal logic—programs that take input for a given state and produce output. System requirements defined as temporal logic specifications enable reactive synthesis to build the discrete control system. Our systems fit this model: the current discrete state and status of guard conditions form the input, while the next discrete state forms the output. @@ -530,9 +530,9 @@ Section 2 established that prior work verified either discrete logic or continuo \textbf{Why will this approach succeed?} Three factors ensure practical feasibility. First, nuclear procedures already decompose operations into discrete phases with explicit transition criteria, allowing formalization of existing structure without imposing artificial abstractions. Second, mode-level verification bounds each verification problem locally, avoiding the state explosion that makes global hybrid system analysis intractable. Third, the Emerson collaboration provides domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility, ensuring solutions address real deployment constraints. -The complete methodology encompasses procedure formalization, discrete synthesis, continuous verification across three mode types, and hardware implementation. +The complete methodology encompasses procedure formalization, discrete synthesis, continuous verification across three mode types, and hardware implementation. -Three operational questions remain: Section 4 addresses \textit{How will success be measured?} Section 5 addresses \textit{What could prevent success?} Section 6 addresses \textit{Who cares? Why now? What difference will it make?} +Three operational questions remain. Section 4 addresses: \textit{How will success be measured?} Section 5 addresses: \textit{What could prevent success?} Section 6 addresses: \textit{Who cares? Why now? What difference will it make?} %%% NOTES (Section 5): % - Get specific details on ARCADE interface from Emerson collaboration diff --git a/4-metrics-of-success/v1.tex b/4-metrics-of-success/v1.tex index e650243..01194fe 100644 --- a/4-metrics-of-success/v1.tex +++ b/4-metrics-of-success/v1.tex @@ -87,4 +87,6 @@ This section answered the Heilmeier question: How do we measure success? \textbf{Answer:} Technology Readiness Level advancement from 2--3 to 5 demonstrates both theoretical correctness and practical feasibility through progressively integrated validation. TRL 3 proves component-level correctness: each part works independently. TRL 4 demonstrates system-level integration in simulation: the parts compose correctly. TRL 5 validates hardware implementation in a relevant environment: the complete system works on real control hardware. Achieving TRL 5 proves the methodology produces verified controllers implementable with current technology. -Success, however, depends on several critical assumptions. If these assumptions prove false, research could stall at lower readiness levels despite sound methodology. Section 5 addresses the complementary question: What could prevent success? +Success, however, depends on several critical assumptions. If these assumptions prove false, research could stall at lower readiness levels despite sound methodology. + +Section 5 addresses the complementary question: What could prevent success? diff --git a/5-risks-and-contingencies/v1.tex b/5-risks-and-contingencies/v1.tex index 0578915..08fe1fa 100644 --- a/5-risks-and-contingencies/v1.tex +++ b/5-risks-and-contingencies/v1.tex @@ -136,10 +136,10 @@ This section answered the Heilmeier question: What could prevent success? Each risk has identifiable early warning indicators enabling detection before failure becomes inevitable. Each risk has viable mitigation strategies preserving research value even when core assumptions fail. -The staged project structure ensures partial success yields publishable results. It identifies remaining barriers to deployment. This design feature maintains contribution regardless of which technical obstacles prove insurmountable. Even "failure" advances the field by documenting precisely which barriers remain. +The staged project structure ensures partial success yields publishable results and identifies remaining barriers to deployment. This design feature maintains contribution regardless of which technical obstacles prove insurmountable. Even "failure" advances the field by documenting precisely which barriers remain. -The technical research plan is complete. Section 3 established what will be done and why it will succeed. Section 4 established how to measure success. This section established what might prevent success and how to mitigate risks. +The technical research plan is complete. Section 3 established what will be done and why it will succeed. Section 4 established how to measure success. This section established what might prevent success and how to mitigate risks. -One critical Heilmeier question remains: Who cares? Why now? What difference will it make? +One critical Heilmeier question remains: Who cares? Why now? What difference will it make? Section 6 connects this technical methodology to urgent economic and infrastructure challenges. diff --git a/6-broader-impacts/v1.tex b/6-broader-impacts/v1.tex index 1a4ef4f..51d07d4 100644 --- a/6-broader-impacts/v1.tex +++ b/6-broader-impacts/v1.tex @@ -66,8 +66,8 @@ This section answered three critical Heilmeier questions: Who cares? Why now? Wh \textbf{Why now?} Two forces converge. First, exponentially growing AI infrastructure demands create immediate need for economical nuclear power at datacenter scale. Projections show datacenter electricity demand reaching 1,050 terawatt-hours annually by 2030. Second, formal methods tools have matured sufficiently to make compositional hybrid verification computationally achievable. What was theoretically possible but practically intractable a decade ago is now feasible. The problem is urgent. The tools exist. -\textbf{What difference will it make?} This research addresses a \$21--28 billion annual cost barrier. It enables autonomous control with mathematical safety guarantees. Beyond immediate economic impact, the methodology establishes a generalizable framework for safety-critical autonomous systems across critical infrastructure. Impact extends beyond nuclear power to any safety-critical system requiring provable correctness. +\textbf{What difference will it make?} This research addresses a \$21--28 billion annual cost barrier and enables autonomous control with mathematical safety guarantees. Beyond immediate economic impact, the methodology establishes a generalizable framework for safety-critical autonomous systems across critical infrastructure. Impact extends beyond nuclear power to any safety-critical system requiring provable correctness. -The complete research plan spans technical approach, success metrics, risk mitigation, and broader impact. One final Heilmeier question remains: How long will it take? +The complete research plan spans technical approach, success metrics, risk mitigation, and broader impact. One final Heilmeier question remains: How long will it take? Section 8 provides a structured 24-month research plan progressing through milestones tied to Technology Readiness Level advancement, demonstrating the proposed work is achievable within a doctoral timeline.