diff --git a/Writing/ERLM/dane_proposal_format.cls b/Writing/ERLM/dane_proposal_format.cls index f5bb701d7..b307cdad3 100644 --- a/Writing/ERLM/dane_proposal_format.cls +++ b/Writing/ERLM/dane_proposal_format.cls @@ -7,7 +7,7 @@ % Core packages \RequirePackage[utf8]{inputenc} -\RequirePackage[margin=2in]{geometry} +\RequirePackage[margin=1in]{geometry} \RequirePackage[hyphens]{url} % Font selection (NSF compliant) diff --git a/Writing/ERLM/goals-and-outcomes/v5.tex b/Writing/ERLM/goals-and-outcomes/v5.tex new file mode 100644 index 000000000..b1dcd8db0 --- /dev/null +++ b/Writing/ERLM/goals-and-outcomes/v5.tex @@ -0,0 +1,130 @@ +\section{Goals and Outcomes} + +The goal of this research is to create a methodology for building high assurance +hybrid autonomous control systems. + +%FIRST PARAGRAPH - INTRO HOOK +Commercial control systems for nuclear power have been stuck in the past, far +behind the state of the art of controls. +% 3-5 SENTENCES KNOWN INFO +Nuclear power control systems are extremely high assurance system, where +failures are intolerable. A control failure in nuclear power has a broader +impact than financial losses. Instead, a failure can create extensive economic +losses for the power utility, interruptions for local customers, or in the worst +case, radiological release in the local environment. Because of this, control of +nuclear power is performed by operators who are extensively trained, use +detailed operating procedures, and follow strict requirements. +% GAP +This method of control has been reliable, but is woefully behind the +capabilities of modern less critical control systems, and by relying on human +operators, prevents the introduction of autonomy. +% CRITICAL NEED +To bring nuclear power control into the 21st century, we need a way to develop +autonomous control systems that have strict guarantees and assurance of their +correct behavior across their operating range. + +% SECOND PARAGRAPH - APPROACH SOLUTION +To do this, we will blend tools from computer science and formal methods with +those from engineering and control theory to build high assurance hybrid systems +to perform autonomous control. +% RATIONALE +Hybrids systems have switching behavior, where discrete transitions between +continuous dynamics occur. Verification of these systems is difficult because of +these transitions. We will address this difficulty by building autonomous hybrid +control systems that are correct by construction. We will synthesize the +discrete mode switching behavior from written operating procedures, while +utilizing reachability analysis and assume-guarantee contracts to prove that +continuous modes behave correctly. +% HYPOTHESIS PAY-OFF/IMPACT +If we are successful in creating a hybrid control system that is correct by +construction, we can implement autonomous control systems in nuclear power with +a great assurance of their safety and performance. Autonomous control is a +technology that is desperately needed for the future of nuclear power. Nuclear +plant designs such as small modular reactors or microcreactors have been +suggested as a way to reduce the enormous capital costs of nuclear power +construction, but are limited in their feasibility by the increased cost of +operator staffing per megawatt generated. If we can reduce the quantity of +operaters needed in these reactors, we can reduce the cost of generating clean +nuclear power and address increasing energy demands. +% QUALIFICATIONS +This work is also situated in the University of Pittsburgh Cyber Energy Center. +This research is colocated with collaboration across the energy industry and +benefits from having access to industry-ready control hardware from Emerson. +The accessibility to industry this research has will ensure that solutions and +capabilities generated are aligned with industry needs. + +If this research is successful, we will be able to do the following: +\begin{enumerate} + % OUTCOME PARAGRAPH 1 TITLE + \item \textbf{ Synthesize written operating procedures into discrete automata. + } + % STRATEGY + Discrete automata are the backbone of a continuous hybrid system. These + automata control the swtiching behavior between continuous modes, and are + directly analogous to operators changing between control laws. The automated + creation of these automata is a mature field called reactive synthesis. + Reactive synthesis is enabled by specifying logical requriements of a + discrete system. These requirements will be created from current written + operating procedures directly, through an intermediate tool called FRET, + which uses a natural-language-like format called FRETish to embed + requirements. + % OUTCOME + By using written operating procedures to create the discrete automata, we + will provide a means for control systems engineers to create discrete + switching behavior without having to become logical experts. This reduces + the barrier to entry for using formal methods tools, making high assurance + switching mechanisms easier to attain. + +% OUTCOME PARAGRAPH 2 +% TITLE + \item \textbf{ + Build hybrid systems using correct by construction principles. + } +% STRATEGY + In addition to the discrete system, hybrid systems use continuous modes + between discrete transitions. These continuous modes will be constructed + using standard control theory practices, but will use formal methods to + ensure their correctness. Because the discrete modes and their transitions + will already be specified from operating requirements, the continuous modes + will be examined to ensure that only allowable state transitions can be + reached. +% OUTCOME + This way, controls engineers can build continuous modes exactly as they + would before, but iterate on their designs to ensure broader system + correctness. + +% OUTCOME PARAGRAPH 3 TITLE + \item \textbf{ Create autonomous control systems with strict safety + guarantees. } + % STRATEGY + By combining the discrete and continuous components while building proof of + their correctness along the way, we can translate these capabilities into + realizable autonomous systems for nuclear power. We will use the methodology + presented in this proposal to build a candidate control system using a + simulation of a small modular reactor in combination with an Emerson Ovation + control system. + % OUTCOME + By realizing an autonomous hybrid control system using this methodology, we + will generate evidence that autonomous hybrid control can be realized in the + nuclear industry with current controls equipment. + + +\end{enumerate} + +% THIRD PARAGRAPH - IMPACT +% INNOVATION +The innovation in this work is the implementation of different formal methods +technologies for the purpose of building hybrid control systems. These +technologies will allow us to build hybrid systems with behavior we can ensure. +% OUTCOME IMPACT +The way that these technologies will be implemented is also designed to incur +the smallest amount of cost possible for possible recreation in industry. +Controls engineers should be able to find this work approachable, and +implementable in new nuclear technology control systems. +% GENERAL IMPACT +New control systems, especially autonomous control, are critical to advancing +the prevalence of nuclear power. Small modular reactors stand to answer the next +energy generation challenge in the United States, but must address the +significant operating cost required by current staffing limits. This work will +allow new reactors to reduce the amount of operators required and improve the +economic feasibility of new reactor designs. diff --git a/Writing/ERLM/goals-and-outcomes/v6.tex b/Writing/ERLM/goals-and-outcomes/v6.tex new file mode 100644 index 000000000..9e48b3a26 --- /dev/null +++ b/Writing/ERLM/goals-and-outcomes/v6.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— such as transitioning from startup +heating to power operation—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, making +high-assurance autonomous control 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. diff --git a/Writing/ERLM/main.aux b/Writing/ERLM/main.aux index 9790329bf..4eec240cb 100644 --- a/Writing/ERLM/main.aux +++ b/Writing/ERLM/main.aux @@ -2,27 +2,27 @@ \bibstyle{unsrt} \providecommand \oddpage@label [2]{} \@writefile{toc}{\contentsline {section}{\numberline {1}Goals and Outcomes}{1}{}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {2}State of the Art and Limits of Current Practice}{3}{}\protected@file@percent } \citation{geromel2006stability} \citation{branicky1998multiple,liberzon2003switching} -\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}Control Theory and Hybrid Systems}{4}{}\protected@file@percent } +\@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 } \citation{mitchell2005time} \citation{yang2024learning} \citation{alur1993hybrid} \citation{alur1995algorithmic} +\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Formal Methods and Reactive Synthesis}{3}{}\protected@file@percent } \citation{giannakopoulou2022fret} -\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Formal Methods and Reactive Synthesis}{6}{}\protected@file@percent } \citation{meyer2018strix,jacobs2017syntcomp} \citation{platzer2008differential,platzer2017complete} \citation{fulton2015keymaera} -\@writefile{toc}{\contentsline {section}{\numberline {3}Research Approach}{8}{}\protected@file@percent } -\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}Requirements: $(Procedures \wedge FRET) \rightarrow Temporal Specifications$}{9}{}\protected@file@percent } -\@writefile{toc}{\contentsline {subsection}{\numberline {3.2}Discrete Synthesis: $(TemporalLogic \wedge ReactiveSynthesis) \rightarrow DiscreteAutomata$}{10}{}\protected@file@percent } -\@writefile{toc}{\contentsline {subsection}{\numberline {3.3}$(DiscreteAutomata \wedge ControlTheory \wedge Reachability) \rightarrow ContinuousModes$}{11}{}\protected@file@percent } +\@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}{14}{}\protected@file@percent } +\@writefile{toc}{\contentsline {subsection}{\numberline {3.4}Broader Impacts}{8}{}\protected@file@percent } \bibdata{references} \bibcite{geromel2006stability}{1} \bibcite{branicky1998multiple}{2} @@ -33,11 +33,11 @@ \bibcite{alur1995algorithmic}{7} \bibcite{giannakopoulou2022fret}{8} \bibcite{meyer2018strix}{9} -\@writefile{toc}{\contentsline {section}{References}{17}{}\protected@file@percent } \bibcite{jacobs2017syntcomp}{10} \bibcite{platzer2008differential}{11} \bibcite{platzer2017complete}{12} \bibcite{fulton2015keymaera}{13} \bibcite{eia_lcoe_2022}{14} \bibcite{eesi_datacenter_2024}{15} -\gdef \@abspage@last{19} +\@writefile{toc}{\contentsline {section}{References}{10}{}\protected@file@percent } +\gdef \@abspage@last{12} diff --git a/Writing/ERLM/main.fdb_latexmk b/Writing/ERLM/main.fdb_latexmk index 1e1cbe793..99b8cb16e 100644 --- a/Writing/ERLM/main.fdb_latexmk +++ b/Writing/ERLM/main.fdb_latexmk @@ -1,13 +1,13 @@ # Fdb version 4 -["bibtex main"] 1759176018.82835 "main.aux" "main.bbl" "main" 1759176019.69068 0 +["bibtex main"] 1759870878.63919 "main.aux" "main.bbl" "main" 1759870879.52101 0 "./references.bib" 1759167577.47323 10304 77c9387d6b0ce7e1af7f15e6fb0e19c3 "" "/usr/share/texlive/texmf-dist/bibtex/bst/base/unsrt.bst" 1292289607 18030 1376b4b231b50c66211e47e42eda2875 "" - "main.aux" 1759176019.55307 2374 b147740a80a9603c73976206e1823736 "pdflatex" + "main.aux" 1759870879.38834 2371 0b7e48a03f45dbd09ec32422fa17b1e2 "pdflatex" (generated) "main.bbl" "main.blg" (rewritten before read) -["pdflatex"] 1759176018.85638 "main.tex" "main.pdf" "main" 1759176019.69098 0 +["pdflatex"] 1759870878.6614 "main.tex" "main.pdf" "main" 1759870879.52119 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 "" @@ -234,11 +234,11 @@ "/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map" 1722610820.43889 128028 f533b797fba58d231669ea19e894e23e "" "/var/lib/texmf/web2c/pdftex/pdflatex.fmt" 1726005817 6800784 2b63e5a224c5ad740802d8f9921962c1 "" "broader-impacts/v1.tex" 1759167577.47123 4916 8f9b155145119717e181909e7ce40ed4 "" - "dane_proposal_format.cls" 1759176012.54199 2553 dc5fb7813ce17dfa84a228efd08fd33b "" - "goals-and-outcomes/v4.tex" 1757896122.20856 5764 a67e489f9ea8343564010d217ae37ec2 "" - "main.aux" 1759176019.55307 2374 b147740a80a9603c73976206e1823736 "pdflatex" - "main.bbl" 1759176018.84906 3654 cb7bb2c7072cb5aea3ed65a8abe6024a "bibtex main" - "main.tex" 1759167577.47323 233 3d97c672204e438a9f988ea9deb7d374 "" + "dane_proposal_format.cls" 1759861808.72975 2553 3bbf169a90a50515ed103fe388c111f0 "" + "goals-and-outcomes/v6.tex" 1759870860.65316 6132 978a430623148b07dc06f1fa9ce4a2e0 "" + "main.aux" 1759870879.38834 2371 0b7e48a03f45dbd09ec32422fa17b1e2 "pdflatex" + "main.bbl" 1759870878.65533 3654 cb7bb2c7072cb5aea3ed65a8abe6024a "bibtex main" + "main.tex" 1759870875.8503 233 b14d908b969b3e0790528a34f9ae8ceb "" "research-approach/v2.tex" 1758557109.9037 13747 97ad683c7942f87218a074a6187782d1 "" "state-of-the-art/v2.tex" 1757962977.69875 10918 a65147e24336b6a318bf18223339313e "" (generated) diff --git a/Writing/ERLM/main.fls b/Writing/ERLM/main.fls index a2573082c..4288ca742 100644 --- a/Writing/ERLM/main.fls +++ b/Writing/ERLM/main.fls @@ -401,19 +401,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/ptmr7t.vf INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm -INPUT ./goals-and-outcomes/v4.tex -INPUT ./goals-and-outcomes/v4.tex -INPUT ./goals-and-outcomes/v4.tex -INPUT ./goals-and-outcomes/v4.tex -INPUT goals-and-outcomes/v4.tex +INPUT ./goals-and-outcomes/v6.tex +INPUT ./goals-and-outcomes/v6.tex +INPUT ./goals-and-outcomes/v6.tex +INPUT ./goals-and-outcomes/v6.tex +INPUT goals-and-outcomes/v6.tex INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmb7t.vf INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb8r.tfm INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmr7t.vf INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmri7t.vf -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri8r.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 @@ -437,6 +434,7 @@ INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm +INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm @@ -449,6 +447,7 @@ INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmr10.tfm INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/zptmcm7m.vf INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/psyro.tfm INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmmi10.tfm +INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri8r.tfm INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/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 @@ -457,16 +456,17 @@ 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 /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmr8c.vf 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 diff --git a/Writing/ERLM/main.log b/Writing/ERLM/main.log index 380f6dffb..1188a3b9e 100644 --- a/Writing/ERLM/main.log +++ b/Writing/ERLM/main.log @@ -1,4 +1,4 @@ -This is pdfTeX, Version 3.141592653-2.6-1.40.25 (TeX Live 2023/Debian) (preloaded format=pdflatex 2024.9.10) 29 SEP 2025 16:00 +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 entering extended mode restricted \write18 enabled. file:line:error style messages enabled. @@ -799,15 +799,15 @@ LaTeX Font Info: ... okay on input line 3. * layout: * layoutoffset:(h,v)=(0.0pt,0.0pt) * modes: -* h-part:(L,W,R)=(144.54pt, 325.21501pt, 144.54pt) -* v-part:(T,H,B)=(144.54pt, 505.89pt, 144.54pt) +* h-part:(L,W,R)=(72.26999pt, 469.75502pt, 72.26999pt) +* v-part:(T,H,B)=(72.26999pt, 650.43001pt, 72.26999pt) * \paperwidth=614.295pt * \paperheight=794.96999pt -* \textwidth=325.21501pt -* \textheight=505.89pt -* \oddsidemargin=72.27pt -* \evensidemargin=72.27pt -* \topmargin=35.27pt +* \textwidth=469.75502pt +* \textheight=650.43001pt +* \oddsidemargin=0.0pt +* \evensidemargin=0.0pt +* \topmargin=-37.0pt * \headheight=12.0pt * \headsep=25.0pt * \topskip=12.0pt @@ -876,172 +876,23 @@ 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/v4.tex [1] -Overfull \hbox (5.84927pt too wide) in paragraph at lines 69--79 -[]\OT1/ptm/b/n/12 Develop and ver-ify for-mal char-ac-ter-i-za-tions of hy-brid mode - [] - - -Overfull \hbox (6.71216pt too wide) in paragraph at lines 69--79 -\OT1/ptm/m/n/12 mat-i-cal frame-works dis-tin-guish-ing tran-si-tory modes with reach- - [] - - -Overfull \hbox (2.73976pt too wide) in paragraph at lines 69--79 -\OT1/ptm/m/n/12 clas-si-cal con-trol the-ory will es-tab-lish sta-bil-ity and per-for-mance - [] - -[2] -Overfull \hbox (4.01187pt too wide) in paragraph at lines 82--90 -\OT1/ptm/b/n/12 se-quences. \OT1/ptm/m/n/12 By syn-the-siz-ing dis-crete con-troller tran-si-tions from - [] - -) (./state-of-the-art/v2.tex [3] +{/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 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. 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. 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. - -Overfull \hbox (10.74564pt too wide) in paragraph at lines 31--45 -\OT1/ptm/m/n/12 punov func-tions re-mains chal-leng-ing. Sta-bil-ity con-di-tions for switched - [] - -[4] -Overfull \hbox (0.72525pt too wide) in paragraph at lines 60--68 -\OT1/ptm/m/n/12 state dimension---current meth-ods re-main lim-ited to 6-8 di-men-sional - [] - - -Overfull \hbox (2.70512pt too wide) in paragraph at lines 60--68 -\OT1/ptm/m/n/12 approximations that be-come in-creas-ingly pes-simistic with each mode - [] - - -Overfull \hbox (3.5701pt too wide) in paragraph at lines 69--78 -\OT1/ptm/m/n/12 for 7-dimensional au-tonomous rac-ing sys-tems [5]. This break-through - [] - -[5] -Overfull \hbox (26.09029pt too wide) detected at line 104 -[]\OT1/cmss/m/n/12 G\OT1/ztmcm/m/n/12 ([] \OMS/ztmcm/m/n/12 ! \OT1/cmss/m/n/12 X\OT1/ztmcm/m/n/12 ([] \OMS/ztmcm/m/n/12 ^ \OT1/ztmcm/m/n/12 (\OMS/ztmcm/m/n/12 :[] \OT1/cmss/m/n/12 U []\OT1/ztmcm/m/n/12 ))) - [] - - -Overfull \hbox (2.39413pt too wide) in paragraph at lines 106--119 -\OT1/ptm/m/n/12 tions, they can be checked us-ing com-pu-ta-tional tools. Cyber-physical - [] - - -Overfull \hbox (0.23428pt too wide) in paragraph at lines 106--119 -\OT1/ptm/m/n/12 graphs with con-tin-u-ous dy-nam-ics. Hy-brid au-tomata bridge program- - [] - - -Overfull \hbox (9.89316pt too wide) in paragraph at lines 106--119 -\OT1/ptm/m/n/12 analysis tech-niques to hy-brid sys-tems with in-fi-nite state spaces through - [] - - -Overfull \hbox (4.67361pt too wide) in paragraph at lines 126--132 -\OT1/ptm/m/n/12 nat-u-ral lan-guage and math-e-mat-i-cal spec-i-fi-ca-tions through FRETish--- - [] - - -Overfull \hbox (5.88588pt too wide) in paragraph at lines 126--132 -\OT1/ptm/m/n/12 with ver-i-fi-ca-tion tools like Co-CoSim, and run-time mon-i-tor-ing through - [] - -[6] -Overfull \hbox (14.64534pt too wide) in paragraph at lines 133--140 -\OT1/ptm/m/n/12 cally gen-er-ate con-trollers. The Re-ac-tive Syn-the-sis Com-pe-ti-tion (SYNT- - [] - + [2] [3] LaTeX Font Info: Trying to load font information for TS1+ptm on input line 168. -(/usr/share/texlive/texmf-dist/tex/latex/psnfss/ts1ptm.fd + (/usr/share/texlive/texmf-dist/tex/latex/psnfss/ts1ptm.fd File: ts1ptm.fd 2001/06/04 font definitions for TS1/ptm. -) [7]) (./research-approach/v2.tex -Overfull \hbox (1.40666pt too wide) in paragraph at lines 188--1 -[]\OT1/ptm/m/n/12 The state of the art re-veals a field in tran-si-tion. Tra-di-tional bound- +)) (./research-approach/v2.tex [4] +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. [] - -Overfull \hbox (13.91393pt too wide) in paragraph at lines 188--1 -\OT1/ptm/m/n/12 aries be-tween con-trol the-ory and for-mal meth-ods are dis-solv-ing through - [] - - -Overfull \hbox (15.72511pt too wide) in paragraph at lines 188--1 -\OT1/ptm/m/n/12 fun-da-men-tal chal-lenges remain---particularly scal-a-bil-ity and the theory- - [] - - -Overfull \hbox (0.72522pt too wide) in paragraph at lines 13--16 -[]\OT1/ptm/m/n/12 Develop con-tin-u-ous con-trollers to op-er-ate be-tween modes, and - [] - - -Overfull \hbox (24.65291pt too wide) in paragraph at lines 21--21 -|[]\OT1/ptm/b/n/12 Requirements: $\OT1/ztmcm/m/n/12 (\OML/ztmcm/m/it/12 Procedures \OMS/ztmcm/m/n/12 ^ \OML/ztmcm/m/it/12 FRET\OT1/ztmcm/m/n/12 ) \OMS/ztmcm/m/n/12 ! \OML/ztmcm/m/it/12 TemporalSpecifications$| - [] - -[8] [9] -Overfull \hbox (2.02168pt too wide) in paragraph at lines 89--96 -\OT1/ptm/m/n/12 hu-man decision-making el-e-ments of re-ac-tor op-er-a-tion by im-ple-ment- - [] - -[10] -Overfull \hbox (1.1066pt too wide) in paragraph at lines 119--128 -[]\OT1/ptm/m/n/12 Correctness of the switch-ing con-troller is paramount to this work. - [] - - -Overfull \hbox (59.43591pt too wide) in paragraph at lines 130--130 -|[]$\OT1/ztmcm/m/n/12 (\OML/ztmcm/m/it/12 DiscreteAutomata \OMS/ztmcm/m/n/12 ^ \OML/ztmcm/m/it/12 ControlTheory \OMS/ztmcm/m/n/12 ^ \OML/ztmcm/m/it/12 Reachability\OT1/ztmcm/m/n/12 ) \OMS/ztmcm/m/n/12 ! \OML/ztmcm/m/it/12 ContinuousModes$| - [] - -[11] -Overfull \hbox (6.13612pt too wide) in paragraph at lines 164--171 -\OT1/ptm/m/n/12 the sys-tem to-ward a sta-bi-liz-ing steady-state mode. These modes - [] - -[12] -Overfull \hbox (12.49698pt too wide) in paragraph at lines 197--216 -\OT1/ptm/m/n/12 em-ploy three main tech-niques: reach-a-bil-ity anal-y-sis, assume-guarantee - [] - -) (./broader-impacts/v1.tex -Overfull \hbox (4.61438pt too wide) in paragraph at lines 225--1 -\OT1/ptm/m/n/12 sys-tem de-sign by bridg-ing for-mal meth-ods and con-trol the-ory through - [] - - -Overfull \hbox (2.7176pt too wide) in paragraph at lines 225--1 -\OT1/ptm/m/n/12 fully au-tonomous sys-tem with higher re-li-a-bil-ity than human-operated - [] - -[13] [14] -Overfull \hbox (11.7537pt too wide) in paragraph at lines 25--37 -\OT1/ptm/m/n/12 cost chal-lenge through im-ple-men-ta-tions of high-assurance au-tonomous - [] - - -Overfull \hbox (2.23761pt too wide) in paragraph at lines 52--63 -\OT1/ptm/m/n/12 Nu-clear Reg-u-la-tory Com-mis-sion cer-ti-fi-ca-tion re-quires ex-ten-sive doc- - [] - - -Overfull \hbox (10.28976pt too wide) in paragraph at lines 52--63 -\OT1/ptm/m/n/12 u-men-ta-tion of con-trol pro-ce-dures, op-er-a-tional re-quire-ments, and safety - [] - -[15]) [16] (./main.bbl -Underfull \hbox (badness 4391) in paragraph at lines 34--37 -[]\OT1/ptm/m/n/12 Rajeev Alur, Costas Cour-cou-betis, Nico-las Halb-wachs, - [] - -[17]) [18] (./main.aux) +[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> @@ -1050,16 +901,16 @@ L3 programming layer <2024-01-22> Here is how much of TeX's memory you used: 25428 strings out of 476182 528199 string characters out of 5795595 - 1931975 words of memory out of 5000000 + 1935975 words of memory out of 5000000 46870 multiletter control sequences out of 15000+600000 590786 words of font info for 108 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 -Output written on main.pdf (19 pages, 128398 bytes). +Output written on main.pdf (12 pages, 124660 bytes). PDF statistics: - 134 PDF objects out of 1000 (max. 8388607) - 80 compressed objects within 1 object stream + 111 PDF objects out of 1000 (max. 8388607) + 64 compressed objects within 1 object stream 0 named destinations out of 1000 (max. 500000) 109 words of extra memory for PDF output out of 10000 (max. 10000000) diff --git a/Writing/ERLM/main.pdf b/Writing/ERLM/main.pdf index 94d8cbb8e..ffcbbf118 100644 Binary files a/Writing/ERLM/main.pdf and b/Writing/ERLM/main.pdf differ diff --git a/Writing/ERLM/main.synctex.gz b/Writing/ERLM/main.synctex.gz index bac65634e..dab9a27a9 100644 Binary files a/Writing/ERLM/main.synctex.gz and b/Writing/ERLM/main.synctex.gz differ diff --git a/Writing/ERLM/main.tex b/Writing/ERLM/main.tex index 842c93455..a6978d007 100644 --- a/Writing/ERLM/main.tex +++ b/Writing/ERLM/main.tex @@ -3,7 +3,7 @@ \begin{document} \maketitle -\input{goals-and-outcomes/v4} +\input{goals-and-outcomes/v6} \input{state-of-the-art/v2} \input{research-approach/v2} \input{broader-impacts/v1}