diff --git a/1-goals-and-outcomes/goals.tex b/1-goals-and-outcomes/goals.tex index 80446ed..b9c5500 100644 --- a/1-goals-and-outcomes/goals.tex +++ b/1-goals-and-outcomes/goals.tex @@ -12,69 +12,65 @@ behavior.\splitnote{Clear thesis statement. Gets right to it.} % INTRODUCTORY PARAGRAPH Hook Nuclear power plants require the highest levels of control system reliability, -where failures can result in significant economic losses, service interruptions, -or radiological release.\splitnote{Stakes established immediately — good hook.} +where failures can result in significant economic losses, service +interruptions, or radiological +release.\splitnote{Stakes established immediately — good hook.} % Known information -Currently, nuclear plant operations rely on extensively trained human operators -who follow detailed written procedures and strict regulatory requirements to -manage reactor control. These operators make critical decisions about when to -switch between different control modes based on their interpretation of plant -conditions and procedural guidance. +Currently, nuclear plant operations rely on extensively trained human +operators who follow detailed written procedures and strict regulatory +requirements to manage reactor control. These operators make critical +decisions about when to switch between different control modes based on their +interpretation of plant conditions and procedural guidance. % Gap -This reliance on human operators prevents autonomous control capabilities and -creates a fundamental economic challenge for next-generation reactor -designs. -\splitinline{The ``and'' here joins two distinct issues (autonomy barrier + -economics). Consider making the causal link explicit: ``This reliance on human -operators not only prevents autonomous control capabilities but also -creates...'' or split into two sentences.} -Small modular reactors, in particular, face per-megawatt staffing costs far -exceeding those of conventional plants and threaten their economic viability. +\oldt{This reliance on human operators prevents autonomous control +capabilities and creates a fundamental economic challenge for next-generation +reactor designs.} \newt{This reliance on human operators prevents autonomous +control and creates a fundamental economic barrier for next-generation +reactor designs.} Small modular reactors face per-megawatt staffing costs +far exceeding those of conventional plants, threatening their economic +viability. % Critical Need -What is needed is a method to create autonomous control systems that safely -manage complex operational sequences with the same assurance as human-operated -systems, but without constant human supervision. -\splitinline{``What is needed is'' — Gopen would call this a weak topic -position. The sentence buries the subject. Try: ``Autonomous control systems -must safely manage complex operational sequences...'' Puts the actor in the -topic position.} +\oldt{What is needed is a method to create autonomous control systems that +safely manage complex operational sequences with the same assurance as +human-operated systems, but without constant human supervision.} +\newt{Autonomous control systems must safely manage complex operational +sequences with the same assurance as human-operated systems, but without +constant human supervision.} % APPROACH PARAGRAPH Solution To address this need, we will combine formal methods 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, -mirroring 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.\splitnote{Excellent setup of the gap — shows why neither approach +mirroring 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.\splitnote{Excellent setup of the gap — shows why neither approach alone is sufficient.} % Hypothesis By synthesizing discrete mode transitions directly from written operating -procedures and verifying continuous behavior between transitions, we can create -hybrid control systems with end-to-end correctness guarantees. If existing -procedures can be formalized into logical specifications and continuous dynamics -verified against transition requirements, then autonomous controllers can be -built that are provably free from design +procedures and verifying continuous behavior between transitions, we can +create hybrid control systems with end-to-end correctness guarantees. If +existing procedures can be formalized into logical specifications and +continuous dynamics verified against transition requirements, then autonomous +controllers can be built that are provably free from design defects.\splitnote{Hypothesis is clear and testable.} % Pay-off -This approach will enable autonomous control in nuclear power plants while -maintaining the high safety standards required by the industry. +\oldt{This approach will enable autonomous control in nuclear power plants +while maintaining the high safety standards required by the industry. % Qualifications -This work is conducted within the University of Pittsburgh Cyber Energy Center, -which provides access to industry collaboration and Emerson control hardware, -ensuring that developed solutions align with practical implementation -requirements. -\splitinline{This qualifications paragraph feels orphaned here. It's important -context but reads as an afterthought. Consider integrating it into the -approach paragraph (``...demonstrated on Emerson hardware through our -partnership with the Cyber Energy Center'') or moving to a ``Why This Will -Succeed'' framing later.} - - +This work is conducted within the University of Pittsburgh Cyber Energy +Center, which provides access to industry collaboration and Emerson control +hardware, ensuring that developed solutions align with practical +implementation requirements.} \newt{This approach will enable autonomous +control in nuclear power plants while maintaining the high safety standards +required by the industry. The University of Pittsburgh Cyber Energy Center's +partnership with Emerson provides access to industry-standard control +hardware, ensuring that developed solutions align with practical +implementation requirements from the outset.} % OUTCOMES PARAGRAPHS If this research is successful, we will be able to do the following: @@ -85,27 +81,30 @@ If this research is successful, we will be able to do the following: \item \textbf{Translate written procedures into verified control logic.} % Strategy We will develop a methodology for converting existing written operating - procedures into formal specifications that can be automatically synthesized - into discrete control logic. This process will use structured intermediate - representations to bridge natural language procedures and mathematical - logic. + procedures into formal specifications that can be automatically + synthesized into discrete control logic. This process will use structured + intermediate representations to bridge natural language procedures and + mathematical logic. % Outcome - Control system engineers will generate verified mode-switching controllers - directly from regulatory procedures without formal methods - expertise,\dasinline{Same comment as in executive - summary. Might not be true and is not the point.} - lowering the barrier to high-assurance control systems. + \oldt{Control system engineers will generate verified mode-switching + controllers directly from regulatory procedures without formal methods + expertise, lowering the barrier to high-assurance control systems.} + \newt{This will lower the barrier to high-assurance control systems by + generating verified mode-switching controllers directly from regulatory + procedures.}\dasinline{Same comment as in executive summary. Might not be + true and is not the point.} % OUTCOME 2 Title \item \textbf{Verify continuous control behavior across mode transitions.} % Strategy We will establish methods for analyzing continuous control modes to ensure they satisfy discrete transition requirements. Using classical control - theory for linear systems and reachability analysis for nonlinear dynamics, - we will verify that each continuous mode safely reaches its intended - transitions. - Engineers will design continuous controllers using standard practices while - iterating to ensure broader system correctness, proving that mode + theory for linear systems and reachability analysis for nonlinear + dynamics, we will verify that each continuous mode safely reaches its + intended transitions. + % Outcome + Engineers will design continuous controllers using standard practices + while iterating to ensure broader system correctness, proving that mode transitions occur safely and at the correct times. % OUTCOME 3 Title @@ -116,31 +115,33 @@ If this research is successful, we will be able to do the following: nuclear reactor startup procedures, implementing it on a small modular reactor simulation using industry-standard control hardware. This demonstration will prove correctness across multiple coordinated control - modes from cold shutdown through criticality to power - operation.\splitnote{``cold shutdown through criticality to power + modes from cold shutdown through criticality to power + operation.\splitnote{``cold shutdown through criticality to power operation'' — concrete and impressive scope.} % Outcome We will demonstrate that autonomous hybrid control can be realized in the - nuclear industry with current equipment, establishing a path toward reduced - operator staffing while maintaining safety. + nuclear industry with current equipment, establishing a path toward + reduced operator staffing while maintaining safety. \end{enumerate} % IMPACT PARAGRAPH Innovation The innovation in this work is unifying discrete synthesis with continuous -verification to enable end-to-end correctness guarantees for hybrid +verification to enable end-to-end correctness guarantees for hybrid systems.\splitnote{Clear ``what's new'' statement.} % Outcome Impact If successful, control engineers will create autonomous controllers from -existing procedures with mathematical proof of correct behavior. High-assurance -autonomous control will become practical for safety-critical applications. +existing procedures with mathematical proof of correct behavior. +High-assurance autonomous control will become practical for safety-critical +applications. % Impact/Pay-off -This capability is essential for the economic viability of next-generation -nuclear power. Small modular reactors offer a promising solution to growing -energy demands, but their success depends on reducing per-megawatt operating -costs through increased autonomy.\dasinline{This paragraph is literally -the same as the rest of the GO. Does not belong here -and feels very redundant.} This research will provide the tools to -achieve that autonomy while maintaining the exceptional safety record the -nuclear industry requires.\splitnote{Strong closing --- ties technical work to -real-world impact and economic necessity.} +\oldt{This capability is essential for the economic viability of +next-generation nuclear power. Small modular reactors offer a promising +solution to growing energy demands, but their success depends on reducing +per-megawatt operating costs through increased autonomy. This research will +provide the tools to achieve that autonomy while maintaining the exceptional +safety record the nuclear industry requires.} \newt{This research will +provide the tools to achieve that autonomy while maintaining the exceptional +safety record the nuclear industry +requires.}\dasinline{This paragraph is literally the same as the rest of the +GO. Does not belong here and feels very redundant.}