Auto sync: 2025-10-20 17:15:21 (9 files changed)
A Writing/ERLM/Sabo_Whitepaper.pdf M Writing/ERLM/dane_proposal_format.cls M Writing/ERLM/main.aux M Writing/ERLM/main.fdb_latexmk M Writing/ERLM/main.fls M Writing/ERLM/main.log M Writing/ERLM/main.pdf M Writing/ERLM/main.synctex.gz
This commit is contained in:
parent
b8ef71e55e
commit
448feaf542
BIN
Writing/ERLM/Sabo_Whitepaper.pdf
Normal file
BIN
Writing/ERLM/Sabo_Whitepaper.pdf
Normal file
Binary file not shown.
@ -103,6 +103,8 @@
|
||||
\\
|
||||
Advisor: Dr. Daniel G. Cole\\
|
||||
dgcole@pitt.edu\\
|
||||
\\
|
||||
Track: PhD Mechanical Engineering
|
||||
}
|
||||
|
||||
\date{\today}
|
||||
|
||||
@ -2,21 +2,17 @@
|
||||
\bibstyle{unsrt}
|
||||
\providecommand \oddpage@label [2]{}
|
||||
\@writefile{toc}{\contentsline {section}{\numberline {1}Objectives}{2}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {section}{\numberline {2}Objectives}{5}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {section}{\numberline {3}Limits of Current Practice}{5}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {section}{\numberline {4}Research Approach}{7}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {section}{\numberline {5}Metrics of Success}{9}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {section}{\numberline {6}Broader Impacts}{10}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {section}{\numberline {2}State of the Art and Limits of Current Practice}{3}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {section}{\numberline {3}Research Approach}{3}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {section}{\numberline {4}Metrics of Success}{5}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {section}{\numberline {5}Broader Impacts}{6}{}\protected@file@percent }
|
||||
\bibcite{10CFR55}{1}
|
||||
\bibcite{princeton}{2}
|
||||
\bibcite{Kemeny1979}{3}
|
||||
\bibcite{NUREG-0899}{4}
|
||||
\bibcite{DOE-HDBK-1028-2009}{5}
|
||||
\bibcite{WNA2020}{6}
|
||||
\bibcite{IAEA-severe-accidents}{7}
|
||||
\bibcite{Wang2025}{8}
|
||||
\bibcite{Kiniry2022}{9}
|
||||
\bibcite{eia_lcoe_2022}{10}
|
||||
\bibcite{eesi_datacenter_2024}{11}
|
||||
\@writefile{toc}{\contentsline {section}{References}{12}{}\protected@file@percent }
|
||||
\gdef \@abspage@last{13}
|
||||
\bibcite{Kemeny1979}{2}
|
||||
\bibcite{NUREG-0899}{3}
|
||||
\bibcite{DOE-HDBK-1028-2009}{4}
|
||||
\bibcite{WNA2020}{5}
|
||||
\bibcite{Kiniry2022}{6}
|
||||
\bibcite{eia_lcoe_2022}{7}
|
||||
\bibcite{eesi_datacenter_2024}{8}
|
||||
\@writefile{toc}{\contentsline {section}{References}{7}{}\protected@file@percent }
|
||||
\gdef \@abspage@last{8}
|
||||
|
||||
@ -1,9 +1,8 @@
|
||||
# Fdb version 4
|
||||
["pdflatex"] 1760990396.64627 "main.tex" "main.pdf" "main" 1760990397.59592 0
|
||||
["pdflatex"] 1760994767.73072 "main.tex" "main.pdf" "main" 1760994768.58948 0
|
||||
"/etc/texmf/web2c/texmf.cnf" 1722610814.59577 475 c0e671620eb5563b2130f56340a5fde8 ""
|
||||
"/usr/share/texlive/texmf-dist/fonts/enc/dvips/base/8r.enc" 1165713224 4850 80dc9bab7f31fb78a000ccfed0e27cab ""
|
||||
"/usr/share/texlive/texmf-dist/fonts/map/fontname/texfonts.map" 1577235249 3524 cb3e574dea2d1052e39280babc910dc8 ""
|
||||
"/usr/share/texlive/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm" 1136768653 1408 5937f58aa508ea2cea4901c07d10f5fe ""
|
||||
"/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/psyro.tfm" 1136768653 1544 23a042a74981a3e4b6ce2e350e390409 ""
|
||||
"/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm" 1136768653 2172 fd0c924230362ff848a33632ed45dc23 ""
|
||||
"/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb8r.tfm" 1136768653 4524 6bce29db5bc272ba5f332261583fee9c ""
|
||||
@ -19,14 +18,7 @@
|
||||
"/usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm" 1246382020 916 f87d7c45f9c908e672703b83b72241a3 ""
|
||||
"/usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm" 1246382020 908 2921f8a10601f252058503cc6570e581 ""
|
||||
"/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmmi10.tfm" 1136768653 1528 abec98dbc43e172678c11b3b9031252a ""
|
||||
"/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmr10.tfm" 1136768653 1296 45809c5a464d5f32c8f98ba97c1bb47f ""
|
||||
"/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmr12.tfm" 1136768653 1288 655e228510b4c2a1abe905c368440826 ""
|
||||
"/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmsy10.tfm" 1136768653 1124 6c73e740cf17375f03eec0ee63599741 ""
|
||||
"/usr/share/texlive/texmf-dist/fonts/tfm/public/rsfs/rsfs10.tfm" 1229303445 688 37338d6ab346c2f1466b29e195316aa4 ""
|
||||
"/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb" 1248133631 36299 5f9df58c2139e7edcf37c8fca4bd384d ""
|
||||
"/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb" 1248133631 35752 024fb6c41858982481f6968b5fc26508 ""
|
||||
"/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb" 1248133631 32569 5e5ddc8df908dea60932f3c484a54c0d ""
|
||||
"/usr/share/texlive/texmf-dist/fonts/type1/urw/symbol/usyr.pfb" 1136849748 33709 b09d2e140b7e807d3a97058263ab6693 ""
|
||||
"/usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmb8a.pfb" 1136849748 44729 811d6c62865936705a31c797a1d5dada ""
|
||||
"/usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmr8a.pfb" 1136849748 46026 6dab18b61c907687b520c72847215a68 ""
|
||||
"/usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmri8a.pfb" 1136849748 45458 a3faba884469519614ca56ba5f6b1de1 ""
|
||||
@ -35,8 +27,6 @@
|
||||
"/usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmr8c.vf" 1136768653 3556 8a9a6dcbcd146ef985683f677f4758a6 ""
|
||||
"/usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmri7t.vf" 1136768653 1384 a9d8adaf491ce34e5fba99dc7bbe5f39 ""
|
||||
"/usr/share/texlive/texmf-dist/fonts/vf/adobe/times/zptmcm7m.vf" 1136768653 1132 27520247d3fe18d4266a226b461885c2 ""
|
||||
"/usr/share/texlive/texmf-dist/fonts/vf/adobe/times/zptmcm7t.vf" 1136768653 1108 d271d6f9de4122c3f8d3b65666167fac ""
|
||||
"/usr/share/texlive/texmf-dist/fonts/vf/adobe/times/zptmcm7y.vf" 1136768653 964 5673178ff30617b900214de28ab32b38 ""
|
||||
"/usr/share/texlive/texmf-dist/tex/context/base/mkii/supp-pdf.mkii" 1461363279 71627 94eb9990bed73c364d7f53f960cc8c5b ""
|
||||
"/usr/share/texlive/texmf-dist/tex/generic/iftex/iftex.sty" 1644112042 7237 bdd120a32c8fdb4b433cf9ca2e7cd98a ""
|
||||
"/usr/share/texlive/texmf-dist/tex/generic/iftex/ifvtex.sty" 1572645307 1057 525c2192b5febbd8c1f662c9468335bb ""
|
||||
@ -221,10 +211,10 @@
|
||||
"/usr/share/texmf/web2c/texmf.cnf" 1707919699 40399 f2c302f7d2af602abb742093540a5834 ""
|
||||
"/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map" 1722610820.43889 128028 f533b797fba58d231669ea19e894e23e ""
|
||||
"/var/lib/texmf/web2c/pdftex/pdflatex.fmt" 1726005817 6800784 2b63e5a224c5ad740802d8f9921962c1 ""
|
||||
"dane_proposal_format.cls" 1760370937.93092 2555 2a01bb8bad8f4ed4e921f0e44566678c ""
|
||||
"main.aux" 1760990397.47327 1085 9e68fae35f59a6899f3340eaf1c73ae0 "pdflatex"
|
||||
"main.tex" 1760990396.41916 316 db7ca25ef1aea8ffbcbf35ffc893f193 ""
|
||||
"whitepaper/v1.tex" 1760990371.68075 59622 b94eab76770c3fd9ee71c7178c32dfef ""
|
||||
"dane_proposal_format.cls" 1760994752.93894 2596 f4b1a6fb5a74347c13e92ea1ba135818 ""
|
||||
"main.aux" 1760994768.47467 923 a0e5e8073ff8be27724bce962cac74dd "pdflatex"
|
||||
"main.tex" 1760990942.42923 316 db7ca25ef1aea8ffbcbf35ffc893f193 ""
|
||||
"whitepaper/v1.tex" 1760994601.26193 23492 0df1332b575872555e2b920878fd817b ""
|
||||
(generated)
|
||||
"main.aux"
|
||||
"main.log"
|
||||
|
||||
@ -413,10 +413,9 @@ INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmb7t.vf
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb8r.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmr7t.vf
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmb7t.vf
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb8r.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmri7t.vf
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri8r.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7t.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7t.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7t.tfm
|
||||
@ -433,34 +432,21 @@ INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/zptmcm7t.vf
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmr10.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/zptmcm7m.vf
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/psyro.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmmi10.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri8r.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmri7t.vf
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/zptmcm7y.vf
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmsy10.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/rsfs/rsfs10.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/ts1ptm.fd
|
||||
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/ts1ptm.fd
|
||||
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/ts1ptm.fd
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr8c.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmr8c.vf
|
||||
INPUT main.aux
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/type1/urw/symbol/usyr.pfb
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmb8a.pfb
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmr8a.pfb
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmri8a.pfb
|
||||
|
||||
@ -1,4 +1,4 @@
|
||||
This is pdfTeX, Version 3.141592653-2.6-1.40.25 (TeX Live 2023/Debian) (preloaded format=pdflatex 2024.9.10) 20 OCT 2025 15:59
|
||||
This is pdfTeX, Version 3.141592653-2.6-1.40.25 (TeX Live 2023/Debian) (preloaded format=pdflatex 2024.9.10) 20 OCT 2025 17:12
|
||||
entering extended mode
|
||||
restricted \write18 enabled.
|
||||
file:line:error style messages enabled.
|
||||
@ -876,46 +876,36 @@ LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <8> not available
|
||||
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 5.
|
||||
[1
|
||||
|
||||
{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}{/usr/share/texlive/texmf-dist/fonts/enc/dvips/base/8r.enc}] (./whitepaper/v1.tex [1] [2] [3] [4]
|
||||
{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}{/usr/share/texlive/texmf-dist/fonts/enc/dvips/base/8r.enc}] (./whitepaper/v1.tex [1] [2] [3]
|
||||
LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <12> not available
|
||||
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 214.
|
||||
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 212.
|
||||
LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <9> not available
|
||||
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 214.
|
||||
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 212.
|
||||
LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <7> not available
|
||||
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 214.
|
||||
[5] [6]
|
||||
Overfull \hbox (79.94554pt too wide) in paragraph at lines 372--378
|
||||
\OT1/ptm/m/n/12 ment trans-lates into tem-po-ral logic as: $\OML/ztmcm/m/it/12 G\OT1/ztmcm/m/n/12 (\OML/ztmcm/m/it/12 HighTemp \OMS/ztmcm/m/n/12 ! \OML/ztmcm/m/it/12 X\OT1/ztmcm/m/n/12 (\OML/ztmcm/m/it/12 RodsInserted \OMS/ztmcm/m/n/12 ^ \OT1/ztmcm/m/n/12 (\OMS/ztmcm/m/n/12 :\OML/ztmcm/m/it/12 RodsWithdrawn U OperatorReset\OT1/ztmcm/m/n/12 )))$\OT1/ptm/m/n/12 .
|
||||
[]
|
||||
|
||||
[7]
|
||||
Overfull \hbox (19.73378pt too wide) in paragraph at lines 412--423
|
||||
\OT1/ptm/m/n/12 op-er-at-ing pro-ce-dures, we can prove that the automaton---and there-fore our hy-brid switch-ing behavior---
|
||||
[]
|
||||
|
||||
[8] [9]
|
||||
LaTeX Font Info: Trying to load font information for TS1+ptm on input line 535.
|
||||
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 212.
|
||||
[4] [5]
|
||||
LaTeX Font Info: Trying to load font information for TS1+ptm on input line 344.
|
||||
(/usr/share/texlive/texmf-dist/tex/latex/psnfss/ts1ptm.fd
|
||||
File: ts1ptm.fd 2001/06/04 font definitions for TS1/ptm.
|
||||
) [10] [11]) [12] (./main.aux)
|
||||
) [6]) [7] (./main.aux)
|
||||
***********
|
||||
LaTeX2e <2023-11-01> patch level 1
|
||||
L3 programming layer <2024-01-22>
|
||||
***********
|
||||
)
|
||||
Here is how much of TeX's memory you used:
|
||||
25373 strings out of 476182
|
||||
526915 string characters out of 5795595
|
||||
25363 strings out of 476182
|
||||
526810 string characters out of 5795595
|
||||
1934975 words of memory out of 5000000
|
||||
46831 multiletter control sequences out of 15000+600000
|
||||
590992 words of font info for 106 fonts, out of 8000000 for 9000
|
||||
46826 multiletter control sequences out of 15000+600000
|
||||
587807 words of font info for 99 fonts, out of 8000000 for 9000
|
||||
14 hyphenation exceptions out of 8191
|
||||
110i,6n,107p,1008b,285s stack positions out of 10000i,1000n,20000p,200000b,200000s
|
||||
</usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/symbol/usyr.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmb8a.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmr8a.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmri8a.pfb>
|
||||
Output written on main.pdf (13 pages, 109205 bytes).
|
||||
</usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmb8a.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmr8a.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmri8a.pfb>
|
||||
Output written on main.pdf (8 pages, 68969 bytes).
|
||||
PDF statistics:
|
||||
110 PDF objects out of 1000 (max. 8388607)
|
||||
64 compressed objects within 1 object stream
|
||||
74 PDF objects out of 1000 (max. 8388607)
|
||||
41 compressed objects within 1 object stream
|
||||
0 named destinations out of 1000 (max. 500000)
|
||||
109 words of extra memory for PDF output out of 10000 (max. 10000000)
|
||||
|
||||
|
||||
Binary file not shown.
Binary file not shown.
@ -1,4 +1,3 @@
|
||||
\newpage
|
||||
|
||||
% PROJECT SUMMARY
|
||||
\section*{Project Summary}
|
||||
@ -99,546 +98,7 @@ correct by construction. Third, we will develop and verify continuous
|
||||
controllers for each discrete mode using standard control theory and
|
||||
reachability analysis. We will classify continuous modes based on their
|
||||
transition objectives, and then employ assume-guarantee contracts and barrier
|
||||
certificates to prove that mod\documentclass[11pt]{article}
|
||||
|
||||
% Page setup
|
||||
\usepackage[margin=1in]{geometry}
|
||||
\usepackage{setspace}
|
||||
\setstretch{1.0}
|
||||
|
||||
% Packages
|
||||
\usepackage{amsmath}
|
||||
\usepackage{cite}
|
||||
|
||||
% Document begins
|
||||
\begin{document}
|
||||
|
||||
% COVER SHEET
|
||||
\begin{center}
|
||||
{\Large \textbf{From Cold Start to Critical: Formal Synthesis of Hybrid \\
|
||||
Controllers for Nuclear Reactor Startup}}
|
||||
|
||||
\vspace{0.5in}
|
||||
|
||||
\textbf{White Paper}
|
||||
|
||||
\vspace{0.25in}
|
||||
|
||||
\textbf{NSF Program:} Cyber-Physical Systems (CPS)
|
||||
|
||||
\vspace{0.25in}
|
||||
|
||||
\textbf{Principal Investigator:} Dane A. Sabo\\
|
||||
Email: dane.sabo@pitt.edu
|
||||
|
||||
\vspace{0.25in}
|
||||
|
||||
\textbf{Faculty Advisor:} Dr. Daniel G. Cole\\
|
||||
Email: dgcole@pitt.edu
|
||||
|
||||
\vspace{0.25in}
|
||||
|
||||
University of Pittsburgh\\
|
||||
Department of Mechanical Engineering and Materials Science\\
|
||||
Swanson School of Engineering
|
||||
|
||||
\end{center}
|
||||
|
||||
\newpage
|
||||
|
||||
% PROJECT SUMMARY
|
||||
\section*{Project Summary}
|
||||
|
||||
\subsection*{Overview}
|
||||
|
||||
This research will develop a methodology for creating autonomous hybrid
|
||||
control systems with mathematical guarantees of safe and correct behavior.
|
||||
Nuclear power plants require the highest levels of control system reliability,
|
||||
where failures can result in significant economic losses or radiological
|
||||
release. Currently, nuclear operations rely on extensively trained human
|
||||
operators who follow detailed written procedures to manage reactor control.
|
||||
However, reliance on human operators prevents introduction of autonomous
|
||||
control capabilities and creates fundamental economic challenges for
|
||||
next-generation reactor designs. Emerging technologies like small modular
|
||||
reactors face significantly higher per-megawatt staffing costs than
|
||||
conventional plants, threatening their economic viability.
|
||||
|
||||
To address this need, we will combine formal methods from computer science
|
||||
with control theory to build hybrid control systems that are correct by
|
||||
construction. Hybrid systems use discrete logic to switch between continuous
|
||||
control modes, similar to 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. 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.
|
||||
|
||||
\subsection*{Intellectual Merit}
|
||||
|
||||
The intellectual merit lies in unifying discrete synthesis and continuous
|
||||
verification to enable end-to-end correctness guarantees for hybrid systems.
|
||||
This research will advance knowledge by developing a systematic,
|
||||
tool-supported methodology for translating written procedures into temporal
|
||||
logic, synthesizing provably correct discrete switching logic, and developing
|
||||
verified continuous controllers. The approach addresses a fundamental gap in
|
||||
hybrid system design by bridging formal methods from computer science and
|
||||
control theory.
|
||||
|
||||
\subsection*{Broader Impacts}
|
||||
|
||||
This research directly addresses the multi-billion dollar operations and
|
||||
maintenance cost challenge facing nuclear power deployment. By synthesizing
|
||||
provably correct hybrid controllers, we can automate routine operational
|
||||
sequences that currently require constant human oversight, enabling a shift
|
||||
from direct operator control to supervisory monitoring. Beyond nuclear
|
||||
applications, this research will establish a generalizable framework for
|
||||
autonomous control of safety-critical systems including chemical process
|
||||
control, aerospace systems, and autonomous transportation.
|
||||
|
||||
\newpage
|
||||
|
||||
% RESEARCH DESCRIPTION
|
||||
\section*{Research Description}
|
||||
|
||||
\section{Objectives}
|
||||
|
||||
The goal of this research is to develop a methodology for creating autonomous
|
||||
hybrid control systems with mathematical guarantees of safe and correct
|
||||
behavior for nuclear reactor operations. Nuclear reactors are quintessential
|
||||
hybrid cyber-physical systems where continuous neutron kinetics and
|
||||
thermal-hydraulics interact with discrete control mode decisions and trip
|
||||
logic. Hybrid systems combine continuous dynamics with discrete mode
|
||||
transitions, formally expressed as $\dot{x}(t) = f(x(t),q(t),u(t))$ for
|
||||
continuous states and $q(k+1) = \nu(x(k),q(k),u(k))$ for discrete
|
||||
transitions.
|
||||
|
||||
If this research is successful, we will be able to do the following:
|
||||
|
||||
\begin{enumerate}
|
||||
\item \textit{Synthesize written procedures into verified control logic.}
|
||||
We will develop a methodology for converting written operating procedures
|
||||
into formal specifications. These specifications will be synthesized into
|
||||
discrete control logic using reactive synthesis tools. This process uses
|
||||
structured intermediate representations to bridge natural language and
|
||||
mathematical logic. Control engineers will be able to generate
|
||||
mode-switching controllers from regulatory procedures with little formal
|
||||
methods expertise, reducing barriers to high-assurance control systems.
|
||||
|
||||
\item \textit{Verify continuous control behavior across mode transitions.}
|
||||
We will develop methods using reachability analysis to ensure continuous
|
||||
control modes satisfy discrete transition requirements. Engineers will be
|
||||
able to design continuous controllers using standard practices while
|
||||
ensuring system correctness and proving mode transitions occur safely at
|
||||
the right times.
|
||||
|
||||
\item \textit{Demonstrate autonomous reactor startup control with safety
|
||||
guarantees.} We will implement this methodology on a small modular
|
||||
reactor simulation using industry-standard control hardware. This trial
|
||||
will include multiple coordinated control modes from cold shutdown through
|
||||
criticality to power operation on a SmAHTR reactor simulation in a
|
||||
hardware-in-the-loop experiment. Control engineers will be able to
|
||||
implement high-assurance autonomous controls on industrial platforms they
|
||||
already use, enabling users to achieve autonomy without retraining costs
|
||||
or developing new equipment.
|
||||
\end{enumerate}
|
||||
|
||||
\section{Limits of Current Practice}
|
||||
|
||||
Nuclear reactor control reveals fundamental verification gaps that motivate
|
||||
formal hybrid control synthesis. These gaps span current operational
|
||||
practices, human reliability, and even the most advanced formal methods
|
||||
attempts to date.
|
||||
|
||||
Current generation nuclear power plants employ over 3,600 active NRC-licensed
|
||||
reactor operators who hold legal authority to make critical decisions
|
||||
including departing from regulations during emergencies. This authority is
|
||||
both necessary and problematic. The Three Mile Island accident demonstrated
|
||||
how personnel error led to partial meltdown when operators misread confusing
|
||||
readings and shut off emergency systems. The President's Commission identified
|
||||
a fundamental ambiguity: operators hold full responsibility without formal
|
||||
verification they can fulfill this under all conditions.
|
||||
|
||||
Nuclear plant procedures exist in a hierarchy from normal operating procedures
|
||||
through Emergency Operating Procedures to Severe Accident Management
|
||||
Guidelines. Despite rigorous development processes including technical
|
||||
evaluation and simulator validation testing, these procedures fundamentally
|
||||
lack formal verification. No mathematical proof exists that procedures cover
|
||||
all possible plant states or that required actions can be completed within
|
||||
available timeframes. This gap between procedural rigor and mathematical
|
||||
certainty creates the first major limitation of current practice.
|
||||
|
||||
The division between automated and human-controlled functions reveals the
|
||||
fundamental hybrid control challenge. Highly automated systems handle reactor
|
||||
protection and emergency core cooling, while human operators retain strategic
|
||||
decision-making. Current practice treats continuous plant dynamics and
|
||||
discrete control logic as separate concerns without formal integration. No
|
||||
application of hybrid control theory exists that could provide mathematical
|
||||
guarantees across mode transitions.
|
||||
|
||||
Human factors compound these verification gaps. Multiple independent analyses
|
||||
show that 70--80\% of all nuclear power plant events are attributed to human
|
||||
error rather than equipment failures. More significantly, the IAEA concluded
|
||||
that human error was the root cause of all severe accidents at nuclear power
|
||||
plants. The persistence of this ratio despite four decades of improvements
|
||||
suggests fundamental cognitive limitations rather than remediable
|
||||
deficiencies.
|
||||
|
||||
The Three Mile Island accident provides the definitive case study. When a
|
||||
pressure-operated relief valve stuck open, instrumentation showed only
|
||||
commanded position, not actual position. This information gap proved decisive.
|
||||
When Emergency Core Cooling pumps automatically activated, operators shut them
|
||||
down based on incorrect assessment. Operators faced over 100 simultaneous
|
||||
alarms, overwhelming their cognitive capacity. The core suffered 44\% fuel
|
||||
meltdown before stabilization.
|
||||
|
||||
Human Reliability Analysis methods quantify these limitations. Nominal Human
|
||||
Error Probabilities stand at 0.01 (1\%) for diagnosis tasks under optimal
|
||||
conditions. These rates degrade dramatically under accident conditions:
|
||||
inadequate time increases error probability 10-fold, extreme stress by 5-fold,
|
||||
high complexity by 5-fold. Under combined adverse conditions, human error
|
||||
probabilities approach 0.1 to 1.0---essentially guaranteed failure.
|
||||
|
||||
The underlying causes are fundamental and cannot be overcome through training
|
||||
alone. Response time limitations constrain effectiveness. Visual perception
|
||||
requires 100-200 milliseconds, decisions 200-400 milliseconds. Reactor
|
||||
transients evolve in seconds. Protection systems must respond in milliseconds,
|
||||
100-1000 times faster than humans. Working memory capacity is limited to
|
||||
7$\pm$2 chunks, explaining why TMI's 100+ alarms exceeded operators'
|
||||
processing capacity. These are not training failures---they are fundamental
|
||||
properties of human cognition.
|
||||
|
||||
Recent efforts to apply formal methods to nuclear control show both promise
|
||||
and remaining gaps. The High Assurance Rigorous Digital Engineering for
|
||||
Nuclear Safety (HARDENS) project represents the most advanced application to
|
||||
date. Completed in nine months at a fraction of typical costs, HARDENS
|
||||
produced a complete Reactor Trip System with full traceability from NRC
|
||||
requirements through formal specifications to verified binaries.
|
||||
|
||||
The project employed impressive formal methods. FRET handled requirements
|
||||
elicitation. Cryptol provided executable specifications. SAW performed
|
||||
verification. Automatic code synthesis generated formally verifiable
|
||||
implementations. This comprehensive approach demonstrated that formal methods
|
||||
are technically feasible and economically viable for nuclear protection
|
||||
systems.
|
||||
|
||||
Despite these accomplishments, HARDENS has a fundamental limitation directly
|
||||
relevant to our work. The project addressed only discrete digital control
|
||||
logic without modeling or verifying continuous reactor dynamics. Real reactor
|
||||
safety depends on interaction between continuous processes---temperature,
|
||||
pressure, neutron flux---and discrete control decisions. HARDENS verified the
|
||||
discrete controller in isolation but not the closed-loop hybrid system
|
||||
behavior.
|
||||
|
||||
Experimental validation presents the second major limitation. HARDENS produced
|
||||
a demonstrator at Technology Readiness Level 3--4 rather than a
|
||||
deployment-ready system. The gap between formal verification and actual
|
||||
deployment involves integration with legacy systems, long-term reliability
|
||||
under harsh environments, and regulatory acceptance of formal methods as
|
||||
primary assurance evidence.
|
||||
|
||||
These three converging lines reveal the research imperative. Current practice
|
||||
lacks formal verification of procedures and mode transitions. Human operators
|
||||
contribute to 70--80\% of incidents despite continuous improvements,
|
||||
suggesting fundamental rather than remediable limitations. HARDENS
|
||||
demonstrated feasibility of formal methods but addressed only discrete logic,
|
||||
leaving hybrid dynamics unverified. The continuous dynamics of reactor physics
|
||||
combined with discrete control logic demand hybrid automata or differential
|
||||
dynamic logic that can verify properties spanning both domains. This gap
|
||||
defines the research opportunity.
|
||||
|
||||
\section{Research Approach}
|
||||
|
||||
This research will overcome the identified limitations by combining formal
|
||||
methods from computer science with control theory to build hybrid control
|
||||
systems that are correct by construction. We accomplish this through three
|
||||
main thrusts that progress from written procedures to verified implementations.
|
||||
|
||||
Commercial nuclear power operations remain manually controlled despite
|
||||
significant advances in control systems. The key insight is that procedures
|
||||
performed by human operators are highly prescriptive and well-documented.
|
||||
Written procedures in nuclear power are sufficiently detailed that we may
|
||||
translate them into logical formulae with minimal effort. This translation
|
||||
forms the foundation of our approach.
|
||||
|
||||
To formalize these procedures, we will use temporal logic, which captures
|
||||
system behaviors through temporal relations. Linear Temporal Logic provides
|
||||
four fundamental operators: next ($X$), eventually ($F$), globally ($G$), and
|
||||
until ($U$). These operators enable precise specification of time-dependent
|
||||
requirements.
|
||||
|
||||
Consider a nuclear reactor SCRAM requirement: ``If a high temperature alarm
|
||||
triggers, control rods must immediately insert and remain inserted until
|
||||
operator reset.'' This natural language statement translates into temporal
|
||||
logic as: $G(HighTemp \rightarrow X(RodsInserted \wedge (\neg RodsWithdrawn\
|
||||
U\ OperatorReset)))$. The specification precisely captures the temporal
|
||||
relationship between alarm, response, and persistence requirement.
|
||||
|
||||
The most efficient path to accomplish this translation is through NASA's
|
||||
Formal Requirements Elicitation Tool (FRET). FRET employs FRETish, a
|
||||
specialized requirements language that restricts requirements to easily
|
||||
understood components while eliminating ambiguity. FRET enforces structure by
|
||||
requiring all requirements to contain six components: Scope, Condition,
|
||||
Component, Shall, Timing, and Response.
|
||||
|
||||
FRET provides functionality to check realizability of a system. Realizability
|
||||
analysis determines whether written requirements are complete by examining the
|
||||
six structural components. Complete requirements neither conflict with one
|
||||
another nor leave any behavior undefined. Systems that are not realizable
|
||||
contain behavioral inconsistencies that represent the physical equivalent of
|
||||
software bugs. Using FRET during autonomous controller development allows us
|
||||
to identify and resolve these errors systematically. FRET exports requirements
|
||||
in temporal logic format compatible with reactive synthesis tools, enabling
|
||||
the second thrust of our approach.
|
||||
|
||||
Reactive synthesis is an active research field focused on generating discrete
|
||||
controllers from temporal logic specifications. The term reactive indicates
|
||||
that the system responds to environmental inputs to produce control outputs.
|
||||
These synthesized systems are finite in size, where each node represents a
|
||||
unique discrete state. The connections between nodes, called state
|
||||
transitions, specify the conditions under which the discrete controller moves
|
||||
from state to state. This complete mapping constitutes a discrete automaton.
|
||||
|
||||
We will employ state-of-the-art reactive synthesis tools, particularly Strix,
|
||||
which has demonstrated superior performance in the Reactive Synthesis
|
||||
Competition through efficient parity game solving algorithms. Strix translates
|
||||
linear temporal logic specifications into deterministic automata automatically
|
||||
while maximizing generated automata quality. Once constructed, the automaton
|
||||
can be straightforwardly implemented using standard programming control flow
|
||||
constructs.
|
||||
|
||||
The discrete automata representation yields an important theoretical
|
||||
guarantee. Because the discrete automaton is synthesized entirely through
|
||||
automated tools from design requirements and operating procedures, we can
|
||||
prove that the automaton---and therefore our hybrid switching behavior---is
|
||||
correct by construction. This correctness guarantee is paramount. Mode
|
||||
switching represents the primary responsibility of human operators in control
|
||||
rooms today. Human operators possess the advantage of real-time
|
||||
judgment---when mistakes occur, they can correct them dynamically. Autonomous
|
||||
control lacks this adaptive advantage. By synthesizing controllers from
|
||||
logical specifications with guaranteed correctness, we eliminate the
|
||||
possibility of switching errors.
|
||||
|
||||
While discrete system components will be synthesized with correctness
|
||||
guarantees, they represent only half of the complete system. The continuous
|
||||
modes will be developed after discrete automaton construction, leveraging the
|
||||
automaton structure and transitions to design multiple smaller, specialized
|
||||
continuous controllers. This progression from discrete to continuous design
|
||||
addresses a key challenge in hybrid system verification.
|
||||
|
||||
The discrete automaton transitions mark decision points for switching between
|
||||
continuous control modes and define their strategic objectives. We will
|
||||
classify three types of high-level continuous controller objectives:
|
||||
Stabilizing modes maintain the hybrid system within its current discrete mode,
|
||||
corresponding to steady-state normal operating modes like full-power
|
||||
load-following control. Transitory modes have the primary goal of
|
||||
transitioning the hybrid system from one discrete state to another, such as
|
||||
controlled warm-up procedures. Expulsory modes are specialized transitory
|
||||
modes with additional safety constraints that ensure the system is directed to
|
||||
a safe stabilizing mode during failure conditions, such as reactor SCRAM.
|
||||
|
||||
Building continuous modes after constructing discrete automata enables local
|
||||
controller design focused on satisfying discrete transitions. The primary
|
||||
challenge in hybrid system verification is ensuring global stability across
|
||||
transitions. Current techniques struggle with this problem because dynamic
|
||||
discontinuities complicate verification. This work alleviates these problems
|
||||
by designing continuous controllers specifically with transitions in mind. By
|
||||
decomposing continuous modes according to their required behavior at
|
||||
transition points, we avoid solving trajectories through the entire hybrid
|
||||
system.
|
||||
|
||||
To ensure continuous modes satisfy their requirements, we will employ three
|
||||
complementary techniques. Reachability analysis computes the reachable set of
|
||||
states for a given input set. We will use reachability to define continuous
|
||||
state ranges at discrete transition boundaries and verify that requirements
|
||||
are satisfied within continuous modes. Assume-guarantee contracts will be
|
||||
employed when continuous state boundaries are not explicitly defined. For any
|
||||
given mode, the input range for reachability analysis is defined by the output
|
||||
ranges of discrete modes that transition to it. This compositional approach
|
||||
ensures each continuous controller is prepared for its possible input range.
|
||||
Barrier certificates will prove that mode transitions are satisfied. Control
|
||||
barrier functions provide a method to certify safety by establishing
|
||||
differential inequality conditions that guarantee forward invariance of safe
|
||||
sets.
|
||||
|
||||
Combining these three techniques will enable us to prove that continuous
|
||||
components satisfy discrete requirements and thus complete system behavior. To
|
||||
demonstrate this methodology, we will develop an autonomous startup controller
|
||||
for a Small Modular Advanced High Temperature Reactor (SmAHTR). SmAHTR
|
||||
represents an ideal test case with well-documented startup procedures that
|
||||
must transition through multiple distinct operational modes: initial cold
|
||||
conditions, controlled heating to operating temperature, approach to
|
||||
criticality, low-power physics testing, and power ascension to full operating
|
||||
capacity.
|
||||
|
||||
We have already developed a high-fidelity SmAHTR model in Simulink that
|
||||
captures the thermal-hydraulic and neutron kinetics behavior. The synthesized
|
||||
hybrid controller will be implemented on an Emerson Ovation control system
|
||||
platform, which is representative of industry-standard control hardware. The
|
||||
Advanced Reactor Cyber Analysis and Development Environment (ARCADE) suite
|
||||
will serve as the integration layer, managing real-time communication between
|
||||
the Simulink simulation and the Ovation controller. This hardware-in-the-loop
|
||||
configuration enables validation of the controller implementation on actual
|
||||
industrial control equipment.
|
||||
|
||||
\section{Metrics of Success}
|
||||
|
||||
This research will be measured by advancement through Technology Readiness
|
||||
Levels, progressing from fundamental concepts to validated prototype
|
||||
demonstration. The work begins at TRL 2--3 and aims to reach TRL 5, where
|
||||
system components operate successfully in a relevant laboratory environment.
|
||||
|
||||
TRLs provide the ideal success metric because they explicitly measure the gap
|
||||
between academic proof-of-concept and practical deployment. This gap is
|
||||
precisely what our work aims to bridge. TRLs capture both theoretical rigor
|
||||
and practical feasibility simultaneously. The nuclear industry already uses
|
||||
TRLs for technology assessment, making this metric directly relevant to
|
||||
potential adopters.
|
||||
|
||||
Moving from current state (TRL 2--3) to target (TRL 5) requires achieving
|
||||
three intermediate levels. TRL 3 demonstrates that each component works in
|
||||
isolation. Startup procedures must be translated into temporal logic
|
||||
specifications that pass realizability analysis. A discrete automaton must be
|
||||
synthesized with interpretable structure. At least one continuous controller
|
||||
must be designed with verified transition requirements. This level proves the
|
||||
fundamental approach on simplified sequences.
|
||||
|
||||
TRL 4 demonstrates a complete integrated hybrid controller in simulation. All
|
||||
startup procedures must be formalized with continuous controllers existing for
|
||||
all discrete modes. Verification must be complete for all mode transitions.
|
||||
The integrated controller must execute complete startup sequences with zero
|
||||
safety violations. This level proves that formal correctness guarantees can be
|
||||
maintained throughout system integration.
|
||||
|
||||
TRL 5 demonstrates the verified controller on industrial control hardware
|
||||
through hardware-in-the-loop testing. The discrete automaton must be
|
||||
implemented on Emerson Ovation hardware and verified to match synthesized
|
||||
specifications exactly. The ARCADE interface must establish stable real-time
|
||||
communication between Ovation hardware and SmAHTR simulation. Complete
|
||||
autonomous startup sequences must execute across the full operational
|
||||
envelope. This level proves that the methodology produces verified controllers
|
||||
implementable with current technology.
|
||||
|
||||
This research succeeds if it achieves TRL 5, establishing both theoretical
|
||||
validity and practical feasibility. Success provides a clear pathway for
|
||||
nuclear industry adoption and broader application to safety-critical
|
||||
autonomous systems.
|
||||
|
||||
\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 for hyperscale
|
||||
datacenters. According to the U.S. Energy Information Administration, advanced
|
||||
nuclear power entering service in 2027 is projected to cost \$88.24 per
|
||||
megawatt-hour. With datacenter electricity demand projected to reach 1,050
|
||||
terawatt-hours annually by 2030, operations and maintenance costs represent
|
||||
approximately 23--30\% of total levelized cost, translating to \$21--28
|
||||
billion annually for projected datacenter demand.
|
||||
|
||||
This research directly addresses the multi-billion dollar O\&M cost challenge.
|
||||
Current nuclear operations require full control room staffing for each
|
||||
reactor. These staffing requirements drive high O\&M costs, particularly for
|
||||
smaller reactor designs where the same overhead must be spread across lower
|
||||
power output. The economic burden threatens the viability of next-generation
|
||||
nuclear technologies.
|
||||
|
||||
By synthesizing provably correct hybrid controllers, we 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 transition fundamentally changes
|
||||
the economics of nuclear operations.
|
||||
|
||||
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. By formally verifying both
|
||||
discrete mode-switching logic and continuous control behavior, this research
|
||||
will produce controllers with mathematical proofs of correctness. These
|
||||
guarantees enable automation to safely handle routine operations that
|
||||
currently require human operators to follow written procedures.
|
||||
|
||||
Small modular reactors represent an ideal deployment target. Nuclear
|
||||
Regulatory Commission certification requires extensive documentation of
|
||||
control procedures, operational requirements, and safety analyses written in
|
||||
structured natural language. These regulatory documents can be translated into
|
||||
temporal logic specifications using FRET, synthesized into discrete switching
|
||||
logic using reactive synthesis tools, and verified using reachability analysis
|
||||
and barrier certificates. The infrastructure of requirements is already
|
||||
complete as part of licensing. This creates a direct pathway from existing
|
||||
regulatory documentation to formally verified autonomous controllers.
|
||||
|
||||
Beyond nuclear applications, 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. These domains share similar economic and safety
|
||||
considerations that favor increased autonomy with provable correctness
|
||||
guarantees. By demonstrating this approach in nuclear power---one of the most
|
||||
regulated and safety-critical domains---this research will establish both
|
||||
technical feasibility and regulatory pathways for broader adoption across
|
||||
critical infrastructure.
|
||||
|
||||
\newpage
|
||||
|
||||
% REFERENCES CITED
|
||||
\section*{References Cited}
|
||||
|
||||
\begin{thebibliography}{99}
|
||||
|
||||
\bibitem{10CFR55}
|
||||
U.S. Nuclear Regulatory Commission. ``10 CFR Part 55 - Operators' Licenses.''
|
||||
\textit{Code of Federal Regulations}, 2024.
|
||||
|
||||
\bibitem{princeton}
|
||||
Princeton University. ``Nuclear Reactor Operator Training.''
|
||||
\textit{Princeton Plasma Physics Laboratory}, 2023.
|
||||
|
||||
\bibitem{Kemeny1979}
|
||||
J. G. Kemeny et al. ``Report of the President's Commission on the Accident
|
||||
at Three Mile Island.'' U.S. Government Printing Office, October 1979.
|
||||
|
||||
\bibitem{NUREG-0899}
|
||||
U.S. Nuclear Regulatory Commission. ``Guidelines for the Preparation of
|
||||
Emergency Operating Procedures.'' NUREG-0899, August 1982.
|
||||
|
||||
\bibitem{DOE-HDBK-1028-2009}
|
||||
U.S. Department of Energy. ``Human Performance Improvement Handbook.''
|
||||
DOE-HDBK-1028-2009, June 2009.
|
||||
|
||||
\bibitem{WNA2020}
|
||||
World Nuclear Association. ``Safety of Nuclear Power Reactors.''
|
||||
\textit{World Nuclear Association Information Library}, 2020.
|
||||
|
||||
\bibitem{IAEA-severe-accidents}
|
||||
International Atomic Energy Agency. ``Lessons Learned from Severe Nuclear
|
||||
Accidents.'' IAEA Technical Report, 2016.
|
||||
|
||||
\bibitem{Wang2025}
|
||||
Y. Wang et al. ``Human Error Analysis of 190 Events at Chinese Nuclear
|
||||
Power Plants from 2007-2020.'' \textit{Nuclear Engineering and Design},
|
||||
vol. 395, 2025.
|
||||
|
||||
\bibitem{Kiniry2022}
|
||||
J. Kiniry et al. ``High Assurance Rigorous Digital Engineering for Nuclear
|
||||
Safety (HARDENS).'' NRC Final Technical Report ML22326A307, September 2022.
|
||||
|
||||
\bibitem{eia_lcoe_2022}
|
||||
U.S. Energy Information Administration. ``Levelized Costs of New Generation
|
||||
Resources in the Annual Energy Outlook 2022.'' Report, March 2022.
|
||||
|
||||
\bibitem{eesi_datacenter_2024}
|
||||
Environmental and Energy Study Institute. ``Data Center Energy Needs are
|
||||
Upending Power Grids and Threatening the Climate.'' Web article, 2024.
|
||||
|
||||
\end{thebibliography}
|
||||
|
||||
\end{document}e transitions occur safely and as defined by the
|
||||
certificates to prove that mode transitions occur safely and as defined by the
|
||||
deterministic automata. This compositional approach enables local verification
|
||||
of continuous modes without requiring global trajectory analysis across the
|
||||
entire hybrid system. We will demonstrate this methodology by developing an
|
||||
@ -692,142 +152,71 @@ If this research is successful, we will be able to do the following:
|
||||
achieve autonomy without retraining costs or developing new equipment.
|
||||
|
||||
\end{enumerate}
|
||||
%
|
||||
% % IMPACT PARAGRAPH Innovation
|
||||
% The innovation is unifying discrete synthesis and continuous verification to
|
||||
% enable end-to-end correctness guarantees for hybrid systems.
|
||||
% % Outcome Impact
|
||||
% If successful, control engineers will be able to create autonomous controllers from existing
|
||||
% procedures with mathematical proof of correct behavior, making high-assurance
|
||||
% autonomous control practical for safety-critical applications.
|
||||
% % Impact/Pay-off
|
||||
% This capability is essential for economic viability of next-generation nuclear
|
||||
% power. Small modular reactors represent a promising solution to growing energy
|
||||
% demands, but 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 required by the nuclear industry.
|
||||
\section{State of the Art and Limits of Current Practice}
|
||||
|
||||
\section{Limits of Current Practice}
|
||||
Current generation nuclear power plants employ over 3,600 active NRC-licensed
|
||||
reactor operators who hold legal authority to make critical decisions
|
||||
including departing from regulations during emergencies. This authority is
|
||||
both necessary and problematic, and has caused major nuclear accidents such as
|
||||
the Three Mile Island Accident. The Three Mile Island accident demonstrated
|
||||
how personnel error led to partial meltdown when operators misread confusing
|
||||
readings and shut off emergency systems. The President's Commission identified
|
||||
a fundamental ambiguity: operators hold full responsibility without formal
|
||||
verification they can fulfill this under all conditions.
|
||||
Automation of some nuclear power operations is already performed today. Highly
|
||||
automated systems handle reactor protection and emergency core cooling, while
|
||||
human operators retain strategic decision-making. Autonomous systems are trusted
|
||||
to handle emergency situations that are considered terminal operations, but
|
||||
otherwise introduce too much risk to reactor operations. Contrary to this notion
|
||||
is the fact that 70--80\% of all nuclear power plant events are attributed to
|
||||
human error rather than equipment failures. The persistence of this ratio despite
|
||||
four decades of improvements to procedures and control rooms suggests
|
||||
fundamental cognitive limitations rather than remediable deficiencies.
|
||||
|
||||
Nuclear plant procedures exist in a hierarchy from normal operating procedures
|
||||
through Emergency Operating Procedures to Severe Accident Management
|
||||
Guidelines. Despite rigorous development processes including technical
|
||||
evaluation and simulator validation testing, these procedures fundamentally
|
||||
lack formal verification. No mathematical proof exists that procedures cover
|
||||
all possible plant states or that required actions can be completed within
|
||||
available timeframes.
|
||||
The Nuclear Regulatory Commission has recognized that introducing automation
|
||||
into the control room is the only way forward. Recent efforts to apply formal
|
||||
methods to nuclear control have shown both promise and remaining gaps. The High
|
||||
Assurance Rigorous Digital Engineering for Nuclear Safety (HARDENS) project
|
||||
represents the most advanced application to date. HARDENS produced a complete
|
||||
Reactor Trip System with full traceability from NRC requirements through formal
|
||||
specifications to verified binaries of a controller implementation. The project
|
||||
employed formal methods along the control design stack. This comprehensive
|
||||
approach demonstrated that formal methods may be technically feasible and
|
||||
economically viable for nuclear protection systems.
|
||||
|
||||
% The division between automated and human-controlled functions reveals the
|
||||
% fundamental hybrid control challenge. Highly automated systems handle reactor
|
||||
% protection and emergency core cooling, while human operators retain strategic
|
||||
% decision-making. Current practice treats continuous plant dynamics and
|
||||
% discrete control logic as separate concerns without formal integration. No
|
||||
% application of hybrid control theory exists that could provide mathematical
|
||||
% guarantees across mode transitions.
|
||||
%
|
||||
Human factors compound these verification gaps. 70--80\% of all nuclear power
|
||||
plant events are attributed to human error rather than equipment failures. More
|
||||
significantly, the IAEA concluded that human error was the root cause of all
|
||||
severe accidents at nuclear power plants. The persistence of this ratio despite
|
||||
four decades of improvements suggests fundamental cognitive limitations rather
|
||||
than remediable deficiencies.
|
||||
|
||||
The Three Mile Island accident provides the definitive case study. When a
|
||||
pressure-operated relief valve stuck open, instrumentation showed only
|
||||
commanded position, not actual position. This information gap proved decisive.
|
||||
When Emergency Core Cooling pumps automatically activated, operators shut them
|
||||
down based on incorrect assessment. Operators faced over 100 simultaneous
|
||||
alarms, overwhelming their cognitive capacity. The core suffered 44\% fuel
|
||||
meltdown before stabilization.
|
||||
|
||||
Human Reliability Analysis methods quantify these limitations. Nominal Human
|
||||
Error Probabilities stand at 0.01 (1\%) for diagnosis tasks under optimal
|
||||
conditions. These rates degrade dramatically under accident conditions:
|
||||
inadequate time increases error probability 10-fold, extreme stress by 5-fold,
|
||||
high complexity by 5-fold. Under combined adverse conditions, human error
|
||||
probabilities approach 0.1 to 1.0---essentially guaranteed failure.
|
||||
|
||||
The underlying causes are fundamental and cannot be overcome through training
|
||||
alone. Response time limitations constrain effectiveness. Visual perception
|
||||
requires 100-200 milliseconds, decisions 200-400 milliseconds. Reactor
|
||||
transients evolve in seconds. Protection systems must respond in milliseconds,
|
||||
100-1000 times faster than humans. Working memory capacity is limited to
|
||||
7$\pm$2 chunks, explaining why TMI's 100+ alarms exceeded operators'
|
||||
processing capacity. These are not training failures---they are fundamental
|
||||
properties of human cognition.
|
||||
|
||||
Recent efforts to apply formal methods to nuclear control show both promise
|
||||
and remaining gaps. The High Assurance Rigorous Digital Engineering for
|
||||
Nuclear Safety (HARDENS) project represents the most advanced application to
|
||||
date. Completed in nine months at a fraction of typical costs, HARDENS
|
||||
produced a complete Reactor Trip System with full traceability from NRC
|
||||
requirements through formal specifications to verified binaries.
|
||||
|
||||
The project employed impressive formal methods. FRET handled requirements
|
||||
elicitation. Cryptol provided executable specifications. SAW performed
|
||||
verification. Automatic code synthesis generated formally verifiable
|
||||
implementations. This comprehensive approach demonstrated that formal methods
|
||||
are technically feasible and economically viable for nuclear protection
|
||||
systems.
|
||||
|
||||
Despite these accomplishments, HARDENS has a fundamental limitation directly
|
||||
relevant to our work. The project addressed only discrete digital control
|
||||
logic without modeling or verifying continuous reactor dynamics. Real reactor
|
||||
safety depends on interaction between continuous processes---temperature,
|
||||
pressure, neutron flux---and discrete control decisions. HARDENS verified the
|
||||
discrete controller in isolation but not the closed-loop hybrid system
|
||||
behavior.
|
||||
|
||||
Experimental validation presents the second major limitation. HARDENS produced
|
||||
a demonstrator at Technology Readiness Level 3--4 rather than a
|
||||
deployment-ready system. The gap between formal verification and actual
|
||||
deployment involves integration with legacy systems, long-term reliability
|
||||
under harsh environments, and regulatory acceptance of formal methods as
|
||||
primary assurance evidence.
|
||||
|
||||
These three converging lines reveal the research imperative. Current practice
|
||||
lacks formal verification of procedures and mode transitions. Human operators
|
||||
contribute to 70--80\% of incidents despite continuous improvements,
|
||||
suggesting fundamental rather than remediable limitations. HARDENS
|
||||
demonstrated feasibility of formal methods but addressed only discrete logic,
|
||||
leaving hybrid dynamics unverified. The continuous dynamics of reactor physics
|
||||
combined with discrete control logic demand hybrid automata or differential
|
||||
dynamic logic that can verify properties spanning both domains. This gap
|
||||
defines the research opportunity.
|
||||
But despite these accomplishments, HARDENS has a fundamental limitation directly
|
||||
relevant to our work. The project addressed only discrete digital control logic
|
||||
without modeling or verifying continuous reactor dynamics. Real reactor safety
|
||||
depends on interaction between continuous processes and discrete control
|
||||
decisions. HARDENS verified the discrete controller in isolation but not the
|
||||
closed-loop hybrid system behavior.
|
||||
|
||||
\section{Research Approach}
|
||||
|
||||
This research will overcome the identified limitations by combining formal
|
||||
methods from computer science with control theory to build hybrid control
|
||||
systems that are correct by construction. We accomplish this through three
|
||||
main thrusts that progress from written procedures to verified implementations.
|
||||
main thrusts:
|
||||
|
||||
\begin{enumerate}
|
||||
|
||||
\item We will translate natural language procedures and
|
||||
requirements into temporal logic specifications using the Formal Requirements
|
||||
Elicitation Tool (FRET).
|
||||
|
||||
\item We will synthesize these temporal logic
|
||||
specifications into the discrete component of the hybrid controller using
|
||||
reactive synthesis.
|
||||
|
||||
\item We will build continuous control modes that satisfy discrete controller
|
||||
transition requirements.
|
||||
|
||||
\end{enumerate}
|
||||
|
||||
Commercial nuclear power operations remain manually controlled despite
|
||||
significant advances in control systems. The key insight is that procedures
|
||||
performed by human operators are highly prescriptive and well-documented.
|
||||
Written procedures in nuclear power are sufficiently detailed that we may
|
||||
translate them into logical formulae with minimal effort. This To formalize
|
||||
these procedures, we will use temporal logic, which captures system behaviors
|
||||
through temporal relations. Linear Temporal Logic provides four fundamental
|
||||
operators: next ($X$), eventually ($F$), globally ($G$), and until ($U$). These
|
||||
operators enable precise specification of time-dependent requirements.
|
||||
|
||||
These specifications precisely define behavior in a way that natural language is
|
||||
not able to reproduce. The most efficient path to accomplish this translation is
|
||||
through NASA's Formal Requirements Elicitation Tool (FRET). FRET employs
|
||||
FRETish, a specialized requirements language that restricts requirements to
|
||||
easily understood components while eliminating ambiguity. FRET enforces
|
||||
structure by requiring all requirements to contain six components: Scope,
|
||||
Condition, Component, Shall, Timing, and Response.
|
||||
performed by human operators are highly prescriptive and well-documented. To
|
||||
formalize these procedures, we will use temporal logic, which captures system
|
||||
behaviors through temporal relations. Linear Temporal Logic provides four
|
||||
fundamental operators: next ($X$), eventually ($F$), globally ($G$), and until
|
||||
($U$). These operators enable precise specification of time-dependent
|
||||
requirements. The most efficient path to accomplish this translation is through
|
||||
NASA's Formal Requirements Elicitation Tool (FRET). FRET employs FRETish, a
|
||||
specialized requirements language that restricts requirements to easily
|
||||
understood components while eliminating ambiguity. FRET enforces structure by
|
||||
requiring all requirements to contain six components: Scope, Condition,
|
||||
Component, Shall, Timing, and Response.
|
||||
|
||||
FRET provides functionality to check realizability of a system. Realizability
|
||||
analysis determines whether written requirements are complete by examining the
|
||||
@ -847,32 +236,28 @@ unique discrete state. The connections between nodes, called state
|
||||
transitions, specify the conditions under which the discrete controller moves
|
||||
from state to state. This complete mapping constitutes a discrete automaton.
|
||||
|
||||
We will employ state-of-the-art reactive synthesis tools, particularly Strix,
|
||||
which has demonstrated superior performance in the Reactive Synthesis
|
||||
Competition through efficient parity game solving algorithms. Strix translates
|
||||
linear temporal logic specifications into deterministic automata automatically
|
||||
while maximizing generated automata quality. Once constructed, the automaton
|
||||
can be straightforwardly implemented using standard programming control flow
|
||||
constructs.
|
||||
|
||||
The discrete automata representation yields an important theoretical
|
||||
We will employ reactive synthesis tools which translate linear temporal logic
|
||||
specifications into deterministic automata automatically while maximizing
|
||||
generated automata quality. Once constructed, the automaton can be
|
||||
straightforwardly implemented using standard programming control flow
|
||||
constructs. The discrete automata representation yields an important theoretical
|
||||
guarantee. Because the discrete automaton is synthesized entirely through
|
||||
automated tools from design requirements and operating procedures, we can
|
||||
prove that the automaton---and therefore our hybrid switching behavior---is
|
||||
correct by construction. This correctness guarantee is paramount. Mode
|
||||
switching represents the primary responsibility of human operators in control
|
||||
rooms today. Human operators possess the advantage of real-time
|
||||
judgment---when mistakes occur, they can correct them dynamically. Autonomous
|
||||
control lacks this adaptive advantage. By synthesizing controllers from
|
||||
logical specifications with guaranteed correctness, we eliminate the
|
||||
possibility of switching errors.
|
||||
correct by construction.
|
||||
|
||||
This correctness guarantee is paramount. Mode switching represents the primary
|
||||
responsibility of human operators in control rooms today. Human operators
|
||||
possess the advantage of real-time judgment. When mistakes occur, they can
|
||||
correct them dynamically. Autonomous control lacks this adaptive advantage. By
|
||||
synthesizing controllers from logical specifications with guaranteed
|
||||
correctness, we eliminate the possibility of switching errors.
|
||||
|
||||
While discrete system components will be synthesized with correctness
|
||||
guarantees, they represent only half of the complete system. The continuous
|
||||
modes will be developed after discrete automaton construction, leveraging the
|
||||
automaton structure and transitions to design multiple smaller, specialized
|
||||
continuous controllers. This progression from discrete to continuous design
|
||||
addresses a key challenge in hybrid system verification.
|
||||
continuous controllers.
|
||||
|
||||
The discrete automaton transitions mark decision points for switching between
|
||||
continuous control modes and define their strategic objectives. We will
|
||||
@ -897,14 +282,14 @@ system.
|
||||
|
||||
To ensure continuous modes satisfy their requirements, we will employ three
|
||||
complementary techniques. Reachability analysis computes the reachable set of
|
||||
states for a given input set. We will use reachability to define continuous
|
||||
state ranges at discrete transition boundaries and verify that requirements
|
||||
are satisfied within continuous modes. Assume-guarantee contracts will be
|
||||
states for a given input set. We will use reachability when continuous
|
||||
state ranges at discrete transition boundaries are defined and verify that
|
||||
continuous modes only can reach such defined ranges. Otherwise, assume-guarantee contracts will be
|
||||
employed when continuous state boundaries are not explicitly defined. For any
|
||||
given mode, the input range for reachability analysis is defined by the output
|
||||
ranges of discrete modes that transition to it. This compositional approach
|
||||
ensures each continuous controller is prepared for its possible input range.
|
||||
Barrier certificates will prove that mode transitions are satisfied. Control
|
||||
Finally, barrier certificates will prove that mode transitions are satisfied. Control
|
||||
barrier functions provide a method to certify safety by establishing
|
||||
differential inequality conditions that guarantee forward invariance of safe
|
||||
sets.
|
||||
@ -917,60 +302,38 @@ represents an ideal test case with well-documented startup procedures that
|
||||
must transition through multiple distinct operational modes: initial cold
|
||||
conditions, controlled heating to operating temperature, approach to
|
||||
criticality, low-power physics testing, and power ascension to full operating
|
||||
capacity.
|
||||
capacity. We have access to an already developed high-fidelity SmAHTR model in Simulink that
|
||||
captures the thermal-hydraulic and neutron kinetics behavior.
|
||||
|
||||
We have already developed a high-fidelity SmAHTR model in Simulink that
|
||||
captures the thermal-hydraulic and neutron kinetics behavior. The synthesized
|
||||
hybrid controller will be implemented on an Emerson Ovation control system
|
||||
platform, which is representative of industry-standard control hardware. The
|
||||
Advanced Reactor Cyber Analysis and Development Environment (ARCADE) suite
|
||||
will serve as the integration layer, managing real-time communication between
|
||||
the Simulink simulation and the Ovation controller. This hardware-in-the-loop
|
||||
configuration enables validation of the controller implementation on actual
|
||||
industrial control equipment.
|
||||
The synthesized hybrid controller will be implemented on an Emerson Ovation
|
||||
control system platform, which is representative of industry-standard control
|
||||
hardware. This control system will be used in a hardware-in-the-loop simulation,
|
||||
where the Advanced Reactor Cyber Analysis and Development Environment
|
||||
(ARCADE) suite will serve as the integration layer. This
|
||||
hardware-in-the-loop configuration enables validation of the controller
|
||||
implementation on actual industrial control equipment.
|
||||
|
||||
\section{Metrics of Success}
|
||||
|
||||
This research will be measured by advancement through Technology Readiness
|
||||
Levels, progressing from fundamental concepts to validated prototype
|
||||
demonstration. The work begins at TRL 2--3 and aims to reach TRL 5, where
|
||||
system components operate successfully in a relevant laboratory environment.
|
||||
This research will be measured by advancement through Technology Readiness
|
||||
Levels, progressing from fundamental concepts to validated prototype
|
||||
demonstration. The work begins at TRL 2--3 and aims to reach TRL 5, where system
|
||||
components operate successfully in a relevant laboratory environment. TRLs
|
||||
provide the ideal success metric because they explicitly measure the gap between
|
||||
academic proof-of-concept and practical deployment. This gap is precisely what
|
||||
our work aims to bridge. TRLs capture both theoretical rigor and practical
|
||||
feasibility simultaneously. The nuclear industry already uses TRLs for
|
||||
technology assessment, making this metric directly relevant to potential
|
||||
adopters.
|
||||
|
||||
TRLs provide the ideal success metric because they explicitly measure the gap
|
||||
between academic proof-of-concept and practical deployment. This gap is
|
||||
precisely what our work aims to bridge. TRLs capture both theoretical rigor
|
||||
and practical feasibility simultaneously. The nuclear industry already uses
|
||||
TRLs for technology assessment, making this metric directly relevant to
|
||||
potential adopters.
|
||||
|
||||
Moving from current state (TRL 2--3) to target (TRL 5) requires achieving
|
||||
three intermediate levels. TRL 3 demonstrates that each component works in
|
||||
isolation. Startup procedures must be translated into temporal logic
|
||||
specifications that pass realizability analysis. A discrete automaton must be
|
||||
synthesized with interpretable structure. At least one continuous controller
|
||||
must be designed with verified transition requirements. This level proves the
|
||||
fundamental approach on simplified sequences.
|
||||
|
||||
TRL 4 demonstrates a complete integrated hybrid controller in simulation. All
|
||||
startup procedures must be formalized with continuous controllers existing for
|
||||
all discrete modes. Verification must be complete for all mode transitions.
|
||||
The integrated controller must execute complete startup sequences with zero
|
||||
safety violations. This level proves that formal correctness guarantees can be
|
||||
maintained throughout system integration.
|
||||
|
||||
TRL 5 demonstrates the verified controller on industrial control hardware
|
||||
through hardware-in-the-loop testing. The discrete automaton must be
|
||||
implemented on Emerson Ovation hardware and verified to match synthesized
|
||||
specifications exactly. The ARCADE interface must establish stable real-time
|
||||
communication between Ovation hardware and SmAHTR simulation. Complete
|
||||
autonomous startup sequences must execute across the full operational
|
||||
envelope. This level proves that the methodology produces verified controllers
|
||||
implementable with current technology.
|
||||
|
||||
This research succeeds if it achieves TRL 5, establishing both theoretical
|
||||
validity and practical feasibility. Success provides a clear pathway for
|
||||
nuclear industry adoption and broader application to safety-critical
|
||||
autonomous systems.
|
||||
Moving from current state (TRL 2--3) to target (TRL 5) requires progressing
|
||||
through component isolation, system integration, and hardware validation. By
|
||||
reaching TRL 5, we will have demonstrated a complete autonomous hybrid
|
||||
controller operating on industrial control hardware through hardware-in-the-loop
|
||||
testing. Achieving TRL 5 establishes both theoretical validity and practical
|
||||
feasibility, proving that the methodology produces verified controllers
|
||||
implementable with current technology and providing a clear pathway for nuclear
|
||||
industry adoption and broader application to safety-critical autonomous systems.
|
||||
|
||||
\section{Broader Impacts}
|
||||
|
||||
@ -984,19 +347,17 @@ terawatt-hours annually by 2030, operations and maintenance costs represent
|
||||
approximately 23--30\% of total levelized cost, translating to \$21--28
|
||||
billion annually for projected datacenter demand.
|
||||
|
||||
This research directly addresses the multi-billion dollar O\&M cost challenge.
|
||||
Current nuclear operations require full control room staffing for each
|
||||
reactor. These staffing requirements drive high O\&M costs, particularly for
|
||||
smaller reactor designs where the same overhead must be spread across lower
|
||||
power output. The economic burden threatens the viability of next-generation
|
||||
nuclear technologies.
|
||||
|
||||
By synthesizing provably correct hybrid controllers, we 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 transition fundamentally changes
|
||||
the economics of nuclear operations.
|
||||
This research directly addresses the multi-billion dollar O\&M cost challenge.
|
||||
Current nuclear operations require full control room staffing for each reactor.
|
||||
These staffing requirements drive high O\&M costs, particularly for smaller
|
||||
reactor designs where the same overhead must be spread across lower power
|
||||
output. The economic burden threatens the viability of next-generation nuclear
|
||||
technologies. But, by synthesizing provably correct hybrid controllers, we can
|
||||
automate routine operational sequences that currently require constant human
|
||||
oversight. This enables a change from direct operator control to
|
||||
supervisory monitoring where operators oversee multiple autonomous reactors
|
||||
rather than manually controlling individual units. The transition fundamentally
|
||||
changes the economics of nuclear operations.
|
||||
|
||||
The correct-by-construction methodology is critical for this transition.
|
||||
Traditional automation approaches cannot provide sufficient safety guarantees
|
||||
@ -1007,27 +368,16 @@ will produce controllers with mathematical proofs of correctness. These
|
||||
guarantees enable automation to safely handle routine operations that
|
||||
currently require human operators to follow written procedures.
|
||||
|
||||
Small modular reactors represent an ideal deployment target. Nuclear
|
||||
Regulatory Commission certification requires extensive documentation of
|
||||
control procedures, operational requirements, and safety analyses written in
|
||||
structured natural language. These regulatory documents can be translated into
|
||||
temporal logic specifications using FRET, synthesized into discrete switching
|
||||
logic using reactive synthesis tools, and verified using reachability analysis
|
||||
and barrier certificates. The infrastructure of requirements is already
|
||||
complete as part of licensing. This creates a direct pathway from existing
|
||||
regulatory documentation to formally verified autonomous controllers.
|
||||
|
||||
Beyond nuclear applications, 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. These domains share similar economic and safety
|
||||
considerations that favor increased autonomy with provable correctness
|
||||
guarantees. By demonstrating this approach in nuclear power---one of the most
|
||||
regulated and safety-critical domains---this research will establish both
|
||||
technical feasibility and regulatory pathways for broader adoption across
|
||||
Beyond nuclear applications, 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. These domains share similar economic and safety considerations
|
||||
that favor increased autonomy with provable correctness guarantees. By
|
||||
demonstrating this approach in nuclear power this research will establish both
|
||||
technical feasibility and regulatory pathways for broader adoption across
|
||||
critical infrastructure.
|
||||
|
||||
\newpage
|
||||
@ -1040,10 +390,6 @@ critical infrastructure.
|
||||
U.S. Nuclear Regulatory Commission. ``10 CFR Part 55 - Operators' Licenses.''
|
||||
\textit{Code of Federal Regulations}, 2024.
|
||||
|
||||
\bibitem{princeton}
|
||||
Princeton University. ``Nuclear Reactor Operator Training.''
|
||||
\textit{Princeton Plasma Physics Laboratory}, 2023.
|
||||
|
||||
\bibitem{Kemeny1979}
|
||||
J. G. Kemeny et al. ``Report of the President's Commission on the Accident
|
||||
at Three Mile Island.'' U.S. Government Printing Office, October 1979.
|
||||
@ -1060,18 +406,9 @@ DOE-HDBK-1028-2009, June 2009.
|
||||
World Nuclear Association. ``Safety of Nuclear Power Reactors.''
|
||||
\textit{World Nuclear Association Information Library}, 2020.
|
||||
|
||||
\bibitem{IAEA-severe-accidents}
|
||||
International Atomic Energy Agency. ``Lessons Learned from Severe Nuclear
|
||||
Accidents.'' IAEA Technical Report, 2016.
|
||||
|
||||
\bibitem{Wang2025}
|
||||
Y. Wang et al. ``Human Error Analysis of 190 Events at Chinese Nuclear
|
||||
Power Plants from 2007-2020.'' \textit{Nuclear Engineering and Design},
|
||||
vol. 395, 2025.
|
||||
|
||||
\bibitem{Kiniry2022}
|
||||
J. Kiniry et al. ``High Assurance Rigorous Digital Engineering for Nuclear
|
||||
Safety (HARDENS).'' NRC Final Technical Report ML22326A307, September 2022.
|
||||
Safety (HARDENS).'' NRC Final Technical Report ML22326A307, October 2022.
|
||||
|
||||
\bibitem{eia_lcoe_2022}
|
||||
U.S. Energy Information Administration. ``Levelized Costs of New Generation
|
||||
@ -1083,4 +420,3 @@ Upending Power Grids and Threatening the Climate.'' Web article, 2024.
|
||||
|
||||
\end{thebibliography}
|
||||
|
||||
\end{document}
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user