diff --git a/.task/backlog.data b/.task/backlog.data index 7b5be322..18d4cd4c 100644 --- a/.task/backlog.data +++ b/.task/backlog.data @@ -33,3 +33,4 @@ {"description":"Read Branicky Lyapunov paper","entry":"20250911T183429Z","modified":"20250911T201816Z","project":"Thesis","status":"pending","uuid":"f4d32147-ec74-4f68-b8d5-146c0b6f35df","tags":["reading"]} {"description":"Write zettel about lipschitz continuity","entry":"20250911T211029Z","modified":"20250911T211029Z","status":"pending","uuid":"b7f68988-8c06-4d18-bf77-91d7e39fd55f","tags":["zk"]} {"description":"Read Branicky Lyapunov paper","end":"20250911T214953Z","entry":"20250911T183429Z","modified":"20250911T214953Z","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":"20250915T003655Z","project":"ERLM","start":"20250915T003655Z","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/pending.data b/.task/pending.data index bd176502..6716fe28 100644 --- a/.task/pending.data +++ b/.task/pending.data @@ -2,7 +2,7 @@ [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:"1757885608" 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:"1757896615" project:"ERLM" start:"1757896615" 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:"Write zettel about lipschitz continuity" entry:"1757625029" modified:"1757625029" status:"pending" tags:"zk" tags_zk:"x" uuid:"b7f68988-8c06-4d18-bf77-91d7e39fd55f"] diff --git a/.task/undo.data b/.task/undo.data index 1efcd4bc..e850b2e3 100644 --- a/.task/undo.data +++ b/.task/undo.data @@ -116,3 +116,7 @@ time 1757627393 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:"1757627393" entry:"1757615669" modified:"1757627393" project:"Thesis" status:"completed" tags:"reading" tags_reading:"x" uuid:"f4d32147-ec74-4f68-b8d5-146c0b6f35df"] --- +time 1757896615 +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:"1757885608" 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:"1757896615" project:"ERLM" start:"1757896615" status:"pending" tags:"writing" tags_writing:"x" uuid:"4bec1530-18bc-43cb-9f0b-61e35dbf1730"] +--- diff --git a/Writing/ERLM/dane_proposal_format.cls b/Writing/ERLM/dane_proposal_format.cls index 3973a66d..eda8f64a 100644 --- a/Writing/ERLM/dane_proposal_format.cls +++ b/Writing/ERLM/dane_proposal_format.cls @@ -2,7 +2,7 @@ \ProvidesClass{prayer_circle}[2025/09/02 Custom class for academic documents] % Pass options and load base class -\PassOptionsToClass{10pt,titlepage}{article} +\PassOptionsToClass{11pt,titlepage}{article} \LoadClass{article} % Core packages diff --git a/Writing/ERLM/main.aux b/Writing/ERLM/main.aux index e8a7a953..8a029eb1 100644 --- a/Writing/ERLM/main.aux +++ b/Writing/ERLM/main.aux @@ -2,10 +2,10 @@ \bibstyle{unsrt} \providecommand \oddpage@label [2]{} \@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} +\bibdata{references} +\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Formal Methods and Reactive Synthesis}{4}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{References}{4}{}\protected@file@percent } +\gdef \@abspage@last{5} diff --git a/Writing/ERLM/main.fdb_latexmk b/Writing/ERLM/main.fdb_latexmk index 19f4820b..ed76ffea 100644 --- a/Writing/ERLM/main.fdb_latexmk +++ b/Writing/ERLM/main.fdb_latexmk @@ -1,14 +1,14 @@ # Fdb version 4 -["bibtex main"] 1757866412.20829 "main.aux" "main.bbl" "main" 1757880660.67738 0 - "./references.bib" 1757866237.16684 0 d41d8cd98f00b204e9800998ecf8427e "" +["bibtex main"] 1757899416.09338 "main.aux" "main.bbl" "main" 1757900978.83336 0 + "./references.bib" 1757896122.21556 0 d41d8cd98f00b204e9800998ecf8427e "" "/usr/share/texlive/texmf-dist/bibtex/bst/base/unsrt.bst" 1292289607 18030 1376b4b231b50c66211e47e42eda2875 "" - "main.aux" 1757880660.60211 759 c340ead263222262cc9d66ce4adc65f5 "pdflatex" + "main.aux" 1757900978.60047 759 3051c697f76ee5e29dc620b2ef1fb2b5 "pdflatex" (generated) "main.bbl" "main.blg" (rewritten before read) -["pdflatex"] 1757880660.23063 "main.tex" "main.pdf" "main" 1757880660.67755 2 - "/etc/texmf/web2c/texmf.cnf" 1726065852.27662 475 c0e671620eb5563b2130f56340a5fde8 "" +["pdflatex"] 1757900977.5298 "main.tex" "main.pdf" "main" 1757900978.8337 0 + "/etc/texmf/web2c/texmf.cnf" 1722610814.59577 475 c0e671620eb5563b2130f56340a5fde8 "" "/usr/share/texlive/texmf-dist/fonts/enc/dvips/base/8r.enc" 1165713224 4850 80dc9bab7f31fb78a000ccfed0e27cab "" "/usr/share/texlive/texmf-dist/fonts/map/fontname/texfonts.map" 1577235249 3524 cb3e574dea2d1052e39280babc910dc8 "" "/usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvb7t.tfm" 1136768653 2240 eb56c13537f4d8a0bd3fafc25572b1bd "" @@ -20,15 +20,15 @@ "/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/cmmi10.tfm" 1136768653 1528 abec98dbc43e172678c11b3b9031252a "" "/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmmi12.tfm" 1136768653 1524 4414a8315f39513458b80dfc63bff03a "" "/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmmi6.tfm" 1136768653 1512 f21f83efb36853c0b70002322c1ab3ad "" "/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmmi8.tfm" 1136768653 1520 eccf95517727cb11801f4f1aee3a21b4 "" + "/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/cmr6.tfm" 1136768653 1300 b62933e007d01cfd073f79b963c01526 "" "/usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmr8.tfm" 1136768653 1292 21c1c5bfeaebccffdb478fd231a0997d "" @@ -36,7 +36,7 @@ "/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/cmmi8.pfb" 1248133631 35469 70d41d2b9ea31d5d813066df7c99281c "" "/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 "" @@ -150,7 +150,7 @@ "/usr/share/texlive/texmf-dist/tex/latex/base/article.cls" 1705352648 20144 147463a6a579f4597269ef9565205cfe "" "/usr/share/texlive/texmf-dist/tex/latex/base/ifthen.sty" 1705352648 5319 2b738d02ce36ada6dcdd9534940db0ee "" "/usr/share/texlive/texmf-dist/tex/latex/base/inputenc.sty" 1705352648 5048 425739d70251273bf93e3d51f3c40048 "" - "/usr/share/texlive/texmf-dist/tex/latex/base/size10.clo" 1705352648 8448 dbc0dbf4156c0bb9ba01a1c685d3bad0 "" + "/usr/share/texlive/texmf-dist/tex/latex/base/size11.clo" 1705352648 8464 59874a3b0776c73e2a138b025d8473dd "" "/usr/share/texlive/texmf-dist/tex/latex/booktabs/booktabs.sty" 1579038678 6078 f1cb470c9199e7110a27851508ed7a5c "" "/usr/share/texlive/texmf-dist/tex/latex/cite/cite.sty" 1425427964 26218 19edeff8cdc2bcb704e8051dc55eb5a7 "" "/usr/share/texlive/texmf-dist/tex/latex/collectbox/collectbox.sty" 1666037909 9124 59c3b56f1a073de66e3eea35f9c173c8 "" @@ -224,14 +224,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" 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/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 "" + "/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" 1757899413.38474 2553 eb32d38752e5298f84dcaa0f93fb1dab "" + "goals-and-outcomes/v4.tex" 1757896122.20856 5764 a67e489f9ea8343564010d217ae37ec2 "" + "main.aux" 1757900978.60047 759 3051c697f76ee5e29dc620b2ef1fb2b5 "pdflatex" + "main.bbl" 1757899416.11972 49 0eba253fc001332e731e8aba3f23127b "bibtex main" + "main.tex" 1757896122.21556 182 46aa668f839c7d4c451f49d8253993e9 "" + "state-of-the-art/v1.tex" 1757900976.00644 6572 9e8f6252c740a1a218b70ad32050abfe "" (generated) "main.aux" "main.log" diff --git a/Writing/ERLM/main.fls b/Writing/ERLM/main.fls index 8f66f649..2ec76e0e 100644 --- a/Writing/ERLM/main.fls +++ b/Writing/ERLM/main.fls @@ -9,9 +9,11 @@ INPUT ./dane_proposal_format.cls INPUT dane_proposal_format.cls INPUT /usr/share/texlive/texmf-dist/tex/latex/base/article.cls INPUT /usr/share/texlive/texmf-dist/tex/latex/base/article.cls -INPUT /usr/share/texlive/texmf-dist/tex/latex/base/size10.clo -INPUT /usr/share/texlive/texmf-dist/tex/latex/base/size10.clo -INPUT /usr/share/texlive/texmf-dist/tex/latex/base/size10.clo +INPUT /usr/share/texlive/texmf-dist/tex/latex/base/size11.clo +INPUT /usr/share/texlive/texmf-dist/tex/latex/base/size11.clo +INPUT /usr/share/texlive/texmf-dist/tex/latex/base/size11.clo +INPUT /usr/share/texlive/texmf-dist/fonts/map/fontname/texfonts.map +INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmr10.tfm INPUT /usr/share/texlive/texmf-dist/tex/latex/base/inputenc.sty INPUT /usr/share/texlive/texmf-dist/tex/latex/base/inputenc.sty INPUT /usr/share/texlive/texmf-dist/tex/latex/geometry/geometry.sty @@ -330,7 +332,6 @@ INPUT /usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfcalendar.code.t INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/ot1phv.fd INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/ot1phv.fd INPUT /usr/share/texlive/texmf-dist/tex/latex/psnfss/ot1phv.fd -INPUT /usr/share/texlive/texmf-dist/fonts/map/fontname/texfonts.map INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvr7t.tfm INPUT /usr/share/texlive/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def INPUT /usr/share/texlive/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def @@ -407,20 +408,18 @@ INPUT /usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvb8r.tfm 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/cm/cmmi10.tfm +INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmsy10.tfm +INPUT /usr/share/texlive/texmf-dist/fonts/tfm/public/cm/cmex10.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 /usr/share/texlive/texmf-dist/fonts/tfm/adobe/helvetic/phvr7t.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/cmmi8.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 diff --git a/Writing/ERLM/main.log b/Writing/ERLM/main.log index a80e99dd..a981d21e 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) 14 SEP 2025 16:11 +This is pdfTeX, Version 3.141592653-2.6-1.40.25 (TeX Live 2023/Debian) (preloaded format=pdflatex 2024.9.10) 14 SEP 2025 21:49 entering extended mode restricted \write18 enabled. file:line:error style messages enabled. @@ -15,8 +15,8 @@ LaTeX Warning: You have requested document class `dane_proposal_format', Document Class: prayer_circle 2025/09/02 Custom class for academic documents (/usr/share/texlive/texmf-dist/tex/latex/base/article.cls Document Class: article 2023/05/17 v1.4n Standard LaTeX document class -(/usr/share/texlive/texmf-dist/tex/latex/base/size10.clo -File: size10.clo 2023/05/17 v1.4n Standard LaTeX file (size option) +(/usr/share/texlive/texmf-dist/tex/latex/base/size11.clo +File: size11.clo 2023/05/17 v1.4n Standard LaTeX file (size option) ) \c@part=\count187 \c@section=\count188 @@ -778,12 +778,12 @@ LaTeX Font Info: ... okay on input line 3. * \topmargin=-37.0pt * \headheight=12.0pt * \headsep=25.0pt -* \topskip=10.0pt +* \topskip=11.0pt * \footskip=30.0pt -* \marginparwidth=65.0pt -* \marginparsep=11.0pt +* \marginparwidth=59.0pt +* \marginparsep=10.0pt * \columnsep=10.0pt -* \skip\footins=9.0pt plus 4.0pt minus 2.0pt +* \skip\footins=10.0pt plus 4.0pt minus 2.0pt * \hoffset=0.0pt * \voffset=0.0pt * \mag=1000 @@ -830,72 +830,31 @@ 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/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 +LaTeX Font Info: Font shape `OT1/phv/m/it' in size <10.95> not available (Font) Font shape `OT1/phv/m/sl' tried instead on input line 33. - -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 - [] - -[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 + [1]) [2] (./state-of-the-art/v1.tex [3]) (./main.bbl LaTeX Warning: Empty `thebibliography' environment on input line 3. -) [3] (./main.aux) +) [4] (./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: - 25303 strings out of 476182 - 525740 string characters out of 5795595 - 1938975 words of memory out of 5000000 - 46762 multiletter control sequences out of 15000+600000 - 576605 words of font info for 76 fonts, out of 8000000 for 9000 + 25302 strings out of 476182 + 525820 string characters out of 5795595 + 1936975 words of memory out of 5000000 + 46763 multiletter control sequences out of 15000+600000 + 577060 words of font info for 75 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 (4 pages, 72104 bytes). + +Output written on main.pdf (5 pages, 81170 bytes). PDF statistics: - 80 PDF objects out of 1000 (max. 8388607) - 43 compressed objects within 1 object stream + 83 PDF objects out of 1000 (max. 8388607) + 45 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 cf097090..909dc1eb 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 01cc2ad4..29b2f9c6 100644 Binary files a/Writing/ERLM/main.synctex.gz and b/Writing/ERLM/main.synctex.gz differ diff --git a/Writing/ERLM/state-of-the-art/v1.tex b/Writing/ERLM/state-of-the-art/v1.tex index 08b13139..c5bb3545 100644 --- a/Writing/ERLM/state-of-the-art/v1.tex +++ b/Writing/ERLM/state-of-the-art/v1.tex @@ -31,10 +31,10 @@ In this description there are two functions: \(f(\cdot)\) and 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 +current continuous states and control input. \(\nu_i(\cdot)\) can be much more +generally created. The only restriction on \(\nu_i(\cdot)\) 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 +\(\nu_i(\cdot)\) 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 @@ -73,3 +73,47 @@ 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} + +Hybrid systems often are realized as cyber-physical systems. Cyber-physical +systems have a computational component responsible for control of a physical +process based on live sensors and actuators. Verification of these systems has +drawn two different communities together. We have previously discussed the +engineering perspective coming from the physical control theory background, but +in this section we discuss work coming from the cyber oriented persuasion. + +Many cyber systems lend themselves to a finite number of possible states. For +these systems, a map of the possible states and the transition between them can +be drawn and analyzed. This is called a \textit{finite state machine}. Finite +state machines can be easily verified, as all possible states can be +exhaustively checked to meet requirements in a process called model checking. +Model checking has been used extensively in high-assurance digital systems and +to ensure software correctness for critical systems. + +In order to check correctness, requirements for these automata must be defined. +Typically this is done using a formal language such as temporal logic. Temporal +logic allows system behaviors to be defined with temporal relations and includes +four operators: next (X), eventually (F), globally (G), and until (U). With +these operators, controller specifications can be created. In a nuclear context, +one might use temporal logic to define safety behaviors of a reactor core +control system. Let's consider an example: + +Suppose we are trying to write safety requirements about SCRAM behavior. In +plain English, one might say "If a high temperature alarm is triggered, the +control rods will immediately be inserted and unable to be withdrawn unless +reset by an operator." In a linear temporal logic specification, this would be +written as follows: + +\begin{equation} +\mathcal{G}(HighTemp \rightarrow \mathcal{X}(RodsInserted \land (\neg +RodsWithdrawn \text{ } \mathcal{U} \text{ } OperatorReset))) +\end{equation} + +A significant body of work has been done around the translation of English +requirements into temporal logic specifications. The Formal Requirements +Elicitation Tool (FRET) developed by the NASA Ames Research Center to help +bridge the gap between natural language and mathematical specification. Using +FRET, one is able to take a bulk number of near-English requirements in a +language called FRETish, and translate them automatically into linear temporal +logic specifications. From this point, it can be examined whether or not +the set of requirements define a realizable system, or if there exists conflicts +between different specifications.