83 lines
5.2 KiB
TeX
83 lines
5.2 KiB
TeX
\section{Broader Impacts}
|
|
|
|
Nuclear power presents both a compelling application domain and an urgent
|
|
economic challenge. Recent interest in powering artificial intelligence
|
|
infrastructure has renewed focus on small modular reactors (SMRs),
|
|
particularly for hyperscale datacenters requiring hundreds of megawatts of
|
|
continuous power. Deploying SMRs at datacenter sites would minimize
|
|
transmission losses and eliminate emissions from hydrocarbon-based
|
|
alternatives. However, nuclear power economics at this scale demand careful
|
|
attention to operating costs.
|
|
|
|
\addedprose{According to the U.S. Energy Information Administration's Annual
|
|
Energy Outlook 2022, advanced nuclear power entering service in 2027 is
|
|
projected to cost \$88.24 per megawatt-hour~\cite{eia_lcoe_2022}. In the
|
|
United States alone, datacenter electricity consumption could reach 560
|
|
terawatt-hours by 2030---up from 4\% to 13\% of total national electricity
|
|
consumption~\cite{deroucy_ai_2025}. If this demand were supplied by nuclear
|
|
power, the total annual cost of power generation would reach approximately
|
|
\$49 billion. Within this figure, operations and maintenance represents a
|
|
substantial component. The EIA estimates that fixed O\&M costs alone account
|
|
for \$16.15 per megawatt-hour, with additional variable O\&M costs embedded
|
|
in fuel and operating expenses~\cite{eia_lcoe_2022}. Combined, O\&M-related
|
|
costs represent approximately 23--30\% of the total levelized cost of
|
|
electricity, translating to \$11--15 billion annually for projected U.S.
|
|
datacenter demand alone.}
|
|
|
|
This research directly addresses the multi-billion-dollar O\&M cost challenge
|
|
through high-assurance autonomous control. Current nuclear operations require
|
|
full control room staffing for each reactor, whether large conventional units
|
|
or small modular designs. Over 3,600 active NRC-licensed reactor operators
|
|
work in the United States~\cite{operator_statistics}, divided into Reactor
|
|
Operators (ROs) and Senior Reactor Operators
|
|
(SROs)~\cite{10CFR55}. Staffing requires at least two ROs and one SRO per
|
|
unit~\cite{10CFR50.54}, with each operator requiring several years of
|
|
training and NRC licensing. These staffing requirements drive the high O\&M
|
|
costs that make nuclear power economically challenging, particularly for
|
|
smaller reactor designs where the same staffing overhead must be spread
|
|
across lower power output. Synthesizing provably correct hybrid controllers
|
|
from formal specifications can automate routine operational sequences that
|
|
currently require constant human oversight. This enables a fundamental shift
|
|
from direct operator control to supervisory monitoring, where operators
|
|
oversee multiple autonomous reactors rather than manually controlling
|
|
individual units.
|
|
|
|
The correct-by-construction methodology is critical for this transition.
|
|
Traditional automation approaches cannot provide sufficient safety guarantees
|
|
for nuclear applications, where regulatory requirements and public safety
|
|
concerns demand the highest levels of assurance. Formally verifying both the
|
|
discrete mode-switching logic and the continuous control behavior, this
|
|
research will produce controllers with mathematical proofs of correctness.
|
|
These guarantees enable automation to safely handle routine
|
|
operations---startup sequences, power level changes, and normal operational
|
|
transitions---that currently require human operators to follow written
|
|
procedures. Operators will remain in supervisory roles to handle off-normal
|
|
conditions and provide authorization for major operational changes, but the
|
|
routine cognitive burden of procedure execution shifts to provably correct
|
|
automated systems that are much cheaper to operate.
|
|
|
|
SMRs represent an ideal deployment target for this technology. Nuclear
|
|
Regulatory Commission certification requires extensive documentation of
|
|
control procedures, operational requirements, and safety analyses written in
|
|
structured natural language. As described in our approach, these regulatory
|
|
documents can be translated into temporal logic specifications using tools
|
|
like FRET, then synthesized into discrete switching logic using reactive
|
|
synthesis tools, and finally verified using reachability analysis and barrier
|
|
certificates for the continuous control modes. The infrastructure of
|
|
requirements and specifications already exists as part of the licensing
|
|
process, creating a direct pathway from existing regulatory documentation to
|
|
formally verified autonomous controllers.
|
|
|
|
Beyond reducing operating costs for new reactors, this research will
|
|
establish a generalizable framework for autonomous control of safety-critical
|
|
systems. The methodology of translating operational procedures into formal
|
|
specifications, synthesizing discrete switching logic, and verifying
|
|
continuous mode behavior applies to any hybrid system with documented
|
|
operational requirements. Potential applications include chemical process
|
|
control, aerospace systems, and autonomous transportation, where similar
|
|
economic and safety considerations favor increased autonomy with provable
|
|
correctness guarantees. Demonstrating this approach in nuclear power---one of
|
|
the most regulated and safety-critical
|
|
domains---will establish both the technical feasibility and regulatory
|
|
pathway for broader adoption across critical infrastructure.
|