diff --git a/.task/backlog.data b/.task/backlog.data index 7be9eeb3..4b5dcba7 100644 --- a/.task/backlog.data +++ b/.task/backlog.data @@ -31,3 +31,5 @@ {"description":"Read Branicky Lyapunov paper","entry":"20250911T183429Z","modified":"20250911T200147Z","project":"Thesis","start":"20250911T200147Z","status":"pending","uuid":"f4d32147-ec74-4f68-b8d5-146c0b6f35df","tags":["reading"]} {"description":"Write first draft of state of the art","due":"20250912T040000Z","entry":"20250909T203258Z","modified":"20250911T200235Z","project":"ERLM","status":"pending","uuid":"4bec1530-18bc-43cb-9f0b-61e35dbf1730","tags":["writing"],"depends":["8e7a8e19-9197-4008-b7d9-521ffcf7ba91","96c76e6b-5c33-4f54-a156-5c59e718f01a","f4d32147-ec74-4f68-b8d5-146c0b6f35df"]} {"description":"Read Branicky Lyapunov paper","entry":"20250911T183429Z","modified":"20250911T201816Z","project":"Thesis","status":"pending","uuid":"f4d32147-ec74-4f68-b8d5-146c0b6f35df","tags":["reading"]} +{"description":"Read Branicky Lyapunov paper","end":"20250914T153618Z","entry":"20250911T183429Z","modified":"20250914T153618Z","project":"Thesis","status":"completed","uuid":"f4d32147-ec74-4f68-b8d5-146c0b6f35df","tags":["reading"]} +{"description":"Write first draft of state of the art","due":"20250912T040000Z","entry":"20250909T203258Z","modified":"20250914T153645Z","project":"ERLM","start":"20250914T153645Z","status":"pending","uuid":"4bec1530-18bc-43cb-9f0b-61e35dbf1730","tags":["writing"],"depends":["8e7a8e19-9197-4008-b7d9-521ffcf7ba91","96c76e6b-5c33-4f54-a156-5c59e718f01a","f4d32147-ec74-4f68-b8d5-146c0b6f35df"]} diff --git a/.task/completed.data b/.task/completed.data index 6dd6daf1..2590105f 100644 --- a/.task/completed.data +++ b/.task/completed.data @@ -1,3 +1,4 @@ +[description:"Read Branicky Lyapunov paper" end:"1757864178" entry:"1757615669" modified:"1757864178" project:"Thesis" status:"completed" tags:"reading" tags_reading:"x" uuid:"f4d32147-ec74-4f68-b8d5-146c0b6f35df"] [description:"Follow up with Daniel about controls bootcamp" due:"1757563200" end:"1757618582" entry:"1757449130" modified:"1757618582" project:"FSAE" status:"completed" uuid:"3eaadead-4e5e-4823-9077-16d6e1800862"] [description:"Follow up with Bajaj about writing TurboSAR paper" due:"1757563200" end:"1757618582" entry:"1757449286" modified:"1757618583" priority:"L" status:"completed" uuid:"fa2699f9-0082-433e-ae0d-cc2553db9865"] [description:"Write outline for state of the art" due:"1757476800" end:"1757516746" entry:"1757443175" modified:"1757516746" project:"ERLM" status:"completed" uuid:"8e7a8e19-9197-4008-b7d9-521ffcf7ba91"] diff --git a/.task/pending.data b/.task/pending.data index a1074898..507d7da8 100644 --- a/.task/pending.data +++ b/.task/pending.data @@ -2,7 +2,6 @@ [description:"Write zettels about webofscience database" entry:"1757443242" modified:"1757443242" project:"zk" status:"pending" uuid:"9cb17c85-f1e6-4280-86da-a5af8f229b15"] [description:"Look over obsidian tasks and see if anything is worth moving over" entry:"1757443262" modified:"1757443262" status:"pending" tags:"taskwarrior" tags_taskwarrior:"x" uuid:"c1a5390d-5b84-4f9c-8acb-ffb970682660"] [description:"Look around for summer internships with national labs" entry:"1757449731" modified:"1757449731" status:"pending" uuid:"d3f3dc53-4feb-4b7e-8de5-86ebf3c535d5"] -[dep_8e7a8e19-9197-4008-b7d9-521ffcf7ba91:"x" dep_96c76e6b-5c33-4f54-a156-5c59e718f01a:"x" dep_f4d32147-ec74-4f68-b8d5-146c0b6f35df:"x" depends:"8e7a8e19-9197-4008-b7d9-521ffcf7ba91,96c76e6b-5c33-4f54-a156-5c59e718f01a,f4d32147-ec74-4f68-b8d5-146c0b6f35df" description:"Write first draft of state of the art" due:"1757649600" entry:"1757449978" modified:"1757620955" project:"ERLM" status:"pending" tags:"writing" tags_writing:"x" uuid:"4bec1530-18bc-43cb-9f0b-61e35dbf1730"] +[dep_8e7a8e19-9197-4008-b7d9-521ffcf7ba91:"x" dep_96c76e6b-5c33-4f54-a156-5c59e718f01a:"x" dep_f4d32147-ec74-4f68-b8d5-146c0b6f35df:"x" depends:"8e7a8e19-9197-4008-b7d9-521ffcf7ba91,96c76e6b-5c33-4f54-a156-5c59e718f01a,f4d32147-ec74-4f68-b8d5-146c0b6f35df" description:"Write first draft of state of the art" due:"1757649600" entry:"1757449978" modified:"1757864205" project:"ERLM" start:"1757864205" status:"pending" tags:"writing" tags_writing:"x" uuid:"4bec1530-18bc-43cb-9f0b-61e35dbf1730"] [description:"get FSAE COM and track data to Matt barry for statics problem. He also wants a cad model?" due:"1758254400" entry:"1757515988" modified:"1757515988" status:"pending" uuid:"48f997bf-b686-4c0b-bee5-ac8e5f874ad9"] [description:"Read Opportunities, Challenges, and Research Needs for Remote Microreactor Operations" entry:"1757516723" modified:"1757516723" project:"Thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"96c76e6b-5c33-4f54-a156-5c59e718f01a"] -[description:"Read Branicky Lyapunov paper" entry:"1757615669" modified:"1757621896" project:"Thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"f4d32147-ec74-4f68-b8d5-146c0b6f35df"] diff --git a/.task/undo.data b/.task/undo.data index 3804958d..96e195de 100644 --- a/.task/undo.data +++ b/.task/undo.data @@ -109,3 +109,11 @@ time 1757621896 old [description:"Read Branicky Lyapunov paper" entry:"1757615669" modified:"1757620907" project:"Thesis" start:"1757620907" status:"pending" tags:"reading" tags_reading:"x" uuid:"f4d32147-ec74-4f68-b8d5-146c0b6f35df"] new [description:"Read Branicky Lyapunov paper" entry:"1757615669" modified:"1757621896" project:"Thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"f4d32147-ec74-4f68-b8d5-146c0b6f35df"] --- +time 1757864178 +old [description:"Read Branicky Lyapunov paper" entry:"1757615669" modified:"1757621896" project:"Thesis" status:"pending" tags:"reading" tags_reading:"x" uuid:"f4d32147-ec74-4f68-b8d5-146c0b6f35df"] +new [description:"Read Branicky Lyapunov paper" end:"1757864178" entry:"1757615669" modified:"1757864178" project:"Thesis" status:"completed" tags:"reading" tags_reading:"x" uuid:"f4d32147-ec74-4f68-b8d5-146c0b6f35df"] +--- +time 1757864205 +old [dep_8e7a8e19-9197-4008-b7d9-521ffcf7ba91:"x" dep_96c76e6b-5c33-4f54-a156-5c59e718f01a:"x" dep_f4d32147-ec74-4f68-b8d5-146c0b6f35df:"x" depends:"8e7a8e19-9197-4008-b7d9-521ffcf7ba91,96c76e6b-5c33-4f54-a156-5c59e718f01a,f4d32147-ec74-4f68-b8d5-146c0b6f35df" description:"Write first draft of state of the art" due:"1757649600" entry:"1757449978" modified:"1757620955" project:"ERLM" status:"pending" tags:"writing" tags_writing:"x" uuid:"4bec1530-18bc-43cb-9f0b-61e35dbf1730"] +new [dep_8e7a8e19-9197-4008-b7d9-521ffcf7ba91:"x" dep_96c76e6b-5c33-4f54-a156-5c59e718f01a:"x" dep_f4d32147-ec74-4f68-b8d5-146c0b6f35df:"x" depends:"8e7a8e19-9197-4008-b7d9-521ffcf7ba91,96c76e6b-5c33-4f54-a156-5c59e718f01a,f4d32147-ec74-4f68-b8d5-146c0b6f35df" description:"Write first draft of state of the art" due:"1757649600" entry:"1757449978" modified:"1757864205" project:"ERLM" start:"1757864205" status:"pending" tags:"writing" tags_writing:"x" uuid:"4bec1530-18bc-43cb-9f0b-61e35dbf1730"] +--- diff --git a/Writing/ERLM/goals-and-outcomes/v4.tex b/Writing/ERLM/goals-and-outcomes/v4.tex index 52455425..f5cd8d7b 100644 --- a/Writing/ERLM/goals-and-outcomes/v4.tex +++ b/Writing/ERLM/goals-and-outcomes/v4.tex @@ -1,4 +1,4 @@ -\section{Goals and Outcomes - REVISED} +\section{Goals and Outcomes} The goal of this research is to develop a unified framework combining temporal logic synthesis with continuous-time verification methods to create autonomous diff --git a/Writing/ERLM/main.aux b/Writing/ERLM/main.aux index 3fd9047e..e8a7a953 100644 --- a/Writing/ERLM/main.aux +++ b/Writing/ERLM/main.aux @@ -1,7 +1,11 @@ \relax \bibstyle{unsrt} \providecommand \oddpage@label [2]{} -\@writefile{toc}{\contentsline {section}{\numberline {1}Goals and Outcomes - ORIGINAL}{1}{}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {2}Goals and Outcomes - REVISED}{2}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {1}Goals and Outcomes}{1}{}\protected@file@percent } \bibdata{references} +\@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}{}{}} +\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Formal Methods and Reactive Synthesis}{3}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{References}{3}{}\protected@file@percent } \gdef \@abspage@last{4} diff --git a/Writing/ERLM/main.bbl b/Writing/ERLM/main.bbl new file mode 100644 index 00000000..9b431fad --- /dev/null +++ b/Writing/ERLM/main.bbl @@ -0,0 +1,3 @@ +\begin{thebibliography}{} + +\end{thebibliography} diff --git a/Writing/ERLM/main.blg b/Writing/ERLM/main.blg new file mode 100644 index 00000000..5b8bc642 --- /dev/null +++ b/Writing/ERLM/main.blg @@ -0,0 +1,48 @@ +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, + 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 +chr.to.int$ -- 0 +cite$ -- 0 +duplicate$ -- 0 +empty$ -- 1 +format.name$ -- 0 +if$ -- 1 +int.to.chr$ -- 0 +int.to.str$ -- 0 +missing$ -- 0 +newline$ -- 3 +num.names$ -- 0 +pop$ -- 0 +preamble$ -- 1 +purify$ -- 0 +quote$ -- 0 +skip$ -- 1 +stack$ -- 0 +substring$ -- 0 +swap$ -- 0 +text.length$ -- 0 +text.prefix$ -- 0 +top$ -- 0 +type$ -- 0 +warning$ -- 0 +while$ -- 0 +width$ -- 0 +write$ -- 2 +(There was 1 error message) diff --git a/Writing/ERLM/main.fdb_latexmk b/Writing/ERLM/main.fdb_latexmk index ef429418..19f4820b 100644 --- a/Writing/ERLM/main.fdb_latexmk +++ b/Writing/ERLM/main.fdb_latexmk @@ -1,13 +1,13 @@ # Fdb version 4 -["bibtex main"] 0 "main.aux" "main.bbl" "main" 1757303867.80253 0 +["bibtex main"] 1757866412.20829 "main.aux" "main.bbl" "main" 1757880660.67738 0 + "./references.bib" 1757866237.16684 0 d41d8cd98f00b204e9800998ecf8427e "" "/usr/share/texlive/texmf-dist/bibtex/bst/base/unsrt.bst" 1292289607 18030 1376b4b231b50c66211e47e42eda2875 "" - "main.aux" 0 -1 0 "pdflatex" - "references.bib" 0 -1 0 "" + "main.aux" 1757880660.60211 759 c340ead263222262cc9d66ce4adc65f5 "pdflatex" (generated) "main.bbl" "main.blg" (rewritten before read) -["pdflatex"] 1757303867.36078 "main.tex" "main.pdf" "main" 1757303867.80269 0 +["pdflatex"] 1757880660.23063 "main.tex" "main.pdf" "main" 1757880660.67755 2 "/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 "" @@ -20,8 +20,10 @@ "/usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/cmextra/cmex7.tfm" 1246382020 1004 54797486969f23fa377b128694d548df "" "/usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/cmextra/cmex8.tfm" 1246382020 988 bdf658c3bfc2d96d3c8b02cfc1c94c20 "" "/usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm" 1246382020 916 f87d7c45f9c908e672703b83b72241a3 "" + "/usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam5.tfm" 1246382020 924 9904cf1d39e9767e7a3622f2a125a565 "" "/usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam7.tfm" 1246382020 928 2dc8d444221b7a635bb58038579b861a "" "/usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm" 1246382020 908 2921f8a10601f252058503cc6570e581 "" + "/usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm5.tfm" 1246382020 940 75ac932a52f80982a9f8ea75d03a34cf "" "/usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm7.tfm" 1246382020 940 228d6584342e91276bf566bcf9716b83 "" "/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmex10.tfm" 1136768653 992 662f679a0b3d2d53c1b94050fdaa3f50 "" "/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmmi12.tfm" 1136768653 1524 4414a8315f39513458b80dfc63bff03a "" @@ -33,6 +35,10 @@ "/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmsy10.tfm" 1136768653 1124 6c73e740cf17375f03eec0ee63599741 "" "/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmsy6.tfm" 1136768653 1116 933a60c408fc0a863a92debe84b2d294 "" "/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmsy8.tfm" 1136768653 1120 8b7d695260f3cff42e636090a8002094 "" + "/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/cmmi7.pfb" 1248133631 36281 c355509802a035cadc5f15869451dcee "" + "/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb" 1248133631 35752 024fb6c41858982481f6968b5fc26508 "" + "/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb" 1248133631 32569 5e5ddc8df908dea60932f3c484a54c0d "" "/usr/share/texlive/texmf-dist/fonts/type1/urw/helvetic/uhvb8a.pfb" 1136849748 35941 f27169cc74234d5bd5e4cca5abafaabb "" "/usr/share/texlive/texmf-dist/fonts/type1/urw/helvetic/uhvr8a.pfb" 1136849748 44648 23115b2a545ebfe2c526c3ca99db8b95 "" "/usr/share/texlive/texmf-dist/fonts/type1/urw/helvetic/uhvro8a.pfb" 1136849748 48169 b4fd9d908b9ee8c65d4305ad39071c5e "" @@ -221,11 +227,11 @@ "/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" 1757301721.12236 2553 19244c04b38f33ab00dc03e30ae573aa "" - "goals-and-outcomes/v3.tex" 1757301547.55586 5020 c5216608eb00ec52f636f47df96d88fd "" - "goals-and-outcomes/v4.tex" 1757301539.49861 5774 40dea2a21d87fa10f58a0ce7c8e4881d "" - "main.aux" 1757303867.72985 340 1aeb9229761d14b595ec7cdb9eb7ceac "pdflatex" - "main.bbl" 0 -1 0 "bibtex main" - "main.tex" 1757301579.18155 181 0c6850b2ae7bcb19fb526354d63edf4a "" + "goals-and-outcomes/v4.tex" 1757864250.3119 5764 a67e489f9ea8343564010d217ae37ec2 "" + "main.aux" 1757880660.60211 759 c340ead263222262cc9d66ce4adc65f5 "pdflatex" + "main.bbl" 1757866412.21917 49 0eba253fc001332e731e8aba3f23127b "bibtex main" + "main.tex" 1757864343.89345 182 46aa668f839c7d4c451f49d8253993e9 "" + "state-of-the-art/v1.tex" 1757880658.25282 4583 ec2578cb906d41d075eddddf82747de7 "" (generated) "main.aux" "main.log" diff --git a/Writing/ERLM/main.fls b/Writing/ERLM/main.fls index d2c63117..8f66f649 100644 --- a/Writing/ERLM/main.fls +++ b/Writing/ERLM/main.fls @@ -388,11 +388,11 @@ INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/helvetic/phvr7t.vf INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvr8r.tfm INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/helvetic/phvr7t.vf INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvr8r.tfm -INPUT ./goals-and-outcomes/v3.tex -INPUT ./goals-and-outcomes/v3.tex -INPUT ./goals-and-outcomes/v3.tex -INPUT ./goals-and-outcomes/v3.tex -INPUT goals-and-outcomes/v3.tex +INPUT ./goals-and-outcomes/v4.tex +INPUT ./goals-and-outcomes/v4.tex +INPUT ./goals-and-outcomes/v4.tex +INPUT ./goals-and-outcomes/v4.tex +INPUT goals-and-outcomes/v4.tex INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvb7t.tfm INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvb7t.tfm INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvro7t.tfm @@ -404,12 +404,25 @@ INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/helvetic/phvro7t.vf INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvro8r.tfm INPUT /usr/share/texlive/texmf-dist/fonts/vf/adobe/helvetic/phvb7t.vf INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvb8r.tfm -INPUT ./goals-and-outcomes/v4.tex -INPUT ./goals-and-outcomes/v4.tex -INPUT ./goals-and-outcomes/v4.tex -INPUT ./goals-and-outcomes/v4.tex -INPUT goals-and-outcomes/v4.tex +INPUT ./state-of-the-art/v1.tex +INPUT ./state-of-the-art/v1.tex +INPUT state-of-the-art/v1.tex +INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/cmextra/cmex7.tfm +INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/cmextra/cmex7.tfm +INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm +INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam7.tfm +INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam5.tfm +INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm +INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm7.tfm +INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm5.tfm +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/cmmi7.pfb +INPUT /usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb +INPUT /usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb INPUT /usr/share/texlive/texmf-dist/fonts/type1/urw/helvetic/uhvb8a.pfb INPUT /usr/share/texlive/texmf-dist/fonts/type1/urw/helvetic/uhvr8a.pfb INPUT /usr/share/texlive/texmf-dist/fonts/type1/urw/helvetic/uhvro8a.pfb diff --git a/Writing/ERLM/main.log b/Writing/ERLM/main.log index cb3b7e00..a80e99dd 100644 --- a/Writing/ERLM/main.log +++ b/Writing/ERLM/main.log @@ -1,4 +1,4 @@ -This is pdfTeX, Version 3.141592653-2.6-1.40.25 (TeX Live 2023/Debian) (preloaded format=pdflatex 2024.9.11) 7 SEP 2025 23:57 +This is pdfTeX, Version 3.141592653-2.6-1.40.25 (TeX Live 2023/Debian) (preloaded format=pdflatex 2024.9.11) 14 SEP 2025 16:11 entering extended mode restricted \write18 enabled. file:line:error style messages enabled. @@ -829,40 +829,73 @@ LaTeX Font Info: Trying to load font information for U+msb on input line 5. File: umsb.fd 2013/01/14 v3.01 AMS symbols B ) [1 -{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}{/usr/share/texlive/texmf-dist/fonts/enc/dvips/base/8r.enc}] (./goals-and-outcomes/v3.tex -LaTeX Font Info: Font shape `OT1/phv/m/it' in size <10> not available -(Font) Font shape `OT1/phv/m/sl' tried instead on input line 28. -) [1] (./goals-and-outcomes/v4.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 Overfull \hbox (10.54005pt too wide) in paragraph at lines 3--23 \OT1/phv/m/n/10 The goal of this re-search is to de-velop a uni-fied frame-work com-bin-ing tem-po-ral logic syn-the-sis with continuous- [] +LaTeX Font Info: Font shape `OT1/phv/m/it' in size <10> not available +(Font) Font shape `OT1/phv/m/sl' tried instead on input line 33. Overfull \hbox (8.5604pt too wide) in paragraph at lines 82--90 []\OT1/phv/b/n/10 Prove that hy-brid sys-tem im-ple-men-ta-tions achieve safety and per-for-mance spec-i-fi-ca-tions across [] -[2]) -No file main.bbl. -[3] (./main.aux) +[1]) [2] (./state-of-the-art/v1.tex +./state-of-the-art/v1.tex:34: Undefined control sequence. +l.34 ...us states and control input. \(\nu_i(\codt + )\) can be much more +The control sequence at the end of the top line +of your error message was never \def'ed. If you have +misspelled it (e.g., `\hobx'), type `I' and the correct +spelling (e.g., `I\hbox'). Otherwise just continue, +and I'll forget about whatever was undefined. + +./state-of-the-art/v1.tex:35: Undefined control sequence. +l.35 ...ted. The only restriction on \(\nu_i(\codt + )\) is that it must +The control sequence at the end of the top line +of your error message was never \def'ed. If you have +misspelled it (e.g., `\hobx'), type `I' and the correct +spelling (e.g., `I\hbox'). Otherwise just continue, +and I'll forget about whatever was undefined. + +./state-of-the-art/v1.tex:37: Undefined control sequence. +l.37 \(\nu_i(\codt + )\) can depend a control input \(u\), or can be +The control sequence at the end of the top line +of your error message was never \def'ed. If you have +misspelled it (e.g., `\hobx'), type `I' and the correct +spelling (e.g., `I\hbox'). Otherwise just continue, +and I'll forget about whatever was undefined. + +) (./main.bbl + +LaTeX Warning: Empty `thebibliography' environment on input line 3. + +) [3] (./main.aux) *********** LaTeX2e <2023-11-01> patch level 1 L3 programming layer <2024-01-22> *********** + + +LaTeX Warning: Label(s) may have changed. Rerun to get cross-references right. + ) Here is how much of TeX's memory you used: - 25280 strings out of 476182 - 525383 string characters out of 5795595 + 25303 strings out of 476182 + 525740 string characters out of 5795595 1938975 words of memory out of 5000000 - 46745 multiletter control sequences out of 15000+600000 - 574906 words of font info for 68 fonts, out of 8000000 for 9000 + 46762 multiletter control sequences out of 15000+600000 + 576605 words of font info for 76 fonts, out of 8000000 for 9000 14 hyphenation exceptions out of 8191 - 110i,6n,107p,1008b,285s stack positions out of 10000i,1000n,20000p,200000b,200000s - -Output written on main.pdf (4 pages, 36357 bytes). + 110i,9n,107p,1008b,285s stack positions out of 10000i,1000n,20000p,200000b,200000s + +Output written on main.pdf (4 pages, 72104 bytes). PDF statistics: - 60 PDF objects out of 1000 (max. 8388607) - 31 compressed objects within 1 object stream + 80 PDF objects out of 1000 (max. 8388607) + 43 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 ebaddf08..cf097090 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 32ae926b..01cc2ad4 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 a5c787a1..6b7eb136 100644 --- a/Writing/ERLM/main.tex +++ b/Writing/ERLM/main.tex @@ -4,10 +4,9 @@ \maketitle -\input{goals-and-outcomes/v3} - -\newpage \input{goals-and-outcomes/v4} +\newpage +\input{state-of-the-art/v1.tex} \bibliography{references} diff --git a/Writing/ERLM/references.bib b/Writing/ERLM/references.bib new file mode 100644 index 00000000..e69de29b diff --git a/Writing/ERLM/state-of-the-art/v1.tex b/Writing/ERLM/state-of-the-art/v1.tex index 248ec01a..08b13139 100644 --- a/Writing/ERLM/state-of-the-art/v1.tex +++ b/Writing/ERLM/state-of-the-art/v1.tex @@ -1,13 +1,75 @@ \section{State of the art and limits of current practice} -%Start with some discussion about what a hybrid system is. Lay it out with some -%knowledge about jumps and flow and what not. Lay down a mathematical -%preliminary here. +This research will improve our ability to build high assurance autonomous hybrid +control systems by connecting tools from different areas of the scientific +literature. We will combine control and dynamics theory of hybrid systems with +the discrete systems analysis found in the computer science space. These two +fields are disparate, but both approach the problem of high assurance hybrid +systems. First, we will discuss the control theory side. Hybrid systems from a +differential equation perspective will be considered, and comparisons to the +current state of the art of nuclear power control will be discussed. Then, we +will discuss approaches for discrete and hybrid systems from the logical and +computer science perspective. These gap between these two fields is the crux of +the intellectual merit of this research. -\subsection{Discrete Systems and Reactive Synthesis} +\subsection{Control Theory and Hybrid Systems} -% LIMITATION: Discrete synthesis is predicated upon +Hybrid systems have two components to their behavior. They have continuous +dynamics called 'flow', and have discrete dynamics called 'jumps'. Hybrid +systems can often be described as a set of differential and difference +equations. An hybrid system can be defined as follows: -\subsection{Continuous System Verification} +\begin{align} + \dot{x}(t) &= f(x(t), q(t), u(t)) \\ + q(k+1) &= \nu(x(k), q(k), u(k)) + \label{eq:hybrid-sys} +\end{align} -\subsection{Hybrid System Verification Approaches} +In this description there are two functions: \(f(\cdot)\) and +\(\nu(\cdot)\). \(f(\cdot)\) defines the continuous dynamics, while +\(\nu(\cdot)\) defines the discrete dynamics. These functions take three +inputs: the continuous states \(x\), the discrete state \(q\), and an optional +control input \(u\). \(f_i(\cdot)\) here is a nonlinear function, where \(q\) +changes the mode of the continuous dynamics, but is otherwise dependent on the +current continuous states and control input. \(\nu_i(\codt)\) can be much more +generally created. The only restriction on \(\nu_i(\codt)\) is that it must +not create an infinite number of jumps in a finite amount of time. +\(\nu_i(\codt)\) can depend a control input \(u\), or can be +\textit{autonomous}, where the discrete mode is defined by the system states +\(x\) and \(q\). While an autonomous system may not have a control input, that +does not mean the system is not controlled, as the continuous dynamics +\(f_i(\cdot)\) can be constructed such that the system is controlled by the +continuous and discrete states \(x\) and \(q\). + +The hybrid systems we are most interested in here are \textit{continuous} autonomous +hybrid systems. These systems are hybrid systems whose continuous states \(x\) +do not change during a jump, and do not rely on an external control input. This +research is primarily aimed at control of physical systems whose continuous +states \(x\) are physically required to be continuous across jumps. For example, +a nuclear reactor control rod system may jump from a warm-up ramp control mode to a load +following controller, but the continuous states of the reactor such as +temperature and rod position can not instantaneously change. + +Continuous hybrid systems are often constructed by piecing together control +systems for different regions in the state space. This way of building a hybrid +control system is intuitive--controllers are built for local regions with local +objectives. The problem arises when analysis of these local controllers is +generalized to the entire, global, hybrid system. Even in the most simple case +of linear time invariant controller modes, global guarantees of stability can +not be made using linear control theory. Instead, approaches using stitched +networks of Lyapunov functions have been introduced. %CITE CITE CITE% +These Lyapunov functions are difficult to find, but can for some linear switched +hybrid systems provide a way to verification. + +Another way of verifying stability of hybrid control systems includes performing +reachability analysis. Reachability is a formal methods tool that uses +abstractifications of a system to determine output ranges of dynamic systems for +a given input. Reachability is not limited to linear systems, and can be +performed on nonlinear systems as well. Reachability for hybrid systems suffers +from two main deficiencies. First, the analysis can take a very long time to +compute. Second, reachability uses approximations. Hybrid systems that have +trajectories of significantly long times can cause problems when using +reachability because either the computation time makes the analysis infeasible, +or the compounding approximation errors makes the analysis meaningless. + +\subsection{Formal Methods and Reactive Synthesis}