Auto sync: 2025-10-07 17:10:58 (10 files changed)
M Writing/ERLM/dane_proposal_format.cls A Writing/ERLM/goals-and-outcomes/v5.tex A Writing/ERLM/goals-and-outcomes/v6.tex M Writing/ERLM/main.aux M Writing/ERLM/main.fdb_latexmk M Writing/ERLM/main.fls M Writing/ERLM/main.log M Writing/ERLM/main.pdf
This commit is contained in:
parent
178e658b6b
commit
6676851ddf
@ -7,7 +7,7 @@
|
||||
|
||||
% Core packages
|
||||
\RequirePackage[utf8]{inputenc}
|
||||
\RequirePackage[margin=2in]{geometry}
|
||||
\RequirePackage[margin=1in]{geometry}
|
||||
\RequirePackage[hyphens]{url}
|
||||
|
||||
% Font selection (NSF compliant)
|
||||
|
||||
130
Writing/ERLM/goals-and-outcomes/v5.tex
Normal file
130
Writing/ERLM/goals-and-outcomes/v5.tex
Normal file
@ -0,0 +1,130 @@
|
||||
\section{Goals and Outcomes}
|
||||
|
||||
The goal of this research is to create a methodology for building high assurance
|
||||
hybrid autonomous control systems.
|
||||
|
||||
%FIRST PARAGRAPH - INTRO HOOK
|
||||
Commercial control systems for nuclear power have been stuck in the past, far
|
||||
behind the state of the art of controls.
|
||||
% 3-5 SENTENCES KNOWN INFO
|
||||
Nuclear power control systems are extremely high assurance system, where
|
||||
failures are intolerable. A control failure in nuclear power has a broader
|
||||
impact than financial losses. Instead, a failure can create extensive economic
|
||||
losses for the power utility, interruptions for local customers, or in the worst
|
||||
case, radiological release in the local environment. Because of this, control of
|
||||
nuclear power is performed by operators who are extensively trained, use
|
||||
detailed operating procedures, and follow strict requirements.
|
||||
% GAP
|
||||
This method of control has been reliable, but is woefully behind the
|
||||
capabilities of modern less critical control systems, and by relying on human
|
||||
operators, prevents the introduction of autonomy.
|
||||
% CRITICAL NEED
|
||||
To bring nuclear power control into the 21st century, we need a way to develop
|
||||
autonomous control systems that have strict guarantees and assurance of their
|
||||
correct behavior across their operating range.
|
||||
|
||||
% SECOND PARAGRAPH - APPROACH SOLUTION
|
||||
To do this, we will blend tools from computer science and formal methods with
|
||||
those from engineering and control theory to build high assurance hybrid systems
|
||||
to perform autonomous control.
|
||||
% RATIONALE
|
||||
Hybrids systems have switching behavior, where discrete transitions between
|
||||
continuous dynamics occur. Verification of these systems is difficult because of
|
||||
these transitions. We will address this difficulty by building autonomous hybrid
|
||||
control systems that are correct by construction. We will synthesize the
|
||||
discrete mode switching behavior from written operating procedures, while
|
||||
utilizing reachability analysis and assume-guarantee contracts to prove that
|
||||
continuous modes behave correctly.
|
||||
% HYPOTHESIS PAY-OFF/IMPACT
|
||||
If we are successful in creating a hybrid control system that is correct by
|
||||
construction, we can implement autonomous control systems in nuclear power with
|
||||
a great assurance of their safety and performance. Autonomous control is a
|
||||
technology that is desperately needed for the future of nuclear power. Nuclear
|
||||
plant designs such as small modular reactors or microcreactors have been
|
||||
suggested as a way to reduce the enormous capital costs of nuclear power
|
||||
construction, but are limited in their feasibility by the increased cost of
|
||||
operator staffing per megawatt generated. If we can reduce the quantity of
|
||||
operaters needed in these reactors, we can reduce the cost of generating clean
|
||||
nuclear power and address increasing energy demands.
|
||||
% QUALIFICATIONS
|
||||
This work is also situated in the University of Pittsburgh Cyber Energy Center.
|
||||
This research is colocated with collaboration across the energy industry and
|
||||
benefits from having access to industry-ready control hardware from Emerson.
|
||||
The accessibility to industry this research has will ensure that solutions and
|
||||
capabilities generated are aligned with industry needs.
|
||||
|
||||
If this research is successful, we will be able to do the following:
|
||||
\begin{enumerate}
|
||||
% OUTCOME PARAGRAPH 1 TITLE
|
||||
\item \textbf{ Synthesize written operating procedures into discrete automata.
|
||||
}
|
||||
% STRATEGY
|
||||
Discrete automata are the backbone of a continuous hybrid system. These
|
||||
automata control the swtiching behavior between continuous modes, and are
|
||||
directly analogous to operators changing between control laws. The automated
|
||||
creation of these automata is a mature field called reactive synthesis.
|
||||
Reactive synthesis is enabled by specifying logical requriements of a
|
||||
discrete system. These requirements will be created from current written
|
||||
operating procedures directly, through an intermediate tool called FRET,
|
||||
which uses a natural-language-like format called FRETish to embed
|
||||
requirements.
|
||||
% OUTCOME
|
||||
By using written operating procedures to create the discrete automata, we
|
||||
will provide a means for control systems engineers to create discrete
|
||||
switching behavior without having to become logical experts. This reduces
|
||||
the barrier to entry for using formal methods tools, making high assurance
|
||||
switching mechanisms easier to attain.
|
||||
|
||||
% OUTCOME PARAGRAPH 2
|
||||
% TITLE
|
||||
\item \textbf{
|
||||
Build hybrid systems using correct by construction principles.
|
||||
}
|
||||
% STRATEGY
|
||||
In addition to the discrete system, hybrid systems use continuous modes
|
||||
between discrete transitions. These continuous modes will be constructed
|
||||
using standard control theory practices, but will use formal methods to
|
||||
ensure their correctness. Because the discrete modes and their transitions
|
||||
will already be specified from operating requirements, the continuous modes
|
||||
will be examined to ensure that only allowable state transitions can be
|
||||
reached.
|
||||
% OUTCOME
|
||||
This way, controls engineers can build continuous modes exactly as they
|
||||
would before, but iterate on their designs to ensure broader system
|
||||
correctness.
|
||||
|
||||
% OUTCOME PARAGRAPH 3 TITLE
|
||||
\item \textbf{ Create autonomous control systems with strict safety
|
||||
guarantees. }
|
||||
% STRATEGY
|
||||
By combining the discrete and continuous components while building proof of
|
||||
their correctness along the way, we can translate these capabilities into
|
||||
realizable autonomous systems for nuclear power. We will use the methodology
|
||||
presented in this proposal to build a candidate control system using a
|
||||
simulation of a small modular reactor in combination with an Emerson Ovation
|
||||
control system.
|
||||
% OUTCOME
|
||||
By realizing an autonomous hybrid control system using this methodology, we
|
||||
will generate evidence that autonomous hybrid control can be realized in the
|
||||
nuclear industry with current controls equipment.
|
||||
|
||||
|
||||
\end{enumerate}
|
||||
|
||||
% THIRD PARAGRAPH - IMPACT
|
||||
% INNOVATION
|
||||
The innovation in this work is the implementation of different formal methods
|
||||
technologies for the purpose of building hybrid control systems. These
|
||||
technologies will allow us to build hybrid systems with behavior we can ensure.
|
||||
% OUTCOME IMPACT
|
||||
The way that these technologies will be implemented is also designed to incur
|
||||
the smallest amount of cost possible for possible recreation in industry.
|
||||
Controls engineers should be able to find this work approachable, and
|
||||
implementable in new nuclear technology control systems.
|
||||
% GENERAL IMPACT
|
||||
New control systems, especially autonomous control, are critical to advancing
|
||||
the prevalence of nuclear power. Small modular reactors stand to answer the next
|
||||
energy generation challenge in the United States, but must address the
|
||||
significant operating cost required by current staffing limits. This work will
|
||||
allow new reactors to reduce the amount of operators required and improve the
|
||||
economic feasibility of new reactor designs.
|
||||
118
Writing/ERLM/goals-and-outcomes/v6.tex
Normal file
118
Writing/ERLM/goals-and-outcomes/v6.tex
Normal file
@ -0,0 +1,118 @@
|
||||
\section{Goals and Outcomes}
|
||||
|
||||
% GOAL PARAGRAPH
|
||||
The goal of this research is to develop a methodology for creating autonomous
|
||||
hybrid control systems with mathematical guarantees of safe and correct
|
||||
behavior.
|
||||
|
||||
% INTRODUCTORY PARAGRAPH Hook
|
||||
Nuclear power plants require the highest levels of control system reliability,
|
||||
where failures can result in significant economic losses, service interruptions,
|
||||
or radiological release.
|
||||
% Known information
|
||||
Currently, nuclear plant operations rely on extensively trained human operators
|
||||
who follow detailed written procedures and strict regulatory requirements to
|
||||
manage reactor control. These operators make critical decisions about when to
|
||||
switch between different control modes— such as transitioning from startup
|
||||
heating to power operation—based on their interpretation of plant conditions and
|
||||
procedural guidance.
|
||||
% Gap
|
||||
However, this reliance on human operators prevents the introduction of
|
||||
autonomous control capabilities and creates a fundamental economic challenge for
|
||||
next-generation reactor designs. Emerging technologies like small modular
|
||||
reactors face significantly higher per-megawatt staffing costs than conventional
|
||||
plants, threatening their economic viability.
|
||||
% Critical Need
|
||||
What is needed is a way to create autonomous control systems that can safely
|
||||
manage complex operational sequences with the same level of assurance as
|
||||
human-operated systems, but without requiring constant human supervision.
|
||||
|
||||
% APPROACH PARAGRAPH Solution
|
||||
To address this need, we will combine formal methods from computer science with
|
||||
control theory to build hybrid control systems that are correct by construction.
|
||||
% Rationale
|
||||
Hybrid systems use discrete logic to switch between continuous control modes,
|
||||
similar to how operators change control strategies. Existing formal methods can
|
||||
generate provably correct switching logic from written requirements, but they
|
||||
cannot handle the continuous dynamics that occur during transitions between
|
||||
modes. Meanwhile, traditional control theory can verify continuous behavior but
|
||||
lacks tools for proving correctness of discrete switching decisions.
|
||||
% Hypothesis
|
||||
By synthesizing discrete mode transitions directly from written operating
|
||||
procedures and verifying continuous behavior between transitions, we can create
|
||||
hybrid control systems with end-to-end correctness guarantees. If we can
|
||||
formalize existing procedures into logical specifications and verify that
|
||||
continuous dynamics satisfy transition requirements, then we can build
|
||||
autonomous controllers that are provably free from design defects.
|
||||
% Pay-off
|
||||
This approach will enable autonomous control in nuclear power plants while
|
||||
maintaining the high safety standards required by the industry.
|
||||
% Qualifications
|
||||
This work is conducted within the University of Pittsburgh Cyber Energy Center,
|
||||
which provides access to industry collaboration and Emerson control hardware,
|
||||
ensuring that solutions developed are aligned with practical implementation
|
||||
requirements.
|
||||
|
||||
% OUTCOMES PARAGRAPHS
|
||||
If this research is successful, we will be able to do the following:
|
||||
|
||||
\begin{enumerate}
|
||||
|
||||
% OUTCOME 1 Title
|
||||
\item \textbf{Translate written procedures into verified control logic.}
|
||||
% Strategy
|
||||
We will develop a methodology for converting existing written operating
|
||||
procedures into formal specifications that can be automatically synthesized
|
||||
into discrete control logic. This process will use structured intermediate
|
||||
representations to bridge natural language procedures and mathematical
|
||||
logic.
|
||||
% Outcome
|
||||
Control system engineers will be able to generate verified mode-switching
|
||||
controllers directly from regulatory procedures without requiring expertise
|
||||
in formal methods, reducing the barrier to creating high-assurance control
|
||||
systems.
|
||||
|
||||
% OUTCOME 2 Title
|
||||
\item \textbf{Verify continuous control behavior across mode transitions.}
|
||||
% Strategy
|
||||
We will establish methods for analyzing continuous control modes to ensure
|
||||
they satisfy the discrete transition requirements. Using a combination of
|
||||
classical control theory for linear systems and reachability analysis for
|
||||
nonlinear dynamics, we will verify that each continuous mode can safely
|
||||
reach its intended transitions.
|
||||
% Outcome
|
||||
Engineers will be able to design continuous controllers using standard
|
||||
practices while iterating to ensure broader system correctness, proving that
|
||||
mode transitions occur safely and at the right times.
|
||||
|
||||
% OUTCOME 3 Title
|
||||
\item \textbf{Demonstrate autonomous reactor startup control with safety
|
||||
guarantees.}
|
||||
% Strategy
|
||||
We will apply this methodology to develop an autonomous controller for
|
||||
nuclear reactor startup procedures, implementing it on a small modular
|
||||
reactor simulation using industry-standard control hardware. This
|
||||
demonstration will prove correctness across multiple coordinated control
|
||||
modes from cold shutdown through criticality to power operation.
|
||||
% Outcome
|
||||
We will provide evidence that autonomous hybrid control can be realized in
|
||||
the nuclear industry with current control equipment, establishing a path
|
||||
toward reducing operator staffing requirements while maintaining safety.
|
||||
|
||||
\end{enumerate}
|
||||
|
||||
% IMPACT PARAGRAPH Innovation
|
||||
The innovation in this work is the unification of discrete synthesis and
|
||||
continuous verification to enable end-to-end correctness guarantees for hybrid
|
||||
systems.
|
||||
% Outcome Impact
|
||||
If successful, control engineers will be able to create autonomous controllers
|
||||
from existing procedures with mathematical proof of correct behavior, making
|
||||
high-assurance autonomous control practical for safety-critical applications.
|
||||
% Impact/Pay-off
|
||||
This capability is essential for the economic viability of next-generation
|
||||
nuclear power. Small modular reactors represent a promising solution to growing
|
||||
energy demands, but their success depends on reducing per-megawatt operating
|
||||
costs through increased autonomy. This research will provide the tools to
|
||||
achieve that autonomy while maintaining the exceptional safety record required
|
||||
by the nuclear industry.
|
||||
@ -2,27 +2,27 @@
|
||||
\bibstyle{unsrt}
|
||||
\providecommand \oddpage@label [2]{}
|
||||
\@writefile{toc}{\contentsline {section}{\numberline {1}Goals and Outcomes}{1}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {section}{\numberline {2}State of the Art and Limits of Current Practice}{3}{}\protected@file@percent }
|
||||
\citation{geromel2006stability}
|
||||
\citation{branicky1998multiple,liberzon2003switching}
|
||||
\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}Control Theory and Hybrid Systems}{4}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {section}{\numberline {2}State of the Art and Limits of Current Practice}{2}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}Control Theory and Hybrid Systems}{2}{}\protected@file@percent }
|
||||
\citation{mitchell2005time}
|
||||
\citation{yang2024learning}
|
||||
\citation{alur1993hybrid}
|
||||
\citation{alur1995algorithmic}
|
||||
\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Formal Methods and Reactive Synthesis}{3}{}\protected@file@percent }
|
||||
\citation{giannakopoulou2022fret}
|
||||
\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Formal Methods and Reactive Synthesis}{6}{}\protected@file@percent }
|
||||
\citation{meyer2018strix,jacobs2017syntcomp}
|
||||
\citation{platzer2008differential,platzer2017complete}
|
||||
\citation{fulton2015keymaera}
|
||||
\@writefile{toc}{\contentsline {section}{\numberline {3}Research Approach}{8}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}Requirements: $(Procedures \wedge FRET) \rightarrow Temporal Specifications$}{9}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {subsection}{\numberline {3.2}Discrete Synthesis: $(TemporalLogic \wedge ReactiveSynthesis) \rightarrow DiscreteAutomata$}{10}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {subsection}{\numberline {3.3}$(DiscreteAutomata \wedge ControlTheory \wedge Reachability) \rightarrow ContinuousModes$}{11}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {section}{\numberline {3}Research Approach}{5}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}Requirements: $(Procedures \wedge FRET) \rightarrow Temporal Specifications$}{5}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {subsection}{\numberline {3.2}Discrete Synthesis: $(TemporalLogic \wedge ReactiveSynthesis) \rightarrow DiscreteAutomata$}{6}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {subsection}{\numberline {3.3}$(DiscreteAutomata \wedge ControlTheory \wedge Reachability) \rightarrow ContinuousModes$}{6}{}\protected@file@percent }
|
||||
\citation{eia_lcoe_2022}
|
||||
\citation{eesi_datacenter_2024}
|
||||
\citation{eia_lcoe_2022}
|
||||
\@writefile{toc}{\contentsline {subsection}{\numberline {3.4}Broader Impacts}{14}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {subsection}{\numberline {3.4}Broader Impacts}{8}{}\protected@file@percent }
|
||||
\bibdata{references}
|
||||
\bibcite{geromel2006stability}{1}
|
||||
\bibcite{branicky1998multiple}{2}
|
||||
@ -33,11 +33,11 @@
|
||||
\bibcite{alur1995algorithmic}{7}
|
||||
\bibcite{giannakopoulou2022fret}{8}
|
||||
\bibcite{meyer2018strix}{9}
|
||||
\@writefile{toc}{\contentsline {section}{References}{17}{}\protected@file@percent }
|
||||
\bibcite{jacobs2017syntcomp}{10}
|
||||
\bibcite{platzer2008differential}{11}
|
||||
\bibcite{platzer2017complete}{12}
|
||||
\bibcite{fulton2015keymaera}{13}
|
||||
\bibcite{eia_lcoe_2022}{14}
|
||||
\bibcite{eesi_datacenter_2024}{15}
|
||||
\gdef \@abspage@last{19}
|
||||
\@writefile{toc}{\contentsline {section}{References}{10}{}\protected@file@percent }
|
||||
\gdef \@abspage@last{12}
|
||||
|
||||
@ -1,13 +1,13 @@
|
||||
# Fdb version 4
|
||||
["bibtex main"] 1759176018.82835 "main.aux" "main.bbl" "main" 1759176019.69068 0
|
||||
["bibtex main"] 1759870878.63919 "main.aux" "main.bbl" "main" 1759870879.52101 0
|
||||
"./references.bib" 1759167577.47323 10304 77c9387d6b0ce7e1af7f15e6fb0e19c3 ""
|
||||
"/usr/share/texlive/texmf-dist/bibtex/bst/base/unsrt.bst" 1292289607 18030 1376b4b231b50c66211e47e42eda2875 ""
|
||||
"main.aux" 1759176019.55307 2374 b147740a80a9603c73976206e1823736 "pdflatex"
|
||||
"main.aux" 1759870879.38834 2371 0b7e48a03f45dbd09ec32422fa17b1e2 "pdflatex"
|
||||
(generated)
|
||||
"main.bbl"
|
||||
"main.blg"
|
||||
(rewritten before read)
|
||||
["pdflatex"] 1759176018.85638 "main.tex" "main.pdf" "main" 1759176019.69098 0
|
||||
["pdflatex"] 1759870878.6614 "main.tex" "main.pdf" "main" 1759870879.52119 0
|
||||
"/etc/texmf/web2c/texmf.cnf" 1722610814.59577 475 c0e671620eb5563b2130f56340a5fde8 ""
|
||||
"/usr/share/texlive/texmf-dist/fonts/enc/dvips/base/8r.enc" 1165713224 4850 80dc9bab7f31fb78a000ccfed0e27cab ""
|
||||
"/usr/share/texlive/texmf-dist/fonts/map/fontname/texfonts.map" 1577235249 3524 cb3e574dea2d1052e39280babc910dc8 ""
|
||||
@ -234,11 +234,11 @@
|
||||
"/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map" 1722610820.43889 128028 f533b797fba58d231669ea19e894e23e ""
|
||||
"/var/lib/texmf/web2c/pdftex/pdflatex.fmt" 1726005817 6800784 2b63e5a224c5ad740802d8f9921962c1 ""
|
||||
"broader-impacts/v1.tex" 1759167577.47123 4916 8f9b155145119717e181909e7ce40ed4 ""
|
||||
"dane_proposal_format.cls" 1759176012.54199 2553 dc5fb7813ce17dfa84a228efd08fd33b ""
|
||||
"goals-and-outcomes/v4.tex" 1757896122.20856 5764 a67e489f9ea8343564010d217ae37ec2 ""
|
||||
"main.aux" 1759176019.55307 2374 b147740a80a9603c73976206e1823736 "pdflatex"
|
||||
"main.bbl" 1759176018.84906 3654 cb7bb2c7072cb5aea3ed65a8abe6024a "bibtex main"
|
||||
"main.tex" 1759167577.47323 233 3d97c672204e438a9f988ea9deb7d374 ""
|
||||
"dane_proposal_format.cls" 1759861808.72975 2553 3bbf169a90a50515ed103fe388c111f0 ""
|
||||
"goals-and-outcomes/v6.tex" 1759870860.65316 6132 978a430623148b07dc06f1fa9ce4a2e0 ""
|
||||
"main.aux" 1759870879.38834 2371 0b7e48a03f45dbd09ec32422fa17b1e2 "pdflatex"
|
||||
"main.bbl" 1759870878.65533 3654 cb7bb2c7072cb5aea3ed65a8abe6024a "bibtex main"
|
||||
"main.tex" 1759870875.8503 233 b14d908b969b3e0790528a34f9ae8ceb ""
|
||||
"research-approach/v2.tex" 1758557109.9037 13747 97ad683c7942f87218a074a6187782d1 ""
|
||||
"state-of-the-art/v2.tex" 1757962977.69875 10918 a65147e24336b6a318bf18223339313e ""
|
||||
(generated)
|
||||
|
||||
@ -401,19 +401,16 @@ INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmr7t.vf
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmr7t.vf
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm
|
||||
INPUT ./goals-and-outcomes/v4.tex
|
||||
INPUT ./goals-and-outcomes/v4.tex
|
||||
INPUT ./goals-and-outcomes/v4.tex
|
||||
INPUT ./goals-and-outcomes/v4.tex
|
||||
INPUT goals-and-outcomes/v4.tex
|
||||
INPUT ./goals-and-outcomes/v6.tex
|
||||
INPUT ./goals-and-outcomes/v6.tex
|
||||
INPUT ./goals-and-outcomes/v6.tex
|
||||
INPUT ./goals-and-outcomes/v6.tex
|
||||
INPUT goals-and-outcomes/v6.tex
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmb7t.vf
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb8r.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmr7t.vf
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmri7t.vf
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri8r.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmb7t.vf
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb8r.tfm
|
||||
INPUT ./state-of-the-art/v2.tex
|
||||
@ -437,6 +434,7 @@ INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm
|
||||
@ -449,6 +447,7 @@ INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmr10.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/zptmcm7m.vf
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/psyro.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmmi10.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri8r.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/zptmcm7y.vf
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmsy10.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/rsfs/rsfs10.tfm
|
||||
@ -457,16 +456,17 @@ INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmss9.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmss8.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmri7t.vf
|
||||
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/ts1ptm.fd
|
||||
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/ts1ptm.fd
|
||||
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/ts1ptm.fd
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr8c.tfm
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmr8c.vf
|
||||
INPUT ./research-approach/v2.tex
|
||||
INPUT ./research-approach/v2.tex
|
||||
INPUT ./research-approach/v2.tex
|
||||
INPUT ./research-approach/v2.tex
|
||||
INPUT research-approach/v2.tex
|
||||
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmr8c.vf
|
||||
INPUT ./broader-impacts/v1.tex
|
||||
INPUT ./broader-impacts/v1.tex
|
||||
INPUT ./broader-impacts/v1.tex
|
||||
|
||||
@ -1,4 +1,4 @@
|
||||
This is pdfTeX, Version 3.141592653-2.6-1.40.25 (TeX Live 2023/Debian) (preloaded format=pdflatex 2024.9.10) 29 SEP 2025 16:00
|
||||
This is pdfTeX, Version 3.141592653-2.6-1.40.25 (TeX Live 2023/Debian) (preloaded format=pdflatex 2024.9.10) 7 OCT 2025 17:01
|
||||
entering extended mode
|
||||
restricted \write18 enabled.
|
||||
file:line:error style messages enabled.
|
||||
@ -799,15 +799,15 @@ LaTeX Font Info: ... okay on input line 3.
|
||||
* layout: <same size as paper>
|
||||
* layoutoffset:(h,v)=(0.0pt,0.0pt)
|
||||
* modes:
|
||||
* h-part:(L,W,R)=(144.54pt, 325.21501pt, 144.54pt)
|
||||
* v-part:(T,H,B)=(144.54pt, 505.89pt, 144.54pt)
|
||||
* h-part:(L,W,R)=(72.26999pt, 469.75502pt, 72.26999pt)
|
||||
* v-part:(T,H,B)=(72.26999pt, 650.43001pt, 72.26999pt)
|
||||
* \paperwidth=614.295pt
|
||||
* \paperheight=794.96999pt
|
||||
* \textwidth=325.21501pt
|
||||
* \textheight=505.89pt
|
||||
* \oddsidemargin=72.27pt
|
||||
* \evensidemargin=72.27pt
|
||||
* \topmargin=35.27pt
|
||||
* \textwidth=469.75502pt
|
||||
* \textheight=650.43001pt
|
||||
* \oddsidemargin=0.0pt
|
||||
* \evensidemargin=0.0pt
|
||||
* \topmargin=-37.0pt
|
||||
* \headheight=12.0pt
|
||||
* \headsep=25.0pt
|
||||
* \topskip=12.0pt
|
||||
@ -876,172 +876,23 @@ LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <8> not available
|
||||
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 5.
|
||||
[1
|
||||
|
||||
{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}{/usr/share/texlive/texmf-dist/fonts/enc/dvips/base/8r.enc}] (./goals-and-outcomes/v4.tex [1]
|
||||
Overfull \hbox (5.84927pt too wide) in paragraph at lines 69--79
|
||||
[]\OT1/ptm/b/n/12 Develop and ver-ify for-mal char-ac-ter-i-za-tions of hy-brid mode
|
||||
[]
|
||||
|
||||
|
||||
Overfull \hbox (6.71216pt too wide) in paragraph at lines 69--79
|
||||
\OT1/ptm/m/n/12 mat-i-cal frame-works dis-tin-guish-ing tran-si-tory modes with reach-
|
||||
[]
|
||||
|
||||
|
||||
Overfull \hbox (2.73976pt too wide) in paragraph at lines 69--79
|
||||
\OT1/ptm/m/n/12 clas-si-cal con-trol the-ory will es-tab-lish sta-bil-ity and per-for-mance
|
||||
[]
|
||||
|
||||
[2]
|
||||
Overfull \hbox (4.01187pt too wide) in paragraph at lines 82--90
|
||||
\OT1/ptm/b/n/12 se-quences. \OT1/ptm/m/n/12 By syn-the-siz-ing dis-crete con-troller tran-si-tions from
|
||||
[]
|
||||
|
||||
) (./state-of-the-art/v2.tex [3]
|
||||
{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}{/usr/share/texlive/texmf-dist/fonts/enc/dvips/base/8r.enc}] (./goals-and-outcomes/v6.tex [1]) (./state-of-the-art/v2.tex
|
||||
LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <12> not available
|
||||
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 15.
|
||||
LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <9> not available
|
||||
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 15.
|
||||
LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <7> not available
|
||||
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 15.
|
||||
|
||||
Overfull \hbox (10.74564pt too wide) in paragraph at lines 31--45
|
||||
\OT1/ptm/m/n/12 punov func-tions re-mains chal-leng-ing. Sta-bil-ity con-di-tions for switched
|
||||
[]
|
||||
|
||||
[4]
|
||||
Overfull \hbox (0.72525pt too wide) in paragraph at lines 60--68
|
||||
\OT1/ptm/m/n/12 state dimension---current meth-ods re-main lim-ited to 6-8 di-men-sional
|
||||
[]
|
||||
|
||||
|
||||
Overfull \hbox (2.70512pt too wide) in paragraph at lines 60--68
|
||||
\OT1/ptm/m/n/12 approximations that be-come in-creas-ingly pes-simistic with each mode
|
||||
[]
|
||||
|
||||
|
||||
Overfull \hbox (3.5701pt too wide) in paragraph at lines 69--78
|
||||
\OT1/ptm/m/n/12 for 7-dimensional au-tonomous rac-ing sys-tems [5]. This break-through
|
||||
[]
|
||||
|
||||
[5]
|
||||
Overfull \hbox (26.09029pt too wide) detected at line 104
|
||||
[]\OT1/cmss/m/n/12 G\OT1/ztmcm/m/n/12 ([] \OMS/ztmcm/m/n/12 ! \OT1/cmss/m/n/12 X\OT1/ztmcm/m/n/12 ([] \OMS/ztmcm/m/n/12 ^ \OT1/ztmcm/m/n/12 (\OMS/ztmcm/m/n/12 :[] \OT1/cmss/m/n/12 U []\OT1/ztmcm/m/n/12 )))
|
||||
[]
|
||||
|
||||
|
||||
Overfull \hbox (2.39413pt too wide) in paragraph at lines 106--119
|
||||
\OT1/ptm/m/n/12 tions, they can be checked us-ing com-pu-ta-tional tools. Cyber-physical
|
||||
[]
|
||||
|
||||
|
||||
Overfull \hbox (0.23428pt too wide) in paragraph at lines 106--119
|
||||
\OT1/ptm/m/n/12 graphs with con-tin-u-ous dy-nam-ics. Hy-brid au-tomata bridge program-
|
||||
[]
|
||||
|
||||
|
||||
Overfull \hbox (9.89316pt too wide) in paragraph at lines 106--119
|
||||
\OT1/ptm/m/n/12 analysis tech-niques to hy-brid sys-tems with in-fi-nite state spaces through
|
||||
[]
|
||||
|
||||
|
||||
Overfull \hbox (4.67361pt too wide) in paragraph at lines 126--132
|
||||
\OT1/ptm/m/n/12 nat-u-ral lan-guage and math-e-mat-i-cal spec-i-fi-ca-tions through FRETish---
|
||||
[]
|
||||
|
||||
|
||||
Overfull \hbox (5.88588pt too wide) in paragraph at lines 126--132
|
||||
\OT1/ptm/m/n/12 with ver-i-fi-ca-tion tools like Co-CoSim, and run-time mon-i-tor-ing through
|
||||
[]
|
||||
|
||||
[6]
|
||||
Overfull \hbox (14.64534pt too wide) in paragraph at lines 133--140
|
||||
\OT1/ptm/m/n/12 cally gen-er-ate con-trollers. The Re-ac-tive Syn-the-sis Com-pe-ti-tion (SYNT-
|
||||
[]
|
||||
|
||||
[2] [3]
|
||||
LaTeX Font Info: Trying to load font information for TS1+ptm on input line 168.
|
||||
(/usr/share/texlive/texmf-dist/tex/latex/psnfss/ts1ptm.fd
|
||||
(/usr/share/texlive/texmf-dist/tex/latex/psnfss/ts1ptm.fd
|
||||
File: ts1ptm.fd 2001/06/04 font definitions for TS1/ptm.
|
||||
) [7]) (./research-approach/v2.tex
|
||||
Overfull \hbox (1.40666pt too wide) in paragraph at lines 188--1
|
||||
[]\OT1/ptm/m/n/12 The state of the art re-veals a field in tran-si-tion. Tra-di-tional bound-
|
||||
)) (./research-approach/v2.tex [4]
|
||||
Overfull \hbox (1.34416pt too wide) in paragraph at lines 44--48
|
||||
[]\OT1/ptm/m/n/12 FRET em-ploys a spe-cial-ized re-quire-ments lan-guage sim-i-lar to nat-u-ral lan-guage called FRETish.
|
||||
[]
|
||||
|
||||
|
||||
Overfull \hbox (13.91393pt too wide) in paragraph at lines 188--1
|
||||
\OT1/ptm/m/n/12 aries be-tween con-trol the-ory and for-mal meth-ods are dis-solv-ing through
|
||||
[]
|
||||
|
||||
|
||||
Overfull \hbox (15.72511pt too wide) in paragraph at lines 188--1
|
||||
\OT1/ptm/m/n/12 fun-da-men-tal chal-lenges remain---particularly scal-a-bil-ity and the theory-
|
||||
[]
|
||||
|
||||
|
||||
Overfull \hbox (0.72522pt too wide) in paragraph at lines 13--16
|
||||
[]\OT1/ptm/m/n/12 Develop con-tin-u-ous con-trollers to op-er-ate be-tween modes, and
|
||||
[]
|
||||
|
||||
|
||||
Overfull \hbox (24.65291pt too wide) in paragraph at lines 21--21
|
||||
|[]\OT1/ptm/b/n/12 Requirements: $\OT1/ztmcm/m/n/12 (\OML/ztmcm/m/it/12 Procedures \OMS/ztmcm/m/n/12 ^ \OML/ztmcm/m/it/12 FRET\OT1/ztmcm/m/n/12 ) \OMS/ztmcm/m/n/12 ! \OML/ztmcm/m/it/12 TemporalSpecifications$|
|
||||
[]
|
||||
|
||||
[8] [9]
|
||||
Overfull \hbox (2.02168pt too wide) in paragraph at lines 89--96
|
||||
\OT1/ptm/m/n/12 hu-man decision-making el-e-ments of re-ac-tor op-er-a-tion by im-ple-ment-
|
||||
[]
|
||||
|
||||
[10]
|
||||
Overfull \hbox (1.1066pt too wide) in paragraph at lines 119--128
|
||||
[]\OT1/ptm/m/n/12 Correctness of the switch-ing con-troller is paramount to this work.
|
||||
[]
|
||||
|
||||
|
||||
Overfull \hbox (59.43591pt too wide) in paragraph at lines 130--130
|
||||
|[]$\OT1/ztmcm/m/n/12 (\OML/ztmcm/m/it/12 DiscreteAutomata \OMS/ztmcm/m/n/12 ^ \OML/ztmcm/m/it/12 ControlTheory \OMS/ztmcm/m/n/12 ^ \OML/ztmcm/m/it/12 Reachability\OT1/ztmcm/m/n/12 ) \OMS/ztmcm/m/n/12 ! \OML/ztmcm/m/it/12 ContinuousModes$|
|
||||
[]
|
||||
|
||||
[11]
|
||||
Overfull \hbox (6.13612pt too wide) in paragraph at lines 164--171
|
||||
\OT1/ptm/m/n/12 the sys-tem to-ward a sta-bi-liz-ing steady-state mode. These modes
|
||||
[]
|
||||
|
||||
[12]
|
||||
Overfull \hbox (12.49698pt too wide) in paragraph at lines 197--216
|
||||
\OT1/ptm/m/n/12 em-ploy three main tech-niques: reach-a-bil-ity anal-y-sis, assume-guarantee
|
||||
[]
|
||||
|
||||
) (./broader-impacts/v1.tex
|
||||
Overfull \hbox (4.61438pt too wide) in paragraph at lines 225--1
|
||||
\OT1/ptm/m/n/12 sys-tem de-sign by bridg-ing for-mal meth-ods and con-trol the-ory through
|
||||
[]
|
||||
|
||||
|
||||
Overfull \hbox (2.7176pt too wide) in paragraph at lines 225--1
|
||||
\OT1/ptm/m/n/12 fully au-tonomous sys-tem with higher re-li-a-bil-ity than human-operated
|
||||
[]
|
||||
|
||||
[13] [14]
|
||||
Overfull \hbox (11.7537pt too wide) in paragraph at lines 25--37
|
||||
\OT1/ptm/m/n/12 cost chal-lenge through im-ple-men-ta-tions of high-assurance au-tonomous
|
||||
[]
|
||||
|
||||
|
||||
Overfull \hbox (2.23761pt too wide) in paragraph at lines 52--63
|
||||
\OT1/ptm/m/n/12 Nu-clear Reg-u-la-tory Com-mis-sion cer-ti-fi-ca-tion re-quires ex-ten-sive doc-
|
||||
[]
|
||||
|
||||
|
||||
Overfull \hbox (10.28976pt too wide) in paragraph at lines 52--63
|
||||
\OT1/ptm/m/n/12 u-men-ta-tion of con-trol pro-ce-dures, op-er-a-tional re-quire-ments, and safety
|
||||
[]
|
||||
|
||||
[15]) [16] (./main.bbl
|
||||
Underfull \hbox (badness 4391) in paragraph at lines 34--37
|
||||
[]\OT1/ptm/m/n/12 Rajeev Alur, Costas Cour-cou-betis, Nico-las Halb-wachs,
|
||||
[]
|
||||
|
||||
[17]) [18] (./main.aux)
|
||||
[5] [6] [7]) (./broader-impacts/v1.tex [8]) [9] (./main.bbl [10]) [11] (./main.aux)
|
||||
***********
|
||||
LaTeX2e <2023-11-01> patch level 1
|
||||
L3 programming layer <2024-01-22>
|
||||
@ -1050,16 +901,16 @@ L3 programming layer <2024-01-22>
|
||||
Here is how much of TeX's memory you used:
|
||||
25428 strings out of 476182
|
||||
528199 string characters out of 5795595
|
||||
1931975 words of memory out of 5000000
|
||||
1935975 words of memory out of 5000000
|
||||
46870 multiletter control sequences out of 15000+600000
|
||||
590786 words of font info for 108 fonts, out of 8000000 for 9000
|
||||
14 hyphenation exceptions out of 8191
|
||||
110i,9n,107p,1008b,285s stack positions out of 10000i,1000n,20000p,200000b,200000s
|
||||
</usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmss12.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/symbol/usyr.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmb8a.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmr8a.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmri8a.pfb>
|
||||
Output written on main.pdf (19 pages, 128398 bytes).
|
||||
Output written on main.pdf (12 pages, 124660 bytes).
|
||||
PDF statistics:
|
||||
134 PDF objects out of 1000 (max. 8388607)
|
||||
80 compressed objects within 1 object stream
|
||||
111 PDF objects out of 1000 (max. 8388607)
|
||||
64 compressed objects within 1 object stream
|
||||
0 named destinations out of 1000 (max. 500000)
|
||||
109 words of extra memory for PDF output out of 10000 (max. 10000000)
|
||||
|
||||
|
||||
Binary file not shown.
Binary file not shown.
@ -3,7 +3,7 @@
|
||||
\begin{document}
|
||||
|
||||
\maketitle
|
||||
\input{goals-and-outcomes/v4}
|
||||
\input{goals-and-outcomes/v6}
|
||||
\input{state-of-the-art/v2}
|
||||
\input{research-approach/v2}
|
||||
\input{broader-impacts/v1}
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user