82 lines
5.1 KiB
TeX
82 lines
5.1 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.
|
|
|
|
\oldt{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}. Datacenter
|
|
electricity demand is projected to reach 1,050 terawatt-hours annually by
|
|
2030~\cite{eesi_datacenter_2024}. If this demand were supplied by nuclear
|
|
power, the total annual cost of power generation would exceed \$92 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 \$21--28 billion annually for projected datacenter demand.}
|
|
\newt{[DANE: Verify these figures are current. Check EIA Annual Energy
|
|
Outlook 2024/2025 for updated LCOE projections. The \$88.24/MWh,
|
|
\$16.15/MWh O\&M, and datacenter demand projections may have newer
|
|
sources.]}\dasinline{Check all of this math and update if newer sources
|
|
exist.}
|
|
|
|
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. 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\splitnote{``If it works here, it works anywhere — strong closing
|
|
argument.}---will establish both the technical feasibility and regulatory
|
|
pathway for broader adoption across critical infrastructure.
|