muh changes

.task/backlog.data

@@ -95,3 +95,16 @@
 {"description":"Complete broader impacts peer review","due":"20251003T040000Z","entry":"20251002T151613Z","modified":"20251002T151613Z","project":"ERLM","status":"pending","uuid":"a5877ce8-f750-413d-8ec1-0e9429395cee"}
 {"description":"Write GO v3","due":"20251006T040000Z","entry":"20251002T151628Z","modified":"20251002T151628Z","project":"ERLM","status":"pending","uuid":"f43f2943-a017-4a3a-a1dd-06ff7a01c22e"}
 {"description":"Complete midterm","due":"20251006T040000Z","entry":"20251002T151541Z","modified":"20251002T152619Z","priority":"H","project":"classes","status":"pending","uuid":"10e41665-b456-4d9f-8ded-577690446a59","tags":["NUCE2101"]}
+{"description":"Write zettel about lipschitz continuity","end":"20251008T182756Z","entry":"20250911T211029Z","modified":"20251008T182804Z","status":"completed","uuid":"b7f68988-8c06-4d18-bf77-91d7e39fd55f","tags":["zk"]}
+{"description":"Complete midterm","due":"20251006T040000Z","end":"20251008T182804Z","entry":"20251002T151541Z","modified":"20251008T182809Z","priority":"H","project":"classes","status":"completed","uuid":"10e41665-b456-4d9f-8ded-577690446a59","tags":["NUCE2101"]}
+{"description":"Write GO v3","due":"20251006T040000Z","end":"20251008T182809Z","entry":"20251002T151628Z","modified":"20251008T182811Z","project":"ERLM","status":"completed","uuid":"f43f2943-a017-4a3a-a1dd-06ff7a01c22e"}
+{"description":"Complete peer review with Simeona","due":"20251009T040000Z","entry":"20251008T183016Z","modified":"20251008T183016Z","project":"ERLM","status":"pending","uuid":"a2970741-1bdf-4f67-a63f-40da1f96315e"}
+{"description":"Write metrics of success section","entry":"20251008T183024Z","modified":"20251008T183024Z","project":"ERLM","status":"pending","uuid":"3bf52991-f8df-4387-9a79-0b5f14f2c5d1","tags":["writing"]}
+{"description":"Make list of internship spots","due":"20251010T040000Z","entry":"20251008T183053Z","modified":"20251008T183053Z","project":"Internship","status":"pending","uuid":"e978e178-5069-44a6-b9de-c835bdf1774f"}
+{"description":"Find INL person Robert mentioned","due":"20251008T040000Z","entry":"20251008T183121Z","modified":"20251008T183121Z","project":"Internship","status":"pending","uuid":"4e709e7a-91f6-47ad-af29-11d3c2cee3d9"}
+{"description":"Do intial play around with Emerson Ovation system","due":"20251010T040000Z","entry":"20251008T184338Z","modified":"20251008T184338Z","status":"pending","uuid":"1116b9e1-e2a9-44e3-939a-1ca7f66d3eea"}
+{"description":"Edit goals and outcomes","end":"20251008T190250Z","entry":"20250924T163953Z","modified":"20251008T190252Z","project":"ERLM","status":"deleted","uuid":"bbc41e22-c647-4209-9500-382e0321b625"}
+{"description":"Fix pagination that Dan was complaining about","end":"20251008T190257Z","entry":"20250924T164344Z","modified":"20251008T190257Z","project":"ERLM","status":"completed","uuid":"306c574b-c3f6-4363-914b-f1eddda04543"}
+{"description":"Complete peer review with Simeona","due":"20251009T040000Z","end":"20251009T200847Z","entry":"20251008T183016Z","modified":"20251009T200847Z","project":"ERLM","status":"completed","uuid":"a2970741-1bdf-4f67-a63f-40da1f96315e"}
+{"description":"Find INL person Robert mentioned","due":"20251008T040000Z","end":"20251009T200847Z","entry":"20251008T183121Z","modified":"20251009T200847Z","project":"Internship","status":"completed","uuid":"4e709e7a-91f6-47ad-af29-11d3c2cee3d9"}
+{"description":"Read Opportunities, Challenges, and Research Needs for Remote Microreactor Operations","entry":"20250910T150523Z","modified":"20251009T200934Z","project":"thesis","start":"20251009T200934Z","status":"pending","uuid":"96c76e6b-5c33-4f54-a156-5c59e718f01a","tags":["reading"]}

.task/completed.data

@@ -1,3 +1,8 @@
+[description:"Edit goals and outcomes" end:"1759950170" entry:"1758731993" modified:"1759950172" project:"ERLM" status:"deleted" uuid:"bbc41e22-c647-4209-9500-382e0321b625"]
+[description:"Fix pagination that Dan was complaining about" end:"1759950177" entry:"1758732224" modified:"1759950177" project:"ERLM" status:"completed" uuid:"306c574b-c3f6-4363-914b-f1eddda04543"]
+[description:"Write zettel about lipschitz continuity" end:"1759948076" entry:"1757625029" modified:"1759948084" status:"completed" tags:"zk" tags_zk:"x" uuid:"b7f68988-8c06-4d18-bf77-91d7e39fd55f"]
+[description:"Complete midterm" due:"1759723200" end:"1759948084" entry:"1759418141" modified:"1759948089" priority:"H" project:"classes" status:"completed" tags:"NUCE2101" tags_NUCE2101:"x" uuid:"10e41665-b456-4d9f-8ded-577690446a59"]
+[description:"Write GO v3" due:"1759723200" end:"1759948089" entry:"1759418188" modified:"1759948091" project:"ERLM" status:"completed" uuid:"f43f2943-a017-4a3a-a1dd-06ff7a01c22e"]
 [dep_47b4efbf-8785-40d2-857d-6c9e44d2369e:"x" depends:"47b4efbf-8785-40d2-857d-6c9e44d2369e" description:"Broader Impacts First Draft" due:"1759118400" end:"1759161466" entry:"1758731886" modified:"1759161466" project:"ERLM" status:"completed" tags:"writing" tags_writing:"x" uuid:"403ad6c3-34b1-424c-a0ac-c50f91756dbf"]
 [description:"get FSAE COM and track data to Matt barry for statics problem. He also wants a cad model?" due:"1758254400" end:"1759156557" entry:"1757515988" modified:"1759156557" status:"completed" uuid:"48f997bf-b686-4c0b-bee5-ac8e5f874ad9"]
 [description:"Broader Impacts Worksheet" end:"1759156557" entry:"1758731868" modified:"1759156557" project:"ERLM" status:"completed" tags:"writing" tags_writing:"x" uuid:"47b4efbf-8785-40d2-857d-6c9e44d2369e"]

.task/pending.data

@@ -2,8 +2,7 @@
 [description:"Write zettels about webofscience database" entry:"1757443242" modified:"1757443242" project:"zk" status:"pending" uuid:"9cb17c85-f1e6-4280-86da-a5af8f229b15"]
 [description:"Look over obsidian tasks and see if anything is worth moving over" entry:"1757443262" modified:"1757443262" status:"pending" tags:"taskwarrior" tags_taskwarrior:"x" uuid:"c1a5390d-5b84-4f9c-8acb-ffb970682660"]
 [description:"Look around for summer internships with national labs" entry:"1757449731" modified:"1757449731" status:"pending" uuid:"d3f3dc53-4feb-4b7e-8de5-86ebf3c535d5"]
-[description:"Read Opportunities, Challenges, and Research Needs for Remote Microreactor Operations" entry:"1757516723" modified:"1758125189" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"96c76e6b-5c33-4f54-a156-5c59e718f01a"]
+[description:"Read Opportunities, Challenges, and Research Needs for Remote Microreactor Operations" entry:"1757516723" modified:"1760040574" project:"thesis" start:"1760040574" status:"pending" tags:"reading" tags_reading:"x" uuid:"96c76e6b-5c33-4f54-a156-5c59e718f01a"]
-[description:"Write zettel about lipschitz continuity" entry:"1757625029" modified:"1757625029" status:"pending" tags:"zk" tags_zk:"x" uuid:"b7f68988-8c06-4d18-bf77-91d7e39fd55f"]
 [description:"The Algorithmic Analysis of Hybrid Systems (1995)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"b15bdc1a-205f-4489-a8fb-e9843306e40d"]
 [description:"Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems (1993)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"6ed5ae99-0296-4011-bb90-39d97021d7ae"]
 [description:"Hybrid Systems: Review and Recent Progress (2003)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"1d8043ca-e583-4835-9d77-65e0e92361c3"]
@@ -30,11 +29,12 @@
 [description:"Learning Local Control Barrier Functions for Hybrid Systems (2024)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"3abf4246-566a-4ba8-b392-cbab5d7a9aa0"]
 [description:"Model Predictive Control of Stochastic Hybrid Systems with Signal Temporal Logic Constraints (2025)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"320ec48e-134f-462f-ac3c-ffaf70698691"]
 [description:"Online Control Synthesis for Uncertain Systems under Signal Temporal Logic Specifications (2024)" entry:"1758125087" modified:"1758125087" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"b47de464-8a66-45d2-b487-6588a60c8112"]
-[description:"Edit goals and outcomes" entry:"1758731993" modified:"1758731993" project:"ERLM" status:"pending" uuid:"bbc41e22-c647-4209-9500-382e0321b625"]
 [description:"Rewrite state of the art for nuclear controls engineering and hybrid systems" due:"1759118400" entry:"1758732019" modified:"1758732076" project:"ERLM" status:"pending" tags:"editing" tags_editing:"x" uuid:"e0636009-9061-47d0-9b59-1f2464a252a7"]
 [description:"Edit goals and outcomes to adjust capabilities. What is new capability, not research task" entry:"1758732156" modified:"1758732156" project:"ERLM" status:"pending" tags:"writing" tags_writing:"x" uuid:"ce706282-31bb-4cba-882d-86f09a76045d"]
 [description:"Add research tasks to research approach section" entry:"1758732208" modified:"1758732208" project:"ERLM" status:"pending" tags:"editing,writing" tags_editing:"x" tags_writing:"x" uuid:"56028c48-5a4b-46cd-a40e-ada624cf6187"]
-[description:"Fix pagination that Dan was complaining about" entry:"1758732224" modified:"1758732224" project:"ERLM" status:"pending" uuid:"306c574b-c3f6-4363-914b-f1eddda04543"]
-[description:"Complete midterm" due:"1759723200" entry:"1759418141" modified:"1759418779" priority:"H" project:"classes" status:"pending" tags:"NUCE2101" tags_NUCE2101:"x" uuid:"10e41665-b456-4d9f-8ded-577690446a59"]
 [description:"Complete broader impacts peer review" due:"1759464000" entry:"1759418173" modified:"1759418173" project:"ERLM" status:"pending" uuid:"a5877ce8-f750-413d-8ec1-0e9429395cee"]
-[description:"Write GO v3" due:"1759723200" entry:"1759418188" modified:"1759418188" project:"ERLM" status:"pending" uuid:"f43f2943-a017-4a3a-a1dd-06ff7a01c22e"]
+[description:"Complete peer review with Simeona" due:"1759982400" end:"1760040527" entry:"1759948216" modified:"1760040527" project:"ERLM" status:"completed" uuid:"a2970741-1bdf-4f67-a63f-40da1f96315e"]
+[description:"Write metrics of success section" entry:"1759948224" modified:"1759948224" project:"ERLM" status:"pending" tags:"writing" tags_writing:"x" uuid:"3bf52991-f8df-4387-9a79-0b5f14f2c5d1"]
+[description:"Make list of internship spots" due:"1760068800" entry:"1759948253" modified:"1759948253" project:"Internship" status:"pending" uuid:"e978e178-5069-44a6-b9de-c835bdf1774f"]
+[description:"Find INL person Robert mentioned" due:"1759896000" end:"1760040527" entry:"1759948281" modified:"1760040527" project:"Internship" status:"completed" uuid:"4e709e7a-91f6-47ad-af29-11d3c2cee3d9"]
+[description:"Do intial play around with Emerson Ovation system" due:"1760068800" entry:"1759949018" modified:"1759949018" status:"pending" uuid:"1116b9e1-e2a9-44e3-939a-1ca7f66d3eea"]

.task/undo.data

@@ -324,3 +324,50 @@ time 1759418779
 old [description:"Complete midterm" due:"1759723200" entry:"1759418141" modified:"1759418141" priority:"H" project:"NUCE2102" status:"pending" uuid:"10e41665-b456-4d9f-8ded-577690446a59"]
 new [description:"Complete midterm" due:"1759723200" entry:"1759418141" modified:"1759418779" priority:"H" project:"classes" status:"pending" tags:"NUCE2101" tags_NUCE2101:"x" uuid:"10e41665-b456-4d9f-8ded-577690446a59"]
 ---
+time 1759948084
+old [description:"Write zettel about lipschitz continuity" entry:"1757625029" modified:"1757625029" status:"pending" tags:"zk" tags_zk:"x" uuid:"b7f68988-8c06-4d18-bf77-91d7e39fd55f"]
+new [description:"Write zettel about lipschitz continuity" end:"1759948076" entry:"1757625029" modified:"1759948084" status:"completed" tags:"zk" tags_zk:"x" uuid:"b7f68988-8c06-4d18-bf77-91d7e39fd55f"]
+---
+time 1759948089
+old [description:"Complete midterm" due:"1759723200" entry:"1759418141" modified:"1759418779" priority:"H" project:"classes" status:"pending" tags:"NUCE2101" tags_NUCE2101:"x" uuid:"10e41665-b456-4d9f-8ded-577690446a59"]
+new [description:"Complete midterm" due:"1759723200" end:"1759948084" entry:"1759418141" modified:"1759948089" priority:"H" project:"classes" status:"completed" tags:"NUCE2101" tags_NUCE2101:"x" uuid:"10e41665-b456-4d9f-8ded-577690446a59"]
+---
+time 1759948091
+old [description:"Write GO v3" due:"1759723200" entry:"1759418188" modified:"1759418188" project:"ERLM" status:"pending" uuid:"f43f2943-a017-4a3a-a1dd-06ff7a01c22e"]
+new [description:"Write GO v3" due:"1759723200" end:"1759948089" entry:"1759418188" modified:"1759948091" project:"ERLM" status:"completed" uuid:"f43f2943-a017-4a3a-a1dd-06ff7a01c22e"]
+---
+time 1759948216
+new [description:"Complete peer review with Simeona" due:"1759982400" entry:"1759948216" modified:"1759948216" project:"ERLM" status:"pending" uuid:"a2970741-1bdf-4f67-a63f-40da1f96315e"]
+---
+time 1759948224
+new [description:"Write metrics of success section" entry:"1759948224" modified:"1759948224" project:"ERLM" status:"pending" tags:"writing" tags_writing:"x" uuid:"3bf52991-f8df-4387-9a79-0b5f14f2c5d1"]
+---
+time 1759948253
+new [description:"Make list of internship spots" due:"1760068800" entry:"1759948253" modified:"1759948253" project:"Internship" status:"pending" uuid:"e978e178-5069-44a6-b9de-c835bdf1774f"]
+---
+time 1759948281
+new [description:"Find INL person Robert mentioned" due:"1759896000" entry:"1759948281" modified:"1759948281" project:"Internship" status:"pending" uuid:"4e709e7a-91f6-47ad-af29-11d3c2cee3d9"]
+---
+time 1759949018
+new [description:"Do intial play around with Emerson Ovation system" due:"1760068800" entry:"1759949018" modified:"1759949018" status:"pending" uuid:"1116b9e1-e2a9-44e3-939a-1ca7f66d3eea"]
+---
+time 1759950172
+old [description:"Edit goals and outcomes" entry:"1758731993" modified:"1758731993" project:"ERLM" status:"pending" uuid:"bbc41e22-c647-4209-9500-382e0321b625"]
+new [description:"Edit goals and outcomes" end:"1759950170" entry:"1758731993" modified:"1759950172" project:"ERLM" status:"deleted" uuid:"bbc41e22-c647-4209-9500-382e0321b625"]
+---
+time 1759950177
+old [description:"Fix pagination that Dan was complaining about" entry:"1758732224" modified:"1758732224" project:"ERLM" status:"pending" uuid:"306c574b-c3f6-4363-914b-f1eddda04543"]
+new [description:"Fix pagination that Dan was complaining about" end:"1759950177" entry:"1758732224" modified:"1759950177" project:"ERLM" status:"completed" uuid:"306c574b-c3f6-4363-914b-f1eddda04543"]
+---
+time 1760040527
+old [description:"Complete peer review with Simeona" due:"1759982400" entry:"1759948216" modified:"1759948216" project:"ERLM" status:"pending" uuid:"a2970741-1bdf-4f67-a63f-40da1f96315e"]
+new [description:"Complete peer review with Simeona" due:"1759982400" end:"1760040527" entry:"1759948216" modified:"1760040527" project:"ERLM" status:"completed" uuid:"a2970741-1bdf-4f67-a63f-40da1f96315e"]
+---
+time 1760040527
+old [description:"Find INL person Robert mentioned" due:"1759896000" entry:"1759948281" modified:"1759948281" project:"Internship" status:"pending" uuid:"4e709e7a-91f6-47ad-af29-11d3c2cee3d9"]
+new [description:"Find INL person Robert mentioned" due:"1759896000" end:"1760040527" entry:"1759948281" modified:"1760040527" project:"Internship" status:"completed" uuid:"4e709e7a-91f6-47ad-af29-11d3c2cee3d9"]
+---
+time 1760040574
+old [description:"Read Opportunities, Challenges, and Research Needs for Remote Microreactor Operations" entry:"1757516723" modified:"1758125189" project:"thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"96c76e6b-5c33-4f54-a156-5c59e718f01a"]
+new [description:"Read Opportunities, Challenges, and Research Needs for Remote Microreactor Operations" entry:"1757516723" modified:"1760040574" project:"thesis" start:"1760040574" status:"pending" tags:"reading" tags_reading:"x" uuid:"96c76e6b-5c33-4f54-a156-5c59e718f01a"]
+---

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

@@ -13,9 +13,8 @@ or radiological release.
 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— such as transitioning from startup
+switch between different control modes based on their interpretation of plant
-heating to power operation—based on their interpretation of plant conditions and
+conditions and procedural guidance. 
-procedural guidance. 
 % Gap
 However, this reliance on human operators prevents the introduction of
 autonomous control capabilities and creates a fundamental economic challenge for
@@ -107,8 +106,9 @@ 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
+from existing procedures with mathematical proof of correct behavior.
-high-assurance autonomous control practical for safety-critical applications. 
+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

Writing/ERLM/main.aux

@@ -2,42 +2,17 @@
 \bibstyle{unsrt}
 \providecommand \oddpage@label [2]{}
 \@writefile{toc}{\contentsline {section}{\numberline {1}Goals and Outcomes}{1}{}\protected@file@percent }
-\citation{geromel2006stability}
-\citation{branicky1998multiple,liberzon2003switching}
 \@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}Control Theory and Hybrid Systems}{2}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {section}{\numberline {3}Research Approach}{2}{}\protected@file@percent }
-\citation{mitchell2005time}
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}$(Procedures \wedge FRET) \rightarrow Temporal Specifications$}{3}{}\protected@file@percent }
-\citation{yang2024learning}
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.2}$(TemporalLogic \wedge ReactiveSynthesis) \rightarrow DiscreteAutomata$}{4}{}\protected@file@percent }
-\citation{alur1993hybrid}
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.3}$(DiscreteAutomata \wedge ControlTheory \wedge Reachability) \rightarrow ContinuousModes$}{5}{}\protected@file@percent }
-\citation{alur1995algorithmic}
-\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Formal Methods and Reactive Synthesis}{3}{}\protected@file@percent }
-\citation{giannakopoulou2022fret}
-\citation{meyer2018strix,jacobs2017syntcomp}
-\citation{platzer2008differential,platzer2017complete}
-\citation{fulton2015keymaera}
-\@writefile{toc}{\contentsline {section}{\numberline {3}Research Approach}{5}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}Requirements: $(Procedures \wedge FRET) \rightarrow Temporal Specifications$}{5}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsection}{\numberline {3.2}Discrete Synthesis: $(TemporalLogic \wedge ReactiveSynthesis) \rightarrow DiscreteAutomata$}{6}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsection}{\numberline {3.3}$(DiscreteAutomata \wedge ControlTheory \wedge Reachability) \rightarrow ContinuousModes$}{6}{}\protected@file@percent }
 \citation{eia_lcoe_2022}
 \citation{eesi_datacenter_2024}
 \citation{eia_lcoe_2022}
-\@writefile{toc}{\contentsline {subsection}{\numberline {3.4}Broader Impacts}{8}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.4}Broader Impacts}{7}{}\protected@file@percent }
 \bibdata{references}
-\bibcite{geromel2006stability}{1}
+\bibcite{eia_lcoe_2022}{1}
-\bibcite{branicky1998multiple}{2}
+\bibcite{eesi_datacenter_2024}{2}
-\bibcite{liberzon2003switching}{3}
+\@writefile{toc}{\contentsline {section}{References}{9}{}\protected@file@percent }
-\bibcite{mitchell2005time}{4}
+\gdef \@abspage@last{10}
-\bibcite{yang2024learning}{5}
-\bibcite{alur1993hybrid}{6}
-\bibcite{alur1995algorithmic}{7}
-\bibcite{giannakopoulou2022fret}{8}
-\bibcite{meyer2018strix}{9}
-\bibcite{jacobs2017syntcomp}{10}
-\bibcite{platzer2008differential}{11}
-\bibcite{platzer2017complete}{12}
-\bibcite{fulton2015keymaera}{13}
-\bibcite{eia_lcoe_2022}{14}
-\bibcite{eesi_datacenter_2024}{15}
-\@writefile{toc}{\contentsline {section}{References}{10}{}\protected@file@percent }
-\gdef \@abspage@last{12}

Writing/ERLM/main.bbl

@@ -1,69 +1,4 @@
-\begin{thebibliography}{10}
+\begin{thebibliography}{1}
-
-\bibitem{geromel2006stability}
-Jos{\'e}~C Geromel and Patrizio Colaneri.
-\newblock Stability and stabilization of continuous-time switched linear systems.
-\newblock {\em SIAM Journal on Control and Optimization}, 45(5):1915--1930, 2006.
-
-\bibitem{branicky1998multiple}
-Michael~S Branicky.
-\newblock Multiple lyapunov functions and other analysis tools for switched and hybrid systems.
-\newblock {\em IEEE Transactions on Automatic Control}, 43(4):475--482, 1998.
-
-\bibitem{liberzon2003switching}
-Daniel Liberzon.
-\newblock {\em Switching in systems and control}.
-\newblock Birkh{\"a}user Boston, 2003.
-
-\bibitem{mitchell2005time}
-Ian~M Mitchell, Alexandre~M Bayen, and Claire~J Tomlin.
-\newblock A time-dependent hamilton-jacobi formulation of reachable sets for continuous dynamic games.
-\newblock {\em IEEE Transactions on Automatic Control}, 50(7):947--957, 2005.
-
-\bibitem{yang2024learning}
-Shuo Yang, Yiwei Chen, Xiang Yin, and Rahul Mangharam.
-\newblock Learning local control barrier functions for hybrid systems.
-\newblock {\em arXiv preprint arXiv:2401.14907}, 2024.
-
-\bibitem{alur1993hybrid}
-Rajeev Alur, Costas Courcoubetis, Thomas~A Henzinger, and Pei-Hsin Ho.
-\newblock Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems.
-\newblock In {\em Hybrid Systems}, pages 209--229. Springer, 1993.
-
-\bibitem{alur1995algorithmic}
-Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs, Thomas~A Henzinger, Pei-Hsin Ho, Xavier Nicollin, Alfredo Olivero, Joseph Sifakis, and Sergio Yovine.
-\newblock The algorithmic analysis of hybrid systems.
-\newblock {\em Theoretical Computer Science}, 138(1):3--34, 1995.
-
-\bibitem{giannakopoulou2022fret}
-Dimitra Giannakopoulou, Anastasia Mavridou, Julian Rhein, Thomas Pressburger, Johann Schumann, and Nija Shi.
-\newblock Capturing and analyzing requirements with fret.
-\newblock Technical Report NASA/TM-20220007610, NASA Ames Research Center, 2022.
-
-\bibitem{meyer2018strix}
-Philipp~J Meyer and Michael Luttenberger.
-\newblock Strix: Explicit reactive synthesis strikes back!
-\newblock In {\em International Conference on Computer Aided Verification}, pages 578--586. Springer, 2018.
-
-\bibitem{jacobs2017syntcomp}
-Swen Jacobs, Roderick Bloem, Romain Brenguier, et~al.
-\newblock The 4th reactive synthesis competition (syntcomp 2017): Benchmarks, participants \& results.
-\newblock In {\em 6th Workshop on Synthesis}, volume 260 of {\em EPTCS}, 2017.
-
-\bibitem{platzer2008differential}
-Andr{\'e} Platzer.
-\newblock Differential dynamic logic for hybrid systems.
-\newblock {\em Journal of Automated Reasoning}, 41(2):143--189, 2008.
-
-\bibitem{platzer2017complete}
-Andr{\'e} Platzer.
-\newblock A complete uniform substitution calculus for differential dynamic logic.
-\newblock {\em Journal of Automated Reasoning}, 59(2):219--265, 2017.
-
-\bibitem{fulton2015keymaera}
-Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus V{\"o}lp, and Andr{\'e} Platzer.
-\newblock Keymaera x: An axiomatic tactical theorem prover for hybrid systems.
-\newblock In {\em International Conference on Automated Deduction}, pages 527--538. Springer, 2015.
 
 \bibitem{eia_lcoe_2022}
 {U.S. Energy Information Administration}.

Writing/ERLM/main.blg

@@ -3,44 +3,44 @@ 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 15 entries,
+You've used 2 entries,
             1791 wiz_defined-function locations,
-            541 strings with 6280 characters,
+            458 strings with 3888 characters,
-and the built_in function-call counts, 3692 in all, are:
+and the built_in function-call counts, 290 in all, are:
-= -- 340
+= -- 27
-> -- 159
+> -- 8
-< -- 5
+< -- 0
-+ -- 60
++ -- 4
-- -- 45
+- -- 2
-* -- 243
+* -- 7
-:= -- 579
+:= -- 58
-add.period$ -- 50
+add.period$ -- 8
-call.type$ -- 15
+call.type$ -- 2
-change.case$ -- 15
+change.case$ -- 3
 chr.to.int$ -- 0
-cite$ -- 15
+cite$ -- 2
-duplicate$ -- 166
+duplicate$ -- 11
-empty$ -- 359
+empty$ -- 31
-format.name$ -- 45
+format.name$ -- 2
-if$ -- 831
+if$ -- 62
 int.to.chr$ -- 0
-int.to.str$ -- 15
+int.to.str$ -- 2
-missing$ -- 13
+missing$ -- 0
-newline$ -- 80
+newline$ -- 15
-num.names$ -- 15
+num.names$ -- 2
-pop$ -- 46
+pop$ -- 7
 preamble$ -- 1
 purify$ -- 0
 quote$ -- 0
-skip$ -- 76
+skip$ -- 3
 stack$ -- 0
-substring$ -- 243
+substring$ -- 0
-swap$ -- 47
+swap$ -- 1
-text.length$ -- 5
+text.length$ -- 0
 text.prefix$ -- 0
 top$ -- 0
 type$ -- 0
 warning$ -- 0
-while$ -- 36
+while$ -- 2
-width$ -- 17
+width$ -- 3
-write$ -- 171
+write$ -- 27

Writing/ERLM/main.fdb_latexmk

@@ -1,13 +1,13 @@
 # Fdb version 4
-["bibtex main"] 1759870878.63919 "main.aux" "main.bbl" "main" 1759870879.52101 0
+["bibtex main"] 1759939327.8125 "main.aux" "main.bbl" "main" 1759939658.21819 0
   "./references.bib" 1759167577.47323 10304 77c9387d6b0ce7e1af7f15e6fb0e19c3 ""
   "/usr/share/texlive/texmf-dist/bibtex/bst/base/unsrt.bst" 1292289607 18030 1376b4b231b50c66211e47e42eda2875 ""
-  "main.aux" 1759870879.38834 2371 0b7e48a03f45dbd09ec32422fa17b1e2 "pdflatex"
+  "main.aux" 1759939658.08244 1289 1d316a99aeb3565c50a880d45385bf39 "pdflatex"
   (generated)
   "main.bbl"
   "main.blg"
   (rewritten before read)
-["pdflatex"] 1759870878.6614 "main.tex" "main.pdf" "main" 1759870879.52119 0
+["pdflatex"] 1759939657.26937 "main.tex" "main.pdf" "main" 1759939658.21842 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 ""
@@ -29,14 +29,10 @@
   "/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmmi10.tfm" 1136768653 1528 abec98dbc43e172678c11b3b9031252a ""
   "/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmr10.tfm" 1136768653 1296 45809c5a464d5f32c8f98ba97c1bb47f ""
   "/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmr12.tfm" 1136768653 1288 655e228510b4c2a1abe905c368440826 ""
-  "/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmss12.tfm" 1136768653 1324 37b971caf729d7edd9cbb9f9b0ea76eb ""
-  "/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmss8.tfm" 1136768653 1296 d77f431d10d47c8ea2cc18cf45346274 ""
-  "/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmss9.tfm" 1136768653 1320 49357c421c0d469f88b867dd0c3d10e8 ""
   "/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmsy10.tfm" 1136768653 1124 6c73e740cf17375f03eec0ee63599741 ""
   "/usr/share/texlive/texmf-dist/fonts/tfm/public/rsfs/rsfs10.tfm" 1229303445 688 37338d6ab346c2f1466b29e195316aa4 ""
   "/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb" 1248133631 36299 5f9df58c2139e7edcf37c8fca4bd384d ""
   "/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb" 1248133631 35752 024fb6c41858982481f6968b5fc26508 ""
-  "/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmss12.pfb" 1248133631 24393 3b7eb51a67a0a62aec5849271bdb9c2e ""
   "/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb" 1248133631 32569 5e5ddc8df908dea60932f3c484a54c0d ""
   "/usr/share/texlive/texmf-dist/fonts/type1/urw/symbol/usyr.pfb" 1136849748 33709 b09d2e140b7e807d3a97058263ab6693 ""
   "/usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmb8a.pfb" 1136849748 44729 811d6c62865936705a31c797a1d5dada ""
@@ -235,12 +231,12 @@
   "/var/lib/texmf/web2c/pdftex/pdflatex.fmt" 1726005817 6800784 2b63e5a224c5ad740802d8f9921962c1 ""
   "broader-impacts/v1.tex" 1759167577.47123 4916 8f9b155145119717e181909e7ce40ed4 ""
   "dane_proposal_format.cls" 1759861808.72975 2553 3bbf169a90a50515ed103fe388c111f0 ""
-  "goals-and-outcomes/v6.tex" 1759870860.65316 6132 978a430623148b07dc06f1fa9ce4a2e0 ""
+  "goals-and-outcomes/v6.tex" 1759931957.10694 6070 286ca847b1aac31431e0658cd2989ea2 ""
-  "main.aux" 1759870879.38834 2371 0b7e48a03f45dbd09ec32422fa17b1e2 "pdflatex"
+  "main.aux" 1759939658.08244 1289 1d316a99aeb3565c50a880d45385bf39 "pdflatex"
-  "main.bbl" 1759870878.65533 3654 cb7bb2c7072cb5aea3ed65a8abe6024a "bibtex main"
+  "main.bbl" 1759939327.82843 534 c978a85388337a36f349b54afe9a8b11 "bibtex main"
-  "main.tex" 1759870875.8503 233 b14d908b969b3e0790528a34f9ae8ceb ""
+  "main.tex" 1759933733.9178 233 46639edff38f24c04a0657b1bb8d4c8f ""
-  "research-approach/v2.tex" 1758557109.9037 13747 97ad683c7942f87218a074a6187782d1 ""
+  "research-approach/v3.tex" 1759939583.16696 17351 6ed3e4ff3c33dd86d80597dbdb0cf36f ""
-  "state-of-the-art/v2.tex" 1757962977.69875 10918 a65147e24336b6a318bf18223339313e ""
+  "state-of-the-art/v3.tex" 1759932892.29406 956 1c5dc5397b94b907f165191b875edbeb ""
   (generated)
   "main.aux"
   "main.log"

Writing/ERLM/main.fls

@@ -413,11 +413,16 @@ 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/ptmb7t.vf
 INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb8r.tfm
-INPUT ./state-of-the-art/v2.tex
+INPUT ./state-of-the-art/v3.tex
-INPUT ./state-of-the-art/v2.tex
+INPUT ./state-of-the-art/v3.tex
-INPUT ./state-of-the-art/v2.tex
+INPUT ./state-of-the-art/v3.tex
-INPUT ./state-of-the-art/v2.tex
+INPUT ./state-of-the-art/v3.tex
-INPUT state-of-the-art/v2.tex
+INPUT state-of-the-art/v3.tex
+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/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
@@ -451,34 +456,23 @@ INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri8r.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/tfm/public/cm/cmss12.tfm
-INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmss9.tfm
-INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmss8.tfm
-INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm
-INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm
 INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmri7t.vf
-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 ./research-approach/v2.tex
-INPUT ./research-approach/v2.tex
-INPUT ./research-approach/v2.tex
-INPUT ./research-approach/v2.tex
-INPUT research-approach/v2.tex
-INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmr8c.vf
 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 /usr/share/texlive/texmf-dist/tex/latex/psnfss/ts1ptm.fd
+INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/ts1ptm.fd
+INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/ts1ptm.fd
+INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr8c.tfm
+INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmr8c.vf
 INPUT ./main.bbl
 INPUT ./main.bbl
 INPUT main.bbl
 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/cmss12.pfb
 INPUT /usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb
 INPUT /usr/share/texlive/texmf-dist/fonts/type1/urw/symbol/usyr.pfb
 INPUT /usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmb8a.pfb

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)  7 OCT 2025 17:01
+This is pdfTeX, Version 3.141592653-2.6-1.40.25 (TeX Live 2023/Debian) (preloaded format=pdflatex 2024.9.10)  8 OCT 2025 12:07
 entering extended mode
  restricted \write18 enabled.
  file:line:error style messages enabled.
@@ -876,41 +876,36 @@ LaTeX Font Info:    Font shape `OT1/ptm/bx/n' in size <8> not available
 (Font)              Font shape `OT1/ptm/b/n' tried instead on input line 5.
  [1
 
-{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}{/usr/share/texlive/texmf-dist/fonts/enc/dvips/base/8r.enc}] (./goals-and-outcomes/v6.tex [1]) (./state-of-the-art/v2.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/v3.tex) (./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 15.
+(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 15.
+(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 15.
+(Font)              Font shape `OT1/ptm/b/n' tried instead on input line 8.
- [2] [3]
+ [2] [3] [4] [5] [6]) (./broader-impacts/v1.tex
-LaTeX Font Info:    Trying to load font information for TS1+ptm on input line 168.
+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.
-)) (./research-approach/v2.tex [4]
+) [7]) [8] (./main.bbl) [9] (./main.aux)
-Overfull \hbox (1.34416pt too wide) in paragraph at lines 44--48
-[]\OT1/ptm/m/n/12 FRET em-ploys a spe-cial-ized re-quire-ments lan-guage sim-i-lar to nat-u-ral lan-guage called FRETish.
- []
-
-[5] [6] [7]) (./broader-impacts/v1.tex [8]) [9] (./main.bbl [10]) [11] (./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:
- 25428 strings out of 476182
+ 25398 strings out of 476182
- 528199 string characters out of 5795595
+ 527675 string characters out of 5795595
  1935975 words of memory out of 5000000
- 46870 multiletter control sequences out of 15000+600000
+ 46843 multiletter control sequences out of 15000+600000
- 590786 words of font info for 108 fonts, out of 8000000 for 9000
+ 588859 words of font info for 103 fonts, out of 8000000 for 9000
  14 hyphenation exceptions out of 8191
- 110i,9n,107p,1008b,285s stack positions out of 10000i,1000n,20000p,200000b,200000s
+ 110i,6n,107p,1008b,285s stack positions out of 10000i,1000n,20000p,200000b,200000s
-</usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmss12.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/symbol/usyr.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmb8a.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmr8a.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmri8a.pfb>
+</usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/symbol/usyr.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmb8a.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmr8a.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmri8a.pfb>
-Output written on main.pdf (12 pages, 124660 bytes).
+Output written on main.pdf (10 pages, 105691 bytes).
 PDF statistics:
- 111 PDF objects out of 1000 (max. 8388607)
+ 100 PDF objects out of 1000 (max. 8388607)
- 64 compressed objects within 1 object stream
+ 57 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)
 

Writing/ERLM/main.tex

@@ -4,8 +4,8 @@
 
 \maketitle
 \input{goals-and-outcomes/v6}
-\input{state-of-the-art/v2}
+\input{state-of-the-art/v3}
-\input{research-approach/v2}
+\input{research-approach/v3}
 \input{broader-impacts/v1}
 
 \newpage

Writing/ERLM/research-approach/v3.tex

@@ -0,0 +1,295 @@
+\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/state-of-the-art/v3.tex

@@ -0,0 +1,25 @@
+\section{State of the Art and Limits of Current Practice}
+
+UNDER CONSTRUCTION
+
+Basically this section is going to talk about:
+\begin{enumerate}
+  \item How operating procedures are written today
+  \item How nuclear operators are trained and what their jobs are
+  \item HARDENS - an early work trying to build a reactor emergency shutdown
+    system with formal methods, by doing a lot of this translation stuff.
+\end{enumerate}
+
+Some key limits are:
+\begin{enumerate}
+  \item Operating procedures are written in natural language. This makes them
+    unavoidable ambiguous and leaves instructions up to interpretation
+
+  \item Human operators can make human errors. Discuss how most nuclear
+    accidents are actually people driven, and not the fault of the plant itself.
+
+  \item HARDENS does not consider continuous dynamics, nor did they really test
+    anything to validate their system works. Dan says TRL 3. I begrudgingly
+    agree.
+
+\end{enumerate}