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