diff --git a/Writing/ERLM/main.aux b/Writing/ERLM/main.aux index a1d23b021..2f7efb537 100644 --- a/Writing/ERLM/main.aux +++ b/Writing/ERLM/main.aux @@ -1,81 +1,22 @@ \relax \bibstyle{unsrt} \providecommand \oddpage@label [2]{} -\@writefile{toc}{\contentsline {section}{\numberline {1}Goals and Outcomes}{1}{}\protected@file@percent } -\citation{DOE-HDBK-1028-2009,WNA2020,Wang2025} -\citation{10CFR55} -\@writefile{toc}{\contentsline {section}{\numberline {2}State of the Art and Limits of Current Practice}{2}{}\protected@file@percent } -\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}Current Reactor Control Practices}{2}{}\protected@file@percent } -\citation{Kemeny1979} -\citation{Kemeny1979} -\citation{NUREG-0899} -\citation{10CFR55} -\citation{IAEA-TECDOC-1580} -\@writefile{toc}{\contentsline {subsubsection}{\numberline {2.1.1}Human Operators Retain Ultimate Decision Authority}{3}{}\protected@file@percent } -\@writefile{toc}{\contentsline {subsubsection}{\numberline {2.1.2}Operating Procedures Lack Formal Verification}{3}{}\protected@file@percent } -\citation{Zerovnik2023} -\citation{Jo2021} -\citation{IAEA2008} -\@writefile{toc}{\contentsline {subsubsection}{\numberline {2.1.3}Control Mode Transitions Lack Formal Safety Verification}{4}{}\protected@file@percent } -\@writefile{toc}{\contentsline {subsubsection}{\numberline {2.1.4}Current Automation Reveals the Hybrid Dynamics Challenge}{4}{}\protected@file@percent } -\citation{Lee2019} -\citation{IEEE2019} -\citation{DOE-HDBK-1028-2009,WNA2020} -\citation{IAEA-severe-accidents} -\citation{Wang2025} -\citation{Dumas1999} -\citation{Kemeny1979} -\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Human Factors in Nuclear Accidents}{5}{}\protected@file@percent } -\@writefile{toc}{\contentsline {subsubsection}{\numberline {2.2.1}Human Error Dominates Nuclear Incident Causation}{5}{}\protected@file@percent } -\@writefile{toc}{\contentsline {subsubsection}{\numberline {2.2.2}Three Mile Island Revealed Critical Human-Automation Interaction Failures}{5}{}\protected@file@percent } -\citation{NUREG-CR-6883} -\citation{NUREG-2114} -\citation{Rasmussen1983} -\citation{Miller1956} -\citation{Reason1990} -\citation{Kiniry2022} -\@writefile{toc}{\contentsline {subsubsection}{\numberline {2.2.3}Human Reliability Analysis Documents Fundamental Cognitive Limitations}{6}{}\protected@file@percent } -\@writefile{toc}{\contentsline {subsection}{\numberline {2.3}HARDENS: Discrete Control with Gaps in Hybrid Dynamics}{6}{}\protected@file@percent } -\@writefile{toc}{\contentsline {subsubsection}{\numberline {2.3.1}Rigorous Digital Engineering Demonstrated Feasibility}{6}{}\protected@file@percent } -\@writefile{toc}{\contentsline {subsubsection}{\numberline {2.3.2}Comprehensive Formal Methods Toolkit Provided Verification}{7}{}\protected@file@percent } -\@writefile{toc}{\contentsline {subsubsection}{\numberline {2.3.3}Critical Limitation: Discrete Control Logic Only}{7}{}\protected@file@percent } -\citation{Kiniry2022} -\@writefile{toc}{\contentsline {subsubsection}{\numberline {2.3.4}Experimental Validation Gap Limits Technology Readiness}{8}{}\protected@file@percent } -\@writefile{toc}{\contentsline {subsection}{\numberline {2.4}Research Imperative: Formal Hybrid Control Synthesis}{8}{}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {3}Research Approach}{9}{}\protected@file@percent } -\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}$(Procedures \wedge FRET) \rightarrow Temporal Specifications$}{10}{}\protected@file@percent } -\@writefile{toc}{\contentsline {subsection}{\numberline {3.2}$(TemporalLogic \wedge ReactiveSynthesis) \rightarrow DiscreteAutomata$}{11}{}\protected@file@percent } -\@writefile{toc}{\contentsline {subsection}{\numberline {3.3}$(DiscreteAutomata \wedge ControlTheory \wedge Reachability) \rightarrow ContinuousModes$}{12}{}\protected@file@percent } -\citation{eia_lcoe_2022} -\citation{eesi_datacenter_2024} -\citation{eia_lcoe_2022} -\@writefile{toc}{\contentsline {subsection}{\numberline {3.4}Broader Impacts}{14}{}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {4}Metrics for Success}{15}{}\protected@file@percent } -\@writefile{toc}{\contentsline {paragraph}{TRL 3 \textit {Critical Function and Proof of Concept}}{16}{}\protected@file@percent } -\@writefile{toc}{\contentsline {paragraph}{TRL 4 \textit {Laboratory Testing of Integrated Components}}{16}{}\protected@file@percent } -\@writefile{toc}{\contentsline {paragraph}{TRL 5 \textit {Laboratory Testing in Relevant Environment}}{16}{}\protected@file@percent } -\bibdata{references} -\bibcite{DOE-HDBK-1028-2009}{1} -\bibcite{WNA2020}{2} -\bibcite{Wang2025}{3} -\bibcite{10CFR55}{4} -\bibcite{Kemeny1979}{5} -\bibcite{NUREG-0899}{6} -\bibcite{IAEA-TECDOC-1580}{7} -\bibcite{Zerovnik2023}{8} -\bibcite{Jo2021}{9} -\bibcite{IAEA2008}{10} -\bibcite{Lee2019}{11} -\bibcite{IEEE2019}{12} -\bibcite{IAEA-severe-accidents}{13} -\bibcite{Dumas1999}{14} -\bibcite{NUREG-CR-6883}{15} -\@writefile{toc}{\contentsline {section}{References}{18}{}\protected@file@percent } -\bibcite{NUREG-2114}{16} -\bibcite{Rasmussen1983}{17} -\bibcite{Miller1956}{18} -\bibcite{Reason1990}{19} -\bibcite{Kiniry2022}{20} -\bibcite{eia_lcoe_2022}{21} -\bibcite{eesi_datacenter_2024}{22} -\gdef \@abspage@last{20} +\@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 } +\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} diff --git a/Writing/ERLM/main.bbl b/Writing/ERLM/main.bbl index 658cf8ea7..5cf47c0e2 100644 --- a/Writing/ERLM/main.bbl +++ b/Writing/ERLM/main.bbl @@ -1,21 +1,5 @@ \begin{thebibliography}{10} -\bibitem{DOE-HDBK-1028-2009} -{U.S. Department of Energy}. -\newblock Human performance handbook. -\newblock Handbook DOE-HDBK-1028-2009, U.S. Department of Energy, 2009. - -\bibitem{WNA2020} -{World Nuclear Association}. -\newblock Safety of nuclear power reactors. -\newblock \url{https://www.world-nuclear.org/information-library/safety-and-security/safety-of-plants/safety-of-nuclear-power-reactors.aspx}, 2020. - -\bibitem{Wang2025} -Y.~Wang et~al. -\newblock Analysis of human error in nuclear power plant operations: A systematic review of events from 2007--2020. -\newblock {\em Journal of Nuclear Safety}, 2025. -\newblock Analysis of 190 events at Chinese nuclear power plants. - \bibitem{10CFR55} {U.S. Nuclear Regulatory Commission}. \newblock Operators' licenses. @@ -32,39 +16,15 @@ John~G. Kemeny et~al. \newblock Guidelines for the preparation of emergency operating procedures. \newblock Technical Report NUREG-0899, U.S. Nuclear Regulatory Commission, 1982. -\bibitem{IAEA-TECDOC-1580} -{International Atomic Energy Agency}. -\newblock Good practices for cost effective maintenance of nuclear power plants. -\newblock Technical Report TECDOC-1580, International Atomic Energy Agency, 2007. +\bibitem{DOE-HDBK-1028-2009} +{U.S. Department of Energy}. +\newblock Human performance handbook. +\newblock Handbook DOE-HDBK-1028-2009, U.S. Department of Energy, 2009. -\bibitem{Zerovnik2023} -Gašper \v{Z}erovnik et~al. -\newblock Knowledge transfer challenges in nuclear operations. -\newblock {\em Nuclear Engineering and Design}, 2023. -\newblock Analysis of knowledge transfer from experienced operators. - -\bibitem{Jo2021} -Y.~Jo et~al. -\newblock Automation paradox in nuclear power plant control: Effects on operator situation awareness. -\newblock {\em Nuclear Engineering and Technology}, 2021. -\newblock Empirical study of automation effects on operator performance. - -\bibitem{IAEA2008} -{International Atomic Energy Agency}. -\newblock Modern instrumentation and control for nuclear power plants: A guidebook. -\newblock Technical Report Technical Reports Series No. 387, International Atomic Energy Agency, 2008. - -\bibitem{Lee2019} -D.~Lee et~al. -\newblock Autonomous control of nuclear reactors using long short-term memory networks. -\newblock {\em Nuclear Engineering and Technology}, 2019. -\newblock Demonstration of LSTM-based autonomous control in LOC and SGTR scenarios. - -\bibitem{IEEE2019} -{IEEE Working Group}. -\newblock Formal verification challenges for nuclear i\&c systems. -\newblock In {\em IEEE Conference on Nuclear Power Instrumentation, Control and Human-Machine Interface Technologies}, 2019. -\newblock Discussion of state space explosion in formal verification. +\bibitem{WNA2020} +{World Nuclear Association}. +\newblock Safety of nuclear power reactors. +\newblock \url{https://www.world-nuclear.org/information-library/safety-and-security/safety-of-plants/safety-of-nuclear-power-reactors.aspx}, 2020. \bibitem{IAEA-severe-accidents} {International Atomic Energy Agency}. @@ -72,11 +32,11 @@ D.~Lee et~al. \newblock IAEA Safety Report. \newblock Analysis of TMI, Chernobyl, and Fukushima accidents. -\bibitem{Dumas1999} -Lloyd Dumas. -\newblock Worker error and safety in nuclear facilities. -\newblock {\em Journal of Nuclear Safety}, 1999. -\newblock Study of incidents at 10 nuclear centers. +\bibitem{Wang2025} +Y.~Wang et~al. +\newblock Analysis of human error in nuclear power plant operations: A systematic review of events from 2007--2020. +\newblock {\em Journal of Nuclear Safety}, 2025. +\newblock Analysis of 190 events at Chinese nuclear power plants. \bibitem{NUREG-CR-6883} D.~Gertman et~al. diff --git a/Writing/ERLM/main.blg b/Writing/ERLM/main.blg index 2e23c9a43..f80765c0b 100644 --- a/Writing/ERLM/main.blg +++ b/Writing/ERLM/main.blg @@ -3,44 +3,46 @@ Capacity: max_strings=200000, hash_size=200000, hash_prime=170003 The top-level auxiliary file: main.aux The style file: unsrt.bst Database file #1: references.bib -You've used 22 entries, +Warning--I didn't find a database entry for "princeton" +You've used 15 entries, 1791 wiz_defined-function locations, - 583 strings with 7229 characters, -and the built_in function-call counts, 3301 in all, are: -= -- 301 -> -- 125 -< -- 7 -+ -- 54 -- -- 32 -* -- 109 -:= -- 599 -add.period$ -- 77 -call.type$ -- 22 -change.case$ -- 23 + 541 strings with 5998 characters, +and the built_in function-call counts, 2274 in all, are: += -- 209 +> -- 85 +< -- 5 ++ -- 37 +- -- 22 +* -- 82 +:= -- 410 +add.period$ -- 51 +call.type$ -- 15 +change.case$ -- 16 chr.to.int$ -- 0 -cite$ -- 22 -duplicate$ -- 161 -empty$ -- 341 -format.name$ -- 32 -if$ -- 726 +cite$ -- 15 +duplicate$ -- 103 +empty$ -- 236 +format.name$ -- 22 +if$ -- 499 int.to.chr$ -- 0 -int.to.str$ -- 22 -missing$ -- 10 -newline$ -- 124 -num.names$ -- 22 -pop$ -- 67 +int.to.str$ -- 15 +missing$ -- 5 +newline$ -- 84 +num.names$ -- 15 +pop$ -- 49 preamble$ -- 1 purify$ -- 0 quote$ -- 0 -skip$ -- 49 +skip$ -- 29 stack$ -- 0 substring$ -- 44 -swap$ -- 21 -text.length$ -- 7 +swap$ -- 13 +text.length$ -- 5 text.prefix$ -- 0 top$ -- 0 type$ -- 0 warning$ -- 0 -while$ -- 26 -width$ -- 24 -write$ -- 253 +while$ -- 19 +width$ -- 17 +write$ -- 171 +(There was 1 warning) diff --git a/Writing/ERLM/main.fdb_latexmk b/Writing/ERLM/main.fdb_latexmk index 50ed1b511..efbf987f4 100644 --- a/Writing/ERLM/main.fdb_latexmk +++ b/Writing/ERLM/main.fdb_latexmk @@ -1,13 +1,5 @@ # Fdb version 4 -["bibtex main"] 1760562752.25076 "main.aux" "main.bbl" "main" 1760562753.16807 0 - "./references.bib" 1760562704.16405 17887 8c959c4bb228b5a8c44fd08ed0751b05 "" - "/usr/share/texlive/texmf-dist/bibtex/bst/base/unsrt.bst" 1292289607 18030 1376b4b231b50c66211e47e42eda2875 "" - "main.aux" 1760562753.03383 5119 322e9dee8ead67f6f988fe1574ee1461 "pdflatex" - (generated) - "main.bbl" - "main.blg" - (rewritten before read) -["pdflatex"] 1760562752.27567 "main.tex" "main.pdf" "main" 1760562753.16828 0 +["pdflatex"] 1760990396.64627 "main.tex" "main.pdf" "main" 1760990397.59592 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 "" @@ -15,8 +7,6 @@ "/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 "" - "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmbi7t.tfm" 1136768653 2228 e564491c42a4540b5ebb710a75ff306c "" - "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmbi8r.tfm" 1136768653 4480 10409ed8bab5aea9ec9a78028b763919 "" "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm" 1136768653 2124 2601a75482e9426d33db523edf23570a "" "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr8c.tfm" 1136768653 1352 fa28a7e6d323c65ce7d13d5342ff6be2 "" "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm" 1136768653 4408 25b74d011a4c66b7f212c0cc3c90061b "" @@ -32,19 +22,15 @@ "/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/cm/cmtt12.tfm" 1136768653 772 9a936b7f5e2ff0557fce0f62822f0bbf "" "/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/public/amsfonts/cm/cmtt12.pfb" 1248133631 24252 1e4e051947e12dfb50fee0b7f4e26e3a "" "/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/utmbi8a.pfb" 1136849748 44656 0cbca70e0534538582128f6b54593cca "" "/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 "" "/usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmb7t.vf" 1136768653 1372 788387fea833ef5963f4c5bffe33eb89 "" - "/usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmbi7t.vf" 1136768653 1384 6ac0f8b839230f5d9389287365b243c0 "" "/usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmr7t.vf" 1136768653 1380 0ea3a3370054be6da6acd929ec569f06 "" "/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 "" @@ -235,15 +221,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 "" - "broader-impacts/v1.tex" 1759167577.47123 4916 8f9b155145119717e181909e7ce40ed4 "" "dane_proposal_format.cls" 1760370937.93092 2555 2a01bb8bad8f4ed4e921f0e44566678c "" - "goals-and-outcomes/v6.tex" 1759931957.10694 6070 286ca847b1aac31431e0658cd2989ea2 "" - "main.aux" 1760562753.03383 5119 322e9dee8ead67f6f988fe1574ee1461 "pdflatex" - "main.bbl" 1760562752.26982 5077 d6ff10b25ca0659d0f11499aae407631 "bibtex main" - "main.tex" 1760562742.31168 262 9f602b4fd5277ffe357ac290893d6a07 "" - "metrics-of-success/v1.tex" 1760371276.72563 6867 9f08b3208bb158042e2fc9bbfeecae68 "" - "research-approach/v3.tex" 1759939583.16696 17351 6ed3e4ff3c33dd86d80597dbdb0cf36f "" - "state-of-the-art/v4.tex" 1760562682.16681 27511 990507df5d11f6d75319d3b7758df3ce "" + "main.aux" 1760990397.47327 1085 9e68fae35f59a6899f3340eaf1c73ae0 "pdflatex" + "main.tex" 1760990396.41916 316 db7ca25ef1aea8ffbcbf35ffc893f193 "" + "whitepaper/v1.tex" 1760990371.68075 59622 b94eab76770c3fd9ee71c7178c32dfef "" (generated) "main.aux" "main.log" diff --git a/Writing/ERLM/main.fls b/Writing/ERLM/main.fls index 1096e1439..48ef389d1 100644 --- a/Writing/ERLM/main.fls +++ b/Writing/ERLM/main.fls @@ -401,98 +401,66 @@ 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/vf/adobe/times/ptmr7t.vf INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm -INPUT ./goals-and-outcomes/v6.tex -INPUT ./goals-and-outcomes/v6.tex -INPUT ./goals-and-outcomes/v6.tex -INPUT ./goals-and-outcomes/v6.tex -INPUT goals-and-outcomes/v6.tex +INPUT ./whitepaper/v1.tex +INPUT ./whitepaper/v1.tex +INPUT ./whitepaper/v1.tex +INPUT ./whitepaper/v1.tex +INPUT whitepaper/v1.tex 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/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 ./state-of-the-art/v4.tex -INPUT ./state-of-the-art/v4.tex -INPUT ./state-of-the-art/v4.tex -INPUT ./state-of-the-art/v4.tex -INPUT state-of-the-art/v4.tex +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 +INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm +INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm +INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm +INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm +INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm +INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm +INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm +INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm +INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm +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/vf/adobe/times/ptmri7t.vf +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/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 -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm -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/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/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/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/zptmcm7y.vf -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmsy10.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/rsfs/rsfs10.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/zptmcm7t.vf -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmr10.tfm -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/fonts/vf/adobe/times/ptmr8c.vf -INPUT ./research-approach/v3.tex -INPUT ./research-approach/v3.tex -INPUT ./research-approach/v3.tex -INPUT ./research-approach/v3.tex -INPUT research-approach/v3.tex -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 ./broader-impacts/v1.tex -INPUT ./broader-impacts/v1.tex -INPUT ./broader-impacts/v1.tex -INPUT ./broader-impacts/v1.tex -INPUT broader-impacts/v1.tex -INPUT ./metrics-of-success/v1.tex -INPUT ./metrics-of-success/v1.tex -INPUT ./metrics-of-success/v1.tex -INPUT ./metrics-of-success/v1.tex -INPUT metrics-of-success/v1.tex -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmbi7t.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmbi7t.vf -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmbi8r.tfm -INPUT ./main.bbl -INPUT ./main.bbl -INPUT main.bbl -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmtt12.tfm 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/public/amsfonts/cm/cmtt12.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/utmbi8a.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 diff --git a/Writing/ERLM/main.log b/Writing/ERLM/main.log index 97f222812..ba3882fc1 100644 --- a/Writing/ERLM/main.log +++ b/Writing/ERLM/main.log @@ -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) 15 OCT 2025 17:12 +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 entering extended mode restricted \write18 enabled. file:line:error style messages enabled. @@ -876,50 +876,46 @@ 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}] (./goals-and-outcomes/v6.tex [1]) (./state-of-the-art/v4.tex -Overfull \hbox (1.5749pt too wide) in paragraph at lines 30--36 -\OT1/ptm/m/n/12 stru-men-ta-tion and con-trol (I&C) sys-tems. Un-der-stand-ing cur-rent practices---and their limitations--- - [] - -[2] [3] [4] -Overfull \hbox (3.86827pt too wide) in paragraph at lines 215--223 -\OT1/ptm/m/n/12 organizational and sys-temic weak-nesses that cre-ate con-di-tions for fail-ure. Lloyd Du-mas's study [14] - [] - -[5] +{/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] 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 275. +(Font) Font shape `OT1/ptm/b/n' tried instead on input line 214. 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 275. +(Font) Font shape `OT1/ptm/b/n' tried instead on input line 214. 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 275. -LaTeX Font Info: Trying to load font information for TS1+ptm on input line 307. +(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. (/usr/share/texlive/texmf-dist/tex/latex/psnfss/ts1ptm.fd File: ts1ptm.fd 2001/06/04 font definitions for TS1/ptm. -) [6] [7] [8]) (./research-approach/v3.tex [9] [10] [11] [12] [13]) (./broader-impacts/v1.tex [14]) (./metrics-of-success/v1.tex [15]) [16] [17] (./main.bbl -Underfull \hbox (badness 10000) in paragraph at lines 9--12 -\OT1/cmtt/m/n/12 nuclear . org / information -[] library / safety -[] and -[] security / safety -[] of -[] - [] - -[18]) [19] (./main.aux) +) [10] [11]) [12] (./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: - 25443 strings out of 476182 - 528350 string characters out of 5795595 + 25373 strings out of 476182 + 526915 string characters out of 5795595 1934975 words of memory out of 5000000 - 46876 multiletter control sequences out of 15000+600000 - 592787 words of font info for 111 fonts, out of 8000000 for 9000 + 46831 multiletter control sequences out of 15000+600000 + 590992 words of font info for 106 fonts, out of 8000000 for 9000 14 hyphenation exceptions out of 8191 - 110i,6n,107p,1008b,327s stack positions out of 10000i,1000n,20000p,200000b,200000s - -Output written on main.pdf (20 pages, 159455 bytes). + 110i,6n,107p,1008b,285s stack positions out of 10000i,1000n,20000p,200000b,200000s + +Output written on main.pdf (13 pages, 109205 bytes). PDF statistics: - 142 PDF objects out of 1000 (max. 8388607) - 85 compressed objects within 1 object stream + 110 PDF objects out of 1000 (max. 8388607) + 64 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) diff --git a/Writing/ERLM/main.pdf b/Writing/ERLM/main.pdf index ed4d45ec0..bc9969ced 100644 Binary files a/Writing/ERLM/main.pdf and b/Writing/ERLM/main.pdf differ diff --git a/Writing/ERLM/main.synctex.gz b/Writing/ERLM/main.synctex.gz index f0e627250..11fea118e 100644 Binary files a/Writing/ERLM/main.synctex.gz and b/Writing/ERLM/main.synctex.gz differ diff --git a/Writing/ERLM/main.tex b/Writing/ERLM/main.tex index d8f80e8ac..a9ebed6a3 100644 --- a/Writing/ERLM/main.tex +++ b/Writing/ERLM/main.tex @@ -3,12 +3,17 @@ \begin{document} \maketitle -\input{goals-and-outcomes/v6} -\input{state-of-the-art/v5} -\input{research-approach/v3} -\input{broader-impacts/v1} -\input{metrics-of-success/v1} +% \input{goals-and-outcomes/v6} +% \input{state-of-the-art/v5} +% \input{research-approach/v3} +% \input{broader-impacts/v1} +% \input{metrics-of-success/v1} +% +% \newpage +% \bibliography{references} + +% White Paper + +\input{whitepaper/v1} -\newpage -\bibliography{references} \end{document} diff --git a/Writing/ERLM/state-of-the-art/v5.tex b/Writing/ERLM/state-of-the-art/v5.tex index 51bfcb057..9c6430b51 100644 --- a/Writing/ERLM/state-of-the-art/v5.tex +++ b/Writing/ERLM/state-of-the-art/v5.tex @@ -33,9 +33,6 @@ responsibility under all conditions~\cite{Kemeny1979}. This tension between operational flexibility and safety assurance remains unresolved in current practice. -<<<<<<< HEAD -%how are procedures tested -======= Nuclear plant procedures exist in a hierarchy: normal operating procedures for routine operations, abnormal operating procedures for off-normal conditions, Emergency Operating Procedures (EOPs) for design-basis accidents, Severe @@ -72,7 +69,6 @@ Safety systems instead operate with implemented automation. Reactor Protection Systems trip automatically on safety signals with millisecond response times, and engineered safety features actuate automatically on accident signals without operator action required. ->>>>>>> 568549999a24c6a86f19411cbdf12b642057ade9 The current division between automated and human-controlled functions reveals the fundamental challenge of hybrid control. Highly @@ -94,34 +90,6 @@ decades of improvements in training and procedures, provides perhaps the most compelling motivation for formal automated control with mathematical safety guarantees. -<<<<<<< HEAD -%Whos in the control room - -%how are reactor operators trained - -% Humans are actually really bad at doing control - -%most accidents are human error - -%Three mile island - -%Human factors probabilities - -\subsection{HARDENS and Formal Methods} -% The NRC recognizes that automation and high assurance are important things to -% pursue - -%They put out a grant to do rigorous digital engineering - -%Won by formal methods group galois. Galois does a bunch of formal methods work. -%What is formal methods? - -%Rigorous digital engineering to create a reactor trip system - -%details of how it worked, and limitations therein - -%Digital system ONLY -======= Multiple independent analyses converge on a striking statistic: \textbf{70--80\% of all nuclear power plant events are attributed to human error} versus approximately 20\% to equipment failures~\cite{DOE-HDBK-1028-2009,WNA2020}. More @@ -387,4 +355,3 @@ demonstrated by HARDENS, urgent safety imperatives documented by persistent human error statistics, and fundamental gaps in current hybrid dynamics treatment creates a compelling and timely research opportunity. ->>>>>>> 568549999a24c6a86f19411cbdf12b642057ade9 diff --git a/Writing/ERLM/whitepaper/v1.tex b/Writing/ERLM/whitepaper/v1.tex new file mode 100644 index 000000000..3ff544203 --- /dev/null +++ b/Writing/ERLM/whitepaper/v1.tex @@ -0,0 +1,1086 @@ +\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. +Without introducing automation, 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} +% GOAL PARAGRAPH +The goal of this research is to develop a methodology for creating autonomous +control systems with event-driven control laws that have guarantees of safe and +correct behavior. + +% INTRODUCTORY PARAGRAPH Hook +Nuclear power relies on extensively trained operators who follow detailed +written procedures to manage reactor control. Based on these procedures and +operators' interpretation of plant conditions, operators make critical decisions +about when to switch between control objectives. +% Gap +While human operators have maintained the nuclear industry's exceptional safety +record, reliance on human operators has created an economic challenge for +next-generation nuclear power plants. Small modular reactors face significantly +higher per-megawatt staffing costs than conventional plants, threatening their +economic viability. Autonomous control systems are needed that can safely manage +complex operational sequences with the same assurance as human-operated systems, +but without constant supervision. + +% APPROACH PARAGRAPH Solution +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. +% Rationale +Hybrid systems use discrete logic to switch between continuous control modes, +similar to how operators change control strategies. Existing formal methods +generate provably correct switching logic but cannot handle continuous dynamics +during transitions, while traditional control theory verifies continuous +behavior but lacks tools for proving discrete switching correctness. +% Hypothesis and Technical Approach +We will bridge this gap through a three-stage methodology. First, we will +translate written operating procedures into temporal logic specifications using +NASA's Formal Requirements Elicitation Tool (FRET), which structures +requirements into scope, condition, component, timing, and response elements. +This structured approach enables realizability checking to identify conflicts +and ambiguities in procedures before implementation. Second, we will synthesize +discrete mode switching logic from these specifications using reactive synthesis +tools such as Strix, which generates deterministic automata that are provably +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 +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 +autonomous startup controller for a Small Modular Advanced High Temperature +Reactor (SmAHTR) and implementing it on an Emerson Ovation control system using +the ARCADE hardware-in-the-loop platform. +% Pay-off +This approach will demonstrate autonomous control can be used for complex +nuclear power operations while maintaining safety guarantees. + +\vspace{11pt} + +% OUTCOMES PARAGRAPHS +If this research is successful, we will be able to do the following: +\begin{enumerate} + % OUTCOME 1 Title + \item \textit{Synthesize written procedures into verified control logic.} + % Strategy + 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. + % Outcome + 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. + + % OUTCOME 2 Title + \item \textit{Verify continuous control behavior across mode transitions. } + % Strategy + We will develop methods using reachability analysis to ensure continuous control modes + satisfy discrete transition requirements. + % Outcome + 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. + + % OUTCOME 3 Title + \item \textit{Demonstrate autonomous reactor startup control with safety + guarantees. } + % Strategy + 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. + % Outcome + 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} +% +% % 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{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. + +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 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. + +\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 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. + +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 + +\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} diff --git a/Writing/WHITEPAPER.zip b/Writing/WHITEPAPER.zip new file mode 100644 index 000000000..2fc5a4816 Binary files /dev/null and b/Writing/WHITEPAPER.zip differ