Auto sync: 2025-12-04 13:52:33 (15 files changed)

A  Writing/ERLM/broader-impacts/v2.tex

M  Writing/ERLM/goals-and-outcomes/v7.tex

M  Writing/ERLM/main.aux

M  Writing/ERLM/main.bbl

M  Writing/ERLM/main.blg

M  Writing/ERLM/main.fdb_latexmk

M  Writing/ERLM/main.fls

M  Writing/ERLM/main.log

Writing/ERLM/broader-impacts/v2.tex

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

Writing/ERLM/goals-and-outcomes/v7.tex

@@ -0,0 +1,118 @@
+\section{Goals and Outcomes}
+
+% GOAL PARAGRAPH
+The goal of this research is to develop a methodology for creating autonomous
+hybrid control systems with mathematical guarantees of safe and correct
+behavior.
+
+% INTRODUCTORY PARAGRAPH Hook
+Nuclear power plants require the highest levels of control system reliability,
+where failures can result in significant economic losses, service interruptions,
+or radiological release. 
+% Known information
+Currently, nuclear plant operations rely on extensively trained human operators
+who follow detailed written procedures and strict regulatory requirements to
+manage reactor control. These operators make critical decisions about when to
+switch between different control modes based on their interpretation of plant
+conditions and procedural guidance. 
+% Gap
+However, this reliance on human operators prevents the introduction of
+autonomous control capabilities and creates a fundamental economic challenge 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. 
+% Critical Need
+What is needed is a way to create autonomous control systems that can safely
+manage complex operational sequences with the same level of assurance as
+human-operated systems, but without requiring constant human 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 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. 
+% Hypothesis
+By synthesizing discrete mode transitions directly from written operating
+procedures and verifying continuous behavior between transitions, we can create
+hybrid control systems with end-to-end correctness guarantees. If we can
+formalize existing procedures into logical specifications and verify that
+continuous dynamics satisfy transition requirements, then we can build
+autonomous controllers that are provably free from design defects. 
+% Pay-off
+This approach will enable autonomous control in nuclear power plants while
+maintaining the high safety standards required by the industry. 
+% Qualifications
+This work is conducted within the University of Pittsburgh Cyber Energy Center,
+which provides access to industry collaboration and Emerson control hardware,
+ensuring that solutions developed are aligned with practical implementation
+requirements.
+
+% OUTCOMES PARAGRAPHS
+If this research is successful, we will be able to do the following:
+
+\begin{enumerate}
+
+  % OUTCOME 1 Title
+  \item \textbf{Translate written procedures into verified control logic.} 
+    % Strategy
+    We will develop a methodology for converting existing written operating
+    procedures into formal specifications that can be automatically synthesized
+    into discrete control logic. This process will use structured intermediate
+    representations to bridge natural language procedures and mathematical
+    logic. 
+    % Outcome
+    Control system engineers will be able to generate verified mode-switching
+    controllers directly from regulatory procedures without requiring expertise
+    in formal methods, reducing the barrier to creating high-assurance control
+    systems.
+
+    % OUTCOME 2 Title
+  \item \textbf{Verify continuous control behavior across mode transitions.} 
+    % Strategy
+    We will establish methods for analyzing continuous control modes to ensure
+    they satisfy the discrete transition requirements. Using a combination of
+    classical control theory for linear systems and reachability analysis for
+    nonlinear dynamics, we will verify that each continuous mode can safely
+    reach its intended transitions. 
+    % Outcome
+    Engineers will be able to design continuous controllers using standard
+    practices while iterating to ensure broader system correctness, proving that
+    mode transitions occur safely and at the right times.
+
+    % OUTCOME 3  Title
+  \item \textbf{Demonstrate autonomous reactor startup control with safety
+    guarantees.} 
+    % Strategy
+    We will apply this methodology to develop an autonomous controller for
+    nuclear reactor startup procedures, implementing it on a small modular
+    reactor simulation using industry-standard control hardware. This
+    demonstration will prove correctness across multiple coordinated control
+    modes from cold shutdown through criticality to power operation. 
+    % Outcome
+    We will provide evidence that autonomous hybrid control can be realized in
+    the nuclear industry with current control equipment, establishing a path
+    toward reducing operator staffing requirements while maintaining safety.
+
+\end{enumerate}
+
+% IMPACT PARAGRAPH Innovation
+The innovation in this work is the unification of 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.
+High-assurance autonomous control will become practical for safety-critical
+applications. 
+% Impact/Pay-off
+This capability is essential for the economic viability of next-generation
+nuclear power. Small modular reactors represent a promising solution to growing
+energy demands, but their success depends on reducing per-megawatt operating
+costs through increased autonomy. This research will provide the tools to
+achieve that autonomy while maintaining the exceptional safety record required
+by the nuclear industry.

Writing/ERLM/main.aux

@@ -2,23 +2,26 @@
 \bibstyle{unsrt}
 \providecommand \oddpage@label [2]{}
 \@writefile{toc}{\contentsline {section}{\numberline {1}Goals and Outcomes}{1}{}\protected@file@percent }
-\citation{10CFR55}
-\citation{princeton}
-\citation{Kemeny1979}
-\citation{Kemeny1979}
 \citation{NUREG-0899}
 \citation{10CFR55}
-\@writefile{toc}{\contentsline {section}{\numberline {2}State of the Art and Limits of Current Practice}{2}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {section}{\numberline {2}State of the Art and Limits of Current Practice}{3}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}Current Reactor Procedures and Operation}{2}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}Current Reactor Procedures and Operation}{3}{}\protected@file@percent }
+\citation{10CFR55}
+\citation{NRC WEBSITE IN ZOTERO FOR PRES}
+\citation{ALSO IN PRES FOLDER}
+\citation{10CFR55}
+\citation{NRC WEBSITE IN ZOTERO FOR PRES}
+\citation{ALSO IN PRES FOLDER}
+\citation{Kemeny1979}
+\citation{Kemeny1979}
 \citation{DOE-HDBK-1028-2009,WNA2020}
 \citation{IAEA-severe-accidents}
 \citation{Wang2025}
-\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Human Factors in Nuclear Accidents}{3}{}\protected@file@percent }
-\citation{Kemeny1979}
 \citation{Reason1990}
-\@writefile{toc}{\contentsline {subsection}{\numberline {2.3}HARDENS and Formal Methods}{4}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Human Factors in Nuclear Accidents}{4}{}\protected@file@percent }
 \citation{Kiniry2022}
-\@writefile{toc}{\contentsline {section}{\numberline {3}Research Approach}{5}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.3}HARDENS and Formal Methods}{5}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {section}{\numberline {3}Research Approach}{6}{}\protected@file@percent }
 \@writefile{toc}{\contentsline {subsection}{\numberline {3.1}$(Procedures \wedge FRET) \rightarrow Temporal Specifications$}{6}{}\protected@file@percent }
 \@writefile{toc}{\contentsline {subsection}{\numberline {3.2}$(TemporalLogic \wedge ReactiveSynthesis) \rightarrow DiscreteAutomata$}{7}{}\protected@file@percent }
 \@writefile{toc}{\contentsline {subsection}{\numberline {3.3}$(DiscreteAutomata \wedge ControlTheory \wedge Reachability) \rightarrow ContinuousModes$}{8}{}\protected@file@percent }
@@ -42,10 +45,10 @@
 \@writefile{toc}{\contentsline {paragraph}{Faculty Advisor}{17}{}\protected@file@percent }
 \@writefile{toc}{\contentsline {subsubsection}{\numberline {7.2.2}Other Personnel}{17}{}\protected@file@percent }
 \@writefile{toc}{\contentsline {paragraph}{Graduate Research Assistant (Principal Investigator)}{17}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsubsection}{\numberline {7.2.3}Fringe Benefits}{17}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {paragraph}{Faculty Fringe Benefits}{17}{}\protected@file@percent }
 \@writefile{lot}{\contentsline {table}{\numberline {1}{\ignorespaces Proposed Budget by Year and Category}}{18}{}\protected@file@percent }
 \newlabel{tab:budget}{{1}{18}{Budget Summary}{}{}}
+\@writefile{toc}{\contentsline {subsubsection}{\numberline {7.2.3}Fringe Benefits}{19}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {paragraph}{Faculty Fringe Benefits}{19}{}\protected@file@percent }
 \@writefile{toc}{\contentsline {paragraph}{Graduate Research Assistant Fringe Benefits}{19}{}\protected@file@percent }
 \@writefile{toc}{\contentsline {subsubsection}{\numberline {7.2.4}Equipment}{19}{}\protected@file@percent }
 \@writefile{toc}{\contentsline {subsubsection}{\numberline {7.2.5}Travel}{19}{}\protected@file@percent }
@@ -57,25 +60,25 @@
 \@writefile{toc}{\contentsline {paragraph}{Publication Costs}{20}{}\protected@file@percent }
 \@writefile{toc}{\contentsline {paragraph}{Computing and Cloud Services}{20}{}\protected@file@percent }
 \@writefile{toc}{\contentsline {subsubsection}{\numberline {7.2.8}H. Indirect Costs (Facilities \& Administrative)}{20}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsubsection}{\numberline {7.2.9}Cost Sharing}{20}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsubsection}{\numberline {7.2.9}Cost Sharing}{21}{}\protected@file@percent }
-\newlabel{sec:cost-sharing}{{7.2.9}{20}{Cost Sharing}{}{}}
+\newlabel{sec:cost-sharing}{{7.2.9}{21}{Cost Sharing}{}{}}
-\@writefile{toc}{\contentsline {paragraph}{Emerson Process Management Partnership}{20}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {paragraph}{Emerson Process Management Partnership}{21}{}\protected@file@percent }
 \@writefile{toc}{\contentsline {paragraph}{University Infrastructure}{21}{}\protected@file@percent }
 \@writefile{toc}{\contentsline {paragraph}{Total In-Kind Contributions}{21}{}\protected@file@percent }
 \@writefile{toc}{\contentsline {subsubsection}{\numberline {7.2.10}Budget Inflation and Escalation}{21}{}\protected@file@percent }
 \@writefile{toc}{\contentsline {section}{\numberline {8}Schedule, Milestones, and Deliverables}{21}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsection}{\numberline {8.1}Milestones and Deliverables}{21}{}\protected@file@percent }
 \gtt@chartextrasize{0}{164.1287pt}
 \@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Project schedule showing major research thrusts, milestones (orange row), and publications (green row). Red diamonds indicate completion points. Overlapping bars indicate parallel work where appropriate.}}{22}{}\protected@file@percent }
 \newlabel{fig:gantt}{{1}{22}{Schedule, Milestones, and Deliverables}{}{}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {8.1}Milestones and Deliverables}{22}{}\protected@file@percent }
 \@writefile{toc}{\contentsline {section}{\numberline {9}Supplemental Sections}{23}{}\protected@file@percent }
 \@writefile{toc}{\contentsline {subsection}{\numberline {9.1}Biosketch}{23}{}\protected@file@percent }
 \@writefile{toc}{\contentsline {subsection}{\numberline {9.2}Data Management Plan}{26}{}\protected@file@percent }
 \@writefile{toc}{\contentsline {subsection}{\numberline {9.3}Facilities}{30}{}\protected@file@percent }
 \bibdata{references}
-\bibcite{10CFR55}{1}
+\bibcite{NUREG-0899}{1}
-\bibcite{Kemeny1979}{2}
+\bibcite{10CFR55}{2}
-\bibcite{NUREG-0899}{3}
+\bibcite{Kemeny1979}{3}
 \bibcite{DOE-HDBK-1028-2009}{4}
 \bibcite{WNA2020}{5}
 \bibcite{IAEA-severe-accidents}{6}

Writing/ERLM/main.bbl

@@ -1,5 +1,10 @@
 \begin{thebibliography}{10}
 
+\bibitem{NUREG-0899}
+{U.S. Nuclear Regulatory Commission}.
+\newblock Guidelines for the preparation of emergency operating procedures.
+\newblock Technical Report NUREG-0899, U.S. Nuclear Regulatory Commission, 1982.
+
 \bibitem{10CFR55}
 {U.S. Nuclear Regulatory Commission}.
 \newblock Operators' licenses.
@@ -11,11 +16,6 @@ John~G. Kemeny et~al.
 \newblock Report of the president's commission on the accident at three mile island.
 \newblock Technical report, President's Commission on the Accident at Three Mile Island, October 1979.
 
-\bibitem{NUREG-0899}
-{U.S. Nuclear Regulatory Commission}.
-\newblock Guidelines for the preparation of emergency operating procedures.
-\newblock Technical Report NUREG-0899, U.S. Nuclear Regulatory Commission, 1982.
-
 \bibitem{DOE-HDBK-1028-2009}
 {U.S. Department of Energy}.
 \newblock Human performance handbook.

Writing/ERLM/main.blg

@@ -2,11 +2,26 @@ This is BibTeX, Version 0.99d (TeX Live 2023/Debian)
 Capacity: max_strings=200000, hash_size=200000, hash_prime=170003
 The top-level auxiliary file: main.aux
 The style file: unsrt.bst
+White space in argument---line 10 of file main.aux
+ : \citation{NRC
+ :               WEBSITE IN ZOTERO FOR PRES}
+I'm skipping whatever remains of this command
+White space in argument---line 11 of file main.aux
+ : \citation{ALSO
+ :                IN PRES FOLDER}
+I'm skipping whatever remains of this command
+White space in argument---line 13 of file main.aux
+ : \citation{NRC
+ :               WEBSITE IN ZOTERO FOR PRES}
+I'm skipping whatever remains of this command
+White space in argument---line 14 of file main.aux
+ : \citation{ALSO
+ :                IN PRES FOLDER}
+I'm skipping whatever remains of this command
 Database file #1: references.bib
-Warning--I didn't find a database entry for "princeton"
 You've used 11 entries,
             1791 wiz_defined-function locations,
-            515 strings with 5435 characters,
+            514 strings with 5426 characters,
 and the built_in function-call counts, 1577 in all, are:
 = -- 140
 > -- 65
@@ -45,4 +60,4 @@ warning$ -- 0
 while$ -- 11
 width$ -- 13
 write$ -- 127
-(There was 1 warning)
+(There were 4 error messages)

Writing/ERLM/main.fdb_latexmk

@@ -1,14 +1,14 @@
 # Fdb version 4
-["bibtex main"] 1764797497.91157 "main.aux" "main.bbl" "main" 1764797499.0949 0
+["bibtex main"] 1764869648.5559 "main.aux" "main.bbl" "main" 1764869648.59189 2
-  "./references.bib" 1760562704.16405 17887 8c959c4bb228b5a8c44fd08ed0751b05 ""
+  "./references.bib" 1760575541.11204 17887 8c959c4bb228b5a8c44fd08ed0751b05 ""
   "/usr/share/texlive/texmf-dist/bibtex/bst/base/unsrt.bst" 1292289607 18030 1376b4b231b50c66211e47e42eda2875 ""
-  "main.aux" 1764797498.95722 7493 145eb36fc16fd242541c91147603703c "pdflatex"
+  "main.aux" 1764869648.39348 7615 5821c96fe1a36195d8b7d010b233e163 "pdflatex"
   (generated)
   "main.bbl"
   "main.blg"
   (rewritten before read)
-["pdflatex"] 1764797497.93427 "main.tex" "main.pdf" "main" 1764797499.09513 0
+["pdflatex"] 1764869647.67076 "main.tex" "main.pdf" "main" 1764869648.59211 0
-  "/etc/texmf/web2c/texmf.cnf" 1722610814.59577 475 c0e671620eb5563b2130f56340a5fde8 ""
+  "/etc/texmf/web2c/texmf.cnf" 1726065852.27662 475 c0e671620eb5563b2130f56340a5fde8 ""
   "/usr/share/texlive/texmf-dist/fonts/enc/dvips/base/8r.enc" 1165713224 4850 80dc9bab7f31fb78a000ccfed0e27cab ""
   "/usr/share/texlive/texmf-dist/fonts/map/fontname/texfonts.map" 1577235249 3524 cb3e574dea2d1052e39280babc910dc8 ""
   "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm" 1136768653 1408 5937f58aa508ea2cea4901c07d10f5fe ""
@@ -239,23 +239,23 @@
   "/usr/share/texlive/texmf-dist/tex/latex/xkeyval/xkeyval.sty" 1655411236 4937 4ce600ce9bd4ec84d0250eb6892fcf4f ""
   "/usr/share/texlive/texmf-dist/web2c/texmf.cnf" 1707919699 40399 f2c302f7d2af602abb742093540a5834 ""
   "/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/fonts/map/pdftex/updmap/pdftex.map" 1760105440.02229 5312232 f3296911be9cc021788f3f879cf0a47d ""
-  "/var/lib/texmf/web2c/pdftex/pdflatex.fmt" 1726005817 6800784 2b63e5a224c5ad740802d8f9921962c1 ""
+  "/var/lib/texmf/web2c/pdftex/pdflatex.fmt" 1726065868 6800790 607442c924ed54405961d2b8ac2a25ae ""
-  "broader-impacts/v1.tex" 1761582743.25611 4913 f040011f0dbfa050cad013bb8737b473 ""
+  "broader-impacts/v1.tex" 1762446356.88898 4913 f040011f0dbfa050cad013bb8737b473 ""
-  "budget/v1.tex" 1762189605.00097 12864 1341c4cfdaf82dc649f2f47f3cc8ecd7 ""
+  "budget/v1.tex" 1762446356.88898 12864 1341c4cfdaf82dc649f2f47f3cc8ecd7 ""
-  "dane_proposal_format.cls" 1760994752.93894 2596 f4b1a6fb5a74347c13e92ea1ba135818 ""
+  "dane_proposal_format.cls" 1761234879.88179 2596 f4b1a6fb5a74347c13e92ea1ba135818 ""
-  "goals-and-outcomes/v6.tex" 1759931957.10694 6070 286ca847b1aac31431e0658cd2989ea2 ""
+  "goals-and-outcomes/v6.tex" 1760575541.11104 6070 286ca847b1aac31431e0658cd2989ea2 ""
-  "main.aux" 1764797498.95722 7493 145eb36fc16fd242541c91147603703c "pdflatex"
+  "main.aux" 1764869648.39348 7615 5821c96fe1a36195d8b7d010b233e163 "pdflatex"
-  "main.bbl" 1764797497.92821 2497 c9440bf2d76ac901d421f7f89b129050 "bibtex main"
+  "main.bbl" 1764869648.58848 2497 61aa87b86cf1e92fd5306af01b0a5409 "bibtex main"
-  "main.tex" 1764797489.4722 768 21c161623549be714dc49726837188d5 ""
+  "main.tex" 1764866127.56542 768 21c161623549be714dc49726837188d5 ""
-  "metrics-of-success/v1.tex" 1760371276.72563 6867 9f08b3208bb158042e2fc9bbfeecae68 ""
+  "metrics-of-success/v1.tex" 1760575541.11204 6867 9f08b3208bb158042e2fc9bbfeecae68 ""
-  "research-approach/v3.tex" 1759939583.16696 17351 6ed3e4ff3c33dd86d80597dbdb0cf36f ""
+  "research-approach/v3.tex" 1760575541.11304 17351 6ed3e4ff3c33dd86d80597dbdb0cf36f ""
-  "risks-and-contingencies/v1.tex" 1761582682.04479 15209 c8ff47d0cfbf72d9c457463c5114f2a8 ""
+  "risks-and-contingencies/v1.tex" 1762446356.89155 15209 c8ff47d0cfbf72d9c457463c5114f2a8 ""
-  "schedule/v1.tex" 1763391736.55412 8440 1c6c59ab8379c2aee45e5ad9b447e61d ""
+  "schedule/v1.tex" 1764192995.54631 8440 1c6c59ab8379c2aee45e5ad9b447e61d ""
-  "state-of-the-art/v6.tex" 1764797462.72603 13363 8453241fdf0e619612b39a75eaaed35f ""
+  "state-of-the-art/v6.tex" 1764869646.62949 14571 be2cbb52663460e4a029066fb8854728 ""
-  "supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf" 1763392988.33612 76839 d12cfa78304f51e96ce0e12460ece1e3 ""
+  "supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf" 1764192995.54731 76839 d12cfa78304f51e96ce0e12460ece1e3 ""
-  "supplemental-sections/cv-1786798.pdf" 1763388592.02957 31602 224112b9f507ae1e989c0341a7eb3f42 ""
+  "supplemental-sections/cv-1786798.pdf" 1764192995.54731 31602 224112b9f507ae1e989c0341a7eb3f42 ""
-  "supplemental-sections/v1.tex" 1763415538.33815 2302 accf9c1dd3b7c2f35a3a051140113d63 ""
+  "supplemental-sections/v1.tex" 1764192995.54731 2302 accf9c1dd3b7c2f35a3a051140113d63 ""
   (generated)
   "main.aux"
   "main.log"

Writing/ERLM/main.fls

@@ -466,13 +466,13 @@ 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 ./risks-and-contingencies/v1.tex
 INPUT ./risks-and-contingencies/v1.tex
 INPUT ./risks-and-contingencies/v1.tex
 INPUT ./risks-and-contingencies/v1.tex
 INPUT risks-and-contingencies/v1.tex
-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 ./broader-impacts/v1.tex
 INPUT ./broader-impacts/v1.tex
 INPUT ./broader-impacts/v1.tex

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)  3 DEC 2025 16:31
+This is pdfTeX, Version 3.141592653-2.6-1.40.25 (TeX Live 2023/Debian) (preloaded format=pdflatex 2024.9.11)  4 DEC 2025 12:34
 entering extended mode
  restricted \write18 enabled.
  file:line:error style messages enabled.
@@ -881,37 +881,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 12.
  [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/v6.tex
+{/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/v6.tex [2] [3]
 
-LaTeX Warning: Citation `princeton' on page 2 undefined on input line 19.
+LaTeX Warning: Citation `NRC WEBSITE IN ZOTERO FOR PRES' on page 4 undefined on input line 77.
 
-[2] [3] [4]) (./research-approach/v3.tex
+
+LaTeX Warning: Citation `ALSO IN PRES FOLDER' on page 4 undefined on input line 79.
+
+
+LaTeX Warning: Citation `NRC WEBSITE IN ZOTERO FOR PRES' on page 4 undefined on input line 85.
+
+
+LaTeX Warning: Citation `ALSO IN PRES FOLDER' on page 4 undefined on input line 86.
+
+[4] [5]) (./research-approach/v3.tex
 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 8.
 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 8.
 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 8.
- [5] [6] [7] [8] [9]) (./metrics-of-success/v1.tex [10]) (./risks-and-contingencies/v1.tex [11] [12] [13] [14]) (./broader-impacts/v1.tex [15]
+ [6] [7] [8] [9]) (./metrics-of-success/v1.tex [10] [11]) (./risks-and-contingencies/v1.tex [12] [13] [14] [15]) (./broader-impacts/v1.tex
 LaTeX Font Info:    Trying to load font information for TS1+ptm on input line 14.
  (/usr/share/texlive/texmf-dist/tex/latex/psnfss/ts1ptm.fd
 File: ts1ptm.fd 2001/06/04 font definitions for TS1/ptm.
 ) [16]) (./budget/v1.tex
 LaTeX Font Info:    Font shape `OT1/ptm/bx/n' in size <6> not available
 (Font)              Font shape `OT1/ptm/b/n' tried instead on input line 22.
- [17] [18] [19]
+ [17] [18] [19] [20]
 Overfull \hbox (22.53047pt too wide) in paragraph at lines 264--271
 [] []\OT1/ptm/b/n/12 Uni-ver-sity In-fras-truc-ture[] \OT1/ptm/m/n/12 The Uni-ver-sity of Pitts-burgh pro-vides com-pre-hen-sive MAT-LAB/Simulink
  []
 
-[20]) (./schedule/v1.tex
+) (./schedule/v1.tex [21]
 Missing character: There is no , in font nullfont!
 
 Overfull \hbox (35.80641pt too wide) in paragraph at lines 61--62
  [][] 
  []
 
-[21] [22]) (./supplemental-sections/v1.tex
+[22]) (./supplemental-sections/v1.tex
 <supplemental-sections/cv-1786798.pdf, id=110, 614.295pt x 794.97pt>
 File: supplemental-sections/cv-1786798.pdf Graphic file (type pdf)
 <use supplemental-sections/cv-1786798.pdf>
@@ -1041,17 +1050,20 @@ L3 programming layer <2024-01-22>
 
 LaTeX Warning: There were undefined references.
 
+
+LaTeX Warning: Label(s) may have changed. Rerun to get cross-references right.
+
  ) 
 Here is how much of TeX's memory you used:
- 26053 strings out of 476182
+ 26054 strings out of 476182
- 542818 string characters out of 5795595
+ 542860 string characters out of 5795595
  1947975 words of memory out of 5000000
- 47472 multiletter control sequences out of 15000+600000
+ 47473 multiletter control sequences out of 15000+600000
  596976 words of font info for 119 fonts, out of 8000000 for 9000
  14 hyphenation exceptions out of 8191
  110i,17n,107p,1062b,952s stack positions out of 10000i,1000n,20000p,200000b,200000s
 </usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt12.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/symbol/usyr.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmb8a.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmbi8a.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmr8a.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmri8a.pfb>
-Output written on main.pdf (32 pages, 255482 bytes).
+Output written on main.pdf (32 pages, 254817 bytes).
 PDF statistics:
  222 PDF objects out of 1000 (max. 8388607)
  131 compressed objects within 2 object streams

Writing/ERLM/metrics-of-success/v2.tex

@@ -0,0 +1,106 @@
+\newpage
+\section{Metrics for Success}
+
+This research will be measured by advancement through Technology Readiness
+Levels, progressing from fundamental concepts to validated prototype
+demonstration. The work begins at TRL 2-3 and aims to reach TRL 5, where system
+components operate successfully in a relevant laboratory environment. This
+section explains why TRL advancement provides the most appropriate success
+metric and defines the specific criteria required to achieve TRL 5.
+
+Technology Readiness Levels provide the ideal success metric because they
+explicitly measure the gap between academic proof-of-concept and practical
+deployment. This gap is precisely what this work aims to bridge. Academic
+metrics like papers published or theorems proved cannot capture practical
+feasibility. Empirical metrics like simulation accuracy or computational speed
+cannot demonstrate theoretical rigor. TRLs measure both dimensions
+simultaneously. Advancing from TRL 3 to TRL 5 requires maintaining theoretical
+rigor while progressively demonstrating practical feasibility. Formal
+verification must remain valid as the system moves from individual components to
+integrated hardware testing.
+
+The nuclear industry requires extremely high assurance before deploying new
+control technologies. Demonstrating theoretical correctness alone is
+insufficient for adoption. Conversely, showing empirical performance without
+formal guarantees fails to meet regulatory requirements. TRLs capture this dual
+requirement naturally. Each level represents both increased practical maturity
+and sustained theoretical validity. Furthermore, TRL assessment forces explicit
+identification of remaining barriers to deployment. The nuclear industry already
+uses TRLs for technology assessment, making this metric directly relevant to
+potential adopters. Reaching TRL 5 provides a clear answer to industry questions
+about feasibility and maturity in a way that academic publications alone cannot.
+
+The work currently exists at TRL 2-3. Formal synthesis and hybrid control
+verification principles have been established through prior research, placing
+the fundamental approach at TRL 2. The SmAHTR simulation model and initial
+procedure analysis place specific components at early TRL 3, where proof of
+concept has been partially demonstrated for individual elements but not
+integrated. The target state is TRL 5. Moving from current state to target
+requires achieving three intermediate levels, each representing a distinct
+validation milestone:
+
+\paragraph{TRL 3 \textit{Critical Function and Proof of Concept}}
+For this research, TRL 3 means demonstrating that each component of the
+methodology works in isolation. SmAHTR 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 reachability analysis proving that
+transition requirements are satisfied. Independent review must confirm that
+specifications match intended procedural behavior. This proves the fundamental
+approach on a simplified startup sequence.
+
+\paragraph{TRL 4 \textit{Laboratory Testing of Integrated Components}}
+For this research, TRL 4 means demonstrating a complete integrated hybrid
+controller in simulation. All SmAHTR startup procedures must be formalized with
+a synthesized automaton covering all operational modes. Continuous controllers
+must exist for all discrete modes. Verification must be complete for all mode
+transitions using reachability analysis, barrier certificates, and
+assume-guarantee contracts. The integrated controller must execute complete
+startup sequences in software simulation with zero safety violations across
+multiple consecutive runs. This proves that formal correctness guarantees can be
+maintained throughout system integration.
+
+\paragraph{TRL 5 \textit{Laboratory Testing in Relevant Environment}}
+For this research, TRL 5 means demonstrating the verified controller on
+industrial control hardware through hardware-in-the-loop testing. The discrete
+automaton must be implemented on the Emerson Ovation control system and verified
+to match synthesized specifications exactly. Continuous controllers must execute
+at required rates. The ARCADE interface must establish stable real-time
+communication between Ovation hardware and SmAHTR simulation. Complete
+autonomous startup sequences must execute via hardware-in-the-loop across the
+full operational envelope. The controller must handle off-nominal scenarios to
+validate that expulsory modes function correctly. For example, simulated sensor
+failures must trigger appropriate fault detection and mode transitions, and loss
+of cooling scenarios must activate SCRAM procedures as specified. Graded
+responses to minor disturbances are outside the scope of this work. Formal
+verification results must remain valid with discrete behavior matching
+specifications and continuous trajectories remaining within verified bounds.
+This proves that the methodology produces verified controllers implementable on
+industrial hardware.
+
+These levels define progressively more demanding demonstrations. TRL 3 proves
+individual components work. TRL 4 proves they work together in simulation. TRL 5
+proves they work on actual hardware in realistic conditions. Each level builds
+on the previous while adding new validation requirements.
+
+Progress will be assessed quarterly through collection of specific data
+comparing actual results against TRL advancement criteria. Specification
+development status indicates progress toward TRL 3. Synthesis results and
+verification coverage indicate progress toward TRL 4. Simulation performance
+metrics and hardware integration milestones indicate progress toward TRL 5. The
+research plan will be revised only when new data invalidates fundamental
+assumptions. Unrealizable specifications indicate procedure conflicts requiring
+refinement or alternative reactor selection. Unverifiable dynamics suggest model
+simplification or alternative verification methods are needed. Unachievable
+real-time performance requires controller simplification or hardware upgrades.
+Any revision will document the invalidating data, the failed assumption, and the
+modified pathway with adjusted scope.
+
+This research succeeds if it achieves TRL 5 by demonstrating a complete
+autonomous hybrid controller with formal correctness guarantees operating on
+industrial control hardware through hardware-in-the-loop testing in a relevant
+laboratory environment. This establishes both theoretical validity and practical
+feasibility, proving that the methodology produces verified controllers and that
+implementation is achievable with current technology. It provides a clear
+pathway for nuclear industry adoption and broader application to safety-critical
+autonomous systems.

Writing/ERLM/research-approach/v4.tex

@@ -0,0 +1,296 @@
+\newpage
+\section{Research Approach}
+
+This research will overcome the limitations of current practice to build 
+high-assurance hybrid control systems for critical infrastructure. Hybrid 
+systems combine continuous dynamics (flows) with discrete transitions (jumps), 
+which can be formally expressed as:
+
+\begin{equation}
+\dot{x}(t) = f(x(t),q(t),u(t))
+\end{equation}
+
+\begin{equation}
+q(k+1) = \nu(x(k),q(k),u(k))
+\end{equation}
+
+Here, $f(\cdot)$ defines the continuous dynamics while $\nu(\cdot)$ governs 
+discrete transitions. The continuous states $x$, discrete state $q$, and 
+control input $u$ interact to produce hybrid behavior. The discrete state $q$ 
+defines which continuous dynamics mode is currently active. Our focus centers 
+on continuous autonomous hybrid systems, where continuous states remain 
+unchanged during jumps—a property naturally exhibited by physical systems. For 
+example, a nuclear reactor switching from warm-up to load-following control 
+cannot instantaneously change its temperature or control rod position, but can
+instantaneously change control laws.
+
+To build these systems with formal correctness guarantees, we must accomplish 
+three main thrusts:
+
+\begin{enumerate}
+  \item Translate operating procedures and requirements into temporal logic
+    formulae
+    
+  \item Create the discrete half of a hybrid controller using reactive synthesis
+
+  \item Develop continuous controllers to operate between modes, and verify
+    their correctness using reachability analysis
+
+\end{enumerate}
+
+The following sections discuss how these thrusts will be accomplished.
+
+\subsection{$(Procedures \wedge FRET) \rightarrow Temporal Specifications$}
+
+The motivation behind this work stems from the fact that commercial nuclear
+power operations remain manually controlled by human operators, despite
+significant advances in control systems sophistication. The key insight is that
+procedures performed by human operators are highly prescriptive and
+well-documented. This suggests that human operators in nuclear power plants may
+not be entirely necessary given today's available technology.
+
+Written procedures and requirements in nuclear power are sufficiently detailed
+that we may be able to translate them into logical formulae with minimal effort.
+If successful, this approach would enable automation of existing procedures
+without requiring system reengineering. To formalize these procedures, we will
+use temporal logic, which captures system behaviors through temporal relations.
+Linear Temporal Logic (LTL) 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 expressed in natural language: 
+\textit{``If a high temperature alarm triggers, control rods must immediately 
+insert and remain inserted until operator reset.''} This plain language 
+requirement can be translated into a rigorous logical specification:
+
+\begin{equation}
+G(HighTemp \rightarrow X(RodsInserted \wedge (\neg RodsWithdrawn\ U\ 
+OperatorReset)))
+\end{equation}
+
+This specification precisely captures the temporal relationship between the 
+alarm condition, the required response, and the persistence requirement. The 
+global operator $G$ ensures this property holds throughout system operation, 
+while the next operator $X$ enforces immediate response. The until operator 
+$U$ maintains the state constraint until the reset condition occurs.
+
+The most efficient path to accomplish this translation is through NASA's 
+Formal Requirements Elicitation Tool (FRET). FRET employs a specialized 
+requirements language called FRETish that restricts requirements to easily 
+understood components while eliminating ambiguity. FRETish bridges natural 
+language and mathematical specifications through a structured English-like 
+syntax that is automatically translatable to temporal logic.
+
+FRET enforces this structure by requiring all requirements to contain six 
+components: %CITE FRET MANUAL
+
+\begin{enumerate}
+  \item Scope: \textit{What modes does this requirement apply to?}
+  \item Condition: \textit{Scope plus additional specificity}
+  \item Component: \textit{What system element does this requirement affect?}
+  \item Shall
+  \item Timing: \textit{When does the response occur?}
+  \item Response: \textit{What action should be taken?}
+\end{enumerate}
+
+FRET provides functionality to check the \textit{realizability} of a system. 
+Realizability analysis determines whether written requirements are complete by 
+examining the six structural components. Complete requirements are those that 
+neither conflict with one another nor leave any behavior undefined. Systems 
+that are not realizable from their procedure definitions and design 
+requirements present problems beyond autonomous control implementation. Such 
+systems 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.
+
+The second category of realizability issues involves undefined behaviors that 
+are typically left to human judgment during control operations. This 
+ambiguity is undesirable for high-assurance systems, since even well-trained 
+humans remain prone to errors. By addressing these specification gaps in FRET 
+during autonomous controller development, we can deliver controllers free from 
+these vulnerabilities.
+
+FRET provides the capability to export requirements in temporal logic format
+compatible with reactive synthesis tools. This export functionality enables
+progression to the next step of our approach: synthesizing discrete mode
+switching behavior from the formalized requirements.
+
+\subsection{$(TemporalLogic \wedge ReactiveSynthesis) \rightarrow
+DiscreteAutomata$}
+
+Reactive synthesis is an active research field in computer science 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 \textit{state transitions}, specify the conditions under which the
+discrete controller moves from state to state. This complete mapping of possible
+states and transitions constitutes a \textit{discrete automaton}. Discrete
+automata can be represented graphically as a series of nodes that are discrete
+states, with traces indicating transitions between states. From the automaton
+graph, it becomes possible to fully describe the dynamics of the discrete system
+and develop intuitive understanding of system behavior. Hybrid systems
+naturally exhibit discrete behavior amenable to formal analysis through these
+finite state representations.
+
+We will employ state-of-the-art reactive synthesis tools, particularly Strix,
+which has demonstrated superior performance in the Reactive Synthesis
+Competition (SYNTCOMP) 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 graphical representation provided by the automaton
+enables inspection and facilitates communication with controls programmers who
+may not have formal methods expertise.
+
+We will use discrete automata to represent the switching behavior of our hybrid
+system. This approach 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 \textit{correct by construction}.
+Correctness of the switching controller is paramount to this work. 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 with capabilities that extend
+beyond written procedures. Autonomous control lacks this adaptive advantage.
+Instead, we must ensure that autonomous controllers replacing human operators
+will not make switching errors between continuous modes. By synthesizing
+controllers from logical specifications with guaranteed correctness, we
+eliminate the possibility of switching errors.
+
+\subsection{$(DiscreteAutomata \wedge ControlTheory \wedge Reachability) 
+\rightarrow ContinuousModes$}
+
+While discrete system components will be synthesized with correctness 
+guarantees, they represent only half of the complete system. Autonomous 
+controllers like those we are developing exhibit continuous dynamics within 
+discrete states, as described by $f(\cdot)$ in Equation 1. This section 
+describes how we will develop continuous control modes, verify their 
+correctness, and address the unique verification challenges of hybrid systems.
+
+The approach described for producing discrete automata yields physics-agnostic 
+specifications that represent only half of a complete hybrid autonomous 
+controller. These automata alone cannot define the full behavior of the 
+control systems we aim to construct. The continuous modes will be developed 
+after discrete automaton construction, leveraging the automaton structure and 
+transitions to design multiple smaller, specialized continuous controllers.
+
+The discrete automaton transitions are key to the supervisory behavior of the 
+autonomous controller. These 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 based 
+on discrete mode transitions:
+
+\begin{enumerate}
+  \item \textbf{Stabilizing:} A stabilizing control mode has one primary 
+    objective: maintaining the hybrid system within its current discrete mode. 
+    This corresponds to steady-state normal operating modes, such as a 
+    full-power load-following controller in a nuclear power plant. Stabilizing 
+    modes can be identified from discrete automata as nodes with only incoming 
+    transitions.
+    
+  \item \textbf{Transitory:} A transitory control mode has the primary goal of 
+    transitioning the hybrid system from one discrete state to another. In 
+    nuclear applications, this might represent a controlled warm-up procedure. 
+    Transitory modes ultimately drive the system toward a stabilizing 
+    steady-state mode. These modes may have secondary objectives within a 
+    discrete state, such as maintaining specific temperature ramp rates before 
+    reaching full-power operation.
+
+  \item \textbf{Expulsory:} An expulsory mode is a specialized transitory mode 
+    with additional safety constraints. Expulsory modes ensure the system is 
+    directed to a safe stabilizing mode during failure conditions. For example, 
+    if a transitory mode fails to achieve its intended transition, the 
+    expulsory mode activates to immediately and irreversibly guide the system 
+    toward a globally safe state. A reactor SCRAM exemplifies an expulsory 
+    continuous mode: when initiated, it must reliably terminate the nuclear 
+    reaction and direct the reactor toward stabilizing decay heat removal.
+
+\end{enumerate}
+
+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. Instead,
+we can use local behavior information at transition boundaries. To ensure
+continuous modes satisfy their requirements, we will employ three main
+techniques: reachability analysis, assume-guarantee contracts, and barrier
+certificates.
+
+\textbf{Reachability Analysis:} Reachability analysis computes the reachable set
+of states for a given input set. While trivial for linear continuous systems,
+recent advances have extended reachability to complex nonlinear systems. We will
+use reachability to define continuous state ranges at discrete transition
+boundaries and verify that requirements are satisfied within continuous modes.
+Recent advances using neural network approximations of Hamilton-Jacobi equations
+have demonstrated significant speedups while maintaining safety guarantees for
+high-dimensional systems, expanding the practical applicability of these
+methods.
+
+\textbf{Assume-Guarantee Contracts:} 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, 
+enabling subsequent reachability analysis without requiring global system 
+analysis.
+
+\textbf{Barrier Certificates:} Finally, we will use barrier certificates to 
+prove that mode transitions are satisfied. Barrier certificates ensure that 
+continuous modes on either side of a transition behave appropriately. Control 
+barrier functions provide a method to certify safety by establishing 
+differential inequality conditions that guarantee forward invariance of safe 
+sets. For example, a barrier certificate can guarantee that a transitory mode 
+transferring control to a stabilizing mode will always move away from the 
+transition boundary, rather than destabilizing the target stabilizing mode.
+
+Combining these three techniques will enable us to prove that continuous
+components of our hybrid controller 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 as a liquid-salt cooled
+reactor design 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 essential for verifying
+continuous controller performance under realistic plant dynamics. The
+synthesized hybrid controller will be implemented on an Emerson Ovation control
+system platform, which is representative of industry-standard control hardware
+deployed in modern nuclear facilities. 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 interfacing
+with a realistic reactor simulation, providing assessment of computational
+performance, real-time execution constraints, and communication latency effects.
+By demonstrating autonomous startup control on this representative platform, we
+will establish both the theoretical validity and practical feasibility of the
+synthesis methodology for deployment in actual small modular reactor systems.
+
+This unified approach addresses a fundamental gap in hybrid system design by
+bridging formal methods and control theory through a systematic, tool-supported
+methodology. By translating existing nuclear procedures into temporal logic,
+synthesizing provably correct discrete switching logic, and developing verified
+continuous controllers, we create a complete framework for autonomous hybrid
+control with mathematical guarantees. The result is an autonomous controller
+that not only replicates human operator decision-making but does so with formal
+assurance that switching logic is correct by construction and continuous
+behavior satisfies safety requirements. This methodology transforms nuclear
+reactor control from a manually intensive operation requiring constant human
+oversight into a fully autonomous system with higher reliability than
+human-operated alternatives. More broadly, this approach establishes a
+replicable framework for developing high-assurance autonomous controllers in any
+domain where operating procedures are well-documented and safety is paramount.
+
+% COMMENTS FOR FUTURE REVISION:
+% 1. Add concrete examples throughout (specific nuclear procedures, requirements)
+% 2. Include a figure showing the overall workflow/methodology
+% 3. Consider adding a subsection on validation approach
+% 4. Strengthen the connections between subsections
+% 5. Add discussion of limitations and assumptions

Writing/ERLM/risks-and-contingencies/v2.tex

@@ -0,0 +1,232 @@
+\newpage
+\section{Risks and Contingencies}
+
+This research relies on several critical assumptions that, if invalidated,
+would require scope adjustment or methodological revision. The primary risks to
+successful completion fall into four categories: computational tractability of
+synthesis and verification, complexity of the discrete-continuous interface,
+completeness of procedure formalization, and hardware-in-the-loop integration
+challenges. Each risk has associated indicators for early detection and
+contingency plans that preserve research value even if core assumptions prove
+false. The staged project structure ensures that partial success yields
+publishable results and clear identification of remaining barriers to
+deployment.
+
+\subsection{Computational Tractability of Synthesis}
+
+The first major assumption is that formalized startup procedures will yield
+automata small enough for efficient synthesis and verification. Reactive
+synthesis scales exponentially with specification complexity, which creates risk
+that temporal logic specifications derived from complete startup procedures may
+produce automata with thousands of states. Such large automata would require
+synthesis times exceeding days or weeks, preventing demonstration of the
+complete methodology within project timelines. Reachability analysis for
+continuous modes with high-dimensional state spaces may similarly prove
+computationally intractable. Either barrier would constitute a fundamental
+obstacle to achieving the research objectives.
+
+Several indicators would provide early warning of computational tractability
+problems. Synthesis times exceeding 24 hours for simplified procedure subsets
+would suggest that complete procedures are intractable. Generated automata
+containing more than 1,000 discrete states would indicate that the discrete
+state space is too large for efficient verification. Specifications flagged as
+unrealizable by FRET or STRIX would reveal fundamental conflicts in the
+formalized procedures. Reachability analysis failing to converge within
+reasonable time bounds would show that continuous mode verification cannot be
+completed with available computational resources.
+
+The contingency plan for computational intractability is to reduce scope to a
+minimal viable startup sequence. This reduced sequence would cover only cold
+shutdown to criticality to low power hold, omitting power ascension and other
+operational phases. The subset would still demonstrate the complete
+methodology while reducing computational burden. The research contribution
+would remain valid even with reduced scope, proving that formal hybrid control
+synthesis is achievable for safety-critical nuclear applications. The limitation
+to simplified operational sequences would be explicitly documented as a
+constraint rather than a failure.
+
+Reachability analysis specifically can exploit time-scale separation inherent in
+reactor dynamics. Fast thermal transients can be treated quasi-steady relative
+to slower nuclear kinetics, which enables decomposition into smaller subsystems.
+Temperature dynamics operate on time scales of seconds to minutes, while neutron
+kinetics respond in milliseconds to seconds for prompt effects and hours for
+xenon poisoning. These distinct time scales permit separate analysis with
+conservative coupling assumptions between subsystems, dramatically reducing the
+dimensionality of reachability computations.
+
+Mitigation strategies exist even before contingency plans become necessary.
+Access to the University of Pittsburgh Center for Research Computing provides
+high-performance computing resources if single-workstation computation proves
+insufficient. Parallel synthesis algorithms and distributed reachability
+analysis can leverage these resources to extend computational feasibility.
+Compositional verification approaches using assume-guarantee reasoning can
+decompose monolithic verification problems into tractable subproblems, each of
+which can be solved independently before composition.
+
+\subsection{Discrete-Continuous Interface Formalization}
+
+The second critical assumption concerns the mapping between boolean guard
+conditions in temporal logic and continuous state boundaries required for mode
+transitions. This interface represents the fundamental challenge of hybrid
+systems: relating discrete switching logic to continuous dynamics. Temporal
+logic operates on boolean predicates, while continuous control requires
+reasoning about differential equations and reachable sets. Guard conditions that
+require complex nonlinear predicates may resist boolean abstraction, making
+synthesis intractable. Continuous safety regions that cannot be expressed as
+conjunctions of verifiable constraints would similarly create insurmountable
+verification challenges. The risk extends beyond static interface definition to
+dynamic behavior across transitions: barrier certificates may fail to exist for
+proposed transitions, or continuous modes may be unable to guarantee convergence
+to discrete transition boundaries.
+
+Early indicators of interface formalization problems would appear during both
+synthesis and verification phases. Guard conditions requiring complex nonlinear
+predicates that resist boolean abstraction would suggest fundamental misalignment
+between discrete specifications and continuous realities. Continuous safety
+regions that cannot be expressed as conjunctions of half-spaces or polynomial
+inequalities would indicate that the interface between discrete guards and
+continuous invariants is too complex. Failure to construct barrier certificates
+proving safety across mode transitions would reveal that the continuous dynamics
+cannot be formally related to discrete switching logic. Reachability analysis
+showing that continuous modes cannot reach intended transition boundaries from
+all possible initial conditions would demonstrate that the synthesized discrete
+controller is incompatible with achievable continuous behavior.
+
+The primary contingency for interface complexity is to restrict continuous modes
+to operate within polytopic invariants. Polytopes are state regions defined as
+intersections of linear half-spaces, which map directly to boolean predicates
+through linear inequality checks. This restriction ensures tractable synthesis
+while maintaining theoretical rigor, though at the cost of limiting
+expressiveness compared to arbitrary nonlinear regions. The discrete-continuous
+interface remains well-defined and verifiable with polytopic restrictions,
+providing a clear fallback position that preserves the core methodology.
+Conservative over-approximations offer an alternative approach: a nonlinear safe
+region can be inner-approximated by a polytope, sacrificing operational
+flexibility to maintain formal guarantees. The three-mode classification already
+structures the problem to minimize complex transitions, with critical safety
+properties concentrated in expulsory modes that can receive additional design
+attention.
+
+Mitigation strategies focus on designing continuous controllers with discrete
+transitions as primary objectives from the outset. Rather than designing
+continuous control laws independently and verifying transitions post-hoc, the
+approach uses transition requirements as design constraints. Control barrier
+functions provide a systematic method to synthesize controllers that guarantee
+forward invariance of safe sets and convergence to transition boundaries. This
+design-for-verification approach reduces the likelihood that interface
+complexity becomes insurmountable. Focusing verification effort on expulsory
+modes---where safety is most critical---allows more complex analysis to be
+applied selectively rather than uniformly across all modes, concentrating
+computational resources where they matter most for safety assurance.
+
+\subsection{Procedure Formalization Completeness}
+
+The third assumption is that existing SmAHTR startup procedures contain
+sufficient detail and clarity for translation into temporal logic specifications.
+Nuclear operating procedures, while extensively detailed, were written for human
+operators who bring contextual understanding and adaptive reasoning to their
+interpretation. Procedures may contain implicit knowledge, ambiguous directives,
+or references to operator judgment that resist formalization in current
+specification languages. Underspecified timing constraints, ambiguous condition
+definitions, or gaps in operational coverage would cause synthesis to fail or
+produce incorrect automata. The risk is not merely that formalization is
+difficult, but that current procedures fundamentally lack the precision required
+for autonomous control, revealing a gap between human-oriented documentation and
+machine-executable specifications.
+
+Several indicators would reveal formalization completeness problems early in the
+project. FRET realizability checks failing due to underspecified behaviors or
+conflicting requirements would indicate that procedures do not form a complete
+specification. Multiple valid interpretations of procedural steps with no clear
+resolution would demonstrate that procedure language is insufficiently precise
+for automated synthesis. Procedures referencing ``operator judgment,'' ``as
+appropriate,'' or similar discretionary language for critical decisions would
+explicitly identify points where human reasoning cannot be directly formalized.
+Domain experts unable to provide crisp answers to specification questions about
+edge cases would suggest that the procedures themselves do not fully define
+system behavior, relying instead on operator training and experience to fill
+gaps.
+
+The contingency plan treats inadequate specification as itself a research
+contribution rather than a project failure. Documenting specific ambiguities
+encountered would create a taxonomy of formalization barriers: timing
+underspecification, missing preconditions, discretionary actions, and undefined
+failure modes. Each category would be analyzed to understand why current
+procedure-writing practices produce these gaps and what specification languages
+would need to address them. Proposed extensions to FRETish or similar
+specification languages would demonstrate how to bridge the gap between current
+procedures and the precision needed for autonomous control. The research output
+would shift from ``here is a complete autonomous controller'' to ``here is what
+formal autonomous control requires that current procedures do not provide, and
+here are language extensions to bridge that gap.'' This contribution remains
+valuable to both the nuclear industry and formal methods community, establishing
+clear requirements for next-generation procedure development and autonomous
+control specification languages.
+
+Early-stage procedure analysis with domain experts provides the primary
+mitigation strategy. Collaboration through the University of Pittsburgh Cyber
+Energy Center enables identification and resolution of ambiguities before
+synthesis attempts, rather than discovering them during failed synthesis runs.
+Iterative refinement with reactor operators and control engineers can clarify
+procedural intent before formalization begins, reducing the risk of discovering
+insurmountable specification gaps late in the project. Comparison with
+procedures from multiple reactor designs---pressurized water reactors, boiling
+water reactors, and advanced designs---may reveal common patterns and standard
+ambiguities amenable to systematic resolution. This cross-design analysis would
+strengthen the generalizability of any proposed specification language
+extensions, ensuring they address industry-wide practices rather than
+SmAHTR-specific quirks.
+
+\subsection{Hardware-in-the-Loop Integration Complexity}
+
+The fourth assumption is that the ARCADE interface can provide stable real-time
+communication between Simulink simulation and Ovation control hardware at
+control rates required for reactor dynamics. Hardware-in-the-loop testing
+introduces timing constraints, communication latency, and platform compatibility
+challenges that are absent in pure simulation. Control rates for reactor systems
+typically range from 10-100 Hz for continuous control to millisecond response
+times for protection system actions. Control loop jitter, communication
+dropouts, or computational limitations in the Ovation PLC could prevent
+successful HIL validation even if the synthesized controller is theoretically
+correct. Real-time operating system constraints, network latency, and hardware
+execution speed may prove incompatible with verified timing assumptions embedded
+in the controller design.
+
+Early indicators would identify hardware integration problems before they derail
+the entire validation effort. Communication dropouts or buffer overruns between ARCADE
+and Ovation would indicate that the interface cannot maintain stable real-time
+data exchange. The Ovation PLC proving unable to execute the synthesized
+automaton at required speed would reveal fundamental computational limitations
+of the target hardware platform. Timing analysis showing that hardware cannot
+meet real-time deadlines assumed during verification would demonstrate
+incompatibility between formal guarantees and physical implementation
+constraints.
+
+The contingency plan is to demonstrate the controller in software-in-the-loop
+configuration with detailed timing analysis showing industrial hardware
+feasibility. Software-in-the-loop testing executes the complete verified
+controller in a real-time software environment that emulates hardware timing
+constraints without requiring physical hardware. Combined with worst-case
+execution time analysis of the synthesized automaton and continuous control
+algorithms, software-in-the-loop validation can provide strong evidence of
+implementability even without physical hardware demonstration. This approach
+maintains TRL 4 rather than TRL 5, but still validates
+the synthesis methodology and establishes a clear pathway to hardware
+deployment. The research contribution remains intact: demonstrating that formal
+hybrid control synthesis produces implementable controllers, with remaining
+barriers clearly identified as hardware integration challenges rather than
+fundamental methodological limitations.
+
+Mitigation strategies leverage existing infrastructure and adopt early testing
+practices. ARCADE has been successfully used for reactor simulation HIL testing
+at the University of Pittsburgh, establishing feasibility in principle and
+providing institutional knowledge about common integration challenges. Conducting
+early integration testing during the synthesis phase, rather than deferring HIL
+attempts until late in the project, identifies timing constraints and
+communication requirements that can inform controller design. Early testing
+ensures that synthesized controllers are compatible with hardware limitations
+from the outset, rather than discovering incompatibilities after synthesis is
+complete. The Ovation platform supports multiple implementation approaches
+including function blocks, structured text, and ladder logic, which provides
+flexibility in how synthesized automata are realized and may enable workarounds
+if one implementation approach proves problematic.

Writing/ERLM/state-of-the-art/v6.tex

@@ -1,3 +1,4 @@
+\newpage
 \section{State of the Art and Limits of Current Practice}
 
 The principal aim of this research is to create autonomous reactor control
@@ -10,29 +11,6 @@ methods based approaches to building reactor control systems.
 
 \subsection{Current Reactor Procedures and Operation}
 
-Current generation nuclear power plants employ 3,600+ active NRC-licensed
-reactor operators in the United States. These operators are divided into Reactor
-Operators (ROs) who manipulate reactor controls and Senior Reactor Operators
-(SROs) who direct plant operations and serve as shift
-supervisors~\cite{10CFR55}. Staffing typically requires 2+ ROs with at least one
-SRO for current generation units. To become a reactor operator, an individual
-might spend up to six years to pass required training~\cite{princeton}.
-
-The role of human operators is paradoxically both critical and
-problematic. Operators hold legal authority under 10 CFR Part 55 to make
-critical decisions including departing from normal regulations during
-emergencies. The Three Mile Island (TMI) accident demonstrated how
-``combination of personnel error, design deficiencies, and component
-failures'' led to partial meltdown when operators ``misread confusing
-and contradictory readings and shut off the emergency water
-system''~\cite{Kemeny1979}. The President's Commission on TMI identified
-a fundamental ambiguity: placing ``responsibility and accountability for
-safe power plant operations...on the licensee in all circumstances''
-without formal verification that operators can fulfill this
-responsibility under all conditions~\cite{Kemeny1979}. This tension
-between operational flexibility and safety assurance remains unresolved
-in current practice.
-
 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
@@ -91,6 +69,37 @@ decades of improvements in training and procedures, provides perhaps the
 most compelling motivation for formal automated control with
 mathematical safety guarantees.
 
+Current generation nuclear power plants employ 3,600+ active NRC-licensed
+reactor operators in the United States. These operators are divided into Reactor
+Operators (ROs) who manipulate reactor controls and Senior Reactor Operators
+(SROs) who direct plant operations and serve as shift
+supervisors~\cite{10CFR55}. Staffing typically requires 2+ ROs with at least one
+SRO for current generation units~\cite{NRC WEBSITE IN ZOTERO FOR PRES}. To
+become a reactor operator, an individual spends several years to pass completed
+training~\cite{ALSO IN PRES FOLDER}. Current generation nuclear power plants
+employ 3,600+ active NRC-licensed reactor operators in the United States. These
+operators are divided into Reactor Operators (ROs) who manipulate reactor
+controls and Senior Reactor Operators (SROs) who direct plant operations and
+serve as shift supervisors~\cite{10CFR55}. Staffing typically requires 2+ ROs
+with at least one SRO for current generation units~\cite{NRC WEBSITE IN ZOTERO
+FOR PRES}. To become a reactor operator, an individual spends several years to
+pass completed training~\cite{ALSO IN PRES FOLDER}.
+
+The role of these human operators is paradoxically both critical and
+problematic. Operators hold legal authority under 10 CFR Part 55 to make
+critical decisions including departing from normal regulations during
+emergencies. The Three Mile Island (TMI) accident demonstrated how ``combination
+of personnel error, design deficiencies, and component failures'' led to partial
+meltdown when operators ``misread confusing and contradictory readings and shut
+off the emergency water system''~\cite{Kemeny1979}. The President's Commission
+on TMI identified a fundamental ambiguity: placing ``responsibility and
+accountability for safe power plant operations...on the licensee in all
+circumstances'' without formal verification that operators can fulfill this
+responsibility under all conditions~\cite{Kemeny1979}.% CHECK THIS SOURCE...
+This tension between operational flexibility and safety assurance remains
+unresolved in current practice as the person responsible for reactor safety
+simultaneously is usually the root cause of a failure.
+
 Multiple independent analyses converge on a striking statistic: 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
@@ -104,26 +113,31 @@ events involved active errors while 92\% were associated with latent errors
 persistence of this 70--80\% human error contribution despite four decades of
 continuous improvements in operator training, control room design, procedures,
 and human factors engineering. This suggests fundamental cognitive limitations
-rather than remediable deficiencies.
+rather than remediable deficiencies. %check all of these sources
 
-The Three Mile Island Unit 2 accident on March 28, 1979 remains the definitive
+%%%%% This seems like a bad paragraph. Doesn't really connect with the idea of 
-case study in human factors failures in nuclear operations. The accident began
+%%%%% autonomy. Seems more like a design issue for the control room. With more
-at 4:00 AM with a routine feedwater pump trip, escalating when a
+%%%%% time it could be explained how doing things this way with requirements to 
-pressure-operated relief valve (PORV) stuck open---draining reactor
+%%%%% logic would catch that no indicator of actual valve position is a problem.
-coolant---but control room instrumentation showed only whether the valve had
+% The Three Mile Island Unit 2 accident on March 28, 1979 remains the definitive
-been commanded to close, not whether it actually closed. When Emergency Core
+% case study in human factors failures in nuclear operations. The accident began
-Cooling System pumps automatically activated as designed, operators made the
+% at 4:00 AM with a routine feedwater pump trip, escalating when a
-fateful decision to shut them down based on their incorrect assessment of plant
+% pressure-operated relief valve (PORV) stuck open---draining reactor
-conditions. The result was a massive loss of coolant accident and the core
+% coolant---but control room instrumentation showed only whether the valve had
-quickly began to overheat. During the emergency, operators faced more than 100
+% been commanded to close, not whether it actually closed. When Emergency Core
-simultaneous alarms, overwhelming their cognitive capacity~\cite{Kemeny1979}.
+% Cooling System pumps automatically activated as designed, operators made the
-The core suffered partial meltdown with 44\% of the fuel melting before the
+% fateful decision to shut them down based on their incorrect assessment of plant
-situation was stabilized. Quantitative risk analysis revealed the magnitude of
+% conditions. The result was a massive loss of coolant accident and the core
-failure in existing safety assessment methods: the actual core damage
+% quickly began to overheat. During the emergency, operators faced more than 100
-probability was approximately 5\% per year while Probabilistic Risk Assessment
+% simultaneous alarms, overwhelming their cognitive capacity~\cite{Kemeny1979}.
-had predicted 0.01\% per year---a 500-fold underestimation. This
+% The core suffered partial meltdown with 44\% of the fuel melting before the
-dramatic failure demonstrated that human reliability could not be adequately
+% situation was stabilized. Quantitative risk analysis revealed the magnitude of
-assessed through expert judgment and historical data alone.
+% failure in existing safety assessment methods: the actual core damage
+% probability was approximately 5\% per year while Probabilistic Risk Assessment
+% had predicted 0.01\% per year---a 500-fold underestimation. This
+% dramatic failure demonstrated that human reliability could not be adequately
+% assessed through expert judgment and historical data alone. 
+% % how does autonomy fix these issues exactly? This seems like
 
 \textbf{LIMITATION:} \textit{Human factors impose fundamental reliability
 limits that cannot be overcome through training alone.} Response time
@@ -143,7 +157,7 @@ project represents the most advanced application of formal methods to nuclear
 reactor control systems to date. HARDENS aimed to address the nuclear industry's
 fundamental dilemma: existing U.S. nuclear control rooms rely on analog
 technologies from the 1950s--60s. This technology is woefully out of date
-compared to modern control technoligies, and incurs significant risk and cost to
+compared to modern control technologies, and incurs significant risk and cost to
 plant operation. The NRC contracted Galois to demonstrate that Model-Based
 Systems Engineering and formal methods could design, verify, and implement a
 complex protection system meeting regulatory criteria at a fraction of typical
@@ -151,12 +165,14 @@ cost. The project delivered a Reactor Trip System (RTS) implementation with full
 traceability from NRC Request for Proposals and IEEE standards through
 formal architecture specifications to formally verified binaries and
 hardware running on FPGA demonstrator boards.
+%%% did it actually do an FPGA demonstration? Dubious.
 
 HARDENS employed an array of formal methods tools and techniques across the
 verification hierarchy. High-level specifications used Lando, SysMLv2, and FRET
 (NASA JPL's Formal Requirements Elicitation Tool) to capture stakeholder
 requirements, domain engineering, certification requirements, and safety
-requirements. Requirements were formally analyzed for consistency, completeness,
+requirements. % this sentence is long af
+Requirements were formally analyzed for consistency, completeness,
 and realizability using SAT and SMT solvers. Executable formal models employed
 Cryptol to create an executable behavioral model of the entire RTS including all
 subsystems, components, and limited digital twin models of sensors, actuators,
@@ -169,14 +185,13 @@ Despite its accomplishments, HARDENS has a fundamental limitation directly
 relevant to hybrid control synthesis: the project addressed only discrete
 digital control logic without modeling or verifying continuous reactor dynamics.
 The Reactor Trip System specification and formal verification covered discrete
-state transitions (trip/no-trip decisions), digital sensor input processing
+state transitions such as trip/no-trip decisions, digital sensor input
-through discrete logic, and discrete actuation outputs (reactor trip commands).
+processing through discrete logic, and discrete actuation outputs such as
-However, the project did not address continuous dynamics of nuclear reactor
+reactor trip commands. However, the project did not address continuous dynamics
-physics. Real reactor safety depends on the interaction between continuous
+of nuclear reactor physics. Real reactor safety depends on the interaction
-processes (temperature, pressure, neutron flux evolving according to
+between continuous processes such as temperature, pressure, neutron flux
-differential equations) and discrete control decisions (trip/no-trip, valve
+evolving due to discrete control decisions. HARDENS verified the discrete
-open/close, pump on/off). HARDENS verified the discrete controller in isolation
+controller in isolation but not the closed-loop hybrid system behavior.
-but not the closed-loop hybrid system behavior.
 
 \textbf{LIMITATION:} \textit{HARDENS addressed discrete control logic without
 continuous dynamics or hybrid system verification.} Verifying discrete control

Zettelkasten/Fleeting Notes/Weekly/2025_49.md

@@ -0,0 +1,76 @@
+---
+id: 2025-49
+title: Weekly — 2025-12-03
+type: Weekly
+created: 2025-12-03T21:01:29-05:00
+modified: 2025-12-03T21:01:29-05:00
+tags: [weekly]
+---
+
+# Weekly - 2025 CW 49 (Wed 2025-12-03)
+
+## Accomplishments
+
+### ERLM
+- ✓ Draft Presentations
+
+### Chair-Search
+- ✓ Make list of tasks for contact about student groups
+
+## Pushed or Rescheduled
+
+The following tasks had their due dates modified during the past week:
+
+- Review and edit Goals and Outcomes section
+- Review and edit State of the Art section
+- Review and edit Research Approach section
+- Review and edit Metrics of Success section
+- Review and edit Risks and Contingencies section
+- Review and edit Broader Impacts section
+- Review and edit Budget section
+- Review and edit Schedule section
+- Verify RFP compliance for all sections
+- Final proofread and polish entire proposal
+- Review and edit Literature Review section
+- Review and edit Methodology Details section
+- Review and edit Expected Contributions section
+- Review and edit Timeline and Milestones section
+- Review and edit Team Qualifications section
+- Review and edit References section
+- Review and edit Appendices
+
+## Cancelled or Deleted
+
+No tasks were cancelled or deleted during this period.
+
+## To Do
+
+### Due This Week (Dec 4-10)
+
+**ERLM Project - Editing Tasks (Due Tomorrow: Dec 4)**
+
+All of the following editing tasks are due tomorrow and are high priority:
+
+- Review and edit Goals and Outcomes section (Urgency: 22.1) ⚡ ACTIVE
+- Review and edit State of the Art section (Urgency: 22.1) ⚡ ACTIVE
+- Review and edit Research Approach section (Urgency: 18.1)
+- Review and edit Metrics of Success section (Urgency: 18.1)
+- Review and edit Risks and Contingencies section (Urgency: 18.1)
+- Review and edit Broader Impacts section (Urgency: 18.1)
+- Review and edit Budget section (Urgency: 18.1)
+- Review and edit Schedule section (Urgency: 18.1)
+- Verify RFP compliance for all sections (Urgency: 18.1)
+- Final proofread and polish entire proposal (Urgency: 18.1)
+- Review and edit Literature Review section (Urgency: 18.1)
+- Review and edit Methodology Details section (Urgency: 18.1)
+- Review and edit Expected Contributions section (Urgency: 18.1)
+- Review and edit Timeline and Milestones section (Urgency: 18.1)
+- Review and edit Team Qualifications section (Urgency: 18.1)
+- Review and edit References section (Urgency: 18.1)
+- Review and edit Appendices (Urgency: 18.1)
+- Update abstract based on final content (Urgency: 18.1)
+- Compile final PDF submission (Urgency: 18.1)
+
+### High Priority
+
+All high-priority tasks are already listed above in the "Due This Week" section.