Auto sync: 2025-09-14 22:44:54 (6 files changed)
M Writing/ERLM/main.aux M Writing/ERLM/main.fdb_latexmk M Writing/ERLM/main.log M Writing/ERLM/main.pdf M Writing/ERLM/main.synctex.gz M Writing/ERLM/state-of-the-art/v1.tex
This commit is contained in:
parent
1c1f398df7
commit
2cf0e2da3a
@ -5,7 +5,7 @@
|
||||
\@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}Control Theory and Hybrid Systems}{3}{}\protected@file@percent }
|
||||
\newlabel{eq:hybrid-sys}{{2}{3}{Control Theory and Hybrid Systems}{}{}}
|
||||
\bibdata{references}
|
||||
\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Formal Methods and Reactive Synthesis}{4}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {section}{References}{4}{}\protected@file@percent }
|
||||
\gdef \@abspage@last{5}
|
||||
\bibdata{references}
|
||||
\@writefile{toc}{\contentsline {section}{References}{5}{}\protected@file@percent }
|
||||
\gdef \@abspage@last{6}
|
||||
|
||||
@ -1,13 +1,13 @@
|
||||
# Fdb version 4
|
||||
["bibtex main"] 1757899416.09338 "main.aux" "main.bbl" "main" 1757900978.83336 0
|
||||
["bibtex main"] 1757903957.85967 "main.aux" "main.bbl" "main" 1757904283.92968 0
|
||||
"./references.bib" 1757896122.21556 0 d41d8cd98f00b204e9800998ecf8427e ""
|
||||
"/usr/share/texlive/texmf-dist/bibtex/bst/base/unsrt.bst" 1292289607 18030 1376b4b231b50c66211e47e42eda2875 ""
|
||||
"main.aux" 1757900978.60047 759 3051c697f76ee5e29dc620b2ef1fb2b5 "pdflatex"
|
||||
"main.aux" 1757904283.75473 759 9d0c4909d3a06d061361cd5dd469f219 "pdflatex"
|
||||
(generated)
|
||||
"main.bbl"
|
||||
"main.blg"
|
||||
(rewritten before read)
|
||||
["pdflatex"] 1757900977.5298 "main.tex" "main.pdf" "main" 1757900978.8337 0
|
||||
["pdflatex"] 1757904282.70024 "main.tex" "main.pdf" "main" 1757904283.93 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 ""
|
||||
@ -228,10 +228,10 @@
|
||||
"/var/lib/texmf/web2c/pdftex/pdflatex.fmt" 1726005817 6800784 2b63e5a224c5ad740802d8f9921962c1 ""
|
||||
"dane_proposal_format.cls" 1757899413.38474 2553 eb32d38752e5298f84dcaa0f93fb1dab ""
|
||||
"goals-and-outcomes/v4.tex" 1757896122.20856 5764 a67e489f9ea8343564010d217ae37ec2 ""
|
||||
"main.aux" 1757900978.60047 759 3051c697f76ee5e29dc620b2ef1fb2b5 "pdflatex"
|
||||
"main.bbl" 1757899416.11972 49 0eba253fc001332e731e8aba3f23127b "bibtex main"
|
||||
"main.aux" 1757904283.75473 759 9d0c4909d3a06d061361cd5dd469f219 "pdflatex"
|
||||
"main.bbl" 1757903957.88911 49 0eba253fc001332e731e8aba3f23127b "bibtex main"
|
||||
"main.tex" 1757896122.21556 182 46aa668f839c7d4c451f49d8253993e9 ""
|
||||
"state-of-the-art/v1.tex" 1757900976.00644 6572 9e8f6252c740a1a218b70ad32050abfe ""
|
||||
"state-of-the-art/v1.tex" 1757904281.15369 10205 c2111caf8273a3ffa8af4fb77055937b ""
|
||||
(generated)
|
||||
"main.aux"
|
||||
"main.log"
|
||||
|
||||
@ -1,4 +1,4 @@
|
||||
This is pdfTeX, Version 3.141592653-2.6-1.40.25 (TeX Live 2023/Debian) (preloaded format=pdflatex 2024.9.10) 14 SEP 2025 21:49
|
||||
This is pdfTeX, Version 3.141592653-2.6-1.40.25 (TeX Live 2023/Debian) (preloaded format=pdflatex 2024.9.10) 14 SEP 2025 22:44
|
||||
entering extended mode
|
||||
restricted \write18 enabled.
|
||||
file:line:error style messages enabled.
|
||||
@ -832,11 +832,11 @@ File: umsb.fd 2013/01/14 v3.01 AMS symbols B
|
||||
{/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
|
||||
LaTeX Font Info: Font shape `OT1/phv/m/it' in size <10.95> not available
|
||||
(Font) Font shape `OT1/phv/m/sl' tried instead on input line 33.
|
||||
[1]) [2] (./state-of-the-art/v1.tex [3]) (./main.bbl
|
||||
[1]) [2] (./state-of-the-art/v1.tex [3] [4]) (./main.bbl
|
||||
|
||||
LaTeX Warning: Empty `thebibliography' environment on input line 3.
|
||||
|
||||
) [4] (./main.aux)
|
||||
) [5] (./main.aux)
|
||||
***********
|
||||
LaTeX2e <2023-11-01> patch level 1
|
||||
L3 programming layer <2024-01-22>
|
||||
@ -851,10 +851,10 @@ Here is how much of TeX's memory you used:
|
||||
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/cmmi8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/helvetic/uhvb8a.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/helvetic/uhvr8a.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/helvetic/uhvro8a.pfb>
|
||||
Output written on main.pdf (5 pages, 81170 bytes).
|
||||
Output written on main.pdf (6 pages, 85625 bytes).
|
||||
PDF statistics:
|
||||
83 PDF objects out of 1000 (max. 8388607)
|
||||
45 compressed objects within 1 object stream
|
||||
86 PDF objects out of 1000 (max. 8388607)
|
||||
47 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.
@ -117,3 +117,49 @@ language called FRETish, and translate them automatically into linear temporal
|
||||
logic specifications. From this point, it can be examined whether or not
|
||||
the set of requirements define a realizable system, or if there exists conflicts
|
||||
between different specifications.
|
||||
|
||||
We have previously discussed that a set of specifications can be checked as to
|
||||
whether or not the constitute a realizable system. If a system is realizable,
|
||||
there are a significant number of tools that can synthesize reactive control
|
||||
systems from the set of logical specifications. Reactive systems are those that
|
||||
take an input, and produce a reaction (an output). They depend on the current
|
||||
system state and input to produce the next state. Competitions such as the
|
||||
Reactive Synthesis Competition (SYNTCOMP) have existed for over a decade where
|
||||
different groups try to produce the best reactive synthesis algorithm. These
|
||||
systems are tested against a series of benchmarks to examine the number,
|
||||
quality, and resources consumed to produce realizations of reactive systems from
|
||||
logical specifications.
|
||||
|
||||
LIMITATION: while reactive synthesis exists, and we have an extensive amount of
|
||||
documentation on nuclear power regulation and operating procedures exists, we
|
||||
have not tried to combine the two together.
|
||||
|
||||
Finally, formal methods has contributed the hybrid automata and differential
|
||||
dynamic logic to try and solve the hybrid system verification problem. Hybrid
|
||||
automata are an expansion of finite automata. Hybrid automata define each node
|
||||
as being a control mode, similar to how finite state automata define each node
|
||||
as a single state. For hybrid automata, the node represents the \textit{discrete
|
||||
state}. Meanwhile, the transitions between states indicate the transitions
|
||||
between continuous modes. These transitions represent the executions of
|
||||
\(\nu(\cdot)\) that change the discrete state \(q\). Hybrid automata introduce a
|
||||
way to graphically represent the transitions between continuous dynamic modes.
|
||||
|
||||
Differential dynamic logic (dL), on the other hand, is an expansion of linear
|
||||
temporal logic to include support for real numbers and differential equation
|
||||
solving. dL introduces two new operators focused on including dynamic behaviors.
|
||||
The first is the box modality \([\alpha]\phi\), which states that for all
|
||||
possible executions of the hybrid system \(\alpha\), \(\phi\) holds. The second
|
||||
is the diamond modality \(\langle \alpha \rangle \phi\), which states that for
|
||||
the hybrid system \(\alpha\), there is a trajectory where \(\phi\) holds. With
|
||||
these two additional modalities, hybrid systems can be reasoned about directly
|
||||
while including the continuous dynamics. That does not mean that working with
|
||||
dL is easy however, as the effort to perform verification is encumbered by the
|
||||
knowledge requirement of differential equations, logical specifications, and
|
||||
then finally, sequent calculus to actually try and prove things written in dL.
|
||||
dL is expressive enough to capture any hybrid system behavior, but the effort to
|
||||
actually prove requirement adherence is challenging, even with automated proof
|
||||
assistant tools.
|
||||
|
||||
In the next section, we will discuss how this research will address these
|
||||
limitations and provide a path forward for building high assurance hybrid
|
||||
control systems.
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user