danesabo/Obsidian
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Auto sync: 2025-09-15 11:31:09 (11 files changed)

Browse Source 
M  Writing/ERLM/main.aux

M  Writing/ERLM/main.bbl

M  Writing/ERLM/main.blg

M  Writing/ERLM/main.fdb_latexmk

M  Writing/ERLM/main.fls

M  Writing/ERLM/main.log

M  Writing/ERLM/main.pdf

M  Writing/ERLM/main.synctex.gz
This commit is contained in:
Dane Sabo 2025-09-15 11:31:09 -04:00
parent ee4f47c9c6
commit 02832ba45e
11 changed files with 682 additions and 79 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

30
Writing/ERLM/main.aux
View File

@ -2,10 +2,32 @@
\bibstyle{unsrt} \bibstyle{unsrt}
\providecommand \oddpage@label [2]{} \providecommand \oddpage@label [2]{}
\@writefile{toc}{\contentsline {section}{\numberline {1}Goals and Outcomes}{1}{}\protected@file@percent } \@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}
\citation{mitchell2005time}
\@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 } \@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}{}{}} \citation{yang2024learning}
\citation{alur1993hybrid}
\citation{alur1995algorithmic}
\citation{giannakopoulou2022fret}
\citation{meyer2018strix,jacobs2017syntcomp}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Formal Methods and Reactive Synthesis}{4}{}\protected@file@percent } \@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Formal Methods and Reactive Synthesis}{4}{}\protected@file@percent }
\citation{platzer2008differential,platzer2017complete}
\citation{fulton2015keymaera}
\bibdata{references} \bibdata{references}
\@writefile{toc}{\contentsline {section}{References}{5}{}\protected@file@percent } \bibcite{geromel2006stability}{1}
\gdef \@abspage@last{6} \bibcite{branicky1998multiple}{2}
\bibcite{liberzon2003switching}{3}
\bibcite{mitchell2005time}{4}
\bibcite{yang2024learning}{5}
\bibcite{alur1993hybrid}{6}
\bibcite{alur1995algorithmic}{7}
\bibcite{giannakopoulou2022fret}{8}
\bibcite{meyer2018strix}{9}
\bibcite{jacobs2017syntcomp}{10}
\bibcite{platzer2008differential}{11}
\bibcite{platzer2017complete}{12}
\bibcite{fulton2015keymaera}{13}
\@writefile{toc}{\contentsline {section}{References}{6}{}\protected@file@percent }
\gdef \@abspage@last{7}

67
Writing/ERLM/main.bbl
View File

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

62
Writing/ERLM/main.blg
View File

@ -2,47 +2,45 @@ This is BibTeX, Version 0.99d (TeX Live 2023/Debian)
Capacity: max_strings=200000, hash_size=200000, hash_prime=170003 Capacity: max_strings=200000, hash_size=200000, hash_prime=170003
The top-level auxiliary file: main.aux The top-level auxiliary file: main.aux
The style file: unsrt.bst The style file: unsrt.bst
I found no \citation commands---while reading file main.aux
Database file #1: references.bib Database file #1: references.bib
You've used 0 entries, You've used 13 entries,
1791 wiz_defined-function locations, 1791 wiz_defined-function locations,
445 strings with 3516 characters, 530 strings with 5916 characters,
and the built_in function-call counts, 18 in all, are: and the built_in function-call counts, 3422 in all, are:
= -- 0 = -- 313
> -- 0 > -- 151
< -- 0 < -- 5
+ -- 0 + -- 56
- -- 0 - -- 43
* -- 2 * -- 238
:= -- 7 := -- 530
add.period$ -- 0 add.period$ -- 42
call.type$ -- 0 call.type$ -- 13
change.case$ -- 0 change.case$ -- 12
chr.to.int$ -- 0 chr.to.int$ -- 0
cite$ -- 0 cite$ -- 13
duplicate$ -- 0 duplicate$ -- 155
empty$ -- 1 empty$ -- 329
format.name$ -- 0 format.name$ -- 43
if$ -- 1 if$ -- 770
int.to.chr$ -- 0 int.to.chr$ -- 0
int.to.str$ -- 0 int.to.str$ -- 13
missing$ -- 0 missing$ -- 13
newline$ -- 3 newline$ -- 68
num.names$ -- 0 num.names$ -- 13
pop$ -- 0 pop$ -- 39
preamble$ -- 1 preamble$ -- 1
purify$ -- 0 purify$ -- 0
quote$ -- 0 quote$ -- 0
skip$ -- 1 skip$ -- 73
stack$ -- 0 stack$ -- 0
substring$ -- 0 substring$ -- 243
swap$ -- 0 swap$ -- 46
text.length$ -- 0 text.length$ -- 5
text.prefix$ -- 0 text.prefix$ -- 0
top$ -- 0 top$ -- 0
type$ -- 0 type$ -- 0
warning$ -- 0 warning$ -- 0
while$ -- 0 while$ -- 34
width$ -- 0 width$ -- 15
write$ -- 2 write$ -- 146
(There was 1 error message)

34
Writing/ERLM/main.fdb_latexmk
View File

@ -1,14 +1,14 @@
# Fdb version 4 # Fdb version 4
["bibtex main"] 1757903957.85967 "main.aux" "main.bbl" "main" 1757904436.44498 0 ["bibtex main"] 1757950134.83183 "main.aux" "main.bbl" "main" 1757950267.92325 0
"./references.bib" 1757896122.21556 0 d41d8cd98f00b204e9800998ecf8427e "" "./references.bib" 1757949790.55852 9415 fb740c67337f78e30e95f745a7cf3dae ""
"/usr/share/texlive/texmf-dist/bibtex/bst/base/unsrt.bst" 1292289607 18030 1376b4b231b50c66211e47e42eda2875 "" "/usr/share/texlive/texmf-dist/bibtex/bst/base/unsrt.bst" 1292289607 18030 1376b4b231b50c66211e47e42eda2875 ""
"main.aux" 1757904436.24501 759 9d0c4909d3a06d061361cd5dd469f219 "pdflatex" "main.aux" 1757950267.84363 1476 86aee14919487c57b3ce6714b0985bff "pdflatex"
(generated) (generated)
"main.bbl" "main.bbl"
"main.blg" "main.blg"
(rewritten before read) (rewritten before read)
["pdflatex"] 1757904435.2107 "main.tex" "main.pdf" "main" 1757904436.44541 0 ["pdflatex"] 1757950267.45324 "main.tex" "main.pdf" "main" 1757950267.9234 0
"/etc/texmf/web2c/texmf.cnf" 1722610814.59577 475 c0e671620eb5563b2130f56340a5fde8 "" "/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/enc/dvips/base/8r.enc" 1165713224 4850 80dc9bab7f31fb78a000ccfed0e27cab ""
"/usr/share/texlive/texmf-dist/fonts/map/fontname/texfonts.map" 1577235249 3524 cb3e574dea2d1052e39280babc910dc8 "" "/usr/share/texlive/texmf-dist/fonts/map/fontname/texfonts.map" 1577235249 3524 cb3e574dea2d1052e39280babc910dc8 ""
"/usr/share/texlive/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm" 1136768653 1408 5937f58aa508ea2cea4901c07d10f5fe "" "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/symbol/psyr.tfm" 1136768653 1408 5937f58aa508ea2cea4901c07d10f5fe ""
@ -16,6 +16,7 @@
"/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm" 1136768653 2172 fd0c924230362ff848a33632ed45dc23 "" "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb7t.tfm" 1136768653 2172 fd0c924230362ff848a33632ed45dc23 ""
"/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb8r.tfm" 1136768653 4524 6bce29db5bc272ba5f332261583fee9c "" "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb8r.tfm" 1136768653 4524 6bce29db5bc272ba5f332261583fee9c ""
"/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm" 1136768653 2124 2601a75482e9426d33db523edf23570a "" "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm" 1136768653 2124 2601a75482e9426d33db523edf23570a ""
"/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr8c.tfm" 1136768653 1352 fa28a7e6d323c65ce7d13d5342ff6be2 ""
"/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm" 1136768653 4408 25b74d011a4c66b7f212c0cc3c90061b "" "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm" 1136768653 4408 25b74d011a4c66b7f212c0cc3c90061b ""
"/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm" 1136768653 2288 f478fc8fed18759effb59f3dad7f3084 "" "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri7t.tfm" 1136768653 2288 f478fc8fed18759effb59f3dad7f3084 ""
"/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri8r.tfm" 1136768653 4640 532ca3305aad10cc01d769f3f91f1029 "" "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri8r.tfm" 1136768653 4640 532ca3305aad10cc01d769f3f91f1029 ""
@ -28,18 +29,22 @@
"/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmmi10.tfm" 1136768653 1528 abec98dbc43e172678c11b3b9031252a "" "/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmmi10.tfm" 1136768653 1528 abec98dbc43e172678c11b3b9031252a ""
"/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmr10.tfm" 1136768653 1296 45809c5a464d5f32c8f98ba97c1bb47f "" "/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmr10.tfm" 1136768653 1296 45809c5a464d5f32c8f98ba97c1bb47f ""
"/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmr12.tfm" 1136768653 1288 655e228510b4c2a1abe905c368440826 "" "/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmr12.tfm" 1136768653 1288 655e228510b4c2a1abe905c368440826 ""
"/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmss12.tfm" 1136768653 1324 37b971caf729d7edd9cbb9f9b0ea76eb ""
"/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmss8.tfm" 1136768653 1296 d77f431d10d47c8ea2cc18cf45346274 ""
"/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmss9.tfm" 1136768653 1320 49357c421c0d469f88b867dd0c3d10e8 ""
"/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmsy10.tfm" 1136768653 1124 6c73e740cf17375f03eec0ee63599741 "" "/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmsy10.tfm" 1136768653 1124 6c73e740cf17375f03eec0ee63599741 ""
"/usr/share/texlive/texmf-dist/fonts/tfm/public/rsfs/rsfs10.tfm" 1229303445 688 37338d6ab346c2f1466b29e195316aa4 "" "/usr/share/texlive/texmf-dist/fonts/tfm/public/rsfs/rsfs10.tfm" 1229303445 688 37338d6ab346c2f1466b29e195316aa4 ""
"/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb" 1248133631 36299 5f9df58c2139e7edcf37c8fca4bd384d "" "/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb" 1248133631 36299 5f9df58c2139e7edcf37c8fca4bd384d ""
"/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb" 1248133631 35752 024fb6c41858982481f6968b5fc26508 "" "/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb" 1248133631 35752 024fb6c41858982481f6968b5fc26508 ""
"/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmss12.pfb" 1248133631 24393 3b7eb51a67a0a62aec5849271bdb9c2e ""
"/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb" 1248133631 32569 5e5ddc8df908dea60932f3c484a54c0d "" "/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb" 1248133631 32569 5e5ddc8df908dea60932f3c484a54c0d ""
"/usr/share/texlive/texmf-dist/fonts/type1/public/rsfs/rsfs10.pfb" 1229303445 16077 4737ac34f0fb5608550f3780a0202c22 ""
"/usr/share/texlive/texmf-dist/fonts/type1/urw/symbol/usyr.pfb" 1136849748 33709 b09d2e140b7e807d3a97058263ab6693 "" "/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/utmb8a.pfb" 1136849748 44729 811d6c62865936705a31c797a1d5dada ""
"/usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmr8a.pfb" 1136849748 46026 6dab18b61c907687b520c72847215a68 "" "/usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmr8a.pfb" 1136849748 46026 6dab18b61c907687b520c72847215a68 ""
"/usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmri8a.pfb" 1136849748 45458 a3faba884469519614ca56ba5f6b1de1 "" "/usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmri8a.pfb" 1136849748 45458 a3faba884469519614ca56ba5f6b1de1 ""
"/usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmb7t.vf" 1136768653 1372 788387fea833ef5963f4c5bffe33eb89 "" "/usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmb7t.vf" 1136768653 1372 788387fea833ef5963f4c5bffe33eb89 ""
"/usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmr7t.vf" 1136768653 1380 0ea3a3370054be6da6acd929ec569f06 "" "/usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmr7t.vf" 1136768653 1380 0ea3a3370054be6da6acd929ec569f06 ""
"/usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmr8c.vf" 1136768653 3556 8a9a6dcbcd146ef985683f677f4758a6 ""
"/usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmri7t.vf" 1136768653 1384 a9d8adaf491ce34e5fba99dc7bbe5f39 "" "/usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmri7t.vf" 1136768653 1384 a9d8adaf491ce34e5fba99dc7bbe5f39 ""
"/usr/share/texlive/texmf-dist/fonts/vf/adobe/times/zptmcm7m.vf" 1136768653 1132 27520247d3fe18d4266a226b461885c2 "" "/usr/share/texlive/texmf-dist/fonts/vf/adobe/times/zptmcm7m.vf" 1136768653 1132 27520247d3fe18d4266a226b461885c2 ""
"/usr/share/texlive/texmf-dist/fonts/vf/adobe/times/zptmcm7t.vf" 1136768653 1108 d271d6f9de4122c3f8d3b65666167fac "" "/usr/share/texlive/texmf-dist/fonts/vf/adobe/times/zptmcm7t.vf" 1136768653 1108 d271d6f9de4122c3f8d3b65666167fac ""
@ -209,6 +214,7 @@
"/usr/share/texlive/texmf-dist/tex/latex/psnfss/omxztmcm.fd" 1137110629 329 c8cddcc90b6f567b28408eb374773c9c "" "/usr/share/texlive/texmf-dist/tex/latex/psnfss/omxztmcm.fd" 1137110629 329 c8cddcc90b6f567b28408eb374773c9c ""
"/usr/share/texlive/texmf-dist/tex/latex/psnfss/ot1ptm.fd" 1137110629 961 15056f4a61917ceed3a44e4ac11fcc52 "" "/usr/share/texlive/texmf-dist/tex/latex/psnfss/ot1ptm.fd" 1137110629 961 15056f4a61917ceed3a44e4ac11fcc52 ""
"/usr/share/texlive/texmf-dist/tex/latex/psnfss/ot1ztmcm.fd" 1137110629 329 aee7226812ba4138ac67a018466b488d "" "/usr/share/texlive/texmf-dist/tex/latex/psnfss/ot1ztmcm.fd" 1137110629 329 aee7226812ba4138ac67a018466b488d ""
"/usr/share/texlive/texmf-dist/tex/latex/psnfss/ts1ptm.fd" 1137110629 619 96f56dc5d1ef1fe1121f1cfeec70ee0c ""
"/usr/share/texlive/texmf-dist/tex/latex/setspace/setspace.sty" 1670275497 22490 8cac309b79a4c53a4ffce4b1b07aead0 "" "/usr/share/texlive/texmf-dist/tex/latex/setspace/setspace.sty" 1670275497 22490 8cac309b79a4c53a4ffce4b1b07aead0 ""
"/usr/share/texlive/texmf-dist/tex/latex/standalone/standalone.sty" 1665433651 34855 01a6d48b146a4c824944925004b07205 "" "/usr/share/texlive/texmf-dist/tex/latex/standalone/standalone.sty" 1665433651 34855 01a6d48b146a4c824944925004b07205 ""
"/usr/share/texlive/texmf-dist/tex/latex/svn-prov/svn-prov.sty" 1272330018 6852 44ea8d7e58290cde708a34ebf3953571 "" "/usr/share/texlive/texmf-dist/tex/latex/svn-prov/svn-prov.sty" 1272330018 6852 44ea8d7e58290cde708a34ebf3953571 ""
@ -225,14 +231,14 @@
"/usr/share/texlive/texmf-dist/tex/latex/xkeyval/xkeyval.sty" 1655411236 4937 4ce600ce9bd4ec84d0250eb6892fcf4f "" "/usr/share/texlive/texmf-dist/tex/latex/xkeyval/xkeyval.sty" 1655411236 4937 4ce600ce9bd4ec84d0250eb6892fcf4f ""
"/usr/share/texlive/texmf-dist/web2c/texmf.cnf" 1707919699 40399 f2c302f7d2af602abb742093540a5834 "" "/usr/share/texlive/texmf-dist/web2c/texmf.cnf" 1707919699 40399 f2c302f7d2af602abb742093540a5834 ""
"/usr/share/texmf/web2c/texmf.cnf" 1707919699 40399 f2c302f7d2af602abb742093540a5834 "" "/usr/share/texmf/web2c/texmf.cnf" 1707919699 40399 f2c302f7d2af602abb742093540a5834 ""
"/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map" 1722610820.43889 128028 f533b797fba58d231669ea19e894e23e "" "/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map" 1726065856.46263 128028 f533b797fba58d231669ea19e894e23e ""
"/var/lib/texmf/web2c/pdftex/pdflatex.fmt" 1726005817 6800784 2b63e5a224c5ad740802d8f9921962c1 "" "/var/lib/texmf/web2c/pdftex/pdflatex.fmt" 1726065868 6800790 607442c924ed54405961d2b8ac2a25ae ""
"dane_proposal_format.cls" 1757904433.20297 2553 3bbf169a90a50515ed103fe388c111f0 "" "dane_proposal_format.cls" 1757942776.53402 2553 3bbf169a90a50515ed103fe388c111f0 ""
"goals-and-outcomes/v4.tex" 1757896122.20856 5764 a67e489f9ea8343564010d217ae37ec2 "" "goals-and-outcomes/v4.tex" 1757864250.3119 5764 a67e489f9ea8343564010d217ae37ec2 ""
"main.aux" 1757904436.24501 759 9d0c4909d3a06d061361cd5dd469f219 "pdflatex" "main.aux" 1757950267.84363 1476 86aee14919487c57b3ce6714b0985bff "pdflatex"
"main.bbl" 1757903957.88911 49 0eba253fc001332e731e8aba3f23127b "bibtex main" "main.bbl" 1757950134.84155 3170 7f578afdcd1e73f308616474dc5a4003 "bibtex main"
"main.tex" 1757896122.21556 182 46aa668f839c7d4c451f49d8253993e9 "" "main.tex" 1757949778.05137 187 67ba5ae29f0e910e3ba112163c915ffd ""
"state-of-the-art/v1.tex" 1757904281.15369 10205 c2111caf8273a3ffa8af4fb77055937b "" "state-of-the-art/v2.tex" 1757950266.45116 10918 a65147e24336b6a318bf18223339313e ""
(generated) (generated)
"main.aux" "main.aux"
"main.log" "main.log"

22
Writing/ERLM/main.fls
View File

@ -416,9 +416,11 @@ 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/ptmri8r.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmb7t.vf 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/tfm/adobe/times/ptmb8r.tfm
INPUT ./state-of-the-art/v1.tex INPUT ./state-of-the-art/v2.tex
INPUT ./state-of-the-art/v1.tex INPUT ./state-of-the-art/v2.tex
INPUT state-of-the-art/v1.tex INPUT ./state-of-the-art/v2.tex
INPUT ./state-of-the-art/v2.tex
INPUT state-of-the-art/v2.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/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
@ -450,20 +452,24 @@ 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/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/cm/cmsy10.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/rsfs/rsfs10.tfm INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/rsfs/rsfs10.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/zptmcm7m.vf INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmss12.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/psyro.tfm INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmss9.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmmi10.tfm INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmss8.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmri8r.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/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/ts1ptm.fd
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/ts1ptm.fd
INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/ts1ptm.fd
INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmr8c.tfm
INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/times/ptmr8c.vf
INPUT ./main.bbl INPUT ./main.bbl
INPUT ./main.bbl INPUT ./main.bbl
INPUT main.bbl INPUT main.bbl
INPUT main.aux 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/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/cmr10.pfb
INPUT /usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmss12.pfb
INPUT /usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb INPUT /usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb
INPUT /usr/share/texlive/texmf-dist/fonts/type1/public/rsfs/rsfs10.pfb
INPUT /usr/share/texlive/texmf-dist/fonts/type1/urw/symbol/usyr.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/utmb8a.pfb
INPUT /usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmr8a.pfb INPUT /usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmr8a.pfb

38
Writing/ERLM/main.log
View File

@ -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 22:47 This is pdfTeX, Version 3.141592653-2.6-1.40.25 (TeX Live 2023/Debian) (preloaded format=pdflatex 2024.9.11) 15 SEP 2025 11:31
entering extended mode entering extended mode
restricted \write18 enabled. restricted \write18 enabled.
file:line:error style messages enabled. file:line:error style messages enabled.
@ -876,36 +876,36 @@ LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <8> not available
(Font) Font shape `OT1/ptm/b/n' tried instead on input line 5. (Font) Font shape `OT1/ptm/b/n' tried instead on input line 5.
[1 [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]) [2] (./state-of-the-art/v1.tex {/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]) [2] (./state-of-the-art/v2.tex
LaTeX Font Info: Font shape `OT1/ptm/bx/n' in size <12> not available 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 22. (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 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 22. (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 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 22. (Font) Font shape `OT1/ptm/b/n' tried instead on input line 15.
[3] [4]) (./main.bbl [3] [4]
LaTeX Font Info: Trying to load font information for TS1+ptm on input line 168.
LaTeX Warning: Empty `thebibliography' environment on input line 3. (/usr/share/texlive/texmf-dist/tex/latex/psnfss/ts1ptm.fd
File: ts1ptm.fd 2001/06/04 font definitions for TS1/ptm.
) [5] (./main.aux) )) [5] (./main.bbl) [6] (./main.aux)
*********** ***********
LaTeX2e <2023-11-01> patch level 1 LaTeX2e <2023-11-01> patch level 1
L3 programming layer <2024-01-22> L3 programming layer <2024-01-22>
*********** ***********
) )
Here is how much of TeX's memory you used: Here is how much of TeX's memory you used:
25360 strings out of 476182 25409 strings out of 476182
526866 string characters out of 5795595 527716 string characters out of 5795595
1935975 words of memory out of 5000000 1934975 words of memory out of 5000000
46813 multiletter control sequences out of 15000+600000 46858 multiletter control sequences out of 15000+600000
591423 words of font info for 107 fonts, out of 8000000 for 9000 590786 words of font info for 108 fonts, out of 8000000 for 9000
14 hyphenation exceptions out of 8191 14 hyphenation exceptions out of 8191
110i,9n,107p,1008b,285s stack positions out of 10000i,1000n,20000p,200000b,200000s 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/cmsy10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/rsfs/rsfs10.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/symbol/usyr.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmb8a.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmr8a.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmri8a.pfb> </usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/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 (6 pages, 94940 bytes). Output written on main.pdf (7 pages, 108704 bytes).
PDF statistics: PDF statistics:
91 PDF objects out of 1000 (max. 8388607) 96 PDF objects out of 1000 (max. 8388607)
50 compressed objects within 1 object stream 54 compressed objects within 1 object stream
0 named destinations out of 1000 (max. 500000) 0 named destinations out of 1000 (max. 500000)
109 words of extra memory for PDF output out of 10000 (max. 10000000) 109 words of extra memory for PDF output out of 10000 (max. 10000000)

BIN
Writing/ERLM/main.pdf
View File

Binary file not shown.

BIN
Writing/ERLM/main.synctex.gz
View File

Binary file not shown.

3
Writing/ERLM/main.tex
View File

@ -6,8 +6,9 @@
\input{goals-and-outcomes/v4} \input{goals-and-outcomes/v4}
\newpage \newpage
\input{state-of-the-art/v1.tex} \input{state-of-the-art/v2}
\newpage
\bibliography{references} \bibliography{references}
\end{document} \end{document}

310
Writing/ERLM/references.bib
View File

@ -0,0 +1,310 @@
% Foundational Papers
@article{alur1995algorithmic,
title={The algorithmic analysis of hybrid systems},
author={Alur, Rajeev and Courcoubetis, Costas and Halbwachs, Nicolas and Henzinger, Thomas A and Ho, Pei-Hsin and Nicollin, Xavier and Olivero, Alfredo and Sifakis, Joseph and Yovine, Sergio},
journal={Theoretical Computer Science},
volume={138},
number={1},
pages={3--34},
year={1995},
publisher={Elsevier}
}
@inproceedings{alur1993hybrid,
title={Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems},
author={Alur, Rajeev and Courcoubetis, Costas and Henzinger, Thomas A and Ho, Pei-Hsin},
booktitle={Hybrid Systems},
pages={209--229},
year={1993},
publisher={Springer}
}
@article{mitchell2005time,
title={A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games},
author={Mitchell, Ian M and Bayen, Alexandre M and Tomlin, Claire J},
journal={IEEE Transactions on Automatic Control},
volume={50},
number={7},
pages={947--957},
year={2005},
publisher={IEEE}
}
@article{platzer2008differential,
title={Differential dynamic logic for hybrid systems},
author={Platzer, Andr{\'e}},
journal={Journal of Automated Reasoning},
volume={41},
number={2},
pages={143--189},
year={2008},
publisher={Springer}
}
@article{platzer2017complete,
title={A complete uniform substitution calculus for differential dynamic logic},
author={Platzer, Andr{\'e}},
journal={Journal of Automated Reasoning},
volume={59},
number={2},
pages={219--265},
year={2017},
publisher={Springer}
}
@inproceedings{donze2010robust,
title={Robust satisfaction of temporal logic over real-valued signals},
author={Donz{\'e}, Alexandre and Maler, Oded},
booktitle={International Conference on Formal Modeling and Analysis of Timed Systems},
pages={92--106},
year={2010},
publisher={Springer}
}
% Control Theory and Stability
@article{geromel2006stability,
title={Stability and stabilization of continuous-time switched linear systems},
author={Geromel, Jos{\'e} C and Colaneri, Patrizio},
journal={SIAM Journal on Control and Optimization},
volume={45},
number={5},
pages={1915--1930},
year={2006},
publisher={SIAM}
}
@book{liberzon2003switching,
title={Switching in systems and control},
author={Liberzon, Daniel},
year={2003},
publisher={Birkh{\"a}user Boston}
}
@article{branicky1998multiple,
title={Multiple Lyapunov functions and other analysis tools for switched and hybrid systems},
author={Branicky, Michael S},
journal={IEEE Transactions on Automatic Control},
volume={43},
number={4},
pages={475--482},
year={1998},
publisher={IEEE}
}
% Recent Advances (2020-2025)
@article{yang2024learning,
title={Learning Local Control Barrier Functions for Hybrid Systems},
author={Yang, Shuo and Chen, Yiwei and Yin, Xiang and Mangharam, Rahul},
journal={arXiv preprint arXiv:2401.14907},
year={2024}
}
@inproceedings{su2024switching,
title={Switching Controller Synthesis for Hybrid Systems Against STL Formulas},
author={Su, Mingyu and Vizel, Yakir and Vardi, Moshe Y},
booktitle={International Symposium on Formal Methods},
pages={231--248},
year={2024},
publisher={Springer}
}
@article{yao2024model,
title={Model predictive control of stochastic hybrid systems with signal temporal logic constraints},
author={Yao, Li and Wang, Yiming and Chen, Xiang},
journal={Automatica},
volume={159},
pages={111037},
year={2024},
publisher={Elsevier}
}
@article{yu2024online,
title={Online control synthesis for uncertain systems under signal temporal logic specifications},
author={Yu, Pian and Gao, Yulong and Jiang, Frank J and Johansson, Karl H and Dimarogonas, Dimos V},
journal={The International Journal of Robotics Research},
volume={43},
number={3},
pages={284--307},
year={2024},
publisher={SAGE}
}
% Tools and Frameworks
@inproceedings{meyer2018strix,
title={Strix: Explicit reactive synthesis strikes back!},
author={Meyer, Philipp J and Luttenberger, Michael},
booktitle={International Conference on Computer Aided Verification},
pages={578--586},
year={2018},
publisher={Springer}
}
@techreport{giannakopoulou2022fret,
title={Capturing and Analyzing Requirements with FRET},
author={Giannakopoulou, Dimitra and Mavridou, Anastasia and Rhein, Julian and Pressburger, Thomas and Schumann, Johann and Shi, Nija},
institution={NASA Ames Research Center},
year={2022},
number={NASA/TM-20220007610}
}
@inproceedings{fulton2015keymaera,
title={KeYmaera X: An axiomatic tactical theorem prover for hybrid systems},
author={Fulton, Nathan and Mitsch, Stefan and Quesel, Jan-David and V{\"o}lp, Marcus and Platzer, Andr{\'e}},
booktitle={International Conference on Automated Deduction},
pages={527--538},
year={2015},
publisher={Springer}
}
@inproceedings{frehse2011spaceex,
title={SpaceEx: Scalable verification of hybrid systems},
author={Frehse, Goran and Le Guernic, Colas and Donz{\'e}, Alexandre and Cotton, Scott and Ray, Rajarshi and Lebeltel, Olivier and Ripado, Rodolfo and Girard, Antoine and Dang, Thao and Maler, Oded},
booktitle={International Conference on Computer Aided Verification},
pages={379--395},
year={2011},
publisher={Springer}
}
@inproceedings{chen2013flow,
title={Flow*: An analyzer for non-linear hybrid systems},
author={Chen, Xin and {\'A}brah{\'a}m, Erika and Sankaranarayanan, Sriram},
booktitle={International Conference on Computer Aided Verification},
pages={258--263},
year={2013},
publisher={Springer}
}
@inproceedings{larsen1997uppaal,
title={UPPAAL in a nutshell},
author={Larsen, Kim G and Pettersson, Paul and Yi, Wang},
journal={International Journal on Software Tools for Technology Transfer},
volume={1},
number={1-2},
pages={134--152},
year={1997},
publisher={Springer}
}
% Reachability and Verification
@INPROCEEDINGS{bansal2017hamilton,
author={Bansal, Somil and Chen, Mo and Herbert, Sylvia and Tomlin, Claire J.},
booktitle={2017 IEEE 56th Annual Conference on Decision and Control (CDC)},
title={Hamilton-Jacobi reachability: A brief overview and recent advances},
year={2017},
volume={},
pages={2242-2253},
keywords={Games;Safety;Tools;Trajectory;Tutorials;Level set;Aircraft},
doi={10.1109/CDC.2017.8263977}
}
@article{althoff2021set,
title={Set propagation techniques for reachability analysis},
author={Althoff, Matthias and Frehse, Goran and Girard, Antoine},
journal={Annual Review of Control, Robotics, and Autonomous Systems},
volume={4},
pages={369--395},
year={2021},
publisher={Annual Reviews}
}
@inproceedings{tabuada2004compositional,
title={Compositional abstractions of hybrid control systems},
author={Tabuada, Paulo and Pappas, George J and Lima, Pedro},
journal={Discrete Event Dynamic Systems},
volume={14},
number={2},
pages={203--238},
year={2004},
publisher={Springer}
}
% Applications
@article{varaiya1993smart,
title={Smart cars on smart roads: Problems of control},
author={Varaiya, Pravin},
journal={IEEE Transactions on Automatic Control},
volume={38},
number={2},
pages={195--207},
year={1993},
publisher={IEEE}
}
@article{verlinden2024hybrid,
title={Hybrid reliability modeling of nuclear safety systems: A case study on the reactor protection system of a research reactor},
author={Verlinden, S and Deridder, F and Wagemans, P},
journal={Nuclear Engineering and Design},
volume={417},
pages={112868},
year={2024},
publisher={Elsevier}
}
% Competitions and Benchmarks
@inproceedings{hscc2024proceedings,
title={Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control},
booktitle={HSCC '24},
year={2024},
publisher={ACM},
address={New York, NY, USA}
}
@inproceedings{jacobs2017syntcomp,
title={The 4th reactive synthesis competition (SYNTCOMP 2017): Benchmarks, participants \& results},
author={Jacobs, Swen and Bloem, Roderick and Brenguier, Romain and others},
booktitle={6th Workshop on Synthesis},
year={2017},
series={EPTCS},
volume={260}
}
% Supporting Papers
@article{wabersich2018linear,
title={Linear model predictive safety certification for learning-based control},
author={Wabersich, Kim P and Zeilinger, Melanie N},
journal={Automatica},
volume={97},
pages={48--59},
year={2018},
publisher={Elsevier}
}
@inproceedings{prajna2004safety,
title={Safety verification of hybrid systems using barrier certificates},
author={Prajna, Stephen and Jadbabaie, Ali},
booktitle={International Workshop on Hybrid Systems: Computation and Control},
pages={477--492},
year={2004},
publisher={Springer}
}
@article{ames2017control,
title={Control barrier function based quadratic programs for safety critical systems},
author={Ames, Aaron D and Xu, Xiangru and Grizzle, Jessy W and Tabuada, Paulo},
journal={IEEE Transactions on Automatic Control},
volume={62},
number={8},
pages={3861--3876},
year={2017},
publisher={IEEE}
}
@article{srinivasan2018control,
title={Control of mobile robots using barrier functions under temporal logic specifications},
author={Srinivasan, Mohit and Coogan, Samuel},
journal={IEEE Transactions on Robotics},
volume={37},
number={2},
pages={363--374},
year={2021},
publisher={IEEE}
}

195
Writing/ERLM/state-of-the-art/v2.tex Normal file
View File

@ -0,0 +1,195 @@
\section{State of the Art and Limits of Current Practice}
This research aims to advance high-assurance autonomous hybrid control systems
by bridging disparate approaches from control theory and computer science. While
both fields tackle hybrid system verification, they approach the problem from
fundamentally different perspectives. Control theory emphasizes performance and
stability, while computer science focuses on correctness through formal
verification. This gap represents both the primary challenge and the key
opportunity for intellectual contribution.
\subsection{Control Theory and Hybrid Systems}
Hybrid systems combine continuous dynamics (`flows') with discrete transitions
(`jumps'). Following the standard formulation, a hybrid system can be expressed as:
\begin{align}
\dot{x}(t) &= f(x(t), q(t), u(t)) \\
q(k+1) &= \nu(x(k), q(k), u(k))
\end{align}
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
the current continuous dynamics mode. The only constraint on $\nu(\cdot)$ is
avoiding Zeno behavior---infinite jumps in finite time. Our focus centers on
continuous autonomous hybrid systems, where continuous states remain unchanged
during jumps and no external control input is required. Physical systems
naturally exhibit this property---a nuclear reactor switching from warm-up to
load-following control cannot instantaneously change its temperature or rod
position.
An intuitive approach to building hybrid controllers is to stitch together
multiple simple controllers for different state space regions. This approach
creates significant verification challenges. Even with linear time-invariant
modes, global stability cannot be guaranteed using linear control theory alone.
Instead, researchers have developed Lyapunov-based approaches, though finding
appropriate Lyapunov functions remains challenging.
Stability conditions for switched linear systems
can provide necessary and sufficient conditions using multiple Lyapunov
functions~\cite{geromel2006stability}, but these methods require
restrictive assumptions. Individual Lyapunov functions must be monotonically
nonincreasing at every switching time, which proves impractical for many
real systems. Common Lyapunov functions face even stricter existence
conditions, often impossible for systems with fundamentally different
dynamics across modes~\cite{branicky1998multiple,liberzon2003switching}.
\textbf{LIMITATION: Lyapunov-based methods of ensuring stability are
prohibitively challenging to apply to hybrid control systems.} Finding Lyapunov
functions to prove stability in the sense of Lyapunov is not practical for
working with hybrid systems. Additional requirements on the Lyapunov functions
makes finding appropriate functions extremely difficult.
Reachability analysis offers an alternative verification approach by computing
system output ranges for given inputs. Unlike Lyapunov methods, reachability
extends naturally to nonlinear systems. Hamilton-Jacobi frameworks established
the mathematical foundation for computing reachable sets in continuous and
hybrid systems, enabling formal verification of safety-critical
applications~\cite{mitchell2005time}.
\textbf{LIMITATION: Reachability analysis is not scalable to large hybrid
systems.} Reachability analysis faces two critical limitations. First,
computational complexity grows exponentially with state dimension---current
methods remain limited to 6-8 dimensional systems despite recent algorithmic
advances. Second, approximation errors compound over long time horizons,
potentially rendering analysis meaningless for extended trajectories.
Zonotope-based methods suffer accuracy degradation when propagating across mode
boundaries, while ellipsoidal methods produce conservative over-approximations
that become increasingly pessimistic with each mode transition.
Recent work on using control barrier functions has improved hybrid system
verification efforts. Neural network based control barrier function
approximations achieve 10-100X speedup over classical Hamilton-Jacobi methods
while maintaining safety guarantees for 7-dimensional autonomous racing
systems~\cite{yang2024learning}. This breakthrough demonstrates that deep neural
networks can approximate Hamilton-Jacobi partial differential equations and
enables application to previously intractable high-dimensional systems, but
future work must address the explainability problem for neural networks to
ensure control barrier functions are valid.
\subsection{Formal Methods and Reactive Synthesis}
Correctness requirements are specified using temporal logic, which captures
system behaviors through temporal relations. Linear Temporal Logic (LTL)
provides four fundamental operators: next ($\mathsf{X}$), eventually
($\mathsf{F}$), globally ($\mathsf{G}$), and until ($\mathsf{U}$).
Consider a nuclear reactor SCRAM requirement:
\vspace{0.2cm}
\textit{Natural language}: ``If a high temperature alarm triggers, control
rods must immediately insert and remain inserted until operator reset.''
\vspace{0.2cm}
This plain language requirement can be translated into a rigorous logical
specification.
\vspace{0.2cm}
\textit{LTL specification}:
\begin{equation}
\mathsf{G}(\text{HighTemp} \rightarrow
\mathsf{X}(\text{RodsInserted} \land
(\neg\text{RodsWithdrawn} \; \mathsf{U} \; \text{OperatorReset})))
\end{equation}
Once requirements are translated into these logical specifications, they can be
checked using computational tools. Cyber-physical systems naturally exhibit
discrete behavior amenable to formal analysis. Systems with finite states can be
modeled as finite state machines, where all possible states and transitions are
explicitly enumerable as logical specifications. This enables exhaustive
verification through model checking---a technique extensively employed in
high-assurance digital systems and safety-critical software. This mathematical
framework has been extended to hybrid automata~\cite{alur1993hybrid}, which
established the standard model combining discrete control graphs with continuous
dynamics. Hybrid automata bridge program-analysis techniques to hybrid systems
with infinite state spaces through symbolic model-checking based on reachability
analysis~\cite{alur1995algorithmic} but are not scalable for the same
limitations mentioned earlier with other reachability techniques.
% Signal Temporal Logic (STL) extends temporal logic to continuous-time signals
% with quantitative semantics~\cite{donze2010robust}. This enables specification
% of real-valued signal properties crucial for cyber-physical systems. Recent
% advances by Su et al. provide the first systematic STL synthesis approach with
% formal correctness guarantees for hybrid systems~\cite{su2024switching}.
NASA's Formal Requirements Elicitation Tool (FRET) bridges natural language
and mathematical specifications through FRETish---a structured English-like
language automatically translatable to temporal logic~\cite{giannakopoulou2022fret}.
FRET enables hierarchical requirement organization, realizability checking for
specification conflicts, integration with verification tools like CoCoSim, and
runtime monitoring through their Copilot tool.
From realizable specifications, reactive synthesis tools automatically generate
controllers. The Reactive Synthesis Competition (SYNTCOMP) has driven
algorithmic improvements for over a decade, with tools like Strix dominating
recent competitions through efficient parity game
solving~\cite{meyer2018strix,jacobs2017syntcomp}. Strix is able to translate
linear temporal logic specifications into deterministic automata automatically
while maximizing generated automata quality.
\textbf{LIMITATION: Unexplored application of temporal logic requirements in
nuclear control.} Despite extensive nuclear power documentation and mature
reactive synthesis tools, little work has combined these for nuclear
control applications. Nuclear procedures are written in structured natural
language that maps well to temporal logic, yet the synthesis community has not
engaged with this domain. This represents a significant unexplored opportunity
where formal methods could provide immediate practical impact.
% \textbf{[NEW CONTENT - Current Tool Capabilities]}
% Strix has won first place in all LTL tracks since 2018 by combining:
% \begin{itemize}
% \item Direct LTL-to-deterministic parity automata translation
% \item Multi-threaded explicit state solving
% \item Efficient automata minimization
% \item Strategy iteration for intermediate games
% \end{itemize}
Hybrid automata extend finite automata by representing discrete states as
control modes with continuous dynamics. Transitions between nodes indicate
discrete state changes through $\nu(\cdot)$ execution. This provides intuitive
graphical representation of mode switching logic. Differential dynamic logic
(dL) expands this idea and offers the most complete logical foundation for
hybrid verification. dL introduced two key
modalities~\cite{platzer2008differential,platzer2017complete}:
\begin{itemize}
\item Box modality $[\alpha]\phi$: for all executions of hybrid system $\alpha$, property $\phi$ holds
\item Diamond modality
$\langle\alpha\rangle\phi$: there exists an execution of $\alpha$ where $\phi$ holds
\end{itemize}
These modalities enable direct reasoning about hybrid systems including
continuous dynamics. The KeYmaera X theorem prover implements dL through
axiomatic tactical proving, successfully verifying collision avoidance in
train and aircraft control~\cite{fulton2015keymaera}.
\textbf{LIMITATION: There is a high expertise barrier for dL verification, and
scalability remains an issue.}
While dL is expressive enough for any hybrid behavior, verification requires
expertise in differential equations, logical specifications, and sequent
calculus. The proof effort remains challenging even with automated assistance.
Users must understand both the mathematical intricacies of their system and
the logical framework, then guide the prover through complex proof steps.
This expertise barrier prevents wider adoption despite the framework's
theoretical completeness.
The state of the art reveals a field in transition. Traditional boundaries
between control theory and formal methods are dissolving through
learning-based approaches and compositional techniques. While fundamental
challenges remain---particularly scalability and the theory-practice
gap---the convergence of approaches promises to enable verification and
synthesis for systems of unprecedented complexity. The next section
describes how this research will contribute to bridging these gaps
through unified synthesis frameworks applied to nuclear reactor control.