diff --git a/Writing/ERLM/main.aux b/Writing/ERLM/main.aux index 7bbf8806..badf478d 100644 --- a/Writing/ERLM/main.aux +++ b/Writing/ERLM/main.aux @@ -2,10 +2,32 @@ \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} +\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 } -\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 } +\citation{platzer2008differential,platzer2017complete} +\citation{fulton2015keymaera} \bibdata{references} -\@writefile{toc}{\contentsline {section}{References}{5}{}\protected@file@percent } -\gdef \@abspage@last{6} +\bibcite{geromel2006stability}{1} +\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} diff --git a/Writing/ERLM/main.bbl b/Writing/ERLM/main.bbl index 9b431fad..80e7178e 100644 --- a/Writing/ERLM/main.bbl +++ b/Writing/ERLM/main.bbl @@ -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} diff --git a/Writing/ERLM/main.blg b/Writing/ERLM/main.blg index 5b8bc642..2c4c14ca 100644 --- a/Writing/ERLM/main.blg +++ b/Writing/ERLM/main.blg @@ -2,47 +2,45 @@ This is BibTeX, Version 0.99d (TeX Live 2023/Debian) Capacity: max_strings=200000, hash_size=200000, hash_prime=170003 The top-level auxiliary file: main.aux The style file: unsrt.bst -I found no \citation commands---while reading file main.aux Database file #1: references.bib -You've used 0 entries, +You've used 13 entries, 1791 wiz_defined-function locations, - 445 strings with 3516 characters, -and the built_in function-call counts, 18 in all, are: -= -- 0 -> -- 0 -< -- 0 -+ -- 0 -- -- 0 -* -- 2 -:= -- 7 -add.period$ -- 0 -call.type$ -- 0 -change.case$ -- 0 + 530 strings with 5916 characters, +and the built_in function-call counts, 3422 in all, are: += -- 313 +> -- 151 +< -- 5 ++ -- 56 +- -- 43 +* -- 238 +:= -- 530 +add.period$ -- 42 +call.type$ -- 13 +change.case$ -- 12 chr.to.int$ -- 0 -cite$ -- 0 -duplicate$ -- 0 -empty$ -- 1 -format.name$ -- 0 -if$ -- 1 +cite$ -- 13 +duplicate$ -- 155 +empty$ -- 329 +format.name$ -- 43 +if$ -- 770 int.to.chr$ -- 0 -int.to.str$ -- 0 -missing$ -- 0 -newline$ -- 3 -num.names$ -- 0 -pop$ -- 0 +int.to.str$ -- 13 +missing$ -- 13 +newline$ -- 68 +num.names$ -- 13 +pop$ -- 39 preamble$ -- 1 purify$ -- 0 quote$ -- 0 -skip$ -- 1 +skip$ -- 73 stack$ -- 0 -substring$ -- 0 -swap$ -- 0 -text.length$ -- 0 +substring$ -- 243 +swap$ -- 46 +text.length$ -- 5 text.prefix$ -- 0 top$ -- 0 type$ -- 0 warning$ -- 0 -while$ -- 0 -width$ -- 0 -write$ -- 2 -(There was 1 error message) +while$ -- 34 +width$ -- 15 +write$ -- 146 diff --git a/Writing/ERLM/main.fdb_latexmk b/Writing/ERLM/main.fdb_latexmk index d1a8f4c1..bfe1d825 100644 --- a/Writing/ERLM/main.fdb_latexmk +++ b/Writing/ERLM/main.fdb_latexmk @@ -1,14 +1,14 @@ # Fdb version 4 -["bibtex main"] 1757903957.85967 "main.aux" "main.bbl" "main" 1757904436.44498 0 - "./references.bib" 1757896122.21556 0 d41d8cd98f00b204e9800998ecf8427e "" +["bibtex main"] 1757950134.83183 "main.aux" "main.bbl" "main" 1757950267.92325 0 + "./references.bib" 1757949790.55852 9415 fb740c67337f78e30e95f745a7cf3dae "" "/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) "main.bbl" "main.blg" (rewritten before read) -["pdflatex"] 1757904435.2107 "main.tex" "main.pdf" "main" 1757904436.44541 0 - "/etc/texmf/web2c/texmf.cnf" 1722610814.59577 475 c0e671620eb5563b2130f56340a5fde8 "" +["pdflatex"] 1757950267.45324 "main.tex" "main.pdf" "main" 1757950267.9234 0 + "/etc/texmf/web2c/texmf.cnf" 1726065852.27662 475 c0e671620eb5563b2130f56340a5fde8 "" "/usr/share/texlive/texmf-dist/fonts/enc/dvips/base/8r.enc" 1165713224 4850 80dc9bab7f31fb78a000ccfed0e27cab "" "/usr/share/texlive/texmf-dist/fonts/map/fontname/texfonts.map" 1577235249 3524 cb3e574dea2d1052e39280babc910dc8 "" "/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/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/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/ptmri7t.tfm" 1136768653 2288 f478fc8fed18759effb59f3dad7f3084 "" "/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/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/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/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/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/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/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/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/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/zptmcm7m.vf" 1136768653 1132 27520247d3fe18d4266a226b461885c2 "" "/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/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/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/standalone/standalone.sty" 1665433651 34855 01a6d48b146a4c824944925004b07205 "" "/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/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/web2c/pdftex/pdflatex.fmt" 1726005817 6800784 2b63e5a224c5ad740802d8f9921962c1 "" - "dane_proposal_format.cls" 1757904433.20297 2553 3bbf169a90a50515ed103fe388c111f0 "" - "goals-and-outcomes/v4.tex" 1757896122.20856 5764 a67e489f9ea8343564010d217ae37ec2 "" - "main.aux" 1757904436.24501 759 9d0c4909d3a06d061361cd5dd469f219 "pdflatex" - "main.bbl" 1757903957.88911 49 0eba253fc001332e731e8aba3f23127b "bibtex main" - "main.tex" 1757896122.21556 182 46aa668f839c7d4c451f49d8253993e9 "" - "state-of-the-art/v1.tex" 1757904281.15369 10205 c2111caf8273a3ffa8af4fb77055937b "" + "/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map" 1726065856.46263 128028 f533b797fba58d231669ea19e894e23e "" + "/var/lib/texmf/web2c/pdftex/pdflatex.fmt" 1726065868 6800790 607442c924ed54405961d2b8ac2a25ae "" + "dane_proposal_format.cls" 1757942776.53402 2553 3bbf169a90a50515ed103fe388c111f0 "" + "goals-and-outcomes/v4.tex" 1757864250.3119 5764 a67e489f9ea8343564010d217ae37ec2 "" + "main.aux" 1757950267.84363 1476 86aee14919487c57b3ce6714b0985bff "pdflatex" + "main.bbl" 1757950134.84155 3170 7f578afdcd1e73f308616474dc5a4003 "bibtex main" + "main.tex" 1757949778.05137 187 67ba5ae29f0e910e3ba112163c915ffd "" + "state-of-the-art/v2.tex" 1757950266.45116 10918 a65147e24336b6a318bf18223339313e "" (generated) "main.aux" "main.log" diff --git a/Writing/ERLM/main.fls b/Writing/ERLM/main.fls index 55345489..eeeb6c56 100644 --- a/Writing/ERLM/main.fls +++ b/Writing/ERLM/main.fls @@ -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/vf/adobe/times/ptmb7t.vf INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/times/ptmb8r.tfm -INPUT ./state-of-the-art/v1.tex -INPUT ./state-of-the-art/v1.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 ./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 @@ -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/tfm/public/cm/cmsy10.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/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/tfm/public/cm/cmss12.tfm +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/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.aux INPUT /usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb INPUT /usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb +INPUT /usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmss12.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/times/utmb8a.pfb INPUT /usr/share/texlive/texmf-dist/fonts/type1/urw/times/utmr8a.pfb diff --git a/Writing/ERLM/main.log b/Writing/ERLM/main.log index b0897570..59b2b49e 100644 --- a/Writing/ERLM/main.log +++ b/Writing/ERLM/main.log @@ -1,4 +1,4 @@ -This is pdfTeX, Version 3.141592653-2.6-1.40.25 (TeX Live 2023/Debian) (preloaded format=pdflatex 2024.9.10) 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 restricted \write18 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. [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 -(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 -(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 -(Font) Font shape `OT1/ptm/b/n' tried instead on input line 22. - [3] [4]) (./main.bbl - -LaTeX Warning: Empty `thebibliography' environment on input line 3. - -) [5] (./main.aux) +(Font) Font shape `OT1/ptm/b/n' tried instead on input line 15. + [3] [4] +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 +File: ts1ptm.fd 2001/06/04 font definitions for TS1/ptm. +)) [5] (./main.bbl) [6] (./main.aux) *********** LaTeX2e <2023-11-01> patch level 1 L3 programming layer <2024-01-22> *********** ) Here is how much of TeX's memory you used: - 25360 strings out of 476182 - 526866 string characters out of 5795595 - 1935975 words of memory out of 5000000 - 46813 multiletter control sequences out of 15000+600000 - 591423 words of font info for 107 fonts, out of 8000000 for 9000 + 25409 strings out of 476182 + 527716 string characters out of 5795595 + 1934975 words of memory out of 5000000 + 46858 multiletter control sequences out of 15000+600000 + 590786 words of font info for 108 fonts, out of 8000000 for 9000 14 hyphenation exceptions out of 8191 110i,9n,107p,1008b,285s stack positions out of 10000i,1000n,20000p,200000b,200000s - -Output written on main.pdf (6 pages, 94940 bytes). + +Output written on main.pdf (7 pages, 108704 bytes). PDF statistics: - 91 PDF objects out of 1000 (max. 8388607) - 50 compressed objects within 1 object stream + 96 PDF objects out of 1000 (max. 8388607) + 54 compressed objects within 1 object stream 0 named destinations out of 1000 (max. 500000) 109 words of extra memory for PDF output out of 10000 (max. 10000000) diff --git a/Writing/ERLM/main.pdf b/Writing/ERLM/main.pdf index f741bc6a..fbd5cb77 100644 Binary files a/Writing/ERLM/main.pdf and b/Writing/ERLM/main.pdf differ diff --git a/Writing/ERLM/main.synctex.gz b/Writing/ERLM/main.synctex.gz index bd0fa512..6b78612c 100644 Binary files a/Writing/ERLM/main.synctex.gz and b/Writing/ERLM/main.synctex.gz differ diff --git a/Writing/ERLM/main.tex b/Writing/ERLM/main.tex index 6b7eb136..6a15ea35 100644 --- a/Writing/ERLM/main.tex +++ b/Writing/ERLM/main.tex @@ -6,8 +6,9 @@ \input{goals-and-outcomes/v4} \newpage -\input{state-of-the-art/v1.tex} +\input{state-of-the-art/v2} +\newpage \bibliography{references} \end{document} diff --git a/Writing/ERLM/references.bib b/Writing/ERLM/references.bib index e69de29b..02e37d0c 100644 --- a/Writing/ERLM/references.bib +++ b/Writing/ERLM/references.bib @@ -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} +} diff --git a/Writing/ERLM/state-of-the-art/v2.tex b/Writing/ERLM/state-of-the-art/v2.tex new file mode 100644 index 00000000..9b60feda --- /dev/null +++ b/Writing/ERLM/state-of-the-art/v2.tex @@ -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.