diff --git a/1-goals-and-outcomes/research_statement_v1.tex b/1-goals-and-outcomes/research_statement_v1.tex index 3f63efb..6745d60 100644 --- a/1-goals-and-outcomes/research_statement_v1.tex +++ b/1-goals-and-outcomes/research_statement_v1.tex @@ -2,18 +2,20 @@ This research develops autonomous control systems with mathematical guarantees of safe and correct behavior. % INTRODUCTORY PARAGRAPH Hook -Today's nuclear reactors operate under the control of extensively trained human operators who follow detailed written procedures and switch between control objectives based on plant conditions. +Today's nuclear reactors operate under the control of extensively trained human operators. These operators follow detailed written procedures and switch between control objectives based on plant conditions. % Gap -Small modular reactors face a fundamental economic challenge: their per-megawatt staffing costs significantly exceed those of conventional plants, threatening their economic viability. Autonomous control systems offer a solution—they could manage complex operational sequences without constant supervision—but only if they provide assurance equal to or exceeding human-operated systems. +Small modular reactors face a fundamental economic challenge: per-megawatt staffing costs significantly exceed those of conventional plants, threatening their economic viability. Autonomous control systems offer a solution by managing complex operational sequences without constant supervision—but only if they provide assurance equal to or exceeding human-operated systems. % APPROACH PARAGRAPH Solution This research combines formal methods from computer science with control theory to produce hybrid control systems that are correct by construction. % Rationale -This approach mirrors how operators already work: discrete logic switches between continuous control modes. Existing formal methods can generate provably correct switching logic, but they fail when continuous dynamics govern transitions. Control theory verifies continuous behavior, but it cannot prove discrete switching correctness. Achieving end-to-end correctness requires both approaches working together. +This approach mirrors how operators already work: discrete logic switches between continuous control modes. Existing formal methods generate provably correct switching logic but fail when continuous dynamics govern transitions. Control theory verifies continuous behavior but cannot prove discrete switching correctness. End-to-end correctness requires both approaches working together. % Hypothesis and Technical Approach -Three stages bridge this gap. First, written operating procedures translate into temporal logic specifications using NASA's Formal Requirements Elicitation Tool (FRET). FRET structures requirements into scope, condition, component, timing, and response. Conflicts and ambiguities emerge through realizability checking—before implementation begins. Second, reactive synthesis generates deterministic automata provably correct by construction. Third, standard control theory designs continuous controllers for each discrete mode. Reachability analysis then verifies each controller. Transition objectives classify continuous modes. Transitory modes drive the plant between conditions. Stabilizing modes maintain operation within regions. Expulsory modes ensure safety under failures. Assume-guarantee contracts and barrier certificates prove safe mode transitions. This enables local verification without global trajectory analysis. The methodology demonstrates on an Emerson Ovation control system. +Three stages bridge this gap. First, written operating procedures translate into temporal logic specifications using NASA's Formal Requirements Elicitation Tool (FRET). FRET structures 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, standard control theory designs continuous controllers for each discrete mode, with reachability analysis verifying each controller. + +Continuous modes classify by transition objective. Transitory modes drive the plant between conditions. Stabilizing modes maintain operation within regions. Expulsory modes ensure safety under failures. Assume-guarantee contracts and barrier certificates prove safe mode transitions, enabling local verification without global trajectory analysis. The methodology demonstrates on an Emerson Ovation control system. % Pay-off -This autonomous control approach manages complex nuclear power operations while maintaining safety guarantees. It directly addresses the economic constraints that threaten small modular reactor viability. +This autonomous control approach manages complex nuclear power operations while maintaining safety guarantees, directly addressing the economic constraints that threaten small modular reactor viability. % OUTCOMES PARAGRAPHS This research, if successful, produces three concrete outcomes: diff --git a/1-goals-and-outcomes/v1.tex b/1-goals-and-outcomes/v1.tex index 5d9d282..92e2345 100644 --- a/1-goals-and-outcomes/v1.tex +++ b/1-goals-and-outcomes/v1.tex @@ -4,9 +4,9 @@ This research develops autonomous hybrid control systems with mathematical guarantees of safe and correct behavior. % INTRODUCTORY PARAGRAPH Hook -Nuclear power plants require the highest levels of control system reliability because control system failures risk economic losses, service interruptions, or radiological release. +Nuclear power plants require the highest levels of control system reliability. Control system failures risk economic losses, service interruptions, or radiological release. % Known information -Today's nuclear plants operate under the control of extensively trained human operators who follow detailed written procedures and strict regulatory requirements while switching between control modes based on plant conditions and procedural guidance. +Today's nuclear plants operate under the control of extensively trained human operators. These operators follow detailed written procedures and strict regulatory requirements while switching 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: per-megawatt staffing costs for small modular reactors far exceed those of conventional plants, threatening their economic viability. Autonomous control systems could manage complex operational sequences without constant human supervision—but only if they provide assurance equal to or exceeding that of human operators. @@ -15,7 +15,7 @@ This research combines formal methods with control theory to produce hybrid cont % Rationale This approach mirrors how operators already work: discrete logic switches between continuous control modes. Existing formal methods can generate provably correct switching logic from written requirements, but they fail when continuous dynamics govern transitions. Control theory verifies continuous behavior, but it cannot prove discrete switching correctness. Achieving end-to-end correctness requires both approaches working together. % Hypothesis -This approach closes the gap through two steps. First, it synthesizes discrete mode transitions directly from written operating procedures. Second, it verifies continuous behavior between transitions. Operating procedures formalize into logical specifications, and continuous dynamics verify against transition requirements. The result is autonomous controllers that are provably free from design defects. +This approach closes the gap through two steps. First, it synthesizes discrete mode transitions directly from written operating procedures. Second, it verifies continuous behavior between transitions. Operating procedures formalize into logical specifications. Continuous dynamics verify against transition requirements. The result: autonomous controllers provably free from design defects. The University of Pittsburgh Cyber Energy Center provides access to industry collaboration and Emerson control hardware, ensuring solutions align with practical implementation requirements. @@ -65,7 +65,7 @@ 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?} This work unifies discrete synthesis with continuous verification to enable end-to-end correctness guarantees for hybrid systems—a bridge that emerges by treating discrete specifications as contracts that continuous controllers must satisfy, allowing each layer to verify independently while guaranteeing correct composition. Formal methods verify discrete logic; control theory verifies continuous dynamics; no existing methodology bridges both with compositional guarantees. Section 2 (State of the Art) examines why prior work has not achieved this integration, and Section 3 (Research Approach) details how this integration will be accomplished. +\textbf{What makes this research new?} This work unifies discrete synthesis with continuous verification to enable end-to-end correctness guarantees for hybrid systems. The key innovation: treating discrete specifications as contracts that continuous controllers must satisfy. This allows each layer to verify independently while guaranteeing correct composition. Formal methods verify discrete logic. Control theory verifies continuous dynamics. No existing methodology bridges both with compositional guarantees. Section 2 (State of the Art) examines why prior work has not achieved this integration. Section 3 (Research Approach) details how this integration will be accomplished. % 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 e3d98e7..979d0b8 100644 --- a/2-state-of-the-art/v2.tex +++ b/2-state-of-the-art/v2.tex @@ -1,14 +1,14 @@ \section{State of the Art and Limits of Current Practice} -\textbf{What has been done? What are the limits of current practice?} This section answers these Heilmeier questions by examining how nuclear reactors operate today and why current approaches—both human-centered and formal methods—cannot provide autonomous control with end-to-end correctness guarantees. Three subsections structure this analysis: first, reactor operators and their operating procedures; second, the fundamental limitations of human-based operation; third, formal methods approaches that verify discrete logic or continuous dynamics but not both together. Understanding these limits establishes the verification gap that Section 3 addresses through compositional hybrid synthesis. +\textbf{What has been done? What are the limits of current practice?} This section answers these Heilmeier questions by examining how nuclear reactors operate today. Current approaches—both human-centered and formal methods—cannot provide autonomous control with end-to-end correctness guarantees. Three subsections structure this analysis. First: reactor operators and their operating procedures. Second: the fundamental limitations of human-based operation. Third: formal methods approaches that verify discrete logic or continuous dynamics but not both together. Understanding these limits establishes the verification gap that Section 3 addresses through compositional hybrid synthesis. \subsection{Current Reactor Procedures and Operation} -Before identifying the limits of current practice, we must first understand how nuclear plants operate today. This subsection examines three aspects: the hierarchy of procedures, the role of operators in executing them, and the operational modes that govern reactor control. +Before identifying the limits of current practice, this subsection examines how nuclear plants operate today. Three aspects structure the analysis: the hierarchy of procedures, the role of operators in executing them, and the operational modes that govern reactor control. 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, and Extensive Damage Mitigation Guidelines (EDMGs) cover catastrophic damage. These 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. While 10 CFR 55.59~\cite{10CFR55.59} requires rigorous assessment through technical evaluation, simulator validation testing, and biennial review, key safety properties escape formal verification. No mathematical proof confirms that procedures cover all possible plant states, that required actions complete within available timeframes, or that safety invariants hold across procedure-set transitions. +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 proof confirms that procedures cover all possible plant states, that required actions complete within available timeframes, or that safety invariants hold across procedure-set transitions. \textbf{LIMITATION:} \textit{Procedures lack formal verification of correctness and completeness.} Current procedure development relies on expert judgment and @@ -21,11 +21,11 @@ could provide. Nuclear plants operate with multiple control modes. Automatic control maintains target parameters through continuous reactivity adjustment. Manual control allows operators to directly manipulate the reactor. Various intermediate modes bridge these extremes. In typical pressurized water reactor operation, the reactor control system automatically maintains a floating average temperature. It compensates for power demand changes through reactivity feedback loops alone. Safety systems already employ extensive automation. Reactor Protection Systems trip automatically on safety signals with millisecond response times. Engineered safety features actuate automatically on accident signals—no operator action required. -The division between automated and human-controlled functions reveals the fundamental challenge of hybrid control. Highly automated systems already handle reactor protection: automatic trips on safety parameters, emergency core cooling actuation, containment isolation, and basic process control~\cite{WRPS.Description, gentillon_westinghouse_1999}. Human operators, meanwhile, retain control of strategic decision-making: power level changes, startup/shutdown sequences, mode transitions, and procedure implementation. +This division between automated and human-controlled functions reveals the fundamental challenge of hybrid control. Highly automated systems already handle reactor protection: automatic trips on safety parameters, emergency core cooling actuation, containment isolation, and basic process control~\cite{WRPS.Description, gentillon_westinghouse_1999}. Human operators, meanwhile, retain control of strategic decision-making: power level changes, startup/shutdown sequences, mode transitions, and procedure implementation. This hybrid structure—discrete human decisions combined with continuous automated control—forms the basis for autonomous hybrid control systems. \subsection{Human Factors in Nuclear Accidents} -The previous subsection established that procedures lack formal verification despite rigorous development, representing only half the reliability challenge. Even 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. While procedures define what to do, human operators determine when and how—and this human element introduces persistent failure modes. +The previous subsection established that procedures lack formal verification despite rigorous development. This represents only half the reliability challenge. Even 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. Human operators determine when and how. This human element introduces persistent failure modes. Current-generation nuclear power plants employ over 3,600 active NRC-licensed reactor operators in the United States~\cite{operator_statistics}. These @@ -56,9 +56,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: procedures lack formal verification, and human operators introduce persistent reliability issues that four decades of training improvements have failed to eliminate. Training and procedural improvements cannot solve these problems—but formal methods might offer mathematical guarantees of correctness that could eliminate both human error and procedural ambiguity. +The previous two subsections revealed two critical limitations of current practice. First: procedures lack formal verification. 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. Formal methods might offer mathematical guarantees of correctness that eliminate both human error and procedural ambiguity. -Even the most advanced formal methods applications in nuclear control, however, leave a critical verification gap for autonomous hybrid systems. This subsection examines two approaches illustrating this gap: HARDENS, which verified discrete logic without continuous dynamics, and differential dynamic logic, which handles hybrid verification only post-hoc. Each demonstrates the current state of formal methods while revealing the verification gap this research addresses. +Even the most advanced formal methods applications in nuclear control leave a critical verification gap for autonomous hybrid systems. 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 this research addresses. \subsubsection{HARDENS: The State of Formal Methods in Nuclear Control} @@ -151,8 +151,8 @@ design loop for complex systems like nuclear reactor startup procedures. This section answered two Heilmeier questions about current practice: -\textbf{What has been done?} Human operators provide operational flexibility but introduce persistent reliability limitations that four decades of training improvements have failed to eliminate. Formal methods provide correctness guarantees but have not scaled to complete hybrid control design. HARDENS verified discrete logic without continuous dynamics. Differential dynamic logic expresses hybrid properties but requires post-design expert analysis and fails to scale to system synthesis. +\textbf{What has been done?} Human operators provide operational flexibility but introduce persistent reliability limitations. Four decades of training improvements have failed to eliminate these limitations. Formal methods provide correctness guarantees but have not scaled to complete hybrid control design. HARDENS verified discrete logic without continuous dynamics. Differential dynamic logic expresses hybrid properties but requires post-design expert analysis and fails to scale to system synthesis. \textbf{What are the limits of current practice?} No existing methodology synthesizes provably correct hybrid controllers from operational procedures with verification integrated into the design process. 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. -Two imperatives converge to make this gap urgent: economic necessity (small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants) and technical opportunity (formal methods tools have matured sufficiently to enable compositional hybrid verification). Section 3 addresses this verification gap by establishing what makes the proposed approach new and why it will succeed where prior work has failed. +Two imperatives converge to make this gap urgent. First, economic necessity: small modular reactors cannot compete with per-megawatt staffing costs matching large conventional plants. Second, technical opportunity: formal methods tools have matured sufficiently to enable compositional hybrid verification. Section 3 addresses this verification gap by establishing what makes the proposed approach new and why it will succeed where prior work has failed. diff --git a/3-research-approach/v3.tex b/3-research-approach/v3.tex index 26b4536..f428692 100644 --- a/3-research-approach/v3.tex +++ b/3-research-approach/v3.tex @@ -15,13 +15,13 @@ % ---------------------------------------------------------------------------- % 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 and test discrete switching logic through simulated control room testing and human factors research. Despite consuming enormous resources, neither method provides rigorous guarantees. +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 despite consuming enormous resources. -This work bridges the gap by composing formal methods from computer science with control-theoretic verification, formalizing reactor operations as hybrid automata. +This work bridges the gap by composing formal methods from computer science with control-theoretic verification. Reactor operations formalize as hybrid automata. -Hybrid system verification faces a fundamental challenge: discrete transitions change the governing vector field, creating discontinuities in system behavior through the interaction between discrete and continuous dynamics. Traditional verification techniques fail to handle this interaction directly. +Hybrid system verification faces a fundamental challenge: discrete transitions change the governing vector field. This creates discontinuities in system behavior through the interaction between discrete and continuous dynamics. Traditional verification techniques fail to handle this interaction directly. -Our methodology decomposes this problem, verifying discrete switching logic and continuous mode behavior separately before composing them to establish guarantees for the complete hybrid system. This two-layer approach mirrors reactor operations, where discrete supervisory logic determines which control mode is active while continuous controllers govern plant behavior within each mode. +Our methodology decomposes this 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. Building a high-assurance hybrid autonomous control system requires a mathematical description of the system. 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. These continuous states represent 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: @@ -48,7 +48,7 @@ where: Creating a HAHACS requires constructing 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?} Section 2 established that existing approaches verify either discrete logic or continuous dynamics—never both compositionally. While reactive synthesis, reachability analysis, and barrier certificates each exist independently, no prior work has integrated them into a systematic design methodology spanning procedures to verified implementation. Three innovations enable this integration: +\textbf{What is new in this research?} Section 2 established that existing approaches verify either discrete logic or continuous dynamics—never both compositionally. Reactive synthesis, reachability analysis, and barrier certificates each exist independently. No prior work has integrated them into a systematic design methodology spanning procedures to verified implementation. Three innovations enable this integration: \begin{enumerate} \item \textbf{Contract-based decomposition:} Instead of attempting global hybrid system verification, this approach inverts the traditional structure. Discrete synthesis defines entry/exit/safety contracts that bound continuous verification, transforming an intractable global problem into tractable local problems. @@ -59,12 +59,12 @@ Creating a HAHACS requires constructing this tuple together with proof artifacts \textbf{Why will it succeed?} Three factors ensure practical feasibility where prior work has failed: \begin{enumerate} -\item \textbf{Leverage existing structure:} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria. This work formalizes existing structure rather than imposing artificial abstractions, making adoption tractable for domain experts without formal methods training. -\item \textbf{Avoid state explosion:} Mode-level verification checks each mode against local contracts rather than attempting global hybrid system analysis. This decomposition bounds computational complexity, transforming an intractable global problem into tractable local verifications. +\item \textbf{Leverage existing structure:} Nuclear procedures already decompose operations into discrete phases with explicit transition criteria. This work formalizes existing structure rather than imposing artificial abstractions. This makes adoption tractable for domain experts without formal methods training. +\item \textbf{Avoid state explosion:} Mode-level verification checks each mode against local contracts rather than attempting global hybrid system analysis. This decomposition bounds computational complexity. It transforms an intractable global problem into tractable local verifications. \item \textbf{Industrial validation:} The Emerson collaboration provides both domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility. This ensures solutions address real deployment constraints, not just theoretical correctness. \end{enumerate} -These factors combine to demonstrate feasibility on production control systems with realistic reactor models, not merely in principle. Figure~\ref{fig:hybrid_automaton} illustrates the hybrid structure for a simplified reactor startup sequence. +These factors combine to demonstrate feasibility on production control systems with realistic reactor models—not merely in principle. Figure~\ref{fig:hybrid_automaton} illustrates the hybrid structure for a simplified reactor startup sequence. \begin{figure} \centering @@ -130,17 +130,17 @@ 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 for describing discrete modes, continuous dynamics, guards, and invariants. The question now becomes: where do these formal descriptions originate? This subsection demonstrates that nuclear operations already possess a natural hybrid structure that maps directly to the automaton formalism through three control scopes: strategic, operational, and tactical. Rather than imposing artificial abstractions, this approach constructs formal hybrid systems from existing operational knowledge. +The previous subsection established the hybrid automaton formalism—a mathematical framework for describing discrete modes, continuous dynamics, guards, and invariants. The question now: where do these formal descriptions originate? This subsection demonstrates that nuclear operations already possess a natural hybrid structure. This structure maps directly to the automaton formalism through three control scopes: strategic, operational, and tactical. Rather than imposing artificial abstractions, this approach constructs formal hybrid systems from existing operational knowledge. -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. +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. It manages labor needs and supply chains to optimize scheduled maintenance and downtime. -The tactical level controls individual components—pumps, turbines, and chemistry. Nuclear power plants have already automated tactical control through ``automatic control'' systems. These continuous systems directly impact the physical state of the plant, maintaining pressurizer level, core temperature, and reactivity through chemical shim. +The tactical level controls individual components: pumps, turbines, and chemistry. Nuclear power plants have already automated tactical control through ``automatic control'' systems. These continuous systems directly impact the physical state of the plant. They maintain pressurizer level, core temperature, and reactivity through chemical shim. -The operational scope links these extremes and represents the primary responsibility of human operators today, implementing tactical control sequences to achieve strategic objectives and bridging high-level goals with low-level execution. +The operational scope links these extremes. It represents the primary responsibility of human operators today. Operators implement tactical control sequences to achieve strategic objectives, bridging high-level goals with low-level execution. An example clarifies this three-level structure. Consider a strategic goal to perform refueling at a certain time. The tactical level currently maintains core temperature. The operational level issues the shutdown procedure, using several smaller tactical goals along the way to achieve this objective. -This structure reveals why the operational and tactical levels fundamentally form a hybrid controller: the tactical level represents continuous plant evolution according to control input and control law, while the operational level represents discrete state evolution determining which tactical control law applies. This operational level becomes the target for autonomous control. +This structure reveals why the operational and tactical levels fundamentally form a hybrid controller. The tactical level represents continuous plant evolution according to control input and control law. The operational level represents discrete state evolution determining which tactical control law applies. Together, these two levels form the complete hybrid system. This operational level becomes the target for autonomous control because it bridges strategic intent with tactical execution through discrete mode-switching decisions. \begin{figure} @@ -246,7 +246,7 @@ FRET has been successfully applied to spacecraft control systems, autonomous veh \subsection{Discrete Controller Synthesis} -The previous subsection showed how operating procedures translate into temporal logic specifications using FRET, defining what the system must do. The next question becomes: how do we implement those requirements? Reactive synthesis provides the answer—a technique that automatically constructs controllers guaranteed to satisfy temporal logic specifications. +The previous subsection showed how operating procedures translate into temporal logic specifications using FRET. These specifications define what the system must do. The next question: how do we implement those requirements? Reactive synthesis provides the answer. This technique automatically constructs 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; the next discrete state forms the output. @@ -257,7 +257,9 @@ Reactive synthesis offers a decisive advantage: the discrete automaton requires This shift carries two critical implications. First, complete traceability: the reasons the controller changes between modes trace back through specifications to requirements, establishing clear liability and justification for system behavior. Second, deterministic guarantees replace probabilistic human judgment. Human operators cannot eliminate error from discrete control decisions; humans are intrinsically fallible. Defining system behavior using temporal logics and synthesizing the controller using deterministic algorithms ensures strategic decisions always follow operating procedures exactly—no exceptions, no deviations, no human factors. -The synthesized automaton translates directly to executable code through standard compilation techniques where each discrete state maps to a control mode, guard conditions map to conditional statements, and the transition function defines the control flow. This compilation process preserves the formal guarantees by ensuring the implemented code is correct by construction—the automaton from which it derives was synthesized to satisfy the temporal logic specifications. +The synthesized automaton translates directly to executable code through standard compilation techniques. Each discrete state maps to a control mode, guard conditions map to conditional statements, and the transition function defines the control flow. This compilation process preserves the formal guarantees by ensuring the implemented code is correct by construction—the automaton from which it derives was synthesized to satisfy the temporal logic specifications. + +Having established how discrete mode-switching logic synthesizes from procedures, the question becomes: what executes within each discrete mode? The next subsection addresses continuous control modes and their verification. Reactive synthesis has proven successful in robotics, avionics, and industrial control. Recent applications include synthesizing robot motion planners from natural language specifications, generating flight control software for unmanned aerial vehicles, and creating verified controllers for automotive systems. These successes demonstrate that reactive synthesis scales beyond toy problems to real-world safety-critical applications. @@ -516,11 +518,11 @@ outcomes can align best with customer needs. This section answered two critical Heilmeier questions about the research approach: -\textbf{What is new in this research?} This work integrates reactive synthesis, reachability analysis, and barrier certificates into a compositional methodology for hybrid control synthesis through three innovations: first, using discrete synthesis to define verification contracts—inverting traditional global analysis; second, classifying continuous modes by objective to select appropriate verification tools; third, leveraging existing procedural structure to avoid intractable state explosion. Section 2 established that prior work verified either discrete logic or continuous dynamics—never both compositionally. Compositional verification enables what global analysis cannot achieve. +\textbf{What is new in this research?} This work integrates reactive synthesis, reachability analysis, and barrier certificates into a compositional methodology for hybrid control synthesis. Three innovations enable this integration. First: using discrete synthesis to define verification contracts, inverting traditional global analysis. Second: classifying continuous modes by objective to select appropriate verification tools. Third: leveraging existing procedural structure to avoid intractable state explosion. Section 2 established that prior work verified either discrete logic or continuous dynamics—never both compositionally. Compositional verification enables what global analysis cannot achieve. -\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 the approach to formalize existing structure rather than impose 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 both domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility. +\textbf{Why will this approach succeed?} Three factors ensure practical feasibility. First: nuclear procedures already decompose operations into discrete phases with explicit transition criteria. This allows the approach to formalize existing structure rather than impose 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 both domain expertise to validate procedure formalization and industrial hardware to demonstrate implementation feasibility. -The methodology is now complete—procedure formalization, discrete synthesis, continuous verification across three mode types, and hardware implementation. What remains are operational questions about executing this research plan: Section 4 addresses \textit{How will success be measured?} through Technology Readiness Level advancement; Section 5 addresses \textit{What could prevent success?} through risk analysis and contingency planning; Section 6 addresses \textit{Who cares? Why now? What difference will it make?} through economic and societal impact analysis. +The methodology is now complete: procedure formalization, discrete synthesis, continuous verification across three mode types, and hardware implementation. What remains are operational questions about executing this research plan. Section 4 addresses \textit{How will success be measured?} through Technology Readiness Level advancement. Section 5 addresses \textit{What could prevent success?} through risk analysis and contingency planning. Section 6 addresses \textit{Who cares? Why now? What difference will it make?} through economic and societal impact analysis. %%% 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 535f2f9..e8e9113 100644 --- a/4-metrics-of-success/v1.tex +++ b/4-metrics-of-success/v1.tex @@ -77,6 +77,6 @@ a relevant laboratory environment. This establishes both theoretical validity and practical feasibility, proving the methodology produces verified controllers implementable with current technology. -This section answered the Heilmeier question \textbf{How do we measure success?} Technology Readiness Level advancement from 2--3 to 5 provides the answer: success means demonstrating both theoretical correctness and practical feasibility through progressively integrated validation. TRL 3 proves component-level correctness; TRL 4 demonstrates system-level integration in simulation; TRL 5 validates hardware implementation in a relevant environment. Achieving TRL 5 proves the methodology produces verified controllers implementable with current technology. +This section answered the Heilmeier question \textbf{How do we measure success?} Technology Readiness Level advancement from 2--3 to 5 provides the answer. Success means demonstrating both theoretical correctness and practical feasibility through progressively integrated validation. TRL 3 proves component-level correctness. TRL 4 demonstrates system-level integration in simulation. TRL 5 validates hardware implementation in a relevant environment. Achieving TRL 5 proves the methodology produces verified controllers implementable with current technology. -Reaching TRL 5 depends on several critical assumptions. If these assumptions prove false, the research could stall at lower readiness levels despite sound methodology. Section 5 addresses the complementary Heilmeier question \textbf{What could prevent success?} by identifying primary risks, establishing early warning indicators, and defining contingency plans that preserve research value even when core assumptions fail. +Reaching TRL 5 depends on several critical assumptions. If these assumptions prove false, the research could stall at lower readiness levels despite sound methodology. Section 5 addresses the complementary Heilmeier question \textbf{What could prevent success?} It identifies primary risks, establishes early warning indicators, and defines contingency plans that preserve research value even when core assumptions fail. diff --git a/5-risks-and-contingencies/v1.tex b/5-risks-and-contingencies/v1.tex index 00f7f1e..ba7b504 100644 --- a/5-risks-and-contingencies/v1.tex +++ b/5-risks-and-contingencies/v1.tex @@ -4,7 +4,7 @@ \subsection{Computational Tractability of Synthesis} -The first major assumption: formalized startup procedures will yield automata small enough for efficient synthesis and verification. Reactive synthesis scales exponentially with specification complexity. Temporal logic specifications derived from complete startup procedures may produce automata with thousands of states, requiring synthesis times exceeding days or weeks—preventing completion of the methodology within project timelines. Reachability analysis for continuous modes with high-dimensional state spaces may similarly prove computationally intractable. Either barrier would constitute a fundamental obstacle to achieving research objectives. +Computational tractability represents the first major risk. The assumption: formalized startup procedures will yield automata small enough for efficient synthesis and verification. This assumption may fail. Reactive synthesis scales exponentially with specification complexity. Temporal logic specifications derived from complete startup procedures may produce automata with thousands of states, requiring synthesis times exceeding days or weeks. This would prevent completion of the methodology within project timelines. Reachability analysis for continuous modes with high-dimensional state spaces may similarly prove computationally intractable. Either barrier would constitute a fundamental obstacle to achieving research objectives. Several indicators would provide early warning of computational tractability problems. Synthesis times exceeding 24 hours for simplified procedure subsets @@ -122,6 +122,6 @@ extensions, ensuring they address industry-wide practices rather than specific quirks. -This section answered the Heilmeier question \textbf{What could prevent success?} Four primary risks threaten project completion: computational tractability of synthesis and verification, complexity of the discrete-continuous interface, completeness of procedure formalization, and hardware-in-the-loop integration challenges. Each risk has identifiable early warning indicators and viable mitigation strategies that preserve research value even when core assumptions fail. The staged project structure ensures that partial success yields publishable results while clearly identifying remaining barriers to deployment—a critical design feature that maintains contribution to the field regardless of which technical obstacles prove insurmountable. +This section answered the Heilmeier question \textbf{What could prevent success?} Four primary risks threaten project completion. First: computational tractability of synthesis and verification. Second: complexity of the discrete-continuous interface. Third: completeness of procedure formalization. Fourth: hardware-in-the-loop integration challenges. Each risk has identifiable early warning indicators and viable mitigation strategies that preserve research value even when core assumptions fail. The staged project structure ensures that partial success yields publishable results while clearly identifying remaining barriers to deployment. This critical design feature maintains contribution to the field regardless of which technical obstacles prove insurmountable. -The technical research plan is now complete: Section 3 established what will be done; Section 4 established how success will be measured; this section established what might prevent it. One critical Heilmeier question remains—\textbf{Who cares? Why now? What difference will it make?}—which Section 6 answers by connecting this technical methodology to urgent economic and infrastructure challenges facing the nuclear industry and broader energy sector. +The technical research plan is now complete. Section 3 established what will be done. Section 4 established how success will be measured. This section established what might prevent it. One critical Heilmeier question remains: \textbf{Who cares? Why now? What difference will it make?} Section 6 answers by connecting this technical methodology to urgent economic and infrastructure challenges facing the nuclear industry and broader energy sector. diff --git a/6-broader-impacts/v1.tex b/6-broader-impacts/v1.tex index 3572626..e6746af 100644 --- a/6-broader-impacts/v1.tex +++ b/6-broader-impacts/v1.tex @@ -2,7 +2,11 @@ \textbf{Who cares? Why now? What difference will it make?} Sections 2--5 established the complete technical research plan: what has been done and its limits (Section 2), what is new and why it will succeed (Section 3), how success will be measured (Section 4), and what could prevent success (Section 5). This section addresses the remaining Heilmeier questions, connecting technical methodology to economic and societal impact. -The technical approach enables compositional hybrid verification—a capability that did not exist before. But why does this matter beyond academic contribution? Three stakeholder groups converge on the same economic constraint: high operating costs driven by staffing requirements. The nuclear industry faces uncompetitive per-megawatt costs for small modular reactors. Datacenter operators need hundreds of megawatts of continuous clean power for AI infrastructure. Clean energy advocates need nuclear power to be economically viable. Exponentially growing AI infrastructure demands have transformed this longstanding challenge into an immediate crisis requiring solutions that did not exist before. +The technical approach enables compositional hybrid verification—a capability that did not exist before. But why does this matter beyond academic contribution? Three stakeholder groups converge on the same economic constraint: high operating costs driven by staffing requirements. + +First, the nuclear industry faces uncompetitive per-megawatt costs for small modular reactors. Second, datacenter operators need hundreds of megawatts of continuous clean power for AI infrastructure. Third, clean energy advocates need nuclear power to be economically viable. + +What has changed? Exponentially growing AI infrastructure demands have transformed this longstanding challenge into an immediate crisis. The market now demands solutions that did not exist before. 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 (SMRs), particularly for hyperscale datacenters requiring hundreds of megawatts of continuous power. SMRs deployed at datacenter sites minimize transmission losses and eliminate emissions, but nuclear power economics at this scale demand careful attention to operating costs. @@ -56,10 +60,10 @@ adoption across critical infrastructure. This section answered three critical Heilmeier questions about impact: -\textbf{Who cares?} Three stakeholder groups face the same constraint: the nuclear industry faces an economic crisis for small modular reactors due to per-megawatt staffing costs; datacenter operators need hundreds of megawatts of continuous clean power for AI infrastructure; clean energy advocates need nuclear power to be economically competitive. All three need autonomous control with safety guarantees. +\textbf{Who cares?} Three stakeholder groups face the same constraint. The nuclear industry faces an economic crisis for small modular reactors due to per-megawatt staffing costs. Datacenter operators need hundreds of megawatts of continuous clean power for AI infrastructure. Clean energy advocates need nuclear power to be economically competitive. All three need autonomous control with safety guarantees. -\textbf{Why now?} Two forces converge: first, exponentially growing AI infrastructure demands have created immediate need for economical nuclear power at datacenter scale, with projections showing datacenter electricity demand reaching 1,050 terawatt-hours annually by 2030; second, formal methods tools have matured, making compositional hybrid verification computationally achievable—what was theoretically possible but practically intractable a decade ago is now feasible. +\textbf{Why now?} Two forces converge. First: exponentially growing AI infrastructure demands have created 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, making compositional hybrid verification computationally achievable. What was theoretically possible but practically intractable a decade ago is now feasible. \textbf{What difference will it make?} This research addresses a \$21--28 billion annual cost barrier by enabling autonomous control with mathematical safety guarantees. Beyond immediate economic impact, the methodology establishes a generalizable framework for safety-critical autonomous systems across critical infrastructure. -The complete research plan now spans technical approach, success metrics, risk mitigation, and broader impact. One final Heilmeier question remains—\textbf{How long will it take?}—which Section 8 answers with 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. +The complete research plan now spans technical approach, success metrics, risk mitigation, and broader impact. One final Heilmeier question remains: \textbf{How long will it take?} Section 8 answers with a structured 24-month research plan progressing through milestones tied to Technology Readiness Level advancement. This demonstrates the proposed work is achievable within a doctoral timeline.