diff --git a/.task/backlog.data b/.task/backlog.data index 91489e748..b9eb53b3e 100644 --- a/.task/backlog.data +++ b/.task/backlog.data @@ -357,3 +357,8 @@ {"description":"ERLM proposal due","due":"20251206T050000Z","entry":"20251202T131547Z","modified":"20251202T132329Z","project":"ERLM","status":"pending","uuid":"f6968367-96f1-4ce2-8691-e45423e27456","tags":["writing"],"depends":["0888fdb8-f5cd-4374-a589-b7b3c1bbd472","0d921ea2-6211-4cd8-bbc4-4f9bf36794d3","14fee599-fe0f-4773-90fc-c5f78291f425","29cc8c63-1fb7-4523-9953-603467b929ee","2a8e9294-aecc-434a-b5dd-a468baf8f4a8","5ba3929b-5ec3-4c9d-b30e-30fd8fe20b54","689420d6-7191-42b6-b691-94ad39c8e0dd","9ce7d23c-0f56-49af-b97d-a684966cfbae","a4c027fa-f50d-4efc-ab61-5b8054810a80","d1fa2409-2f2f-4855-81be-14ee617df5d2","e354ab0c-cef7-41e2-bfb4-d98886e512b7"]} {"description":"Review and edit Goals and Outcomes section","due":"20251205T050000Z","entry":"20251202T132235Z","modified":"20251202T152712Z","project":"ERLM","start":"20251202T152712Z","status":"pending","uuid":"0888fdb8-f5cd-4374-a589-b7b3c1bbd472","tags":["editing"]} {"description":"Review and edit State of the Art section","due":"20251205T050000Z","entry":"20251202T132235Z","modified":"20251203T211706Z","project":"ERLM","start":"20251203T211706Z","status":"pending","uuid":"0d921ea2-6211-4cd8-bbc4-4f9bf36794d3","tags":["editing"]} +{"description":"Review and edit State of the Art section","due":"20251205T050000Z","end":"20251205T225952Z","entry":"20251202T132235Z","modified":"20251205T225952Z","project":"ERLM","status":"completed","uuid":"0d921ea2-6211-4cd8-bbc4-4f9bf36794d3","tags":["editing"]} +{"description":"Review and edit Research Approach section","due":"20251205T050000Z","entry":"20251202T132235Z","modified":"20251205T230823Z","project":"ERLM","start":"20251205T230823Z","status":"pending","uuid":"9ce7d23c-0f56-49af-b97d-a684966cfbae","tags":["editing"]} +{"description":"Review and edit Goals and Outcomes section","due":"20251205T050000Z","end":"20251206T004937Z","entry":"20251202T132235Z","modified":"20251206T004937Z","project":"ERLM","status":"completed","uuid":"0888fdb8-f5cd-4374-a589-b7b3c1bbd472","tags":["editing"]} +{"description":"Review and edit Research Approach section","due":"20251205T050000Z","end":"20251206T004937Z","entry":"20251202T132235Z","modified":"20251206T004937Z","project":"ERLM","status":"completed","uuid":"9ce7d23c-0f56-49af-b97d-a684966cfbae","tags":["editing"]} +{"description":"Review and edit Metrics of Success section","due":"20251205T050000Z","entry":"20251202T132235Z","modified":"20251206T004956Z","project":"ERLM","start":"20251206T004956Z","status":"pending","uuid":"29cc8c63-1fb7-4523-9953-603467b929ee","tags":["editing"]} diff --git a/.task/completed.data b/.task/completed.data index 09816b0e4..26b3e0306 100644 --- a/.task/completed.data +++ b/.task/completed.data @@ -1,3 +1,6 @@ +[description:"Review and edit Goals and Outcomes section" due:"1764910800" end:"1764982177" entry:"1764681755" modified:"1764982177" project:"ERLM" status:"completed" tags:"editing" tags_editing:"x" uuid:"0888fdb8-f5cd-4374-a589-b7b3c1bbd472"] +[description:"Review and edit Research Approach section" due:"1764910800" end:"1764982177" entry:"1764681755" modified:"1764982177" project:"ERLM" status:"completed" tags:"editing" tags_editing:"x" uuid:"9ce7d23c-0f56-49af-b97d-a684966cfbae"] +[description:"Review and edit State of the Art section" due:"1764910800" end:"1764975592" entry:"1764681755" modified:"1764975592" project:"ERLM" status:"completed" tags:"editing" tags_editing:"x" uuid:"0d921ea2-6211-4cd8-bbc4-4f9bf36794d3"] [description:"Get information from FSAE about job placements and a couple sentences about their value for the website" due:"1764738000" end:"1764681587" entry:"1763750758" modified:"1764681590" project:"Chair-Search" status:"deleted" uuid:"fb997f7c-c3d8-4f3c-b02c-f6d55cc9b1c8"] [description:"Make list of tasks for contact about student groups" due:"1764133200" end:"1764681551" entry:"1763750783" modified:"1764681551" project:"Chair-Search" status:"completed" uuid:"0addf099-132c-41af-90d8-19f5f9a9c832"] [description:"Draft Presentations" due:"1763787540" end:"1764681215" entry:"1762886561" modified:"1764681215" project:"ERLM" status:"completed" uuid:"aa7dde10-50d7-4e92-8732-e9f97e049fd9"] diff --git a/.task/pending.data b/.task/pending.data index 03e407d88..5f7c78964 100644 --- a/.task/pending.data +++ b/.task/pending.data @@ -67,10 +67,7 @@ [description:"Reach out to SOAR for job placement info and website content" due:"1764824400" entry:"1764681551" modified:"1764681551" project:"Chair-Search" status:"pending" uuid:"535c2ffc-f233-46f0-ac33-a93cbfd12f81"] [description:"Reach out to Material Advantage for job placement info and website content" due:"1764824400" entry:"1764681551" modified:"1764681551" project:"Chair-Search" status:"pending" uuid:"00072514-5622-4a44-9826-49690be83767"] [description:"Reach out to FSAE for job placement info and website content" due:"1764824400" entry:"1764681551" modified:"1764681551" project:"Chair-Search" status:"pending" uuid:"ca5f0450-483f-4a93-aba1-d06e71b4df5c"] -[description:"Review and edit Goals and Outcomes section" due:"1764910800" entry:"1764681755" modified:"1764689232" project:"ERLM" start:"1764689232" status:"pending" tags:"editing" tags_editing:"x" uuid:"0888fdb8-f5cd-4374-a589-b7b3c1bbd472"] -[description:"Review and edit State of the Art section" due:"1764910800" entry:"1764681755" modified:"1764796626" project:"ERLM" start:"1764796626" status:"pending" tags:"editing" tags_editing:"x" uuid:"0d921ea2-6211-4cd8-bbc4-4f9bf36794d3"] -[description:"Review and edit Research Approach section" due:"1764910800" entry:"1764681755" modified:"1764681755" project:"ERLM" status:"pending" tags:"editing" tags_editing:"x" uuid:"9ce7d23c-0f56-49af-b97d-a684966cfbae"] -[description:"Review and edit Metrics of Success section" due:"1764910800" entry:"1764681755" modified:"1764681755" project:"ERLM" status:"pending" tags:"editing" tags_editing:"x" uuid:"29cc8c63-1fb7-4523-9953-603467b929ee"] +[description:"Review and edit Metrics of Success section" due:"1764910800" entry:"1764681755" modified:"1764982196" project:"ERLM" start:"1764982196" status:"pending" tags:"editing" tags_editing:"x" uuid:"29cc8c63-1fb7-4523-9953-603467b929ee"] [description:"Review and edit Risks and Contingencies section" due:"1764910800" entry:"1764681755" modified:"1764681755" project:"ERLM" status:"pending" tags:"editing" tags_editing:"x" uuid:"e354ab0c-cef7-41e2-bfb4-d98886e512b7"] [description:"Review and edit Broader Impacts section" due:"1764910800" entry:"1764681756" modified:"1764681756" project:"ERLM" status:"pending" tags:"editing" tags_editing:"x" uuid:"d1fa2409-2f2f-4855-81be-14ee617df5d2"] [description:"Review and edit Budget section" due:"1764910800" entry:"1764681756" modified:"1764681756" project:"ERLM" status:"pending" tags:"editing" tags_editing:"x" uuid:"689420d6-7191-42b6-b691-94ad39c8e0dd"] diff --git a/.task/undo.data b/.task/undo.data index a2ad08eca..9956d277d 100644 --- a/.task/undo.data +++ b/.task/undo.data @@ -1274,3 +1274,23 @@ time 1764796626 old [description:"Review and edit State of the Art section" due:"1764910800" entry:"1764681755" modified:"1764681755" project:"ERLM" status:"pending" tags:"editing" tags_editing:"x" uuid:"0d921ea2-6211-4cd8-bbc4-4f9bf36794d3"] new [description:"Review and edit State of the Art section" due:"1764910800" entry:"1764681755" modified:"1764796626" project:"ERLM" start:"1764796626" status:"pending" tags:"editing" tags_editing:"x" uuid:"0d921ea2-6211-4cd8-bbc4-4f9bf36794d3"] --- +time 1764975592 +old [description:"Review and edit State of the Art section" due:"1764910800" entry:"1764681755" modified:"1764796626" project:"ERLM" start:"1764796626" status:"pending" tags:"editing" tags_editing:"x" uuid:"0d921ea2-6211-4cd8-bbc4-4f9bf36794d3"] +new [description:"Review and edit State of the Art section" due:"1764910800" end:"1764975592" entry:"1764681755" modified:"1764975592" project:"ERLM" status:"completed" tags:"editing" tags_editing:"x" uuid:"0d921ea2-6211-4cd8-bbc4-4f9bf36794d3"] +--- +time 1764976103 +old [description:"Review and edit Research Approach section" due:"1764910800" entry:"1764681755" modified:"1764681755" project:"ERLM" status:"pending" tags:"editing" tags_editing:"x" uuid:"9ce7d23c-0f56-49af-b97d-a684966cfbae"] +new [description:"Review and edit Research Approach section" due:"1764910800" entry:"1764681755" modified:"1764976103" project:"ERLM" start:"1764976103" status:"pending" tags:"editing" tags_editing:"x" uuid:"9ce7d23c-0f56-49af-b97d-a684966cfbae"] +--- +time 1764982177 +old [description:"Review and edit Goals and Outcomes section" due:"1764910800" entry:"1764681755" modified:"1764689232" project:"ERLM" start:"1764689232" status:"pending" tags:"editing" tags_editing:"x" uuid:"0888fdb8-f5cd-4374-a589-b7b3c1bbd472"] +new [description:"Review and edit Goals and Outcomes section" due:"1764910800" end:"1764982177" entry:"1764681755" modified:"1764982177" project:"ERLM" status:"completed" tags:"editing" tags_editing:"x" uuid:"0888fdb8-f5cd-4374-a589-b7b3c1bbd472"] +--- +time 1764982177 +old [description:"Review and edit Research Approach section" due:"1764910800" entry:"1764681755" modified:"1764976103" project:"ERLM" start:"1764976103" status:"pending" tags:"editing" tags_editing:"x" uuid:"9ce7d23c-0f56-49af-b97d-a684966cfbae"] +new [description:"Review and edit Research Approach section" due:"1764910800" end:"1764982177" entry:"1764681755" modified:"1764982177" project:"ERLM" status:"completed" tags:"editing" tags_editing:"x" uuid:"9ce7d23c-0f56-49af-b97d-a684966cfbae"] +--- +time 1764982196 +old [description:"Review and edit Metrics of Success section" due:"1764910800" entry:"1764681755" modified:"1764681755" project:"ERLM" status:"pending" tags:"editing" tags_editing:"x" uuid:"29cc8c63-1fb7-4523-9953-603467b929ee"] +new [description:"Review and edit Metrics of Success section" due:"1764910800" entry:"1764681755" modified:"1764982196" project:"ERLM" start:"1764982196" status:"pending" tags:"editing" tags_editing:"x" uuid:"29cc8c63-1fb7-4523-9953-603467b929ee"] +--- diff --git a/Writing/ERLM/goals-and-outcomes/research_statement.tex b/Writing/ERLM/1-goals-and-outcomes/research_statement.tex similarity index 100% rename from Writing/ERLM/goals-and-outcomes/research_statement.tex rename to Writing/ERLM/1-goals-and-outcomes/research_statement.tex diff --git a/Writing/ERLM/goals-and-outcomes/v1.tex b/Writing/ERLM/1-goals-and-outcomes/v1.tex similarity index 100% rename from Writing/ERLM/goals-and-outcomes/v1.tex rename to Writing/ERLM/1-goals-and-outcomes/v1.tex diff --git a/Writing/ERLM/goals-and-outcomes/v2.tex b/Writing/ERLM/1-goals-and-outcomes/v2.tex similarity index 100% rename from Writing/ERLM/goals-and-outcomes/v2.tex rename to Writing/ERLM/1-goals-and-outcomes/v2.tex diff --git a/Writing/ERLM/goals-and-outcomes/v3.tex b/Writing/ERLM/1-goals-and-outcomes/v3.tex similarity index 100% rename from Writing/ERLM/goals-and-outcomes/v3.tex rename to Writing/ERLM/1-goals-and-outcomes/v3.tex diff --git a/Writing/ERLM/goals-and-outcomes/v4.tex b/Writing/ERLM/1-goals-and-outcomes/v4.tex similarity index 100% rename from Writing/ERLM/goals-and-outcomes/v4.tex rename to Writing/ERLM/1-goals-and-outcomes/v4.tex diff --git a/Writing/ERLM/goals-and-outcomes/v5.tex b/Writing/ERLM/1-goals-and-outcomes/v5.tex similarity index 100% rename from Writing/ERLM/goals-and-outcomes/v5.tex rename to Writing/ERLM/1-goals-and-outcomes/v5.tex diff --git a/Writing/ERLM/goals-and-outcomes/v6.tex b/Writing/ERLM/1-goals-and-outcomes/v6.tex similarity index 100% rename from Writing/ERLM/goals-and-outcomes/v6.tex rename to Writing/ERLM/1-goals-and-outcomes/v6.tex diff --git a/Writing/ERLM/goals-and-outcomes/v7.tex b/Writing/ERLM/1-goals-and-outcomes/v7.tex similarity index 100% rename from Writing/ERLM/goals-and-outcomes/v7.tex rename to Writing/ERLM/1-goals-and-outcomes/v7.tex diff --git a/Writing/ERLM/state-of-the-art/outline.md b/Writing/ERLM/2-state-of-the-art/outline.md similarity index 100% rename from Writing/ERLM/state-of-the-art/outline.md rename to Writing/ERLM/2-state-of-the-art/outline.md diff --git a/Writing/ERLM/state-of-the-art/v1.tex b/Writing/ERLM/2-state-of-the-art/v1.tex similarity index 100% rename from Writing/ERLM/state-of-the-art/v1.tex rename to Writing/ERLM/2-state-of-the-art/v1.tex diff --git a/Writing/ERLM/state-of-the-art/v2.tex b/Writing/ERLM/2-state-of-the-art/v2.tex similarity index 100% rename from Writing/ERLM/state-of-the-art/v2.tex rename to Writing/ERLM/2-state-of-the-art/v2.tex diff --git a/Writing/ERLM/state-of-the-art/v3.tex b/Writing/ERLM/2-state-of-the-art/v3.tex similarity index 100% rename from Writing/ERLM/state-of-the-art/v3.tex rename to Writing/ERLM/2-state-of-the-art/v3.tex diff --git a/Writing/ERLM/state-of-the-art/v4.tex b/Writing/ERLM/2-state-of-the-art/v4.tex similarity index 100% rename from Writing/ERLM/state-of-the-art/v4.tex rename to Writing/ERLM/2-state-of-the-art/v4.tex diff --git a/Writing/ERLM/state-of-the-art/v5.tex b/Writing/ERLM/2-state-of-the-art/v5.tex similarity index 100% rename from Writing/ERLM/state-of-the-art/v5.tex rename to Writing/ERLM/2-state-of-the-art/v5.tex diff --git a/Writing/ERLM/state-of-the-art/v6.tex b/Writing/ERLM/2-state-of-the-art/v6.tex similarity index 99% rename from Writing/ERLM/state-of-the-art/v6.tex rename to Writing/ERLM/2-state-of-the-art/v6.tex index 91f3af893..495059ff3 100644 --- a/Writing/ERLM/state-of-the-art/v6.tex +++ b/Writing/ERLM/2-state-of-the-art/v6.tex @@ -1,4 +1,3 @@ -\newpage \section{State of the Art and Limits of Current Practice} The principal aim of this research is to create autonomous reactor control diff --git a/Writing/ERLM/research-approach/outline.md b/Writing/ERLM/3-research-approach/outline.md similarity index 100% rename from Writing/ERLM/research-approach/outline.md rename to Writing/ERLM/3-research-approach/outline.md diff --git a/Writing/ERLM/research-approach/v1.tex b/Writing/ERLM/3-research-approach/v1.tex similarity index 100% rename from Writing/ERLM/research-approach/v1.tex rename to Writing/ERLM/3-research-approach/v1.tex diff --git a/Writing/ERLM/research-approach/v2.tex b/Writing/ERLM/3-research-approach/v2.tex similarity index 100% rename from Writing/ERLM/research-approach/v2.tex rename to Writing/ERLM/3-research-approach/v2.tex diff --git a/Writing/ERLM/research-approach/v3.tex b/Writing/ERLM/3-research-approach/v3.tex similarity index 100% rename from Writing/ERLM/research-approach/v3.tex rename to Writing/ERLM/3-research-approach/v3.tex diff --git a/Writing/ERLM/research-approach/v4.tex b/Writing/ERLM/3-research-approach/v4.tex similarity index 60% rename from Writing/ERLM/research-approach/v4.tex rename to Writing/ERLM/3-research-approach/v4.tex index 55b89305c..820e90734 100644 --- a/Writing/ERLM/research-approach/v4.tex +++ b/Writing/ERLM/3-research-approach/v4.tex @@ -1,30 +1,7 @@ -\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 +high-assurance hybrid control systems for critical infrastructure. To build these systems with formal correctness guarantees, we must accomplish three main thrusts: \begin{enumerate} @@ -34,51 +11,26 @@ three main thrusts: \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 + their correctness \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. +power operations remain manually controlled by human operators, but 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. -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 +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~\cite{katis_capture_2022}. 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 @@ -111,12 +63,35 @@ 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. +compatible with reactive synthesis tools. Linear Temporal Logic (LTL) builds +upon modal logic's foundational operators for necessity ($\Box$, ``box'') and +possibility ($\Diamond$, ``diamond''), extending them to reason about temporal +behavior~\cite{baier_principles_2008}. The box operator $\Box$ expresses that a +property holds at all future times (necessarily always), while the diamond +operator $\Diamond$ expresses that a property holds at some future time +(possibly eventually). These are complemented by the next operator ($X$) for the +immediate successor state and the until operator ($U$) for expressing +persistence conditions. -\subsection{$(TemporalLogic \wedge ReactiveSynthesis) \rightarrow -DiscreteAutomata$} +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} + \Box(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 +necessity operator $\Box$ ensures this safety property holds throughout all +possible future system executions, while the next operator $X$ enforces +immediate response. The until operator $U$ maintains the state constraint until +the reset condition occurs. There is no ambiguity on the control in this +scenario because all decisions are represented by discrete variables. +Formulating operating rules using this logic enforces a finite and correct way +of operating. Reactive synthesis is an active research field in computer science focused on generating discrete controllers from temporal logic specifications. The term @@ -135,8 +110,9 @@ 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 +Competition (SYNTCOMP) through efficient parity game solving +algorithms~\cite{meyer_strix_2018,jacobs_reactive_2024}. Strix +translates linear temporal logic specifications into deterministic autom\cite 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 @@ -158,15 +134,30 @@ 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. These systems, called hybrid systems, combine continuous +dynamics (flows) with discrete transitions (jumps). These dynamics can be +formally expressed as~\cite{branicky_multiple_1998}: -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. +\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. The approach described for producing discrete automata yields physics-agnostic specifications that represent only half of a complete hybrid autonomous @@ -211,67 +202,70 @@ on discrete mode transitions: 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. +transitions~\cite{branicky_multiple_1998}. Current techniques struggle with this +problem because dynamic discontinuities complicate +verification~\cite{bansal_hamilton-jacobi_2017,guernic_reachability_2009}. 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. +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~\cite{frehse_spaceex_2011,mitchell_time-dependent_2005}. We will use +reachability to define continuous state ranges at discrete transition boundaries +and verify that requirements are satisfied within continuous modes. +Assume-guarantee contracts will be employed when continuous state boundaries are +not explicitly defined. For any given mode, the input range for reachability +analysis is defined by the output ranges of discrete modes that transition to +it. This compositional approach ensures each continuous controller is prepared +for its possible input range, enabling subsequent reachability analysis without +requiring global system analysis. 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 by ensuring +no system trajectories cross a given barrier. Control barrier functions provide +a method to certify safety by establishing differential inequality conditions +that guarantee forward invariance of safe sets~\cite{prajna_safety_2004}. 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. -\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. +This compositional approach has several advantages. First, this research +approach breaks down the autonomous controller design into smaller chunks. For +designers of future autonomous control systems, the barrier to entry is small, +while milestones in design are clear by the procedural nature of this research +plan. Second, the ability to measure design progress also enables the +measurement of regulatory adherence. Each step in this development procedure +generates an artifact that can be independently evaluated as proof of safety and +performance. Finally, the compositional component of this development plan +enables incremental refinement between control system layers. For example, +difficulty in developing a continuous mode may reflect a discrete automata that +is too restrictive, which in turn may result in refinement of system design +requirements. This synthesis between levels will promote broader understanding +of the autonomous controller. -\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 +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. +Reactor (SmAHTR). 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 diff --git a/Writing/ERLM/metrics-of-success/v1.tex b/Writing/ERLM/4-metrics-of-success/v1.tex similarity index 100% rename from Writing/ERLM/metrics-of-success/v1.tex rename to Writing/ERLM/4-metrics-of-success/v1.tex diff --git a/Writing/ERLM/metrics-of-success/v2.tex b/Writing/ERLM/4-metrics-of-success/v2.tex similarity index 100% rename from Writing/ERLM/metrics-of-success/v2.tex rename to Writing/ERLM/4-metrics-of-success/v2.tex diff --git a/Writing/ERLM/risks-and-contingencies/assumptions.md b/Writing/ERLM/5-risks-and-contingencies/assumptions.md similarity index 100% rename from Writing/ERLM/risks-and-contingencies/assumptions.md rename to Writing/ERLM/5-risks-and-contingencies/assumptions.md diff --git a/Writing/ERLM/risks-and-contingencies/v1.tex b/Writing/ERLM/5-risks-and-contingencies/v1.tex similarity index 100% rename from Writing/ERLM/risks-and-contingencies/v1.tex rename to Writing/ERLM/5-risks-and-contingencies/v1.tex diff --git a/Writing/ERLM/risks-and-contingencies/v2.tex b/Writing/ERLM/5-risks-and-contingencies/v2.tex similarity index 100% rename from Writing/ERLM/risks-and-contingencies/v2.tex rename to Writing/ERLM/5-risks-and-contingencies/v2.tex diff --git a/Writing/ERLM/broader-impacts/v1.tex b/Writing/ERLM/6-broader-impacts/v1.tex similarity index 100% rename from Writing/ERLM/broader-impacts/v1.tex rename to Writing/ERLM/6-broader-impacts/v1.tex diff --git a/Writing/ERLM/broader-impacts/v2.tex b/Writing/ERLM/6-broader-impacts/v2.tex similarity index 100% rename from Writing/ERLM/broader-impacts/v2.tex rename to Writing/ERLM/6-broader-impacts/v2.tex diff --git a/Writing/ERLM/budget/v1.tex b/Writing/ERLM/7-budget/v1.tex similarity index 100% rename from Writing/ERLM/budget/v1.tex rename to Writing/ERLM/7-budget/v1.tex diff --git a/Writing/ERLM/schedule/v1.tex b/Writing/ERLM/8-schedule/v1.tex similarity index 100% rename from Writing/ERLM/schedule/v1.tex rename to Writing/ERLM/8-schedule/v1.tex diff --git a/Writing/ERLM/supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf b/Writing/ERLM/9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf similarity index 100% rename from Writing/ERLM/supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf rename to Writing/ERLM/9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf diff --git a/Writing/ERLM/supplemental-sections/cv-1786798.pdf b/Writing/ERLM/9-supplemental-sections/cv-1786798.pdf similarity index 100% rename from Writing/ERLM/supplemental-sections/cv-1786798.pdf rename to Writing/ERLM/9-supplemental-sections/cv-1786798.pdf diff --git a/Writing/ERLM/supplemental-sections/v1.tex b/Writing/ERLM/9-supplemental-sections/v1.tex similarity index 93% rename from Writing/ERLM/supplemental-sections/v1.tex rename to Writing/ERLM/9-supplemental-sections/v1.tex index 895cbd4db..4fac5e405 100644 --- a/Writing/ERLM/supplemental-sections/v1.tex +++ b/Writing/ERLM/9-supplemental-sections/v1.tex @@ -1,10 +1,10 @@ \section{Supplemental Sections} \subsection{Biosketch} -\includepdf[pages=-]{supplemental-sections/cv-1786798.pdf} +\includepdf[pages=-]{9-supplemental-sections/cv-1786798.pdf} \subsection{Data Management Plan} -\includepdf[pages=-]{supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf} +\includepdf[pages=-]{9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf} \subsection{Facilities} diff --git a/Writing/ERLM/main.aux b/Writing/ERLM/main.aux index 2406b4541..cc2fc6c03 100644 --- a/Writing/ERLM/main.aux +++ b/Writing/ERLM/main.aux @@ -3,9 +3,9 @@ \@writefile{toc}{\contentsline {section}{\numberline {1}Goals and Outcomes}{1}{}\protected@file@percent } \citation{NUREG-0899,10CFR50.34} \citation{10CFR55.59} +\@writefile{toc}{\contentsline {section}{\numberline {2}State of the Art and Limits of Current Practice}{2}{}\protected@file@percent } +\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}Current Reactor Procedures and Operation}{2}{}\protected@file@percent } \citation{WRPS.Description,gentillon_westinghouse_1999} -\@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}{3}{}\protected@file@percent } \citation{operator_statistics} \citation{10CFR55} \citation{10CFR50.54} @@ -13,27 +13,33 @@ \citation{WNA2020} \citation{hogberg_root_2013} \citation{zhang_analysis_2025} +\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Human Factors in Nuclear Accidents}{3}{}\protected@file@percent } +\citation{Kiniry2024} \citation{Kiniry2024} -\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Human Factors in Nuclear Accidents}{4}{}\protected@file@percent } \@writefile{toc}{\contentsline {subsection}{\numberline {2.3}HARDENS and Formal Methods}{4}{}\protected@file@percent } -\citation{Kiniry2024} -\@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 } +\citation{katis_capture_2022} +\@writefile{toc}{\contentsline {section}{\numberline {3}Research Approach}{5}{}\protected@file@percent } +\citation{baier_principles_2008} +\citation{meyer_strix_2018,jacobs_reactive_2024} +\citation{a} +\citation{branicky_multiple_1998} +\citation{branicky_multiple_1998} +\citation{bansal_hamilton-jacobi_2017,guernic_reachability_2009} +\citation{frehse_spaceex_2011,mitchell_time-dependent_2005} +\citation{prajna_safety_2004} \@writefile{toc}{\contentsline {section}{\numberline {4}Metrics for Success}{10}{}\protected@file@percent } -\@writefile{toc}{\contentsline {paragraph}{TRL 3 \textit {Critical Function and Proof of Concept}}{11}{}\protected@file@percent } -\@writefile{toc}{\contentsline {paragraph}{TRL 4 \textit {Laboratory Testing of Integrated Components}}{11}{}\protected@file@percent } +\@writefile{toc}{\contentsline {paragraph}{TRL 3 \textit {Critical Function and Proof of Concept}}{10}{}\protected@file@percent } +\@writefile{toc}{\contentsline {paragraph}{TRL 4 \textit {Laboratory Testing of Integrated Components}}{10}{}\protected@file@percent } \@writefile{toc}{\contentsline {paragraph}{TRL 5 \textit {Laboratory Testing in Relevant Environment}}{11}{}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {5}Risks and Contingencies}{12}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {5}Risks and Contingencies}{11}{}\protected@file@percent } \@writefile{toc}{\contentsline {subsection}{\numberline {5.1}Computational Tractability of Synthesis}{12}{}\protected@file@percent } -\@writefile{toc}{\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{13}{}\protected@file@percent } -\@writefile{toc}{\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{14}{}\protected@file@percent } -\@writefile{toc}{\contentsline {subsection}{\numberline {5.4}Hardware-in-the-Loop Integration Complexity}{15}{}\protected@file@percent } +\@writefile{toc}{\contentsline {subsection}{\numberline {5.2}Discrete-Continuous Interface Formalization}{12}{}\protected@file@percent } +\@writefile{toc}{\contentsline {subsection}{\numberline {5.3}Procedure Formalization Completeness}{13}{}\protected@file@percent } +\@writefile{toc}{\contentsline {subsection}{\numberline {5.4}Hardware-in-the-Loop Integration Complexity}{14}{}\protected@file@percent } \citation{eia_lcoe_2022} \citation{eesi_datacenter_2024} \citation{eia_lcoe_2022} -\@writefile{toc}{\contentsline {section}{\numberline {6}Broader Impacts}{16}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {6}Broader Impacts}{15}{}\protected@file@percent } \bibstyle{ieeetr} \bibdata{references} \bibcite{NUREG-0899}{1} @@ -49,7 +55,19 @@ \bibcite{hogberg_root_2013}{11} \bibcite{zhang_analysis_2025}{12} \bibcite{Kiniry2024}{13} -\@writefile{toc}{\contentsline {section}{References}{18}{}\protected@file@percent } +\bibcite{katis_capture_2022}{14} +\bibcite{baier_principles_2008}{15} +\bibcite{meyer_strix_2018}{16} +\bibcite{jacobs_reactive_2024}{17} +\@writefile{toc}{\contentsline {section}{References}{17}{}\protected@file@percent } +\bibcite{branicky_multiple_1998}{18} +\bibcite{bansal_hamilton-jacobi_2017}{19} +\bibcite{guernic_reachability_2009}{20} +\bibcite{frehse_spaceex_2011}{21} +\bibcite{mitchell_time-dependent_2005}{22} +\bibcite{prajna_safety_2004}{23} +\bibcite{eia_lcoe_2022}{24} +\bibcite{eesi_datacenter_2024}{25} \@writefile{toc}{\contentsline {section}{\numberline {7}Budget and Budget Justification}{19}{}\protected@file@percent } \@writefile{toc}{\contentsline {subsection}{\numberline {7.1}Budget Summary}{19}{}\protected@file@percent } \@writefile{lot}{\contentsline {table}{\numberline {1}{\ignorespaces Proposed Budget by Year and Category}}{19}{}\protected@file@percent } diff --git a/Writing/ERLM/main.bbl b/Writing/ERLM/main.bbl index 3f5a46eaf..e96849844 100644 --- a/Writing/ERLM/main.bbl +++ b/Writing/ERLM/main.bbl @@ -41,4 +41,43 @@ M.~Zhang, L.~Dai, W.~Chen, and E.~Pang, ``Analysis of human errors in nuclear po J.~Kiniry, A.~Bakst, S.~Hansen, M.~Podhradsky, and A.~Bivin, ``High assurance rigorous digital engineering for nuclear safety (hardens) final technical report,'' Tech. Rep. TLR-RES-RES/DE-2024-005, Galois, Inc. / U.S. Nuclear Regulatory Commission, 2024. \newblock NRC Contract 31310021C0014. +\bibitem{katis_capture_2022} +A.~Katis, A.~Mavridou, D.~Giannakopoulou, T.~Pressburger, and J.~Schumann, ``Capture, analyze, diagnose: Realizability checking of requirements in {FRET},'' in {\em Computer Aided Verification} (S.~Shoham and Y.~Vizel, eds.), pp.~490--504, Springer International Publishing. + +\bibitem{baier_principles_2008} +C.~Baier and J.-P. Katoen, {\em Principles of Model Checking}. +\newblock {MIT} Press. + +\bibitem{meyer_strix_2018} +P.~J. Meyer, S.~Sickert, and M.~Luttenberger, ``Strix: Explicit reactive synthesis strikes back!,'' in {\em Computer Aided Verification} (H.~Chockler and G.~Weissenbacher, eds.), pp.~578--586, Springer International Publishing. + +\bibitem{jacobs_reactive_2024} +S.~Jacobs {\em et~al.}, ``The reactive synthesis competition ({SYNTCOMP}): 2018-2021.'' + +\bibitem{branicky_multiple_1998} +M.~Branicky, ``Multiple lyapunov functions and other analysis tools for switched and hybrid systems,'' vol.~43, no.~4, pp.~475--482. + +\bibitem{bansal_hamilton-jacobi_2017} +S.~Bansal, M.~Chen, S.~Herbert, and C.~J. Tomlin, ``Hamilton-jacobi reachability: A brief overview and recent advances,'' in {\em 2017 {IEEE} 56th Annual Conference on Decision and Control ({CDC})}, pp.~2242--2253. + +\bibitem{guernic_reachability_2009} +C.~L. Guernic, ``Reachability analysis of hybrid systems with linear continuous dynamics.'' + +\bibitem{frehse_spaceex_2011} +G.~Frehse, C.~Le~Guernic, A.~Donzé, S.~Cotton, R.~Ray, O.~Lebeltel, R.~Ripado, A.~Girard, T.~Dang, and O.~Maler, ``{SpaceEx}: Scalable verification of hybrid systems,'' in {\em Computer Aided Verification} (G.~Gopalakrishnan and S.~Qadeer, eds.), pp.~379--395, Springer. + +\bibitem{mitchell_time-dependent_2005} +I.~Mitchell, A.~Bayen, and C.~Tomlin, ``A time-dependent hamilton-jacobi formulation of reachable sets for continuous dynamic games,'' vol.~50, no.~7, pp.~947--957. + +\bibitem{prajna_safety_2004} +S.~Prajna and A.~Jadbabaie, ``Safety verification of hybrid systems using barrier certificates,'' in {\em Hybrid Systems: Computation and Control} (R.~Alur and G.~J. Pappas, eds.), pp.~477--492, Springer. + +\bibitem{eia_lcoe_2022} +{U.S. Energy Information Administration}, ``Levelized costs of new generation resources in the annual energy outlook 2022,'' report, U.S. Energy Information Administration, March 2022. +\newblock See Table 1b, page 9. + +\bibitem{eesi_datacenter_2024} +{Environmental and Energy Study Institute}, ``Data center energy needs are upending power grids and threatening the climate.'' Web article, 2024. +\newblock Accessed: 2025-09-29. + \end{thebibliography} diff --git a/Writing/ERLM/main.blg b/Writing/ERLM/main.blg index 7e4046e72..c4e1688e1 100644 --- a/Writing/ERLM/main.blg +++ b/Writing/ERLM/main.blg @@ -9,53 +9,64 @@ Warning--entry type for "operator_statistics" isn't style-file defined --line 45 of file references.bib Warning--entry type for "10CFR50.54" isn't style-file defined --line 59 of file references.bib -Warning--I didn't find a database entry for "eia_lcoe_2022" -Warning--I didn't find a database entry for "eesi_datacenter_2024" +Warning--entry type for "guernic_reachability_2009" isn't style-file defined +--line 221 of file references.bib +Warning--I didn't find a database entry for "a" Warning--empty author in WRPS.Description Warning--empty year in WRPS.Description Warning--empty journal in hogberg_root_2013 Warning--empty year in hogberg_root_2013 Warning--empty journal in zhang_analysis_2025 Warning--empty year in zhang_analysis_2025 -You've used 13 entries, +Warning--empty year in katis_capture_2022 +Warning--empty year in baier_principles_2008 +Warning--empty year in meyer_strix_2018 +Warning--empty journal in branicky_multiple_1998 +Warning--empty year in branicky_multiple_1998 +Warning--empty year in bansal_hamilton-jacobi_2017 +Warning--empty year in frehse_spaceex_2011 +Warning--empty journal in mitchell_time-dependent_2005 +Warning--empty year in mitchell_time-dependent_2005 +Warning--empty year in prajna_safety_2004 +You've used 25 entries, 1876 wiz_defined-function locations, - 544 strings with 5480 characters, -and the built_in function-call counts, 2138 in all, are: -= -- 192 -> -- 92 + 609 strings with 7729 characters, +and the built_in function-call counts, 5612 in all, are: += -- 511 +> -- 249 < -- 2 -+ -- 38 -- -- 25 -* -- 130 -:= -- 326 -add.period$ -- 14 -call.type$ -- 13 -change.case$ -- 15 ++ -- 93 +- -- 68 +* -- 382 +:= -- 798 +add.period$ -- 27 +call.type$ -- 25 +change.case$ -- 27 chr.to.int$ -- 0 -cite$ -- 19 -duplicate$ -- 92 -empty$ -- 229 -format.name$ -- 25 -if$ -- 511 +cite$ -- 41 +duplicate$ -- 260 +empty$ -- 567 +format.name$ -- 68 +if$ -- 1343 int.to.chr$ -- 0 -int.to.str$ -- 13 -missing$ -- 2 -newline$ -- 44 -num.names$ -- 12 -pop$ -- 57 +int.to.str$ -- 25 +missing$ -- 11 +newline$ -- 83 +num.names$ -- 32 +pop$ -- 125 preamble$ -- 1 purify$ -- 0 quote$ -- 0 -skip$ -- 74 +skip$ -- 204 stack$ -- 0 -substring$ -- 44 -swap$ -- 22 +substring$ -- 276 +swap$ -- 86 text.length$ -- 2 text.prefix$ -- 0 top$ -- 0 type$ -- 0 -warning$ -- 6 -while$ -- 16 -width$ -- 15 -write$ -- 107 -(There were 11 warnings) +warning$ -- 16 +while$ -- 53 +width$ -- 27 +write$ -- 210 +(There were 21 warnings) diff --git a/Writing/ERLM/main.fdb_latexmk b/Writing/ERLM/main.fdb_latexmk index 1c5fe408b..e574ac0f5 100644 --- a/Writing/ERLM/main.fdb_latexmk +++ b/Writing/ERLM/main.fdb_latexmk @@ -1,13 +1,13 @@ # Fdb version 4 -["bibtex main"] 1764974760.71217 "main.aux" "main.bbl" "main" 1764975051.10496 0 - "./references.bib" 1764974759.12837 5129 de2dc116e7908a86456f09f33e7d7ac7 "" +["bibtex main"] 1764980933.98858 "main.aux" "main.bbl" "main" 1764982133.83346 0 + "./references.bib" 1764980611.90841 14069 2a4f74c587187a8a71049043171eb0fe "" "/usr/share/texlive/texmf-dist/bibtex/bst/base/ieeetr.bst" 1292289607 18361 1a00e58565e7f19bf2b3e1bfb82254ae "" - "main.aux" 1764975050.94085 7608 f4f0b295bef52d13062032206cc95973 "pdflatex" + "main.aux" 1764982133.67597 7881 be02d2f847fcfd08f6011a189f2fc9cf "pdflatex" (generated) "main.bbl" "main.blg" (rewritten before read) -["pdflatex"] 1764975050.20677 "main.tex" "main.pdf" "main" 1764975051.10514 0 +["pdflatex"] 1764982132.94482 "main.tex" "main.pdf" "main" 1764982133.83364 0 "/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 "" @@ -40,6 +40,7 @@ "/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb" 1248133631 35752 024fb6c41858982481f6968b5fc26508 "" "/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb" 1248133631 32569 5e5ddc8df908dea60932f3c484a54c0d "" "/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt12.pfb" 1248133631 24252 1e4e051947e12dfb50fee0b7f4e26e3a "" + "/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/symbols/msam10.pfb" 1248133631 31764 459c573c03a4949a528c2cc7f557e217 "" "/usr/share/texlive/texmf-dist/fonts/type1/urw/symbol/usyr.pfb" 1136849748 33709 b09d2e140b7e807d3a97058263ab6693 "" "/usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmb8a.pfb" 1136849748 44729 811d6c62865936705a31c797a1d5dada "" "/usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmbi8a.pfb" 1136849748 44656 0cbca70e0534538582128f6b54593cca "" @@ -241,21 +242,21 @@ "/usr/share/texmf/web2c/texmf.cnf" 1707919699 40399 f2c302f7d2af602abb742093540a5834 "" "/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map" 1760105440.02229 5312232 f3296911be9cc021788f3f879cf0a47d "" "/var/lib/texmf/web2c/pdftex/pdflatex.fmt" 1726065868 6800790 607442c924ed54405961d2b8ac2a25ae "" - "broader-impacts/v1.tex" 1762446356.88898 4913 f040011f0dbfa050cad013bb8737b473 "" - "budget/v1.tex" 1762446356.88898 12864 1341c4cfdaf82dc649f2f47f3cc8ecd7 "" + "1-goals-and-outcomes/v6.tex" 1760575541.11104 6070 286ca847b1aac31431e0658cd2989ea2 "" + "2-state-of-the-art/v6.tex" 1764975691.95583 13373 7b26a8331e52f6fdbd3c6203283d61a8 "" + "3-research-approach/v4.tex" 1764982131.29739 17588 1f9490df80ab110e8accd0d34a67ef15 "" + "4-metrics-of-success/v1.tex" 1760575541.11204 6867 9f08b3208bb158042e2fc9bbfeecae68 "" + "5-risks-and-contingencies/v1.tex" 1762446356.89155 15209 c8ff47d0cfbf72d9c457463c5114f2a8 "" + "6-broader-impacts/v1.tex" 1762446356.88898 4913 f040011f0dbfa050cad013bb8737b473 "" + "7-budget/v1.tex" 1762446356.88898 12864 1341c4cfdaf82dc649f2f47f3cc8ecd7 "" + "8-schedule/v1.tex" 1764192995.54631 8440 1c6c59ab8379c2aee45e5ad9b447e61d "" + "9-supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf" 1764192995.54731 76839 d12cfa78304f51e96ce0e12460ece1e3 "" + "9-supplemental-sections/cv-1786798.pdf" 1764192995.54731 31602 224112b9f507ae1e989c0341a7eb3f42 "" + "9-supplemental-sections/v1.tex" 1764975820.90587 2306 2e5bf084cf72f93d80cf9138d1569d6f "" "dane_proposal_format.cls" 1764974397.2375 2570 f29186d8a9397205c58fccc0fcffb76c "" - "goals-and-outcomes/v6.tex" 1760575541.11104 6070 286ca847b1aac31431e0658cd2989ea2 "" - "main.aux" 1764975050.94085 7608 f4f0b295bef52d13062032206cc95973 "pdflatex" - "main.bbl" 1764974760.75697 2467 75ddd8bc744ac1d7c685bc124699a008 "bibtex main" - "main.tex" 1764974466.74023 804 d25a45e5732ab0e63adac220a8893f96 "" - "metrics-of-success/v1.tex" 1760575541.11204 6867 9f08b3208bb158042e2fc9bbfeecae68 "" - "research-approach/v3.tex" 1760575541.11304 17351 6ed3e4ff3c33dd86d80597dbdb0cf36f "" - "risks-and-contingencies/v1.tex" 1762446356.89155 15209 c8ff47d0cfbf72d9c457463c5114f2a8 "" - "schedule/v1.tex" 1764192995.54631 8440 1c6c59ab8379c2aee45e5ad9b447e61d "" - "state-of-the-art/v6.tex" 1764975048.60283 13382 c10ff226a1b21f79fbc41b5ad41d2e48 "" - "supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf" 1764192995.54731 76839 d12cfa78304f51e96ce0e12460ece1e3 "" - "supplemental-sections/cv-1786798.pdf" 1764192995.54731 31602 224112b9f507ae1e989c0341a7eb3f42 "" - "supplemental-sections/v1.tex" 1764192995.54731 2302 accf9c1dd3b7c2f35a3a051140113d63 "" + "main.aux" 1764982133.67597 7881 be02d2f847fcfd08f6011a189f2fc9cf "pdflatex" + "main.bbl" 1764980934.02731 5012 668a266823d48f68a9ac1ddb0c83466e "bibtex main" + "main.tex" 1764979384.78263 822 20061a5e271518c18336f9c3c88b120c "" (generated) "main.aux" "main.log" diff --git a/Writing/ERLM/main.fls b/Writing/ERLM/main.fls index cf3273c79..f16aa88f8 100644 --- a/Writing/ERLM/main.fls +++ b/Writing/ERLM/main.fls @@ -260,311 +260,3 @@ INPUT /usr/share/texlive/texmf-dist/tex/latex/gincltex/gincltex.sty INPUT /usr/share/texlive/texmf-dist/tex/latex/gincltex/gincltex.sty INPUT /usr/share/texlive/texmf-dist/tex/latex/gincltex/gincltex.sty INPUT /usr/share/texlive/texmf-dist/tex/latex/svn-prov/svn-prov.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/svn-prov/svn-prov.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/adjustbox/adjustbox.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/adjustbox/adjustbox.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/adjustbox/adjcalc.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/adjustbox/adjcalc.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/adjustbox/trimclip.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/adjustbox/trimclip.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/collectbox/collectbox.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/collectbox/collectbox.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/adjustbox/tc-pdftex.def -INPUT /usr/share/texlive/texmf-dist/tex/latex/adjustbox/tc-pdftex.def -INPUT /usr/share/texlive/texmf-dist/tex/latex/adjustbox/tc-pdftex.def -INPUT /usr/share/texlive/texmf-dist/tex/latex/ifoddpage/ifoddpage.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/ifoddpage/ifoddpage.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/ifoddpage/ifoddpage.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/varwidth/varwidth.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/varwidth/varwidth.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/varwidth/varwidth.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/filemod/filemod-expmin.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/filemod/filemod-expmin.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/booktabs/booktabs.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/booktabs/booktabs.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/tools/tabularx.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/tools/tabularx.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/tools/array.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/tools/array.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/makecell/makecell.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/makecell/makecell.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/tools/dcolumn.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/tools/dcolumn.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/multirow/multirow.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/multirow/multirow.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/graphics/lscape.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/graphics/lscape.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/enumitem/enumitem.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/enumitem/enumitem.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/listings/listings.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/listings/listings.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/listings/lstmisc.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/listings/lstmisc.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/listings/lstmisc.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/listings/listings.cfg -INPUT /usr/share/texlive/texmf-dist/tex/latex/listings/listings.cfg -INPUT /usr/share/texlive/texmf-dist/tex/latex/listings/listings.cfg -INPUT /usr/share/texlive/texmf-dist/tex/latex/pgfgantt/pgfgantt.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/pgfgantt/pgfgantt.sty -INPUT /usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarybackgrounds.code.tex -INPUT /usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarybackgrounds.code.tex -INPUT /usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarypatterns.code.tex -INPUT /usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarypatterns.code.tex -INPUT /usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/pgflibrarypatterns.code.tex -INPUT /usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/pgflibrarypatterns.code.tex -INPUT /usr/share/texlive/texmf-dist/tex/latex/pgf/utilities/pgfcalendar.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/pgf/utilities/pgfcalendar.sty -INPUT /usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfcalendar.code.tex -INPUT /usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfcalendar.code.tex -INPUT /usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfcalendar.code.tex -INPUT /usr/share/texlive/texmf-dist/tex/latex/colortbl/colortbl.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/colortbl/colortbl.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/graphics/color.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/ot1ptm.fd -INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/ot1ptm.fd -INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/ot1ptm.fd -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm -INPUT /usr/share/texlive/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def -INPUT /usr/share/texlive/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def -INPUT ./main.aux -INPUT ./main.aux -INPUT main.aux -OUTPUT main.aux -INPUT /usr/share/texlive/texmf-dist/tex/latex/fmtcount/fc-english.def -INPUT /usr/share/texlive/texmf-dist/tex/latex/fmtcount/fc-english.def -INPUT /usr/share/texlive/texmf-dist/tex/latex/fmtcount/fc-english.def -INPUT /usr/share/texlive/texmf-dist/tex/context/base/mkii/supp-pdf.mkii -INPUT /usr/share/texlive/texmf-dist/tex/context/base/mkii/supp-pdf.mkii -INPUT /usr/share/texlive/texmf-dist/tex/context/base/mkii/supp-pdf.mkii -INPUT /usr/share/texlive/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg -INPUT /usr/share/texlive/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg -INPUT /usr/share/texlive/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg -INPUT /usr/share/texlive/texmf-dist/tex/latex/pdflscape/pdflscape.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/pdflscape/pdflscape.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/pdflscape/pdflscape-nometadata.sty -INPUT /usr/share/texlive/texmf-dist/tex/latex/pdflscape/pdflscape-nometadata.sty -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/tex/latex/psnfss/ot1ztmcm.fd -INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/ot1ztmcm.fd -INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/ot1ztmcm.fd -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7t.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7t.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7t.tfm -INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/omlztmcm.fd -INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/omlztmcm.fd -INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/omlztmcm.fd -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm -INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/omsztmcm.fd -INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/omsztmcm.fd -INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/omsztmcm.fd -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm -INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/omxztmcm.fd -INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/omxztmcm.fd -INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/omxztmcm.fd -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr7t.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 /var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map -INPUT /usr/share/texlive/texmf-dist/fonts/enc/dvips/base/8r.enc -INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmr7t.vf -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmr7t.vf -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm -INPUT ./goals-and-outcomes/v6.tex -INPUT ./goals-and-outcomes/v6.tex -INPUT ./goals-and-outcomes/v6.tex -INPUT ./goals-and-outcomes/v6.tex -INPUT goals-and-outcomes/v6.tex -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmb7t.vf -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb8r.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/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/v6.tex -INPUT ./state-of-the-art/v6.tex -INPUT ./state-of-the-art/v6.tex -INPUT ./state-of-the-art/v6.tex -INPUT state-of-the-art/v6.tex -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmri7t.vf -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri8r.tfm -INPUT ./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 -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/zptmcm7t.vf -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmr10.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/zptmcm7m.vf -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/psyro.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmmi10.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/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 ./metrics-of-success/v1.tex -INPUT ./metrics-of-success/v1.tex -INPUT ./metrics-of-success/v1.tex -INPUT ./metrics-of-success/v1.tex -INPUT metrics-of-success/v1.tex -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmbi7t.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmbi7t.vf -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmbi8r.tfm -INPUT ./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 ./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 /usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmtt12.tfm -INPUT ./budget/v1.tex -INPUT ./budget/v1.tex -INPUT ./budget/v1.tex -INPUT ./budget/v1.tex -INPUT budget/v1.tex -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7t.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7m.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7y.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/zptmcm7v.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/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/msbm10.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr8c.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/ptmr8c.vf -INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmri7t.vf -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri8r.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb8c.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmb8c.vf -INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri8c.tfm -INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmri8c.vf -INPUT ./schedule/v1.tex -INPUT ./schedule/v1.tex -INPUT ./schedule/v1.tex -INPUT ./schedule/v1.tex -INPUT schedule/v1.tex -INPUT ./supplemental-sections/v1.tex -INPUT ./supplemental-sections/v1.tex -INPUT ./supplemental-sections/v1.tex -INPUT ./supplemental-sections/v1.tex -INPUT supplemental-sections/v1.tex -INPUT ./supplemental-sections/cv-1786798.pdf -INPUT ./supplemental-sections/cv-1786798.pdf -INPUT ./supplemental-sections/cv-1786798.pdf -INPUT ./supplemental-sections/cv-1786798.pdf -INPUT ./supplemental-sections/cv-1786798.pdf -INPUT ./supplemental-sections/cv-1786798.pdf -INPUT ./supplemental-sections/cv-1786798.pdf -INPUT ./supplemental-sections/cv-1786798.pdf -INPUT ./supplemental-sections/cv-1786798.pdf -INPUT ./supplemental-sections/cv-1786798.pdf -INPUT ./supplemental-sections/cv-1786798.pdf -INPUT ./supplemental-sections/cv-1786798.pdf -INPUT ./supplemental-sections/cv-1786798.pdf -INPUT ./supplemental-sections/cv-1786798.pdf -INPUT ./supplemental-sections/cv-1786798.pdf -INPUT ./supplemental-sections/cv-1786798.pdf -INPUT ./supplemental-sections/cv-1786798.pdf -INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf -INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf -INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf -INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf -INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf -INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf -INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf -INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf -INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf -INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf -INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf -INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf -INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf -INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf -INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf -INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf -INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf -INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf -INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf -INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf -INPUT ./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf -INPUT main.aux -INPUT /usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb -INPUT /usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb -INPUT /usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb -INPUT /usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt12.pfb -INPUT /usr/share/texlive/texmf-dist/fonts/type1/urw/symbol/usyr.pfb -INPUT /usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmb8a.pfb -INPUT /usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmbi8a.pfb -INPUT /usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmr8a.pfb -INPUT /usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmri8a.pfb diff --git a/Writing/ERLM/main.log b/Writing/ERLM/main.log index f58c369ec..261b9341d 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.11) 5 DEC 2025 17:50 +This is pdfTeX, Version 3.141592653-2.6-1.40.25 (TeX Live 2023/Debian) (preloaded format=pdflatex 2024.9.11) 5 DEC 2025 19:50 entering extended mode restricted \write18 enabled. file:line:error style messages enabled. @@ -491,576 +491,4 @@ File: tikzlibrarychains.code.tex 2023-01-15 v3.1.10 (3.1.10) \pgfdecoratedinputsegmentremainingdistance=\dimen274 \pgf@decorate@distancetomove=\dimen275 \pgf@decorate@repeatstate=\count321 -\pgfdecorationsegmentamplitude=\dimen276 -\pgfdecorationsegmentlength=\dimen277 -) -\tikz@lib@dec@box=\box86 -) (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/decorations/pgflibrarydecorations.markings.code.tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryshadows.code.tex -File: tikzlibraryshadows.code.tex 2023-01-15 v3.1.10 (3.1.10) - (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibraryfadings.code.tex -File: tikzlibraryfadings.code.tex 2023-01-15 v3.1.10 (3.1.10) - (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/pgflibraryfadings.code.tex -File: pgflibraryfadings.code.tex 2023-01-15 v3.1.10 (3.1.10) -))) (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/pgflibraryarrows.meta.code.tex -File: pgflibraryarrows.meta.code.tex 2023-01-15 v3.1.10 (3.1.10) -\pgfarrowinset=\dimen278 -\pgfarrowlength=\dimen279 -\pgfarrowwidth=\dimen280 -\pgfarrowlinewidth=\dimen281 -) (/usr/share/texlive/texmf-dist/tex/latex/standalone/standalone.sty -Package: standalone 2022/10/10 v1.3b Package to include TeX sub-files with preambles - (/usr/share/texlive/texmf-dist/tex/latex/tools/shellesc.sty -Package: shellesc 2023/07/08 v1.0d unified shell escape interface for LaTeX -Package shellesc Info: Restricted shell escape enabled on input line 77. -) (/usr/share/texlive/texmf-dist/tex/latex/currfile/currfile.sty -Package: currfile 2022/10/10 v0.8 Provides the file path elements of the current input file - (/usr/share/texlive/texmf-dist/tex/latex/kvoptions/kvoptions.sty -Package: kvoptions 2022-06-15 v3.15 Key value format for package options (HO) - (/usr/share/texlive/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty -Package: ltxcmds 2023-12-04 v1.26 LaTeX kernel commands for general use (HO) -) (/usr/share/texlive/texmf-dist/tex/latex/kvsetkeys/kvsetkeys.sty -Package: kvsetkeys 2022-10-05 v1.19 Key value parser (HO) -)) (/usr/share/texlive/texmf-dist/tex/latex/filehook/filehook.sty -Package: filehook 2022/10/25 v0.8b Hooks for input files - (/usr/share/texlive/texmf-dist/tex/latex/filehook/filehook-2020.sty -Package: filehook-2020 2022/10/25 v0.8b Hooks for input files -)) -\c@currfiledepth=\count322 -) (/usr/share/texlive/texmf-dist/tex/latex/gincltex/gincltex.sty (/usr/share/texlive/texmf-dist/tex/latex/svn-prov/svn-prov.sty -Package: svn-prov 2010/04/24 v3.1862 Package Date/Version from SVN Keywords -) -Package: gincltex 2011/09/04 v0.3 Include external LaTeX files like graphics - (/usr/share/texlive/texmf-dist/tex/latex/adjustbox/adjustbox.sty -Package: adjustbox 2022/10/17 v1.3a Adjusting TeX boxes (trim, clip, ...) - (/usr/share/texlive/texmf-dist/tex/latex/adjustbox/adjcalc.sty -Package: adjcalc 2012/05/16 v1.1 Provides advanced setlength with multiple back-ends (calc, etex, pgfmath) -) (/usr/share/texlive/texmf-dist/tex/latex/adjustbox/trimclip.sty -Package: trimclip 2020/08/19 v1.2 Trim and clip general TeX material - (/usr/share/texlive/texmf-dist/tex/latex/collectbox/collectbox.sty -Package: collectbox 2022/10/17 v0.4c Collect macro arguments as boxes -\collectedbox=\box87 -) -\tc@llx=\dimen282 -\tc@lly=\dimen283 -\tc@urx=\dimen284 -\tc@ury=\dimen285 -Package trimclip Info: Using driver 'tc-pdftex.def'. - (/usr/share/texlive/texmf-dist/tex/latex/adjustbox/tc-pdftex.def -File: tc-pdftex.def 2019/01/04 v2.2 Clipping driver for pdftex -)) -\adjbox@Width=\dimen286 -\adjbox@Height=\dimen287 -\adjbox@Depth=\dimen288 -\adjbox@Totalheight=\dimen289 -\adjbox@pwidth=\dimen290 -\adjbox@pheight=\dimen291 -\adjbox@pdepth=\dimen292 -\adjbox@ptotalheight=\dimen293 - (/usr/share/texlive/texmf-dist/tex/latex/ifoddpage/ifoddpage.sty -Package: ifoddpage 2022/10/18 v1.2 Conditionals for odd/even page detection -\c@checkoddpage=\count323 -) -(/usr/share/texlive/texmf-dist/tex/latex/varwidth/varwidth.sty -Package: varwidth 2009/03/30 ver 0.92; Variable-width minipages -\@vwid@box=\box88 -\sift@deathcycles=\count324 -\@vwid@loff=\dimen294 -\@vwid@roff=\dimen295 -)) -\gincltex@box=\box89 -) (/usr/share/texlive/texmf-dist/tex/latex/filemod/filemod-expmin.sty -Package: filemod-expmin 2011/09/19 v1.2 Get and compare file modification times (expandable; minimal) -)) (/usr/share/texlive/texmf-dist/tex/latex/booktabs/booktabs.sty -Package: booktabs 2020/01/12 v1.61803398 Publication quality tables -\heavyrulewidth=\dimen296 -\lightrulewidth=\dimen297 -\cmidrulewidth=\dimen298 -\belowrulesep=\dimen299 -\belowbottomsep=\dimen300 -\aboverulesep=\dimen301 -\abovetopsep=\dimen302 -\cmidrulesep=\dimen303 -\cmidrulekern=\dimen304 -\defaultaddspace=\dimen305 -\@cmidla=\count325 -\@cmidlb=\count326 -\@aboverulesep=\dimen306 -\@belowrulesep=\dimen307 -\@thisruleclass=\count327 -\@lastruleclass=\count328 -\@thisrulewidth=\dimen308 -) (/usr/share/texlive/texmf-dist/tex/latex/tools/tabularx.sty -Package: tabularx 2023/07/08 v2.11c `tabularx' package (DPC) - (/usr/share/texlive/texmf-dist/tex/latex/tools/array.sty -Package: array 2023/10/16 v2.5g Tabular extension package (FMi) -\col@sep=\dimen309 -\ar@mcellbox=\box90 -\extrarowheight=\dimen310 -\NC@list=\toks43 -\extratabsurround=\skip57 -\backup@length=\skip58 -\ar@cellbox=\box91 -) -\TX@col@width=\dimen311 -\TX@old@table=\dimen312 -\TX@old@col=\dimen313 -\TX@target=\dimen314 -\TX@delta=\dimen315 -\TX@cols=\count329 -\TX@ftn=\toks44 -) (/usr/share/texlive/texmf-dist/tex/latex/makecell/makecell.sty -Package: makecell 2009/08/03 V0.1e Managing of Tab Column Heads and Cells -\rotheadsize=\dimen316 -\c@nlinenum=\count330 -\TeXr@lab=\toks45 -) (/usr/share/texlive/texmf-dist/tex/latex/tools/dcolumn.sty -Package: dcolumn 2023/07/08 v1.06 decimal alignment package (DPC) -) (/usr/share/texlive/texmf-dist/tex/latex/multirow/multirow.sty -Package: multirow 2021/03/15 v2.8 Span multiple rows of a table -\multirow@colwidth=\skip59 -\multirow@cntb=\count331 -\multirow@dima=\skip60 -\bigstrutjot=\dimen317 -) (/usr/share/texlive/texmf-dist/tex/latex/graphics/lscape.sty -Package: lscape 2020/05/28 v3.02 Landscape Pages (DPC) -) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty -Package: amsmath 2023/05/13 v2.17o AMS math features -\@mathmargin=\skip61 - -For additional information on amsmath, use the `?' option. -(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty -Package: amstext 2021/08/26 v2.01 AMS text -) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty -Package: amsbsy 1999/11/29 v1.2d Bold Symbols -\pmbraise@=\dimen318 -) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty -Package: amsopn 2022/04/08 v2.04 operator names -) -\inf@bad=\count332 -LaTeX Info: Redefining \frac on input line 234. -\uproot@=\count333 -\leftroot@=\count334 -LaTeX Info: Redefining \overline on input line 399. -LaTeX Info: Redefining \colon on input line 410. -\classnum@=\count335 -\DOTSCASE@=\count336 -LaTeX Info: Redefining \ldots on input line 496. -LaTeX Info: Redefining \dots on input line 499. -LaTeX Info: Redefining \cdots on input line 620. -\Mathstrutbox@=\box92 -\strutbox@=\box93 -LaTeX Info: Redefining \big on input line 722. -LaTeX Info: Redefining \Big on input line 723. -LaTeX Info: Redefining \bigg on input line 724. -LaTeX Info: Redefining \Bigg on input line 725. -\big@size=\dimen319 -LaTeX Font Info: Redeclaring font encoding OML on input line 743. -LaTeX Font Info: Redeclaring font encoding OMS on input line 744. -\macc@depth=\count337 -LaTeX Info: Redefining \bmod on input line 905. -LaTeX Info: Redefining \pmod on input line 910. -LaTeX Info: Redefining \smash on input line 940. -LaTeX Info: Redefining \relbar on input line 970. -LaTeX Info: Redefining \Relbar on input line 971. -\c@MaxMatrixCols=\count338 -\dotsspace@=\muskip17 -\c@parentequation=\count339 -\dspbrk@lvl=\count340 -\tag@help=\toks46 -\row@=\count341 -\column@=\count342 -\maxfields@=\count343 -\andhelp@=\toks47 -\eqnshift@=\dimen320 -\alignsep@=\dimen321 -\tagshift@=\dimen322 -\tagwidth@=\dimen323 -\totwidth@=\dimen324 -\lineht@=\dimen325 -\@envbody=\toks48 -\multlinegap=\skip62 -\multlinetaggap=\skip63 -\mathdisplay@stack=\toks49 -LaTeX Info: Redefining \[ on input line 2953. -LaTeX Info: Redefining \] on input line 2954. -) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty -Package: amssymb 2013/01/14 v3.01 AMS font symbols - (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty -Package: amsfonts 2013/01/14 v3.01 Basic AMSFonts support -\symAMSa=\mathgroup6 -\symAMSb=\mathgroup7 -LaTeX Font Info: Overwriting math alphabet `\mathfrak' in version `bold' -(Font) U/euf/m/n --> U/euf/b/n on input line 106. -)) (/usr/share/texlive/texmf-dist/tex/latex/enumitem/enumitem.sty -Package: enumitem 2019/06/20 v3.9 Customized lists -\labelindent=\skip64 -\enit@outerparindent=\dimen326 -\enit@toks=\toks50 -\enit@inbox=\box94 -\enit@count@id=\count344 -\enitdp@description=\count345 -) (/usr/share/texlive/texmf-dist/tex/latex/listings/listings.sty -\lst@mode=\count346 -\lst@gtempboxa=\box95 -\lst@token=\toks51 -\lst@length=\count347 -\lst@currlwidth=\dimen327 -\lst@column=\count348 -\lst@pos=\count349 -\lst@lostspace=\dimen328 -\lst@width=\dimen329 -\lst@newlines=\count350 -\lst@lineno=\count351 -\lst@maxwidth=\dimen330 - (/usr/share/texlive/texmf-dist/tex/latex/listings/lstmisc.sty -File: lstmisc.sty 2023/02/27 1.9 (Carsten Heinz) -\c@lstnumber=\count352 -\lst@skipnumbers=\count353 -\lst@framebox=\box96 -) (/usr/share/texlive/texmf-dist/tex/latex/listings/listings.cfg -File: listings.cfg 2023/02/27 1.9 listings configuration -)) -Package: listings 2023/02/27 1.9 (Carsten Heinz) - (/usr/share/texlive/texmf-dist/tex/latex/pgfgantt/pgfgantt.sty -Package: pgfgantt 2018/01/10 v5.0 Draw Gantt diagrams with TikZ - (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarybackgrounds.code.tex -File: tikzlibrarybackgrounds.code.tex 2023-01-15 v3.1.10 (3.1.10) -\pgf@layerbox@background=\box97 -\pgf@layerboxsaved@background=\box98 -) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tikzlibrarypatterns.code.tex -File: tikzlibrarypatterns.code.tex 2023-01-15 v3.1.10 (3.1.10) - (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/pgflibrarypatterns.code.tex -File: pgflibrarypatterns.code.tex 2023-01-15 v3.1.10 (3.1.10) -)) (/usr/share/texlive/texmf-dist/tex/latex/pgf/utilities/pgfcalendar.sty (/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfcalendar.code.tex -File: pgfcalendar.code.tex 2023-01-15 v3.1.10 (3.1.10) -\pgfcalendarcurrentjulian=\count354 -\pgf@cal@easter@Y=\count355 -\pgf@cal@easter@G=\count356 -\pgf@cal@easter@C=\count357 -\pgf@cal@easter@X=\count358 -\pgf@cal@easter@Z=\count359 -\pgf@cal@easter@D=\count360 -\pgf@cal@easter@E=\count361 -\pgf@cal@easter@N=\count362 -\pgf@cal@easter@M=\count363 -\pgf@cal@easter@julianday=\count364 -)) -\gtt@currentline=\count365 -\gtt@lasttitleline=\count366 -\gtt@currgrid=\count367 -\gtt@chartwidth=\count368 -\gtt@lasttitleslot=\count369 -\gtt@elementid=\count370 -\gtt@today@slot=\count371 -\gtt@startjulian=\count372 -\gtt@endjulian=\count373 -\gtt@chartid=\count374 -\gtt@vrule@slot=\count375 -\gtt@calendar@slots=\count376 -\gtt@calendar@weeknumber=\count377 -\gtt@calendar@startofweek=\count378 -\gtt@left@slot=\count379 -\gtt@right@slot=\count380 -) -\figurewidth=\skip65 -\figureheight=\skip66 -\c@task=\count381 -) (/usr/share/texlive/texmf-dist/tex/latex/colortbl/colortbl.sty -Package: colortbl 2022/06/20 v1.0f Color table columns (DPC) -\everycr=\toks52 -\minrowclearance=\skip67 -\rownum=\count382 -) -LaTeX Font Info: Trying to load font information for OT1+ptm on input line 10. - (/usr/share/texlive/texmf-dist/tex/latex/psnfss/ot1ptm.fd -File: ot1ptm.fd 2001/06/04 font definitions for OT1/ptm. -) (/usr/share/texlive/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def -File: l3backend-pdftex.def 2024-01-04 L3 backend support: PDF output (pdfTeX) -\l__color_backend_stack_int=\count383 -\l__pdf_internal_box=\box99 -) (./main.aux) -\openout1 = `main.aux'. - -LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 10. -LaTeX Font Info: ... okay on input line 10. -LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 10. -LaTeX Font Info: ... okay on input line 10. -LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 10. -LaTeX Font Info: ... okay on input line 10. -LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 10. -LaTeX Font Info: ... okay on input line 10. -LaTeX Font Info: Checking defaults for TS1/cmr/m/n on input line 10. -LaTeX Font Info: ... okay on input line 10. -LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 10. -LaTeX Font Info: ... okay on input line 10. -LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 10. -LaTeX Font Info: ... okay on input line 10. - -*geometry* driver: auto-detecting -*geometry* detected driver: pdftex -*geometry* verbose mode - [ preamble ] result: -* driver: pdftex -* paper: -* layout: -* layoutoffset:(h,v)=(0.0pt,0.0pt) -* modes: -* 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=469.75502pt -* \textheight=650.43001pt -* \oddsidemargin=0.0pt -* \evensidemargin=0.0pt -* \topmargin=-37.0pt -* \headheight=12.0pt -* \headsep=25.0pt -* \topskip=12.0pt -* \footskip=30.0pt -* \marginparwidth=44.0pt -* \marginparsep=10.0pt -* \columnsep=10.0pt -* \skip\footins=10.8pt plus 4.0pt minus 2.0pt -* \hoffset=0.0pt -* \voffset=0.0pt -* \mag=1000 -* \@twocolumnfalse -* \@twosidefalse -* \@mparswitchfalse -* \@reversemarginfalse -* (1in=72.27pt=25.4mm, 1cm=28.453pt) - -(/usr/share/texlive/texmf-dist/tex/latex/fmtcount/fc-english.def -File: fc-english.def 2016/01/12 -) (/usr/share/texlive/texmf-dist/tex/context/base/mkii/supp-pdf.mkii -[Loading MPS to PDF converter (version 2006.09.02).] -\scratchcounter=\count384 -\scratchdimen=\dimen331 -\scratchbox=\box100 -\nofMPsegments=\count385 -\nofMParguments=\count386 -\everyMPshowfont=\toks53 -\MPscratchCnt=\count387 -\MPscratchDim=\dimen332 -\MPnumerator=\count388 -\makeMPintoPDFobject=\count389 -\everyMPtoPDFconversion=\toks54 -) (/usr/share/texlive/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty -Package: epstopdf-base 2020-01-24 v2.11 Base part for package epstopdf -Package epstopdf-base Info: Redefining graphics rule for `.eps' on input line 485. - (/usr/share/texlive/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg -File: epstopdf-sys.cfg 2010/07/13 v1.3 Configuration of (r)epstopdf for TeX Live -)) (/usr/share/texlive/texmf-dist/tex/latex/pdflscape/pdflscape.sty -Package: pdflscape 2022-10-27 v0.13 Display of landscape pages in PDF - (/usr/share/texlive/texmf-dist/tex/latex/pdflscape/pdflscape-nometadata.sty -Package: pdflscape-nometadata 2022-10-28 v0.13 Display of landscape pages in PDF (HO) -Package pdflscape Info: Auto-detected driver: pdftex on input line 81. -)) -\c@lstlisting=\count390 -LaTeX Font Info: Trying to load font information for OT1+ztmcm on input line 12. - (/usr/share/texlive/texmf-dist/tex/latex/psnfss/ot1ztmcm.fd -File: ot1ztmcm.fd 2000/01/03 Fontinst v1.801 font definitions for OT1/ztmcm. -) -LaTeX Font Info: Trying to load font information for OML+ztmcm on input line 12. - (/usr/share/texlive/texmf-dist/tex/latex/psnfss/omlztmcm.fd -File: omlztmcm.fd 2000/01/03 Fontinst v1.801 font definitions for OML/ztmcm. -) -LaTeX Font Info: Trying to load font information for OMS+ztmcm on input line 12. - (/usr/share/texlive/texmf-dist/tex/latex/psnfss/omsztmcm.fd -File: omsztmcm.fd 2000/01/03 Fontinst v1.801 font definitions for OMS/ztmcm. -) -LaTeX Font Info: Trying to load font information for OMX+ztmcm on input line 12. - (/usr/share/texlive/texmf-dist/tex/latex/psnfss/omxztmcm.fd -File: omxztmcm.fd 2000/01/03 Fontinst v1.801 font definitions for OMX/ztmcm. -) -LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <14.4> not available -(Font) Font shape `OT1/ptm/b/n' tried instead on input line 12. -LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <10.95> not available -(Font) Font shape `OT1/ptm/b/n' tried instead on input line 12. -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 [2] [3] [4]) (./research-approach/v3.tex [5] -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. - [6] [7] [8] [9]) (./metrics-of-success/v1.tex [10] [11]) (./risks-and-contingencies/v1.tex [12] [13] [14]) (./broader-impacts/v1.tex [15] -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. -) - -LaTeX Warning: Citation `eia_lcoe_2022' on page 16 undefined on input line 14. - - -LaTeX Warning: Citation `eesi_datacenter_2024' on page 16 undefined on input line 16. - - -LaTeX Warning: Citation `eia_lcoe_2022' on page 16 undefined on input line 21. - -[16]) [17] (./main.bbl -Underfull \hbox (badness 10000) in paragraph at lines 32--33 -\OT1/cmtt/m/n/12 nuclear . org / information -[] library / safety -[] and -[] security / safety -[] of -[] - [] - -) [18] (./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. - [19] [20] [21] -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 - [] - -) (./schedule/v1.tex [22] -Missing character: There is no , in font nullfont! - -Overfull \hbox (35.80641pt too wide) in paragraph at lines 61--62 - [][] - [] - -[23]) (./supplemental-sections/v1.tex [24] - -File: supplemental-sections/cv-1786798.pdf Graphic file (type pdf) - -Package pdftex.def Info: supplemental-sections/cv-1786798.pdf used on input line 4. -(pdftex.def) Requested size: 614.29349pt x 794.96806pt. -File: supplemental-sections/cv-1786798.pdf Graphic file (type pdf) - -Package pdftex.def Info: supplemental-sections/cv-1786798.pdf used on input line 4. -(pdftex.def) Requested size: 614.29349pt x 794.96806pt. - -File: supplemental-sections/cv-1786798.pdf Graphic file (type pdf) - -Package pdftex.def Info: supplemental-sections/cv-1786798.pdf , page1 used on input line 4. -(pdftex.def) Requested size: 614.29349pt x 794.96806pt. -File: supplemental-sections/cv-1786798.pdf Graphic file (type pdf) - -Package pdftex.def Info: supplemental-sections/cv-1786798.pdf , page1 used on input line 4. -(pdftex.def) Requested size: 614.58406pt x 795.3441pt. - [25] -File: supplemental-sections/cv-1786798.pdf Graphic file (type pdf) - -Package pdftex.def Info: supplemental-sections/cv-1786798.pdf , page1 used on input line 4. -(pdftex.def) Requested size: 614.58406pt x 795.3441pt. -File: supplemental-sections/cv-1786798.pdf Graphic file (type pdf) - -Package pdftex.def Info: supplemental-sections/cv-1786798.pdf , page1 used on input line 4. -(pdftex.def) Requested size: 614.58406pt x 795.3441pt. -File: supplemental-sections/cv-1786798.pdf Graphic file (type pdf) - -Package pdftex.def Info: supplemental-sections/cv-1786798.pdf , page1 used on input line 4. -(pdftex.def) Requested size: 614.58406pt x 795.3441pt. - [26 - - <./supplemental-sections/cv-1786798.pdf>] - -File: supplemental-sections/cv-1786798.pdf Graphic file (type pdf) - -Package pdftex.def Info: supplemental-sections/cv-1786798.pdf , page2 used on input line 4. -(pdftex.def) Requested size: 614.58406pt x 795.3441pt. -File: supplemental-sections/cv-1786798.pdf Graphic file (type pdf) - -Package pdftex.def Info: supplemental-sections/cv-1786798.pdf , page2 used on input line 4. -(pdftex.def) Requested size: 614.58406pt x 795.3441pt. -File: supplemental-sections/cv-1786798.pdf Graphic file (type pdf) - -Package pdftex.def Info: supplemental-sections/cv-1786798.pdf , page2 used on input line 4. -(pdftex.def) Requested size: 614.58406pt x 795.3441pt. - [27 - - <./supplemental-sections/cv-1786798.pdf>] - -File: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf Graphic file (type pdf) - -Package pdftex.def Info: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf used on input line 7. -(pdftex.def) Requested size: 614.29349pt x 794.96806pt. -File: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf Graphic file (type pdf) - -Package pdftex.def Info: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf used on input line 7. -(pdftex.def) Requested size: 614.29349pt x 794.96806pt. - -File: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf Graphic file (type pdf) - -Package pdftex.def Info: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf , page1 used on input line 7. -(pdftex.def) Requested size: 614.29349pt x 794.96806pt. -File: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf Graphic file (type pdf) - -Package pdftex.def Info: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf , page1 used on input line 7. -(pdftex.def) Requested size: 614.58406pt x 795.3441pt. - [28] -File: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf Graphic file (type pdf) - -Package pdftex.def Info: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf , page1 used on input line 7. -(pdftex.def) Requested size: 614.58406pt x 795.3441pt. -File: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf Graphic file (type pdf) - -Package pdftex.def Info: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf , page1 used on input line 7. -(pdftex.def) Requested size: 614.58406pt x 795.3441pt. -File: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf Graphic file (type pdf) - -Package pdftex.def Info: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf , page1 used on input line 7. -(pdftex.def) Requested size: 614.58406pt x 795.3441pt. - [29 - - <./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf>] - -File: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf Graphic file (type pdf) - -Package pdftex.def Info: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf , page2 used on input line 7. -(pdftex.def) Requested size: 614.58406pt x 795.3441pt. -File: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf Graphic file (type pdf) - -Package pdftex.def Info: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf , page2 used on input line 7. -(pdftex.def) Requested size: 614.58406pt x 795.3441pt. -File: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf Graphic file (type pdf) - -Package pdftex.def Info: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf , page2 used on input line 7. -(pdftex.def) Requested size: 614.58406pt x 795.3441pt. - [30 - - <./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf>] - -File: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf Graphic file (type pdf) - -Package pdftex.def Info: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf , page3 used on input line 7. -(pdftex.def) Requested size: 614.58406pt x 795.3441pt. -File: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf Graphic file (type pdf) - -Package pdftex.def Info: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf , page3 used on input line 7. -(pdftex.def) Requested size: 614.58406pt x 795.3441pt. -File: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf Graphic file (type pdf) - -Package pdftex.def Info: supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf , page3 used on input line 7. -(pdftex.def) Requested size: 614.58406pt x 795.3441pt. - [31 - - <./supplemental-sections/High_Assurance_Autonomous_Control_Systems.pdf>]) [32] (./main.aux) - *********** -LaTeX2e <2023-11-01> patch level 1 -L3 programming layer <2024-01-22> - *********** - - -LaTeX Warning: There were undefined references. - - ) -Here is how much of TeX's memory you used: - 26056 strings out of 476182 - 542834 string characters out of 5795595 - 1947975 words of memory out of 5000000 - 47475 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 - -Output written on main.pdf (33 pages, 254858 bytes). -PDF statistics: - 225 PDF objects out of 1000 (max. 8388607) - 133 compressed objects within 2 object streams - 0 named destinations out of 1000 (max. 500000) - 164 words of extra memory for PDF output out of 10000 (max. 10000000) - +\pgfdecorationsegmentamplitude=\ \ No newline at end of file diff --git a/Writing/ERLM/main.pdf b/Writing/ERLM/main.pdf index 0a1affeb4..3b29eec81 100644 Binary files a/Writing/ERLM/main.pdf and b/Writing/ERLM/main.pdf differ diff --git a/Writing/ERLM/main.synctex(busy) b/Writing/ERLM/main.synctex(busy) new file mode 100644 index 000000000..e69de29bb diff --git a/Writing/ERLM/main.synctex.gz b/Writing/ERLM/main.synctex.gz index 3033ea37f..720c528b8 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 821a98998..d0de01f43 100644 --- a/Writing/ERLM/main.tex +++ b/Writing/ERLM/main.tex @@ -10,19 +10,19 @@ \begin{document} \maketitle -\input{goals-and-outcomes/v6} -\input{state-of-the-art/v6} -\input{research-approach/v3} -\input{metrics-of-success/v1} -\input{risks-and-contingencies/v1} -\input{broader-impacts/v1} +\input{1-goals-and-outcomes/v7} +\input{2-state-of-the-art/v6} +\input{3-research-approach/v4} +\input{4-metrics-of-success/v2} +\input{5-risks-and-contingencies/v1} +\input{6-broader-impacts/v1} \newpage \bibliographystyle{ieeetr} \bibliography{references} \newpage -\input{budget/v1} -\input{schedule/v1} -\input{supplemental-sections/v1} +\input{7-budget/v1} +\input{8-schedule/v1} +\input{9-supplemental-sections/v1} % White Paper diff --git a/Writing/ERLM/references.bib b/Writing/ERLM/references.bib index b898de9c9..b932bd60e 100644 --- a/Writing/ERLM/references.bib +++ b/Writing/ERLM/references.bib @@ -122,3 +122,190 @@ Publisher: Idaho National Engineering and Environmental Laboratory}, number = {TLR-RES-RES/DE-2024-005}, note = {NRC Contract 31310021C0014} } + +@techreport{eia_lcoe_2022, + author = {{U.S. Energy Information Administration}}, + title = {Levelized Costs of New Generation Resources in the Annual Energy Outlook 2022}, + institution = {U.S. Energy Information Administration}, + year = {2022}, + month = {March}, + type = {Report}, + url = {https://www.eia.gov/outlooks/aeo/pdf/electricity_generation.pdf}, + note = {See Table 1b, page 9} +} + +@misc{eesi_datacenter_2024, + author = {{Environmental and Energy Study Institute}}, + title = {Data Center Energy Needs Are Upending Power Grids and Threatening the Climate}, + howpublished = {Web article}, + year = {2024}, + url = {https://www.eesi.org/articles/view/data-center-energy-needs-are-upending-power-grids-and-threatening-the-climate}, + note = {Accessed: 2025-09-29} +} + +@book{baier_principles_2008, + location = {Cambridge, {MA}, {USA}}, + title = {Principles of Model Checking}, + isbn = {978-0-262-02649-9}, + abstract = {A comprehensive introduction to the foundations of model checking, a fully automated technique for finding flaws in hardware and software; with extensive examples and both practical and theoretical exercises.}, + pagetotal = {984}, + publisher = {{MIT} Press}, + author = {Baier, Christel and Katoen, Joost-Pieter}, + date = {2008-04-25}, + langid = {english}, +} + +@inproceedings{katis_capture_2022, + location = {Cham}, + title = {Capture, Analyze, Diagnose: Realizability Checking Of Requirements in {FRET}}, + isbn = {978-3-031-13188-2}, + doi = {10.1007/978-3-031-13188-2_24}, + shorttitle = {Capture, Analyze, Diagnose}, + pages = {490--504}, + booktitle = {Computer Aided Verification}, + publisher = {Springer International Publishing}, + author = {Katis, Andreas and Mavridou, Anastasia and Giannakopoulou, Dimitra and Pressburger, Thomas and Schumann, Johann}, + editor = {Shoham, Sharon and Vizel, Yakir}, + date = {2022}, + langid = {english}, + file = {Full Text PDF:/home/danesabo/Zotero/storage/3JPVH8U2/Katis et al. - 2022 - Capture, Analyze, Diagnose Realizability Checking Of Requirements in FRET.pdf:application/pdf}, +} + +@inproceedings{meyer_strix_2018, + location = {Cham}, + title = {Strix: Explicit Reactive Synthesis Strikes Back!}, + isbn = {978-3-319-96145-3}, + doi = {10.1007/978-3-319-96145-3_31}, + shorttitle = {Strix}, + pages = {578--586}, + booktitle = {Computer Aided Verification}, + publisher = {Springer International Publishing}, + author = {Meyer, Philipp J. and Sickert, Salomon and Luttenberger, Michael}, + editor = {Chockler, Hana and Weissenbacher, Georg}, + date = {2018}, + langid = {english}, +} + +@misc{jacobs_reactive_2024, + title = {The Reactive Synthesis Competition ({SYNTCOMP}): 2018-2021}, + url = {http://arxiv.org/abs/2206.00251}, + doi = {10.48550/arXiv.2206.00251}, + shorttitle = {The Reactive Synthesis Competition ({SYNTCOMP})}, + number = {{arXiv}:2206.00251}, + publisher = {{arXiv}}, + author = {Jacobs, Swen and others}, + urldate = {2025-12-06}, + date = {2024-05-06}, + eprinttype = {arxiv}, + eprint = {2206.00251 [cs]}, + keywords = {Computer Science - Logic in Computer Science}, + file = {Preprint PDF:/home/danesabo/Zotero/storage/GU6W5UH4/Jacobs et al. - 2024 - The Reactive Synthesis Competition (SYNTCOMP) 2018-2021.pdf:application/pdf;Snapshot:/home/danesabo/Zotero/storage/57UPK6A5/2206.html:text/html}, +} + +@article{branicky_multiple_1998, + title = {Multiple Lyapunov functions and other analysis tools for switched and hybrid systems}, + volume = {43}, + issn = {1558-2523}, + url = {https://ieeexplore.ieee.org/document/664150}, + doi = {10.1109/9.664150}, + pages = {475--482}, + number = {4}, + journaltitle = {{IEEE} Transactions on Automatic Control}, + author = {Branicky, M.S.}, + urldate = {2025-09-10}, + date = {1998-04}, + keywords = {Automata, Control systems, Difference equations, Differential equations, Lagrangian functions, Limit-cycles, Lyapunov method, Stability analysis, Switched systems, Switches}, + file = {PDF:/home/danesabo/Zotero/storage/5AQWDPAA/Branicky - 1998 - Multiple Lyapunov functions and other analysis tools for switched and hybrid systems.pdf:application/pdf}, +} + +@thesis{guernic_reachability_2009, + title = {Reachability Analysis of Hybrid Systems with Linear Continuous Dynamics}, + url = {https://theses.hal.science/tel-00422569}, + institution = {Université Joseph-Fourier - Grenoble I}, + type = {phdthesis}, + author = {Guernic, Colas Le}, + urldate = {2025-09-14}, + date = {2009-10-28}, + langid = {english}, + file = {Full Text PDF:/home/danesabo/Zotero/storage/A5XNTDZ9/Guernic - 2009 - Reachability Analysis of Hybrid Systems with Linear Continuous Dynamics.pdf:application/pdf}, +} + +@inproceedings{alur_hybrid_1993, + location = {Berlin, Heidelberg}, + title = {Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems}, + isbn = {978-3-540-48060-0}, + doi = {10.1007/3-540-57318-6_30}, + shorttitle = {Hybrid automata}, + pages = {209--229}, + booktitle = {Hybrid Systems}, + publisher = {Springer}, + author = {Alur, Rajeev and Courcoubetis, Costas and Henzinger, Thomas A. and Ho, Pei -Hsin}, + editor = {Grossman, Robert L. and Nerode, Anil and Ravn, Anders P. and Rischel, Hans}, + date = {1993}, + langid = {english}, + keywords = {Acceptance Condition, Hybrid Automaton, Hybrid System, Mutual Exclusion, Reachability Problem}, + file = {Full Text PDF:/home/danesabo/Zotero/storage/WBXYUC86/Alur et al. - 1993 - Hybrid automata An algorithmic approach to the specification and verification of hybrid systems.pdf:application/pdf}, +} + +@article{mitchell_time-dependent_2005, + title = {A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games}, + volume = {50}, + issn = {1558-2523}, + url = {https://ieeexplore.ieee.org/abstract/document/1463302}, + doi = {10.1109/TAC.2005.851439}, + pages = {947--957}, + number = {7}, + journaltitle = {{IEEE} Transactions on Automatic Control}, + author = {Mitchell, I.M. and Bayen, A.M. and Tomlin, C.J.}, + urldate = {2025-09-15}, + date = {2005-07}, + keywords = {Aircraft, Collaborative software, Collision avoidance, Computational modeling, Differential games, Hamilton–Jacobi equations, Nonlinear equations, Nonlinear systems, Partial differential equations, reachability, Trajectory, Vehicle dynamics, verification, Viscosity}, + file = {Snapshot:/home/danesabo/Zotero/storage/SLKV9PEI/1463302.html:text/html;Submitted Version:/home/danesabo/Zotero/storage/9YWL2UDH/Mitchell et al. - 2005 - A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games.pdf:application/pdf}, +} + +@inproceedings{frehse_spaceex_2011, + location = {Berlin, Heidelberg}, + title = {{SpaceEx}: Scalable Verification of Hybrid Systems}, + isbn = {978-3-642-22110-1}, + doi = {10.1007/978-3-642-22110-1_30}, + shorttitle = {{SpaceEx}}, + pages = {379--395}, + booktitle = {Computer Aided Verification}, + publisher = {Springer}, + author = {Frehse, Goran and Le Guernic, Colas and Donzé, Alexandre and Cotton, Scott and Ray, Rajarshi and Lebeltel, Olivier and Ripado, Rodolfo and Girard, Antoine and Dang, Thao and Maler, Oded}, + editor = {Gopalakrishnan, Ganesh and Qadeer, Shaz}, + date = {2011}, + langid = {english}, + keywords = {Hybrid Automaton, Hybrid System, Reachability Analysis, Reachable State, Support Function}, + file = {Full Text PDF:/home/danesabo/Zotero/storage/LPQK8GY2/Frehse et al. - 2011 - SpaceEx Scalable Verification of Hybrid Systems.pdf:application/pdf}, +} + +@inproceedings{bansal_hamilton-jacobi_2017, + title = {Hamilton-Jacobi reachability: A brief overview and recent advances}, + url = {https://ieeexplore.ieee.org/abstract/document/8263977}, + doi = {10.1109/CDC.2017.8263977}, + shorttitle = {Hamilton-Jacobi reachability}, + eventtitle = {2017 {IEEE} 56th Annual Conference on Decision and Control ({CDC})}, + pages = {2242--2253}, + booktitle = {2017 {IEEE} 56th Annual Conference on Decision and Control ({CDC})}, + author = {Bansal, Somil and Chen, Mo and Herbert, Sylvia and Tomlin, Claire J.}, + urldate = {2025-09-15}, + date = {2017-12}, + keywords = {Aircraft, Games, Level set, Safety, Tools, Trajectory, Tutorials}, + file = {Snapshot:/home/danesabo/Zotero/storage/EEK5IE93/8263977.html:text/html;Submitted Version:/home/danesabo/Zotero/storage/BMNLZ9DW/Bansal et al. - 2017 - Hamilton-Jacobi reachability A brief overview and recent advances.pdf:application/pdf}, +} + +@inproceedings{prajna_safety_2004, + location = {Berlin, Heidelberg}, + title = {Safety Verification of Hybrid Systems Using Barrier Certificates}, + isbn = {978-3-540-24743-2}, + doi = {10.1007/978-3-540-24743-2_32}, + pages = {477--492}, + booktitle = {Hybrid Systems: Computation and Control}, + publisher = {Springer}, + author = {Prajna, Stephen and Jadbabaie, Ali}, + editor = {Alur, Rajeev and Pappas, George J.}, + date = {2004}, + langid = {english}, + keywords = {Continuous State, Discrete Transition, Hybrid System, Integral Constraint, Reachability Analysis}, +}