From ff8416d4c2735e56cdb66c632a578c2ef918b3d9 Mon Sep 17 00:00:00 2001 From: Dane Sabo Date: Wed, 30 Jul 2025 10:10:45 -0400 Subject: [PATCH] vault backup: 2025-07-30 10:10:45 --- .obsidian/app.json | 3 +- .obsidian/plugins/colored-tags/data.json | 7 +- .../data.json | 2 +- .sessions/Journal.vim | 10 +- Journal/2025_07_30.md | 1 + Templates/Literature Note.md | 13 +- Templates/Paper Notes.md | 6 +- ...Vehicle Based on Support Vector Machine.md | 44 --- ...mal Methods applied to Machine Learning.md | 283 ------------------ ...wise Linear Neural Network Verification.md | 56 ---- ...ification of Artificial Neural Networks.md | 46 --- ...control framework for advanced reactors.md | 119 -------- ...tate estimation and trajectory tracking.md | 39 --- ...lex evidence - audit of primary sources.md | 53 ---- ...Networks with Mixed Integer Programming.md | 86 ------ ...ification of Avionics Software Products.md | 48 --- ...ise Linear Feed-Forward Neural Networks.md | 42 --- ...rmal requirements elicitation with FRET.md | 46 --- ...ht control systems - Present and future.md | 44 --- .../Nonlinear Identification and Control.md | 38 --- ...surance of Machine Learning Controllers.md | 107 ------- ...nges for Remote Microreactor Operations.md | 43 --- ...eeds for Remote Microreactor Operations.md | 196 ------------ ...is for Deep Feedforward Neural Networks.md | 50 ---- ...eural Networks with Provable Guarantees.md | 38 --- ... Assurance Using Reinforcement Learning.md | 164 ---------- ...a Shielding under Partial Observability.md | 43 --- ...fe Reinforcement Learning via Shielding.md | 63 ---- ...er-Physical Systems - A Focus on Models.md | 37 --- ...icClassificationNeuralnetworkbased1997.md} | 17 +- ... => albertiAutomationLevelsNuclear2023.md} | 15 +- ...=> bryanRemoteNuclearMicroreactors2023.md} | 19 +- ...rks.md => katzReluplexEfficientSMT2017.md} | 22 +- .../leePresentFutureCyberPhysical2015.md | 69 +++++ ...d => mignaccaEconomicsFinanceSmall2020.md} | 20 +- ....md => sunFormalVerificationNeural2019.md} | 48 +-- ...taylorEnhancingCyberPhysicalSystem2025.md} | 19 +- Zettelkasten/Literature Notes/testing note.md | 1 - 38 files changed, 193 insertions(+), 1764 deletions(-) delete mode 100644 Zettelkasten/Literature Notes/A Novel Lane Change Decision-Making Model of Autonomous Vehicle Based on Support Vector Machine.md delete mode 100644 Zettelkasten/Literature Notes/A Review of Formal Methods applied to Machine Learning.md delete mode 100644 Zettelkasten/Literature Notes/A Unified View of Piecewise Linear Neural Network Verification.md delete mode 100644 Zettelkasten/Literature Notes/An Abstraction-Refinement Approach to Verification of Artificial Neural Networks.md delete mode 100644 Zettelkasten/Literature Notes/An autonomous control framework for advanced reactors.md delete mode 100644 Zettelkasten/Literature Notes/Differential neural networks for robust nonlinear control - identification, state estimation and trajectory tracking.md delete mode 100644 Zettelkasten/Literature Notes/Effectiveness and efficiency of search methods in systematic reviews of complex evidence - audit of primary sources.md delete mode 100644 Zettelkasten/Literature Notes/Evaluating Robustness of Neural Networks with Mixed Integer Programming.md delete mode 100644 Zettelkasten/Literature Notes/Formal Verification of Avionics Software Products.md delete mode 100644 Zettelkasten/Literature Notes/Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks.md delete mode 100644 Zettelkasten/Literature Notes/Formal requirements elicitation with FRET.md delete mode 100644 Zettelkasten/Literature Notes/Neural network-based flight control systems - Present and future.md delete mode 100644 Zettelkasten/Literature Notes/Nonlinear Identification and Control.md delete mode 100644 Zettelkasten/Literature Notes/On Using Real-Time Reachability for the Safety Assurance of Machine Learning Controllers.md delete mode 100644 Zettelkasten/Literature Notes/Opportunities and Challenges for Remote Microreactor Operations.md delete mode 100644 Zettelkasten/Literature Notes/Opportunities, Challenges, and Research Needs for Remote Microreactor Operations.md delete mode 100644 Zettelkasten/Literature Notes/Output Range Analysis for Deep Feedforward Neural Networks.md delete mode 100644 Zettelkasten/Literature Notes/Reachability Analysis of Deep Neural Networks with Provable Guarantees.md delete mode 100644 Zettelkasten/Literature Notes/Runtime Safety Assurance Using Reinforcement Learning.md delete mode 100644 Zettelkasten/Literature Notes/Safe Reinforcement Learning via Shielding under Partial Observability.md delete mode 100644 Zettelkasten/Literature Notes/Safe Reinforcement Learning via Shielding.md delete mode 100644 Zettelkasten/Literature Notes/The Past, Present and Future of Cyber-Physical Systems - A Focus on Models.md rename Zettelkasten/Literature Notes/{A systematic classification of neural-network-based control.md => agarwalSystematicClassificationNeuralnetworkbased1997.md} (88%) rename Zettelkasten/Literature Notes/{Automation levels for nuclear reactor operations - A revised perspective.md => albertiAutomationLevelsNuclear2023.md} (96%) rename Zettelkasten/Literature Notes/{Remote nuclear microreactors - a preliminary economic evaluation of digital twins and centralized offsite control.md => bryanRemoteNuclearMicroreactors2023.md} (89%) rename Zettelkasten/Literature Notes/{Reluplex - An Efficient SMT Solver for Verifying Deep Neural Networks.md => katzReluplexEfficientSMT2017.md} (93%) create mode 100644 Zettelkasten/Literature Notes/leePresentFutureCyberPhysical2015.md rename Zettelkasten/Literature Notes/{Economics and finance of Small Modular Reactors - A systematic review and research agenda.md => mignaccaEconomicsFinanceSmall2020.md} (91%) rename Zettelkasten/Literature Notes/{Formal verification of neural network controlled autonomous systems.md => sunFormalVerificationNeural2019.md} (79%) rename Zettelkasten/Literature Notes/{Enhancing Cyber-Physical System Dependability via Synthesis - Challenges and Future Directions.md => taylorEnhancingCyberPhysicalSystem2025.md} (71%) delete mode 100644 Zettelkasten/Literature Notes/testing note.md diff --git a/.obsidian/app.json b/.obsidian/app.json index c5d1ae3d..0c2168b7 100755 --- a/.obsidian/app.json +++ b/.obsidian/app.json @@ -15,5 +15,6 @@ "readableLineLength": true, "strictLineBreaks": true, "defaultViewMode": "preview", - "livePreview": false + "livePreview": false, + "showInlineTitle": false } \ No newline at end of file diff --git a/.obsidian/plugins/colored-tags/data.json b/.obsidian/plugins/colored-tags/data.json index c70b1a71..4531e236 100755 --- a/.obsidian/plugins/colored-tags/data.json +++ b/.obsidian/plugins/colored-tags/data.json @@ -311,7 +311,12 @@ "remote-operation": 299, "digital-twin": 300, "fission-battery": 301, - "Artificial-intelligence": 302 + "Artificial-intelligence": 302, + "uncertainty": 303, + "Assurance-arguments": 304, + "Cyber-physical-Systems": 305, + "machine-learning": 306, + "Remote-operation": 307 }, "_version": 3 } \ No newline at end of file diff --git a/.obsidian/plugins/obsidian-zotero-desktop-connector/data.json b/.obsidian/plugins/obsidian-zotero-desktop-connector/data.json index b65ab7cf..b0b13b68 100755 --- a/.obsidian/plugins/obsidian-zotero-desktop-connector/data.json +++ b/.obsidian/plugins/obsidian-zotero-desktop-connector/data.json @@ -14,7 +14,7 @@ "exportFormats": [ { "name": "Create Literature Note", - "outputPathTemplate": "Zettelkasten/Literature Notes/{{title}}.md", + "outputPathTemplate": "Zettelkasten/Literature Notes/{{citekey}}.md", "imageOutputPathTemplate": "Zettelkasten/Literature Notes/{{citekey}}/", "imageBaseNameTemplate": "image", "cslStyle": "ieee", diff --git a/.sessions/Journal.vim b/.sessions/Journal.vim index c757dac5..49a256c3 100644 --- a/.sessions/Journal.vim +++ b/.sessions/Journal.vim @@ -13,11 +13,13 @@ if &shortmess =~ 'A' else set shortmess=aoO endif -badd +21 Journal/2025_07_30.md +badd +22 Journal/2025_07_30.md +badd +17 Zettelkasten/Literature\ Notes/Nonlinear\ Identification\ and\ Control.md argglobal %argdel edit Journal/2025_07_30.md argglobal +balt Zettelkasten/Literature\ Notes/Nonlinear\ Identification\ and\ Control.md setlocal foldmethod=manual setlocal foldexpr=0 setlocal foldmarker={{{,}}} @@ -28,12 +30,12 @@ setlocal foldnestmax=20 setlocal foldenable silent! normal! zE let &fdl = &fdl -let s:l = 21 - ((20 * winheight(0) + 27) / 55) +let s:l = 22 - ((21 * winheight(0) + 27) / 55) if s:l < 1 | let s:l = 1 | endif keepjumps exe s:l normal! zt -keepjumps 21 -normal! 012| +keepjumps 22 +normal! 0 tabnext 1 if exists('s:wipebuf') && len(win_findbuf(s:wipebuf)) == 0 && getbufvar(s:wipebuf, '&buftype') isnot# 'terminal' silent exe 'bwipe ' . s:wipebuf diff --git a/Journal/2025_07_30.md b/Journal/2025_07_30.md index 735aae00..4b77f9d9 100644 --- a/Journal/2025_07_30.md +++ b/Journal/2025_07_30.md @@ -19,3 +19,4 @@ Anyways, here's the goals for today: - [ ] Write down 6 ideas for a thesis - [ ] Review literature notes, and organize my notes + diff --git a/Templates/Literature Note.md b/Templates/Literature Note.md index 6de022e5..faaaa275 100755 --- a/Templates/Literature Note.md +++ b/Templates/Literature Note.md @@ -1,5 +1,4 @@ --- -title: {{title}} authors: {% for type, creators in creators | groupby('creatorType') -%} {% for creator in creators %} @@ -33,7 +32,9 @@ pages: {{ pages }} last_import: {{ importDate | format("YYYY-MM-DD") }} --- -# Indexing Information +# {{title}} + +## Indexing Information Published: {{ date | format("YYYY-MM") }} {% if DOI -%} @@ -97,11 +98,11 @@ Published: {{ date | format("YYYY-MM") }} >[!seealso] Related Papers >{% for r in relations %}[{{ r.title }}]({{ r.citekey }}){% if not loop.last %}, {% endif %}{% endfor %} -# Annotations -## Notes +## Annotations +### Notes ![[Zettelkasten/Literature Notes/Notes on Papers/{{ title | replace(':', '-') | replace('&', 'and') | replace('<', '') | replace('>', '') | replace('#', '') | replace('*', '') | replace('(', '') | replace(')', '') | replace('[', '') | replace(']', '') }}-notes.md]] -## Highlights From Zotero +### Highlights From Zotero {#- Process non-Purple highlights -#} {% for a in annotations -%} {% if (a.type == "highlight" or a.type == "underline") and a.colorCategory != "Purple" %} @@ -126,7 +127,7 @@ Published: {{ date | format("YYYY-MM") }} {% endif %} {% endfor %} -## Follow-Ups +### Follow-Ups {# Create a separate loop for Purple highlights as tasks #} {% for a in annotations -%} {% if a.type == "highlight" and a.colorCategory == "Purple" -%} diff --git a/Templates/Paper Notes.md b/Templates/Paper Notes.md index 3cb6ebfa..526f63bc 100644 --- a/Templates/Paper Notes.md +++ b/Templates/Paper Notes.md @@ -1,4 +1,4 @@ -# First Pass +## First Pass **Category:** **Context:** @@ -9,14 +9,14 @@ **Clarity:** -# Second Pass +## Second Pass **What is the main thrust?** **What is the supporting evidence?** **What are the key findings?** -# Third Pass +## Third Pass **Recreation Notes:** **Hidden Findings:** diff --git a/Zettelkasten/Literature Notes/A Novel Lane Change Decision-Making Model of Autonomous Vehicle Based on Support Vector Machine.md b/Zettelkasten/Literature Notes/A Novel Lane Change Decision-Making Model of Autonomous Vehicle Based on Support Vector Machine.md deleted file mode 100644 index 567c2b7e..00000000 --- a/Zettelkasten/Literature Notes/A Novel Lane Change Decision-Making Model of Autonomous Vehicle Based on Support Vector Machine.md +++ /dev/null @@ -1,44 +0,0 @@ ---- -authors: - - - "Liu, Yonggang" - - - "Wang, Xiao" - - - "Li, Liang" - - - "Cheng, Shuo" - - - "Chen, Zheng" - -citekey: "liuNovelLaneChange2019" -publish_date: 2019-01-01 -journal: "IEEE Access" -volume: 7 -pages: 26543-26550 -last_import: 2025-07-21 ---- - -# Indexing Information -Published: 2019-01 - -**DOI** -[10.1109/ACCESS.2019.2900416](https://doi.org/10.1109/ACCESS.2019.2900416) -#Trajectory, #Autonomous-vehicles, #Safety, #Autonomous-vehicle, #Bayesian-optimization, #Decision-making, #drivers’-habits, #Hidden-Markov-models, #lane-change-decision-making, #support-vector-machine, #Support-vector-machines - - -#ToRead - - ->[!Abstract] ->Autonomous driving is a crucial issue of the automobile industry, and research on lane change is its significant part. Previous works on the autonomous vehicle lane change mainly focused on lane change path planning and path tracking, but autonomous vehicle lane change decision making is rarely mentioned. Therefore, this paper establishes an autonomous lane change decision-making model based on benefit, safety, and tolerance by analyzing the factors of the autonomous vehicle lane change. Then, because of the multi-parameter and non-linearity of the autonomous lane change decision-making process, a support vector machine (SVM) algorithm with the Bayesian parameters optimization is adopted to solve this problem. Finally, we compare a lane change model based on rules with the proposed SVM model in the test set, and results illustrate that the SVM model performs better than the rule-based lane change model. Moreover, the real car experiment is carried out to verify the effectiveness of the decision model.>[!seealso] Related Papers -> - -# Annotations -## Notes -![[Notes on Papers/A Novel Lane Change Decision-Making Model of Autonomous Vehicle Based on Support Vector Machine.md]] - -## Highlights From Zotero - -## Follow-Ups - diff --git a/Zettelkasten/Literature Notes/A Review of Formal Methods applied to Machine Learning.md b/Zettelkasten/Literature Notes/A Review of Formal Methods applied to Machine Learning.md deleted file mode 100644 index 51bb2861..00000000 --- a/Zettelkasten/Literature Notes/A Review of Formal Methods applied to Machine Learning.md +++ /dev/null @@ -1,283 +0,0 @@ --- -authors: - - - "Urban, Caterina" - - - "Miné, Antoine" - -citekey: "urbanReviewFormalMethods2021" -publish_date: 2021-04-21 -last_import: 2025-07-07 ---- - -# Indexing Information -Published: 2021-04 - -**DOI** -[10.48550/arXiv.2104.02466](https://doi.org/10.48550/arXiv.2104.02466) -#Computer-Science---Machine-Learning, #Computer-Science---Logic-in-Computer-Science, #Computer-Science---Programming-Languages - - -#ToRead - - ->[!Abstract] ->We review state-of-the-art formal methods applied to the emerging field of the verification of machine learning systems. Formal methods can provide rigorous correctness guarantees on hardware and software systems. Thanks to the availability of mature tools, their use is well established in the industry, and in particular to check safety-critical applications as they undergo a stringent certification process. As machine learning is becoming more popular, machine-learned components are now considered for inclusion in critical systems. This raises the question of their safety and their verification. Yet, established formal methods are limited to classic, i.e. non machine-learned software. Applying formal methods to verify systems that include machine learning has only been considered recently and poses novel challenges in soundness, precision, and scalability. We first recall established formal methods and their current use in an exemplar safety-critical field, avionic software, with a focus on abstract interpretation based techniques as they provide a high level of scalability. This provides a golden standard and sets high expectations for machine learning verification. We then provide a comprehensive and detailed review of the formal methods developed so far for machine learning, highlighting their strengths and limitations. The large majority of them verify trained neural networks and employ either SMT, optimization, or abstract interpretation techniques. We also discuss methods for support vector machines and decision tree ensembles, as well as methods targeting training and data preparation, which are critical but often neglected aspects of machine learning. Finally, we offer perspectives for future research directions towards the formal verification of machine learning systems.>[!seealso] Related Papers -> - -# Annotations -## Notes -![[Paper Notes/A Review of Formal Methods applied to Machine Learning.md]] - -## Highlights From Zotero ->[!tip] Brilliant -> Recent advances in artificial intelligence and machine learning and the availability of vast amounts of data allow us to develop computer software that efficiently and autonomously perform complex tasks that are difficult or even impossible to design using traditional explicit programming (e.g., image classification, speech recognition, etc.). This makes machine-learned software particularly attractive even in safetycritical applications, as it enables performing a whole world of new functions that could not be envisioned before -> 2025-05-06 5:03 pm -> - ->[!warning] Dubious -> Safety-critical applications require an extremely high level of insurance that the software systems behave correctly and reliably. -> 2025-05-06 5:04 pm -> - ->[!quote] Other Highlight -> For instance, they are used at an industrial level in avionics [146], where the development processes of aircraft software systems have very stringent assurance and verification requirements mandated by international standards (i.e., DO-178C). -> 2025-05-12 11:25 am -> - ->[!highlight] Highlight -> In contrast, research in formal methods for the development and assurance of machine learning systems remains today extremely limited. It is however rapidly gaining interest and popularity, mostly driven by the growing needs of the automotive and avionics industries. -> 2025-05-06 5:07 pm -> - ->[!highlight] Highlight -> Specifically, in the following, we give an introduction to formal methods (Section 2) with a particular focus on static analysis by abstract interpretation [37], as it offers a unifying theory for reasoning about disparate formal verification approaches (Section 2.3). -> 2025-05-06 5:07 pm -> - ->[!done] Important -> Formal methods are an array of techniques that employ logic and mathematics in order to provide rigorous guarantees about the correctness of computer software. -> 2025-06-23 2:23 pm -> - ->[!done] Important -> Developing and checking by hand the very large proofs that are required to verify real-sized applications in realistic languages would be intractable. -> 2025-06-23 2:24 pm -> - ->[!tip] Brilliant -> However, a requirement of all formal methods is that they should be sound, that is, any correctness property established by the tool is indeed true of the actual executions of the program. -> 2025-06-23 2:38 pm -> -> *A good definition of soundness* - - ->[!highlight] Highlight -> Deductive Verification. Deductive methods stem directly from the work of Floyd, Hoare, and Naur [68, 83, 121]. The user provides a program and a formal specification expressed in a logic language. The specification is then propagated through the program source code, using symbolic execution as proposed by Burstall [23] or weakest preconditions as proposed by Dijkstra [51]. -> 2025-06-23 2:53 pm -> - ->[!done] Important -> One benefit of deductive verification is its ability to handle complex specifications using decidable logical theories (reasoning about, e.g., integers, floating-point numbers, pointers, arrays, recursive data-structures) and to perform modular verification by breaking down the specification into function contracts with preconditions and postconditions. -> 2025-06-23 2:53 pm -> - ->[!highlight] Highlight -> Proof Assistants. Interactive proof assistants are general-purpose tools able to produce reliable proofs of theorems, with application to mathematics, logic, and computer science. Their strength lies in the use of very expressive logic and the ability to check every proof with a small trusted core, reducing the possibilities of errors. Although they can offer some degree of automation (e.g., through tactics), they employ undecidable logics and essentially rely on a very tight interaction between the programmer and the tool, which can prove time consuming. -> 2025-06-23 2:56 pm -> - ->[!highlight] Highlight -> and other liveness properties), and the ability to check concurrent models. Model -> 2025-06-23 2:35 pm -> - ->[!tip] Brilliant -> Crafting a model that is both faithful and efficiently checked is a difficult task. Even then, the soundness and completeness properties only hold with respect to the model, not the original system. -> 2025-06-24 10:06 am -> - ->[!done] Important -> Bounded model checking [14] (e.g., the CBMC tool [35]) limits the exploration to execution traces of fixed length. The drawback of this method is that it loses soundness and completeness with respect to the full program; while it can uncover errors occurring at the beginning of the execution of the program, it cannot prove the absence of errors. -> 2025-06-24 10:07 am -> - ->[!done] Important -> The benefit of static analysis by abstract interpretation is full automation, parameterized precision, and the ability to verify large programs in real languages at the source level (C, Java, etc.) or binary level. The analysis is however inherently incomplete, and can fail to verify a desired property due to over-approximations. Thus, it can output false alarms, that must be checked by other means. -> 2025-06-24 10:08 am -> - ->[!done] Important -> As a critical aircraft component, avionic software is subject to certification by certification authorities and must obey the DO-178 international standard, which notably describes the verification process that such software must follow. Traditional methods consist in massive test campaigns and intellectual reviews, which have difficulties scaling up and maintaining a reasonable cost (which already accounts for more than half of the cost of overall software development). A shift occurred in the 2010s with the new DO-178C revision (and its DO-333 supplement) which opens the door to certification by formal methods. One key aspect of the standard is the emphasis on employing sound formal methods. Another key aspect is that any verification technique (formal or not) employed at the source level cannot be considered valid at the binary level unless the compilation process is also certified, which is important in practice as some tools can only reason at the source level. -> 2025-06-24 10:11 am -> - - ->[!highlight] Highlight -> This state semantics forgets about the history of computation (i.e., which state appears before which state), and so, cannot be used to verify temporal properties. -> 2025-06-24 10:18 am -> - ->[!warning] Dubious -> With this abstraction, we can no longer prove that X never takes the value 4. -> 2025-06-24 10:19 am -> -> *Huh?* - - ->[!warning] Dubious -> As machine learning enters critical industries, it would be interesting to combine verification techniques for traditional software and for artificial intelligence using abstract interpretation as a common theory, and develop an analyzer adapted to this new generation of critical software. -> 2025-06-25 12:44 pm -> -> *This posits that artificial intelligence and software are the same thing, kind of.* - - ->[!done] Important -> The training phase is highly non-deterministic, which is in contrast with predictability and traceability requirements of traditional safety-critical software development processes -> 2025-06-25 12:45 pm -> - ->[!highlight] Highlight -> Most formal verification methods proposed so far in the literature apply to trained machine learning models (Section 3.1) while only few are dedicated to the data preparation and model training phases (Section 3.2). -> 2025-06-25 12:46 pm -> - - ->[!fail] This ain't right -> they generally require several hours for neural networks with hundreds or thousands of neurons) -> 2025-06-25 12:51 pm -> -> *Relative to what???* - - ->[!highlight] Highlight -> Note, however, that soundness is not typically guaranteed with respect to floating-point arithmetic, but only with respect to computations on reals that ignore rounding errors and may thus differ from the actual computations [122, 105]. -> 2025-06-25 12:51 pm -> - ->[!done] Important -> SMT-based formal methods reduce the safety verification problem to a constraint satisfiability problem. Specifically, they encode a given neural network and (the negation of a) desired safety property as a set of constraints. If the constraints are satisfiable, the corresponding solution represents a counterexample to the safety property. Otherwise, the constraints are unsatisfiable, no counterexample can exist and thus the safety property holds. -> 2025-06-25 12:52 pm -> - - ->[!tip] Brilliant -> The approach is evaluated on a small vehicle collision avoidance use case and on a neural network with over a thousand neurons trained for digit recognition on the MNIST dataset [101]. -> 2025-06-25 1:00 pm -> - ->[!tip] Brilliant -> The approach is applied to the verification of the ACAS Xu neural networks [90], developed as early prototype for the next-generation airborne collision avoidance system for unmanned aircraft. The neural networks take sensor data as input (i.e., speed and present course of the current aircraft and of any nearby intruder) and issue appropriate navigation advisories. They consist of six hidden layers with 300 neurons each. -> 2025-06-25 1:02 pm -> - ->[!done] Important -> The experimental evaluation shows that Marabou (in divide-and-conquer mode running on four cores) generally outperforms both Planet [60] and Reluplex and is able to verify all ACAS Xu benchmarks within a one hour timeout per benchmark. -> 2025-06-25 1:03 pm -> - - ->[!highlight] Highlight -> Other Complete Formal Methods. Ruan et al. [134] presented an approach based on global optimization for verifying Lipschitz continuous neural networks [148], such as neural network with piecewise linear layers (i.e., fully-connected, max- and averagepooling, and convolutional layers) and ReLU as well as sigmoid and tanh activations. Specifically, given inputs to the neural networks and a Lipschitz continuous functions over its outputs (e.g., a function determining the confidence of the neural network in classifying an input), their approach computes lower and upper bounds on the function values. The approach is implemented in a tool named DeepGO (https://github.com/trustAI/DeepGO). Compared to Reluplex [92] and Sherlock [58], DeepGO on average is 36 times faster than Sherlock and almost 100 times faster than Reluplex. Moreover, DeepGO is shown to be able to scale to state-of-the-art neural networks with millions of neurons trained on the MNIST dataset [101]. -> 2025-06-25 5:53 pm -> - ->[!highlight] Highlight -> On the ACAS Xu neural networks, Neurify is on average 20 times faster than ReluVal and 5000 times faster than Reluplex. The experimental evaluation also shows that Neurify is able to verify safety properties of neural networks with over ten thousands hidden neurons such as the self-driving car convolutional neural network Dave [15]. -> 2025-06-25 5:56 pm -> - ->[!highlight] Highlight -> Incomplete formal verification methods are generally able to scale to large neural network architectures (they generally require at most a few minutes for neural networks with thousands of neurons) and are sound (often also with respect to floating-point arithmetic [140, 141, 105]) but suffer from false positives. -> 2025-06-30 10:26 am -> - - ->[!done] Important -> The experimental evaluation on 90 of the ACAS Xu benchmarks shows that Marabou [93] combined with their abstraction framework outperforms Marabou alone. Within a 20 hours timeout, it is able to verify 58 benchmarks, while Marabou alone can only verify 35 benchmarks. The abstractionenhanced Marabou is also orders of magnitude faster than Marabou alone. -> 2025-06-30 10:44 am -> - - ->[!done] Important -> Support vector machines [44] partition their input space in regions using hyperplanes that separate the training inputs according to their labels. They hyperplanes are chosen (i.e., learned during training) to maximize their distance (called margin) to their closest training inputs (called support vectors). -> 2025-06-30 1:59 pm -> - ->[!tip] Brilliant -> hen the training inputs are not linearly separable in the input space, the input space is implicitly projected, using so-called kernel functions, into a much higher-dimensional space in which the training inputs become linearly separable. This allows a support vector machine to also learn non-linear decision boundaries. -> 2025-07-07 11:41 am -> - ->[!done] Important -> Robust training aims at minimizing the worst-case loss for each given input, that is, the maximum loss (i.e., model error) over all possible perturbations of a given training input. However, since calculating the exact worst-case loss can be computationally costly in practice, robust training approaches typically minimize an estimate of the worst-case loss. -> 2025-06-30 3:14 pm -> - ->[!highlight] Highlight -> Another interesting possibility is to develop approaches to determine constraints on the training process that enforce a desired property on the trained model. For instance, one could enforce a specific behavior for a given input range of interest, or a particular structure of the trained model that facilitates its subsequent verification [171] (or its abstraction for verification [125, 145, 62]). -> 2025-05-06 5:10 pm -> - ->[!highlight] Highlight -> More generally, verification methods should allow verifying the behavior of trained models under all circumstances and not just over the expected safe input space. This is particularly useful in cases in which the trained model is part of a larger machine learning-based system [53] and is thus more susceptible to receive unexpected inputs, e.g., from malfunctioning sensors -> 2025-05-06 5:11 pm -> - ->[!highlight] Highlight -> In this case, it would be useful to design verification methods able to relate the behavior of the inexact model to the optimal expected behavior, e.g., by determining the worst-case approximation of the trained model. -> 2025-05-06 5:12 pm -> - ->[!highlight] Highlight -> Finally, there is a need for further approaches that support diverse model structures, such as recurrent neural networks [95, 175], and that can verify model implementations by taking floating-point rounding errors into account [140, 141, 105]. -> 2025-05-06 5:13 pm -> - - - - - - -## Follow-Ups - ->[!example] - >The CompCert certified compiler [103] is used to compile the C code into binary. - >- [ ] #Follow-Up - ->[!example] - >Kurd and Kelly [98] were the among the first to propose a characterizations of verification goals for neural networks used in safety-critical applications. - >- [ ] #Follow-Up - ->[!example] - >Note that the presence of these non-linear ReLU constraints makes the problem NP-complete [92] - >- [ ] What does 'NP Complete' mean? #Follow-Up - ->[!example] - >MILP-based Formal Methods. - >- [ ] What the fuck is MILP #Follow-Up - ->[!example] - >Their framework supports the abstract domains of intervals [36], zonotopes [73], and polyhedra [38], as well as their bounded powersets. - >- [ ] My brain hurty. #Follow-Up - ->[!example] - >Finally, a couple of theoretical results on the abstract interpretation of neural networks can be found in the literature. Baader et al. [5] show that for any continuous function f there exists a feed-forward fully-connected neural network with ReLU activations whose abstract interpretation using the domains of intervals [36] from an input region B is an arbitrarily close approximation of f on B. - >- [ ] #Follow-Up - ->[!example] - >[4] A. Atki, A. Brahmi, D. Delmas, H. Essoussi, T. Marie, and F. Randimbivololona. Formalise to Automate: Deployment of a Safe and Cost-Efficient Process for Avionics Software. In ERTS 2018 - >- [ ] #Follow-Up - ->[!example] - >[60] R. Ehlers. Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks. In ATVA 2017. - >- [ ] #Follow-Up - ->[!example] - >[107] B. Livshits, M. Sridharan, Y. Smaragdakis, O. Lhot ́ak, J. Nelson Amaral, B.-Y. E. Chang, S. Z. Guyer, U. P. Khedker, A. Møller, and Dimitrios Vardoulakis. In Defense of Soundiness: A Manifesto. 2015. - >- [ ] #Follow-Up - ->[!example] - >[131] F. Ranzato, M. Zanella Robustness Verification of Support Vector Machines. In SAS 2019. - >- [ ] #Follow-Up - diff --git a/Zettelkasten/Literature Notes/A Unified View of Piecewise Linear Neural Network Verification.md b/Zettelkasten/Literature Notes/A Unified View of Piecewise Linear Neural Network Verification.md deleted file mode 100644 index c9ebfe67..00000000 --- a/Zettelkasten/Literature Notes/A Unified View of Piecewise Linear Neural Network Verification.md +++ /dev/null @@ -1,56 +0,0 @@ ---- -authors: - - - "Bunel, Rudy R" - - - "Turkaslan, Ilker" - - - "Torr, Philip" - - - "Kohli, Pushmeet" - - - "Mudigonda, Pawan K" - -citekey: "bunelUnifiedViewPiecewise2018" -publish_date: 2018-01-01 -volume: 31 -publisher: "Curran Associates, Inc." -last_import: 2025-05-12 ---- - -# Indexing Information -Published: 2018-01 - - - - -#ToRead - - ->[!Abstract] ->The success of Deep Learning and its potential use in many safety-critical - applications has motivated research on formal verification of Neural Network - (NN) models. Despite the reputation of learned NN models to behave as black - boxes and the theoretical hardness of proving their properties, researchers - have been successful in verifying some classes of models by exploiting their - piecewise linear structure and taking insights from formal methods such as - Satisifiability Modulo Theory. These methods are however still far from - scaling to realistic neural networks. To facilitate progress on this crucial - area, we make two key contributions. First, we present a unified framework - that encompasses previous methods. This analysis results in the identification - of new methods that combine the strengths of multiple existing approaches, - accomplishing a speedup of two orders of magnitude compared to the previous - state of the art. Second, we propose a new data set of benchmarks which - includes a collection of previously released testcases. We use the benchmark - to provide the first experimental comparison of existing algorithms and - identify the factors impacting the hardness of verification problems.>[!seealso] Related Papers -> - -# Annotations -## Notes -![[Paper Notes/A Unified View of Piecewise Linear Neural Network Verification.md]] - -## Highlights From Zotero - -## Follow-Ups - diff --git a/Zettelkasten/Literature Notes/An Abstraction-Refinement Approach to Verification of Artificial Neural Networks.md b/Zettelkasten/Literature Notes/An Abstraction-Refinement Approach to Verification of Artificial Neural Networks.md deleted file mode 100644 index 167db9d2..00000000 --- a/Zettelkasten/Literature Notes/An Abstraction-Refinement Approach to Verification of Artificial Neural Networks.md +++ /dev/null @@ -1,46 +0,0 @@ ---- -authors: - - - "Pulina, Luca" - - - "Tacchella, Armando" - - - "Touili, Tayssir" - - - "Cook, Byron" - - - "Jackson, Paul" - -citekey: "pulinaAbstractionRefinementApproachVerification2010" -publish_date: 2010-01-01 -publisher: "Springer" -location: "Berlin, Heidelberg" -pages: 243-257 -last_import: 2025-05-12 ---- - -# Indexing Information -Published: 2010-01 - -**DOI** -[10.1007/978-3-642-14295-6_24](https://doi.org/10.1007/978-3-642-14295-6_24) -**ISBN** -[978-3-642-14295-6](https://www.isbnsearch.org/isbn/978-3-642-14295-6) -#Abstract-Domain, #Generalization-Error, #Hide-Layer, #Input-Vector, #Root-Mean-Square-Error - - -#ToRead - - ->[!Abstract] ->A key problem in the adoption of artificial neural networks in safety-related applications is that misbehaviors can be hardly ruled out with traditional analytical or probabilistic techniques. In this paper we focus on specific networks known as Multi-Layer Perceptrons (MLPs), and we propose a solution to verify their safety using abstractions to Boolean combinations of linear arithmetic constraints. We show that our abstractions are consistent, i.e., whenever the abstract MLP is declared to be safe, the same holds for the concrete one. Spurious counterexamples, on the other hand, trigger refinements and can be leveraged to automate the correction of misbehaviors. We describe an implementation of our approach based on the HySAT solver, detailing the abstraction-refinement process and the automated correction strategy. Finally, we present experimental results confirming the feasibility of our approach on a realistic case study.>[!seealso] Related Papers -> - -# Annotations -## Notes -![[Paper Notes/An Abstraction-Refinement Approach to Verification of Artificial Neural Networks.md]] - -## Highlights From Zotero - -## Follow-Ups - diff --git a/Zettelkasten/Literature Notes/An autonomous control framework for advanced reactors.md b/Zettelkasten/Literature Notes/An autonomous control framework for advanced reactors.md deleted file mode 100644 index 2c76a036..00000000 --- a/Zettelkasten/Literature Notes/An autonomous control framework for advanced reactors.md +++ /dev/null @@ -1,119 +0,0 @@ ---- -authors: - - - "Wood, Richard T." - - - "Upadhyaya, Belle R." - - - "Floyd, Dan C." - -citekey: "woodAutonomousControlFramework2017" -publish_date: 2017-08-01 -journal: "Nuclear Engineering and Technology" -volume: 49 -issue: 5 -pages: 896-904 -last_import: 2025-07-07 ---- - -# Indexing Information -Published: 2017-08 - -**DOI** -[10.1016/j.net.2017.07.001](https://doi.org/10.1016/j.net.2017.07.001) -#Autonomous-Control, #Instrumentation-and-Control-System, #Small-Modular-Reactor - - -#InSecondPass - - - ->[!Abstract] ->Several Generation IV nuclear reactor concepts have goals for optimizing investment recovery through phased introduction of multiple units on a common site with shared facilities and/or reconfigurable energy conversion systems. Additionally, small modular reactors are suitable for remote deployment to support highly localized microgrids in isolated, underdeveloped regions. The long-term economic viability of these advanced reactor plants depends on significant reductions in plant operations and maintenance costs. To accomplish these goals, intelligent control and diagnostic capabilities are needed to provide nearly autonomous operations with anticipatory maintenance. A nearly autonomous control system should enable automatic operation of a nuclear power plant while adapting to equipment faults and other upsets. It needs to have many intelligent capabilities, such as diagnosis, simulation, analysis, planning, reconfigurability, self-validation, and decision. These capabilities have been the subject of research for many years, but an autonomous control system for nuclear power generation remains as-yet an unrealized goal. This article describes a functional framework for intelligent, autonomous control that can facilitate the integration of control, diagnostic, and decision-making capabilities to satisfy the operational and performance goals of power plants based on multimodular advanced reactors.>[!seealso] Related Papers -> - -# Annotations -## Notes -![[An autonomous control framework for advanced reactors-Note]] - -## Highlights From Zotero ->[!tip] Brilliant -> The long-term economic viability of these advanced reactor plants depends on significant reductions in plant operations and maintenance costs. To accomplish these goals, intelligent control and diagnostic capabilities are needed to provide nearly autonomous operations with anticipatory maintenance. -> 2025-07-06 12:44 pm -> - ->[!done] Important -> An SMR is generally characterized by: (1) an electrical generating capacity of less than 300 MWe (megawatt electric), (2) a primary system that is entirely or substantially fabricated within a factory, and (3) a primary system that can be transported by truck or rail to the plant site. -> 2025-07-06 12:47 pm -> - ->[!tip] Brilliant -> he current US nuclear industry average for O&M staff is roughly one person per every 2 megawatts of generated power. -> 2025-07-06 12:48 pm -> - ->[!done] Important -> Current automated control technologies for nuclear power plants are reasonably mature, and highly automated control for an SMR is clearly feasible under optimum circumstances. Autonomous control is primarily intended to account for the nonoptimum circumstances when degradation, failure, and other off-normal events challenge the performance of the reactor, and the capability for immediate human intervention is constrained. There are clear gaps in the development and demonstration of autonomous control capabilities for the specific domain of nuclear power operations. -> 2025-07-06 1:04 pm -> - - ->[!done] Important -> Autonomy extends the scope of primary control functions. Such capabilities can consist of automated control during all operating modes, process performance optimization (e.g., self-tuning), continuous monitoring, and diagnosis of performance indicators as well as trends for operational and safety-related parameters, diagnosis of component health, flexible control to address both anticipated and unanticipated events and to provide protection of life-limited components (such as batteries and actuators), adaptation to changing or degrading conditions, and validation and maintenance of control system performance. Key characteristics of autonomy include intelligence, robustness, optimization, flexibility, and adaptability. Intelligence facilitates minimal or no reliance on human intervention and can accommodate an integrated, whole system approach to control. It implies embedded decision-making and management/planning authority. Intelligence in control provides for anticipatory action based on system knowledge and event prediction. -> 2025-07-06 6:03 pm -> - ->[!highlight] Highlight -> As a minimum requirement of autonomy, the SMR plant control system must be able to switch between normal operational modes automatically (i.e., automatic control). Additionally, reactor protective action must be available if the desired operational conditions cannot be achieved. -> 2025-07-06 6:07 pm -> - ->[!done] Important -> Unlike conventional reactor operational concepts, in which the primary defense against potentially adverse conditions resulting from off-normal events is to scram the reactor, the objective of autonomous control is to limit the progression of off-normal events and minimize the need for shutdown. This is especially true in situations where the nuclear power plant is the stabilizing generation source on a small electric grid. -> 2025-07-06 6:10 pm -> - ->[!tip] Brilliant -> To illustrate the autonomous functionality that can be provided for the SMR plant control system, two fault management scenarios are considered in which detection and response are described. The first scenario relates to fault adaptation in the case of sensor failure. The indicators from surveillance and diagnostic functions that the plant control system can employ include divergence of redundant measurements, conflict between predicted (based on analytical or relational estimation) and measured values, and detection and isolation of a confirmed fault. The prospective response can include substitution of a redundant measurement or utilization of a diverse measurement. An example of the latter would be using neutron flux instead of temperature (i.e., core thermal power) as a power measurement. Switching to an alternate control algorithm may prove necessary for faulted or suspect measurements. The second scenario relates to fault avoidance in the case of a degrading actuator. The indicators of an incipient failure can be prediction of actuator failure based on prognostic modeling (e.g., fault forecasting) or detection of sluggish response to commands. The prospective response can be to switch to an alternate control strategy to avoid incipient failure by reducing stress on the suspect component. An example would be utilizing manipulation of core heat removal (e.g., coolant density change) instead of direct reactivity insertion (e.g., control element movement) to control reactor power. -> 2025-07-06 6:15 pm -> - ->[!done] Important -> Although having a highly reliable plant control system is important, that fact is of limited value if the control system cannot accommodate plant degradation without immediate human intervention or scram. In such a case, the result is a highly reliable control system that becomes ineffective because the plant has changed. -> 2025-07-06 6:16 pm -> - ->[!highlight] Highlight -> A three-level hierarchy is typical for robotic applications [8,30,31]. The three layers in top-to-bottom hierarchical order are the planner layer, the executive layer, and the functional layer. The general concept of the hierarchy is that commands are issued by higher levels to lower levels, and response data flows from lower levels to higher levels in the multi-tiered framework. Intelligence increases with increasing level within the hierarchy. Each of the three interacting tiers has a principal role. Basically, the functional layer provides direct control, the executive layer provides sequencing of action, and the planner layer provides deliberative planning. -> 2025-07-06 6:19 pm -> -> *Kinda mimmics the Purdue model? Application layer, scada layer, then what would be enterprise layer?* - - - ->[!tip] Brilliant -> Key characteristics that are feasible through autonomous control include Intelligence to confirm system performance and detect degraded or failed conditions Optimization to minimize stress on SMR components and efficiently react to operational events without compromising system integrity Robustness to accommodate uncertainties and changing conditions Flexibility and adaptability to accommodate failures through reconfiguration among available control system elements or adjustment of control system strategies, algorithms, or parameters -> 2025-07-06 12:51 pm -> - ->[!done] Important -> Given anticipated operational imperatives to utilize technology with demonstrated (or at least high probability) readiness, it is not practical to strive for the high-end extreme of autonomy in first-generation SMRs. Instead, modest advancement beyond fully automatic control to allow extended fault tolerance for anticipated events or degraded conditions and some predefined reconfigurability is the most realistic goal for an initial application of SMR plant autonomous control. -> 2025-07-06 1:00 pm -> - ->[!tip] Brilliant -> The primary technical gap relates to decision capabilities (e.g., strategic, interpretive, adaptive, predictive). Technology development and demonstration activities are needed to provide the desired technical readiness for implementation of an SMR autonomous control system. In particular, the capabilities to monitor, trend, detect, diagnose, decide, and self-adjust must be established within an integrated functional architecture to enable control system autonomy. -> 2025-07-06 1:00 pm -> - - -## Follow-Ups - ->[!example] - >One of the most fully digital plants currently in operation in the United States is the Oconee Nuclear Station [14]. The three units at Oconee have digital reactor protection systems and a digital integrated control system (ICS). The digital ICS coordinates the main control actions of multiple control loops through an integrated master controller that establishes feedforward control demands based on desired overall core thermal power. The ICS also has provisions for supplementary support actions among control loops to facilitate optimized performance. - >- [ ] #Follow-Up - ->[!example] - >There is an architectural approach for nearly autonomous control systems that has been developed through simulated nuclear power applications (see Fig. 2). As part of research into advanced multimodular nuclear reactor concepts, such as the ALMR, the International Reactor Innovative and Secure (IRIS), and representative advanced SMR concepts, a supervisory control system architecture was devised [24e26]. This approach provides a framework for autonomous control while supporting a high-level interface with operations staff, who can act as plant supervisors. The final authority for decisions and goal setting remains with the human, but the control system assumes expanded responsibilities for normal control action, abnormal event response, and system fault tolerance. - >- [ ] #Follow-Up - diff --git a/Zettelkasten/Literature Notes/Differential neural networks for robust nonlinear control - identification, state estimation and trajectory tracking.md b/Zettelkasten/Literature Notes/Differential neural networks for robust nonlinear control - identification, state estimation and trajectory tracking.md deleted file mode 100644 index d0f21494..00000000 --- a/Zettelkasten/Literature Notes/Differential neural networks for robust nonlinear control - identification, state estimation and trajectory tracking.md +++ /dev/null @@ -1,39 +0,0 @@ ---- -authors: - - - "Poznyak, Alexander S." - - - "Yu, Wen" - - - "Sanchez, Edgar N." - -citekey: "poznyakDifferentialNeuralNetworks2001" -publish_date: 2001-01-01 -publisher: "World Scientific" -location: "Singapore ;" -last_import: 2025-05-12 ---- - -# Indexing Information -Published: 2001-01 - -**ISBN** -[9786611956738](https://www.isbnsearch.org/isbn/9786611956738) -#Neural-networks-Computer-science, #Nonlinear-control-theory - - -#ToRead - - ->[!Abstract] ->This book deals with continuous time dynamic neural networks theory applied to the solution of basic problems in robust control theory, including identification, state space estimation (based on neuro-observers) and trajectory tracking. The plants to be identified and controlled are assumed to be a priori unknown but belonging to a given class containing internal unmodelled dynamics and external perturbations as well. The error stability analysis and the corresponding error bounds for different problems are presented. The effectiveness of the suggested approach is illustrated by its ap>[!seealso] Related Papers -> - -# Annotations -## Notes -![[Paper Notes/Differential neural networks for robust nonlinear control- identification, state estimation and trajectory tracking.md]] - -## Highlights From Zotero - -## Follow-Ups - diff --git a/Zettelkasten/Literature Notes/Effectiveness and efficiency of search methods in systematic reviews of complex evidence - audit of primary sources.md b/Zettelkasten/Literature Notes/Effectiveness and efficiency of search methods in systematic reviews of complex evidence - audit of primary sources.md deleted file mode 100644 index c20e9065..00000000 --- a/Zettelkasten/Literature Notes/Effectiveness and efficiency of search methods in systematic reviews of complex evidence - audit of primary sources.md +++ /dev/null @@ -1,53 +0,0 @@ ---- -authors: - - - "Greenhalgh, Trisha" - - - "Peacock, Richard" - -citekey: "greenhalghEffectivenessEfficiencySearch2005" -publish_date: 2005-11-03 -journal: "BMJ" -volume: 331 -issue: 7524 -pages: 1064-1065 -last_import: 2025-05-12 ---- - -# Indexing Information -**DOI** -[10.1136/bmj.38636.593461.68](https://doi.org/10.1136/bmj.38636.593461.68) - - - -#InSecondPass - - - ->[!Abstract] ->Objective To describe where papers come from in a systematic review of complex evidence. -Method Audit of how the 495 primary sources for the review were originally identified. -Results Only 30% of sources were obtained from the protocol defined at the outset of the study (that is, from the database and hand searches). Fifty one per cent were identified by “snowballing” (such as pursuing references of references), and 24% by personal knowledge or personal contacts. -Conclusion Systematic reviews of complex evidence cannot rely solely on protocol-driven search strategies.>[!seealso] Related Papers -> - -# Annotations -## Notes -![[Paper Notes/Effectiveness and efficiency of search methods in systematic reviews of complex evidence- audit of primary sources.md]] - -## Highlights From Zotero ->[!tip] Brilliant -> Results Only 30% of sources were obtained from theprotocol defined at the outset of the study (that is,from the database and hand searches). Fifty one per cent were identified by “snowballing” (such as pursuing references of references), and 24% bypersonal knowledge or personal contacts. -> 2025-05-11 9:33 am - ->[!done] Important -> Citation tracking: using special citation trackingdatabases (Science Citation Index, Social Science Cita-tion Index, and Arts and Humanities Citation Index),we forward tracked selected key papers publishedmore than three years previously, thereby identifying articles in mainstream journals that had subsequentlycited those papers -> 2025-05-11 9:39 am - ->[!done] Important -> Overall, the greatest yield was from pursuing selected references of references -> 2025-05-11 9:40 am - - -## Follow-Ups - diff --git a/Zettelkasten/Literature Notes/Evaluating Robustness of Neural Networks with Mixed Integer Programming.md b/Zettelkasten/Literature Notes/Evaluating Robustness of Neural Networks with Mixed Integer Programming.md deleted file mode 100644 index 1fa5e04e..00000000 --- a/Zettelkasten/Literature Notes/Evaluating Robustness of Neural Networks with Mixed Integer Programming.md +++ /dev/null @@ -1,86 +0,0 @@ ---- -authors: - - - "Tjeng, Vincent" - - - "Xiao, Kai" - - - "Tedrake, Russ" - -citekey: "tjengEvaluatingRobustnessNeural2019" -publish_date: 2019-02-18 -last_import: 2025-07-21 ---- - -# Indexing Information -Published: 2019-02 - -**DOI** -[10.48550/arXiv.1711.07356](https://doi.org/10.48550/arXiv.1711.07356) -#Computer-Science---Cryptography-and-Security, #Computer-Science---Machine-Learning, #Computer-Science---Computer-Vision-and-Pattern-Recognition - - -#InSecondPass - - - ->[!Abstract] ->Neural networks have demonstrated considerable success on a wide variety of real-world problems. However, networks trained only to optimize for training accuracy can often be fooled by adversarial examples - slightly perturbed inputs that are misclassified with high confidence. Verification of networks enables us to gauge their vulnerability to such adversarial examples. We formulate verification of piecewise-linear neural networks as a mixed integer program. On a representative task of finding minimum adversarial distortions, our verifier is two to three orders of magnitude quicker than the state-of-the-art. We achieve this computational speedup via tight formulations for non-linearities, as well as a novel presolve algorithm that makes full use of all information available. The computational speedup allows us to verify properties on convolutional networks with an order of magnitude more ReLUs than networks previously verified by any complete verifier. In particular, we determine for the first time the exact adversarial accuracy of an MNIST classifier to perturbations with bounded $l_\infty$ norm $\epsilon=0.1$: for this classifier, we find an adversarial example for 4.38% of samples, and a certificate of robustness (to perturbations with bounded norm) for the remainder. Across all robust training procedures and network architectures considered, we are able to certify more samples than the state-of-the-art and find more adversarial examples than a strong first-order attack.>[!note] Markdown Notes ->Comment: Accepted as a conference paper at ICLR 2019}>[!seealso] Related Papers -> - -# Annotations -## Notes -![[Evaluating Robustness of Neural Networks with Mixed Integer Programming-Note]] - -## Highlights From Zotero ->[!tip] Brilliant -> In particular, we determine for the first time the exact adversarial accuracy ofan MNIST classifier to perturbations with bounded l∞ norm = 0.1: for this classifier, we find an adversarial example for 4.38% of samples, and a certificate of robustness to norm-bounded perturbations for the remainder. Across all robusttraining procedures and network architectures considered, and for both the MNISTand CIFAR-10 datasets, we are able to certify more samples than the state-of-the-artand find more adversarial examples than a strong first-order attack. -> 2025-07-09 7:56 am -> - ->[!tip] Brilliant -> Second, since the predicted label is determined bythe unit in the final layer with the maximum activation, proving that a unit never has themaximum activation over all bounded perturbations eliminates it from consideration. Weexploit both phenomena, reducing the overall number of non-linearities considered. -> 2025-07-09 9:09 am -> -> *Can this he used to say that safely controller has no false positives for a region??* - - ->[!highlight] Highlight -> Verification as solving an MILP. The general problem of verification is to determine whether someproperty P on the output of a neural network holds for all input in a bounded input domain C ⊆ Rm.For the verification problem to be expressible as solving an MILP, P must be expressible as theconjunction or disjunction of linear properties Pi,j over some set of polyhedra Ci, where C = ∪Ci. -> 2025-07-09 9:16 am -> - ->[!highlight] Highlight -> Let G(x) denote the region in the input domain corresponding to all allowable perturbations of a particular input x. -> 2025-07-14 9:01 pm -> - ->[!highlight] Highlight -> As in Madry et al. (2018), we say that a neural network is robust toperturbations on x if the predicted probability of the true label λ(x) exceeds that of every other labelfor all perturbations: -> 2025-07-09 9:19 am -> - ->[!highlight] Highlight -> As long as G(x) ∩ Xvalid can be expressed as the union of a set of polyhedra, the feasibility problem can be expressed as an MILP. -> 2025-07-14 9:01 pm -> - ->[!highlight] Highlight -> Let d(·, ·) denote a distance metric that measures the perceptual similarity between two input images -> 2025-07-14 9:01 pm -> - ->[!tip] Brilliant -> Determining tight bounds is critical for problem tractability: tight bounds strengthen the problem formulation and thus improve solve times (Vielma, 2015). For instance, if we can prove that the phase of a ReLU is stable, we can avoid introducing a binary variable. More generally, loose bounds on input to some unit will propagate downstream, leading to units in later layers having looser bounds. -> 2025-07-14 9:23 pm -> - ->[!tip] Brilliant -> The key observation is that, for piecewise-linear non-linearities, there are thresholds beyond which further refining a bound will not improve the problem formulation. With this in mind, we adopt a progressive bounds tightening approach: we begin by determining coarse bounds using fast procedures and only spend time refining bounds using procedures with higher computational complexity if doing so could provide additional information to improve the problem formulation.4 -> 2025-07-14 9:28 pm -> - - -## Follow-Ups - diff --git a/Zettelkasten/Literature Notes/Formal Verification of Avionics Software Products.md b/Zettelkasten/Literature Notes/Formal Verification of Avionics Software Products.md deleted file mode 100644 index 8929bcfd..00000000 --- a/Zettelkasten/Literature Notes/Formal Verification of Avionics Software Products.md +++ /dev/null @@ -1,48 +0,0 @@ ---- -authors: - - - "Souyris, Jean" - - - "Wiels, Virginie" - - - "Delmas, David" - - - "Delseny, Hervé" - - - "Cavalcanti, Ana" - - - "Dams, Dennis R." - -citekey: "souyrisFormalVerificationAvionics2009" -publish_date: 2009-01-01 -publisher: "Springer" -location: "Berlin, Heidelberg" -pages: 532-546 -last_import: 2025-05-12 ---- - -# Indexing Information -Published: 2009-01 - -**DOI** -[10.1007/978-3-642-05089-3_34](https://doi.org/10.1007/978-3-642-05089-3_34) -**ISBN** -[978-3-642-05089-3](https://www.isbnsearch.org/isbn/978-3-642-05089-3) -#formal-verification, #verification, #Abstract-Interpretation, #avionics-software, #development-process, #safety, #static-analysis - - -#ToRead - - ->[!Abstract] ->This paper relates an industrial experience in the field of formal verification of avionics software products. Ten years ago we presented our very first technological research results in [18]. What was just an idea plus some experimental results at that time is now an industrial reality. Indeed, since 2001, Airbus has been integrating several tool supported formal verification techniques into the development process of avionics software products. Just like all aspects of such processes, the use of formal verification techniques must comply with DO-178B [9] objectives and Airbus has been a pioneer in this domain.>[!seealso] Related Papers -> - -# Annotations -## Notes -![[Paper Notes/Formal Verification of Avionics Software Products.md]] - -## Highlights From Zotero - -## Follow-Ups - diff --git a/Zettelkasten/Literature Notes/Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks.md b/Zettelkasten/Literature Notes/Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks.md deleted file mode 100644 index 6ee5ff8d..00000000 --- a/Zettelkasten/Literature Notes/Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks.md +++ /dev/null @@ -1,42 +0,0 @@ ---- -authors: - - - "Ehlers, Rüdiger" - - - "D'Souza, Deepak" - - - "Narayan Kumar, K." - -citekey: "ehlersFormalVerificationPieceWise2017" -publish_date: 2017-01-01 -publisher: "Springer International Publishing" -location: "Cham" -pages: 269-286 -last_import: 2025-05-12 ---- - -# Indexing Information -Published: 2017-01 - -**DOI** -[10.1007/978-3-319-68167-2_19](https://doi.org/10.1007/978-3-319-68167-2_19) -**ISBN** -[978-3-319-68167-2](https://www.isbnsearch.org/isbn/978-3-319-68167-2) - - - -#ToRead - - ->[!Abstract] ->We present an approach for the verification of feed-forward neural networks in which all nodes have a piece-wise linear activation function. Such networks are often used in deep learning and have been shown to be hard to verify for modern satisfiability modulo theory (SMT) and integer linear programming (ILP) solvers.>[!seealso] Related Papers -> - -# Annotations -## Notes -![[Paper Notes/Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks.md]] - -## Highlights From Zotero - -## Follow-Ups - diff --git a/Zettelkasten/Literature Notes/Formal requirements elicitation with FRET.md b/Zettelkasten/Literature Notes/Formal requirements elicitation with FRET.md deleted file mode 100644 index 1130f564..00000000 --- a/Zettelkasten/Literature Notes/Formal requirements elicitation with FRET.md +++ /dev/null @@ -1,46 +0,0 @@ ---- -authors: - - - "Giannakopoulou, Dimitra" - - - "Mavridou, Anastasia" - - - "Rhein, Julian" - - - "Pressburger, Thomas" - - - "Schumann, Johann" - - - "Shi, Nija" - -citekey: "giannakopoulouFormalRequirementsElicitation2020" -publish_date: 2020-01-01 -last_import: 2025-07-21 ---- - -# Indexing Information -Published: 2020-01 - - - - -#InSecondPass - - - ->[!seealso] Related Papers -> - -# Annotations -## Notes -![[Formal requirements elicitation with FRET-Note]] - -## Highlights From Zotero ->[!tip] Brilliant -> A fretish requirement description is automatically parsed into six sequential fields, with the fret editordynamically coloring the text corresponding to the fields as the requirement is typed in (Figure 2): scope, condition, component, shall, timing, and response. -> 2025-07-15 11:32 pm -> - - -## Follow-Ups - diff --git a/Zettelkasten/Literature Notes/Neural network-based flight control systems - Present and future.md b/Zettelkasten/Literature Notes/Neural network-based flight control systems - Present and future.md deleted file mode 100644 index ae340496..00000000 --- a/Zettelkasten/Literature Notes/Neural network-based flight control systems - Present and future.md +++ /dev/null @@ -1,44 +0,0 @@ ---- -authors: - - - "Emami, Seyyed Ali" - - - "Castaldi, Paolo" - - - "Banazadeh, Afshin" - -citekey: "emamiNeuralNetworkbasedFlight2022" -publish_date: 2022-01-01 -journal: "Annual Reviews in Control" -volume: 53 -pages: 97-137 -last_import: 2025-05-12 ---- - -# Indexing Information -Published: 2022-01 - -**DOI** -[10.1016/j.arcontrol.2022.04.006](https://doi.org/10.1016/j.arcontrol.2022.04.006) -#Neural-networks, #Flight-control, #Intelligent-control, #Reinforcement-learning - - -#ToRead - - ->[!Abstract] ->As the first review in this field, this paper presents an in-depth mathematical view of Intelligent Flight Control Systems (IFCSs), particularly those based on artificial neural networks. The rapid evolution of IFCSs in the last two decades in both the methodological and technical aspects necessitates a comprehensive view of them to better demonstrate the current stage and the crucial remaining steps towards developing a truly intelligent flight management unit. To this end, in this paper, we will provide a detailed mathematical view of Neural Network (NN)-based flight control systems and the challenging problems that still remain. The paper will cover both the model-based and model-free IFCSs. The model-based methods consist of the basic feedback error learning scheme, the pseudocontrol strategy, and the neural backstepping method. Besides, different approaches to analyze the closed-loop stability in IFCSs, their requirements, and their limitations will be discussed in detail. Various supplementary features, which can be integrated with a basic IFCS such as the fault-tolerance capability, the consideration of system constraints, and the combination of NNs with other robust and adaptive elements like disturbance observers, would be covered, as well. On the other hand, concerning model-free flight controllers, both the indirect and direct adaptive control systems including indirect adaptive control using NN-based system identification, the approximate dynamic programming using NN, and the reinforcement learning-based adaptive optimal control will be carefully addressed. Finally, by demonstrating a well-organized view of the current stage in the development of IFCSs, the challenging issues, which are critical to be addressed in the future, are thoroughly identified. As a result, this paper can be considered as a comprehensive road map for all researchers interested in the design and development of intelligent control systems, particularly in the field of aerospace applications.>[!seealso] Related Papers -> - -# Annotations -## Notes -![[Paper Notes/Neural network-based flight control systems- Present and future.md]] - -## Highlights From Zotero ->[!highlight] Highlight -> Although the words Intelligence and Autonomy have been widely employed interchangeably, there is an essential conceptual difference between them [1]. Different definitions have been given for both concepts in the literature [2, 3]. However, in a general view, the intelligence may be defined as a very general mental capability that involves the ability to reason, plan, solve problems, think abstractly, comprehend complex ideas, learn quickly and learn from experience [3]. On the other hand, the ability to generate one’s own purposes without any instruction from outside can be interpreted as the autonomy of a system [1] -> 2025-04-07 12:54 pm - - -## Follow-Ups - diff --git a/Zettelkasten/Literature Notes/Nonlinear Identification and Control.md b/Zettelkasten/Literature Notes/Nonlinear Identification and Control.md deleted file mode 100644 index c05eb7ff..00000000 --- a/Zettelkasten/Literature Notes/Nonlinear Identification and Control.md +++ /dev/null @@ -1,38 +0,0 @@ ---- -authors: - - - "Liu, G. P." - - - "Grimble, Michael J." - - - "Johnson, Michael A." - -citekey: "liuNonlinearIdentificationControl2001" -publish_date: 2001-01-01 -publisher: "Springer" -location: "London" -last_import: 2025-05-12 ---- - -# Indexing Information -Published: 2001-01 - -**ISBN** -[978-1-4471-1076-7 978-1-4471-0345-5](https://www.isbnsearch.org/isbn/978-1-4471-1076-7 978-1-4471-0345-5) -#Adaptive-control, #Control, #artificial-intelligence, #complexity, #Control-Engineering, #development, #genetic-algorithms, #Identification, #learning, #model, #Modelling, #Neural-Networks, #Nonlinear-control, #Wavelets - - -#ToRead - - ->[!seealso] Related Papers -> - -# Annotations -## Notes -![[Paper Notes/Nonlinear Identification and Control.md]] - -## Highlights From Zotero - -## Follow-Ups - diff --git a/Zettelkasten/Literature Notes/On Using Real-Time Reachability for the Safety Assurance of Machine Learning Controllers.md b/Zettelkasten/Literature Notes/On Using Real-Time Reachability for the Safety Assurance of Machine Learning Controllers.md deleted file mode 100644 index 0a14783d..00000000 --- a/Zettelkasten/Literature Notes/On Using Real-Time Reachability for the Safety Assurance of Machine Learning Controllers.md +++ /dev/null @@ -1,107 +0,0 @@ ---- -authors: - - - "Musau, Patrick" - - - "Hamilton, Nathaniel" - - - "Lopez, Diego Manzanas" - - - "Robinette, Preston" - - - "Johnson, Taylor T." - -citekey: "musauUsingRealTimeReachability2022" -publish_date: 2022-03-01 -pages: 1-10 -last_import: 2025-07-07 ---- - -# Indexing Information -Published: 2022-03 - -**DOI** -[10.1109/ICAA52185.2022.00010](https://doi.org/10.1109/ICAA52185.2022.00010) -#formal-verification, #Real-time-systems, #Reinforcement-learning, #Safety, #deep-reinforcement-learning, #hybrid-automaton, #imitation-learning, #reachability-analysis, #Runtime, #Sensors, #Switches, #Vehicle-dynamics - - -#InSecondPass - - - ->[!Abstract] ->Over the last decade, advances in machine learning and sensing technology have paved the way for the belief that safe, accessible, and convenient autonomous vehicles may be realized in the near future. Despite the prolific competencies of machine learning models for learning the nuances of sensing, actuation, and control, they are notoriously difficult to assure. The challenge here is that some models, such as neural networks, are “black box” in nature, making verification and validation difficult, and sometimes infeasible. Moreover, these models are often tasked with operating in uncertain and dynamic environments where design time assurance may only be partially transferable. Thus, it is critical to monitor these components at runtime. One approach for providing runtime assurance of systems with unverified components is the simplex architecture, where an unverified component is wrapped with a safety controller and a switching logic designed to prevent dangerous behavior. In this paper, we propose the use of a real-time reachability algorithm for the implementation of such an architecture for the safety assurance of a 1/10 scale open source autonomous vehicle platform known as F1/10. The reachability algorithm (a) provides provable guarantees of safety, and (b) is used to detect potentially unsafe scenarios. In our approach, the need to analyze the underlying controller is abstracted away, instead focusing on the effects of the controller’s decisions on the system’s future states. We demonstrate the efficacy of our architecture through experiments conducted both in simulation and on an embedded hardware platform.>[!seealso] Related Papers -> - -# Annotations -## Notes -![[On Using Real-Time Reachability for the Safety Assurance of Machine Learning Controllers-Note]] - -## Highlights From Zotero ->[!done] Important -> One approach for providing runtime assurance of systems with unveried components is the simplex architecture, where an unveried component is wrapped with a safety controller and a switching logic designed to prevent dangerous behavior. In this paper, we propose the use of a real-time reachability algorithm for the implementation of such an architecture for the safety assurance of a 1/10 scale open source autonomous vehicle platform known as F1/10. The reachability algorithm (a) provides provable guarantees of safety, and (b) is used to detect potentially unsafe scenarios. In our approach, the need to analyze the underlying controller is abstracted away, instead focusing on the effects of the controller’s decisions on the system’s future states. We demonstrate the efcacy of our architecture through experiments conducted both in simulation and on an embedded hardware platform. -> 2025-07-03 12:31 pm -> - ->[!done] Important -> In summary, the contributions of this paper are: (1) We modify the real-time reachability algorithm presented in [8] to handle static obstacles in a sound and real-time manner. (2) We implement a simplex control architecture that uses real-time reachability for online collision avoidance. (3) We show our method working with multiple machine learning controllers. (4) We demonstrate success using our method to safely navigate through obstacles the trained controllers have no prior experience with. (5) We evaluate the safety of machine learning components transferred to real-world hardware without additional training. -> 2025-07-03 12:40 pm -> - ->[!warning] Dubious -> Using MATLAB’s Grey-Box SystemIdentification toolbox, we obtained the following parametersfor the simulation model: ca = 19569, cm = 00342,ch = −371967, lf = 0225, lr = 0225. -> 2025-07-03 11:00 pm -> - ->[!done] Important -> Despite the growing success of DRL approaches in many contexts, these methods are mainly leveraged within simulation due to challenges with ensuring safe training in real-world systems, designing rewardfunctions that deal with noisy and uncertain state information, and ensuring trained controllers are able to generalize beyond fixed scenarios [21]. While training a controller in simulation and moving it into the real world is possible, a process known as sim2real transfer, it often results in undesired, poor, and/or dangerous behavior [21]. -> 2025-07-04 8:47 am -> - ->[!warning] Dubious -> ARS focuses on the use of a linear policy, i.e. a weight matrix. Instead of passing the inputthrough multiple layers with non-linear activation functions, the input is multiplied by a single weight matrix to generatethe control output. -> 2025-07-04 8:51 am -> -> *Um is this just state space?* - - ->[!highlight] Highlight -> The real-time reachability algorithm always returns an overapproximation of the reachable set of states. The over-approximation error decreases with successive iterations, provided that there is enough runtimefor re-computations. -> 2025-07-04 8:54 am -> - ->[!highlight] Highlight -> Given a fixed runtime, Truntime, we compute the reachable set R[0,Treach]. If there is remaining runtime, we restart the reachability computation with a smaller step size. Inboth this work and [8], the step-size is halved in each successive iteration, leading to more accurate determinations of the reachable set. -> 2025-07-04 8:56 am -> - ->[!highlight] Highlight -> Ideally, to ensure there were no missed deadlines, we would build our system in a Real-Time Operating System (RTOS), which allows for the specification of task priorities, executing them within established time frames. However, ourimplementation does not make use of an RTOS, and insteaddepends on native Linux and ROS to handle task management. -To combat this shortcoming and reduce the number of misseddeadlines, we estimate how the time required to compute the next reachability loop. If our estimate exceeds the remaining allotted time, the process terminates. There is an inherenttradeoff between the conservativeness of our runtime estimates and the conservativeness of the resulting reachable set. In this work, we chose to maximize the number of iterations usedin constructing the reachable set at the risk of occasionally missing deadlines. Our experiments demonstrate that we weresuccessful in minimizing the number of missed deadlinesduring operation. -> 2025-07-04 9:02 am -> - ->[!highlight] Highlight -> In our design, we decouple thecontrol of the car’s steering and throttle control. The steering control, δ, is governed by the ML controller, and the throttle control is designed to maintain a constant speed, u, when the learning-based controller is in use. -> 2025-07-04 9:06 am -> - ->[!highlight] Highlight -> In the traditional simplex architecture, both the decisionmodule and the safety controller must be verified for the system to be verified as correct [8]. While this is straightforward for relatively simple controllers, it is significantly more challenging for many classes of controllers, especially whenreal-time execution is considered [18]. However, the mainfocus of this work is evaluating the use of the reachability algorithm as a switching logic for the simplex architecture. -Thus, we opted not to develop a “formally verified” safetycontroller. Instead, we selected a controller based on a gapfollowing algorithm optimized to avoid collisions with obstacles. A detailed description of the gap-following algorithm can be found in the following report [25]. It was primarily selecteddue to its robust collision avoidance ability and simplicity. -> 2025-07-04 9:07 am -> - ->[!highlight] Highlight -> While the reachability algorithm presented in this work possesses provable guarantees, our architecture does not. Obtaining these guarantees requires developing a formally verified safety controller and switching logic, which was outside thescope of the work presented herein. Therefore, it is possible toenter a state in our framework in which all future trajectories will result in a collision. These states are known as inevitable collision states and have been well studied within the motionplanning literature [27]. In future work, we hope to address this limitation by leveraging approaches such as viability kernels, and dynamic safety envelopes that allow for the synthesis ofprovable safe control regimes [28]. -> 2025-07-04 9:19 am -> - - - -## Follow-Ups - ->[!example] - >[11] D. Seto, E. Ferriera, and T. Marz, “Case study: Development of a baseline controller for automatic landing of an f-16 aircraft using linear matrix inequalities (lmis),” Software Engineering Institute, Carnegie Mellon University, Pittsburgh, PA, Tech. Rep. CMU/SEI-99-TR-020, 2000. - >- [ ] #Follow-Up - diff --git a/Zettelkasten/Literature Notes/Opportunities and Challenges for Remote Microreactor Operations.md b/Zettelkasten/Literature Notes/Opportunities and Challenges for Remote Microreactor Operations.md deleted file mode 100644 index 8f955d50..00000000 --- a/Zettelkasten/Literature Notes/Opportunities and Challenges for Remote Microreactor Operations.md +++ /dev/null @@ -1,43 +0,0 @@ ---- -authors: - - - "Stevens, Kaeley Renee" - - - "Oncken, Joseph Eugene" - - - "Bryan, Haydn C." - - - "Gutowska, Izabela" - - - "Ulrich, Thomas A." - - - "Boring PhD, Ronald Laurids" - - - "Culler, Megan Jordan" - -citekey: "stevensOpportunitiesChallengesRemote2023" -publish_date: 2023-07-15 -last_import: 2025-07-23 ---- - -# Indexing Information -Published: 2023-07 - - - - -#ToRead - - ->[!Abstract] ->The nuclear industry is developing new advanced reactor technologies, and many companies are embracing this advancement by pursuing the development of microreactors. The term microreactor generally refers to a nuclear reactor with an operating power of 20 MW or less. The power range of microreactors makes them appealing for many use cases, such as powering remote communities, mining sites, and military bases. Most of the microreactor designs being pursued will incorporate remote facility operations into the final product. However, no framework has yet been developed to determine what remote operations systems require for reliable, resilient, and secure operation of a microreactor. This work identifies the challenges unique to remote operations and monitoring for microreactors specifically regarding instrumentation and control, communication methods, regulatory requirements, and operational policies. The types of commands and sensor measurements that must be transmitted between the facilities as well as methods for verifying the trustworthiness of these signals are assessed. This work evaluates the security, reliability, and performance requirements that must be met when considering the selection of communication hardware and protocols for use in remote operations. Also, an assessment was performed to study how remote operations fit within current regulatory requirements and what may need to be updated in regulatory policy to allow for remote operation. Finally, the operational contingencies unique to remote operations that must be in place for response to abnormal events are identified. This paper details these challenges and research opportunities to provide a foundation for the design of remote operation systems.>[!seealso] Related Papers -> - -# Annotations -## Notes -![[Notes on Papers/Opportunities and Challenges for Remote Microreactor Operations.md]] - -## Highlights From Zotero - -## Follow-Ups - diff --git a/Zettelkasten/Literature Notes/Opportunities, Challenges, and Research Needs for Remote Microreactor Operations.md b/Zettelkasten/Literature Notes/Opportunities, Challenges, and Research Needs for Remote Microreactor Operations.md deleted file mode 100644 index b41d7f60..00000000 --- a/Zettelkasten/Literature Notes/Opportunities, Challenges, and Research Needs for Remote Microreactor Operations.md +++ /dev/null @@ -1,196 +0,0 @@ ---- -authors: - - - "Stevens, Kaeley" - - - "Oncken, Joseph" - - - "Boring, Ronald" - - - "Ulrich, Thomas" - - - "Culler, Megan" - - - "Bryan, Haydn" - - - "Browning, Jeren" - - - "Gutowska, Izabela" - -citekey: "stevensOpportunitiesChallengesResearch2024" -publish_date: 2024-12-01 -journal: "Nuclear Technology" -volume: 210 -issue: 12 -pages: 2257-2273 -last_import: 2025-07-23 ---- - -# Indexing Information -Published: 2024-12 - -**DOI** -[10.1080/00295450.2024.2344903](https://doi.org/10.1080/00295450.2024.2344903) -#Microreactor, #digital-twin, #remote-operation - - -#ToRead - - ->[!Abstract] ->As the nuclear industry develops new advanced reactor technologies, many companies are embracing this advancement by pursuing the development of microreactors. The term microreactor generally refers to a nuclear reactor with an operating power of 20 MW(thermal) or less. The power range of microreactors makes them appealing for many use cases, such as powering remote communities, mining sites, and military bases. Most of the microreactor designs being pursued are expected to incorporate remote facility operations into the final product. However, no framework has yet been developed to determine what remote operations systems require for reliable, resilient, and secure operation of a microreactor. This work identifies the research needs for challenges that are unique to remote operations and monitoring for microreactors, specifically regarding instrumentation and control, communication methods, regulatory requirements, and operational policies. The types of commands and sensor measurements that must be transmitted between the facilities, as well as methods for verifying the trustworthiness of these signals, are assessed. This work evaluates the security, reliability, and performance requirements that must be met when considering the selection of communication hardware and protocols for use in remote operations. Also, an assessment was performed to study how remote operations fit within current regulatory requirements and what may need to be updated in regulatory policy to allow for remote operation. Finally, the operational contingencies unique to remote operations that must be in place for responses to abnormal events are identified. This paper identifies the challenges and research opportunities within the areas of importance for the design of remote operation systems.>[!seealso] Related Papers -> - -# Annotations -## Notes -![[Notes on Papers/Opportunities, Challenges, and Research Needs for Remote Microreactor Operations.md]] - -## Highlights From Zotero ->[!fail] This ain't right -> Microreactors are being considered for use in remote locations, which introduces a unique set of challenges. There is uncertainty concerning development costs, undefined licensing requirements, and the ability of microcompetitive reactors to be cost -> 2024-12-25 11:54 am -> - ->[!fail] This ain't right -> Implementing remote operations for microreactors has the potential to greatly improve the economics of the facility. -> 2024-12-25 11:54 am -> - ->[!fail] This ain't right -> so it may be difficult to find the number of qualified staff that would be necessary for onsite operation. -> 2024-12-25 11:54 am -> - ->[!fail] This ain't right -> A semi-autonomous remote operating system could allow for operation from a centralized location while also reducing the necessary number of staff. It could even be possible to operate and monitor multiple microreactor sites from one centrally located remote operating center. -> 2024-12-25 11:56 am -> - ->[!fail] This ain't right -> While remote operations applications for other industries do exist, they have not been pursued in the nuclear industry where heightened safety concerns for nuclear applications produce caution. -> 2024-12-25 6:59 pm -> - ->[!fail] This ain't right -> This paper discusses the challenges and research needs in four focus areas: instrumentation and control (I&C), communications, regulation, and human factors. -> 2024-12-26 8:07 am -> - ->[!fail] This ain't right -> remote operation and monitoring of microreactors are crucial for the successful application of microreactor technology. -> 2024-12-26 8:10 am -> - ->[!fail] This ain't right -> with specific technological constraints or high-cost, next-best alternatives. -> 2024-12-26 8:12 am -> - ->[!fail] This ain't right -> Historically, primary costs drivers of nuclear plants have included construction management and onsite labor.[ -> 2024-12-26 8:12 am -> - ->[!done] Important -> Remote operation of microreactors can improve these significant cost drivers by reducing construction costs (by eliminating the need to build a complete control system onsite) and labor costs (because many microreactors could be operated simultaneously from a centralized hub in an area with lower labor costs). -> 2024-12-26 8:12 am -> - ->[!fail] This ain't right -> Early adoption of any technology is critical for its continued success in the commercial space. -> 2024-12-26 8:13 am -> - ->[!fail] This ain't right -> Remote operation capabilities, as enabled by digital-twin technology, may stand as a make-or-break factor for microreactor economic competitiveness for early adopters. -> 2024-12-25 12:03 pm -> - ->[!fail] This ain't right -> A remote operation system for a microreactor intended to power a mining site may require different sensors to obtain the information needed for operation than a microreactor powering a hospital, for instance. -> 2024-12-25 12:03 pm -> - ->[!fail] This ain't right -> Another essential aspect of the remote operation system in determining its I&C requirements would be the level of automation desired for the system. -> 2024-12-25 12:04 pm -> - ->[!fail] This ain't right -> A low level of automation integrated with a remote operations system may involve an operator at the remote operations center sending a power-level request to the reactor, while an automated control system for the reactor that maneuvers the reactivity control actuators to positions that meet the requested power level. A high level of automation, integrated with a remote operations system, may replicate an autonomous control system located at the reactor, making power-level decisions and executing the power change without human involvement except for human monitoring of the performance of the autonomous system. -> 2024-12-25 12:04 pm -> - ->[!fail] This ain't right -> Ramuhalli and Cetiner discussed many concepts for operation,[ [14] autonomous such as the various requirements, concepts, and potential approaches for autonomous microreactor operation. A key concept for these operation systems is the degree of automation, which is increased by gradually incorporating more autonomy, where the system has the ability to “reason” and make decisions on operations that can be performed without human input or guidance, to the system. Increased autonomy of operation increases the potential for machine error, but reduces the need for human intervention. It is important to find an ideal level of autonomy for the remote operation system that considers the tradeoffs involving reduced staffing, system complexity, operaetc.[ tional flexibility, -> 2024-12-25 12:04 pm -> - ->[!fail] This ain't right -> its economic benefit by allowing for a reduction in staffing requirements and increasing the number of microreactors that could be monitored from one remote operations facility. -> 2024-12-26 12:45 pm -> - ->[!highlight] Highlight -> Sheridan. -> 2024-12-26 12:46 pm -> - ->[!done] Important -> The U.S. Nuclear Regulatory Commission (NRC) provides guidelines for automation in reactor operations 0700.[ [17] in section 9 of NUREG-0 However, it has been noted that if consideration is limited to these guidelines, they would not “align with long-term economic and commercial goals of the advanced reactor community.”[ -> 2024-12-26 12:47 pm -> - ->[!fail] This ain't right -> Defining the system’s autonomous control levels will help identify the necessary sensor measurements to be transmitted from the reactor to the remote operations system. -> 2024-12-26 12:48 pm -> - ->[!fail] This ain't right -> Higher levels of autonomy (more detailed commands) would lead to a more complex verification system. -> 2024-12-26 12:48 pm -> - ->[!fail] This ain't right -> The communication system that supports remote operation of a microreactor must also support the operational requirements for remote monitoring and control, the reliability requirements for integration with power systems, and the security requirements for protecting the integrity and availability of the system. -> 2024-12-25 12:05 pm -> - ->[!fail] This ain't right -> While remote operations are common in many industries, the fact that the proposed operation of a microreactor would include a remotely operated critical infrastructure industrial control system (ICS) makes the security and reliability of the system of utmost importance. -> 2024-12-26 12:50 pm -> - ->[!fail] This ain't right -> Standard best practices for securing traffic across networks will also help reduce the risk of cybersecurity events. H -> 2024-12-26 1:00 pm -> - ->[!done] Important -> Historically, the power system leverages masterslave, unencrypted protocol schemes that enable fast, easy access to data. However, these systems were designed to be closed loop, isolated from the Internet. Now, best practices recommend protocols that use encryption, authentication, and nonrepudiation of transmitted information -> 2024-12-26 1:01 pm -> - ->[!done] Important -> These standard practices help ensure the availability, integrity, and confidentiality of data. -> 2024-12-26 1:12 pm -> - ->[!done] Important -> digital-twin technology can be used to validate that the sensor data received match the expected measurements, and the received commands do not jeopardize safe operation of the system. -> 2024-12-26 1:12 pm -> - ->[!done] Important -> represents application layer additions to the design of the communication network. -> 2024-12-26 1:20 pm -> - ->[!done] Important -> Checking the data with digital-twin intelligence can help identify problems in the communication network that may be relevant for operator awareness or response. -> 2024-12-26 1:20 pm -> - - -## Follow-Ups - diff --git a/Zettelkasten/Literature Notes/Output Range Analysis for Deep Feedforward Neural Networks.md b/Zettelkasten/Literature Notes/Output Range Analysis for Deep Feedforward Neural Networks.md deleted file mode 100644 index c4254e7d..00000000 --- a/Zettelkasten/Literature Notes/Output Range Analysis for Deep Feedforward Neural Networks.md +++ /dev/null @@ -1,50 +0,0 @@ ---- -authors: - - - "Dutta, Souradeep" - - - "Jha, Susmit" - - - "Sankaranarayanan, Sriram" - - - "Tiwari, Ashish" - - - "Dutle, Aaron" - - - "Muñoz, César" - - - "Narkawicz, Anthony" - -citekey: "duttaOutputRangeAnalysis2018" -publish_date: 2018-01-01 -publisher: "Springer International Publishing" -location: "Cham" -pages: 121-138 -last_import: 2025-05-12 ---- - -# Indexing Information -Published: 2018-01 - -**DOI** -[10.1007/978-3-319-77935-5_9](https://doi.org/10.1007/978-3-319-77935-5_9) -**ISBN** -[978-3-319-77935-5](https://www.isbnsearch.org/isbn/978-3-319-77935-5) - - - -#ToRead - - ->[!Abstract] ->Given a neural network (NN) and a set of possible inputs to the network described by polyhedral constraints, we aim to compute a safe over-approximation of the set of possible output values. This operation is a fundamental primitive enabling the formal analysis of neural networks that are extensively used in a variety of machine learning tasks such as perception and control of autonomous systems. Increasingly, they are deployed in high-assurance applications, leading to a compelling use case for formal verification approaches. In this paper, we present an efficient range estimation algorithm that iterates between an expensive global combinatorial search using mixed-integer linear programming problems, and a relatively inexpensive local optimization that repeatedly seeks a local optimum of the function represented by the NN. We implement our approach and compare it with Reluplex, a recently proposed solver for deep neural networks. We demonstrate applications of our approach to computing flowpipes for neural network-based feedback controllers. We show that the use of local search in conjunction with mixed-integer linear programming solvers effectively reduces the combinatorial search over possible combinations of active neurons in the network by pruning away suboptimal nodes.>[!seealso] Related Papers -> - -# Annotations -## Notes -![[Paper Notes/Output Range Analysis for Deep Feedforward Neural Networks.md]] - -## Highlights From Zotero - -## Follow-Ups - diff --git a/Zettelkasten/Literature Notes/Reachability Analysis of Deep Neural Networks with Provable Guarantees.md b/Zettelkasten/Literature Notes/Reachability Analysis of Deep Neural Networks with Provable Guarantees.md deleted file mode 100644 index 8014cc96..00000000 --- a/Zettelkasten/Literature Notes/Reachability Analysis of Deep Neural Networks with Provable Guarantees.md +++ /dev/null @@ -1,38 +0,0 @@ ---- -authors: - - - "Ruan, Wenjie" - - - "Huang, Xiaowei" - - - "Kwiatkowska, Marta" - -citekey: "ruanReachabilityAnalysisDeep2018" -publish_date: 2018-05-06 -last_import: 2025-05-12 ---- - -# Indexing Information -Published: 2018-05 - -**DOI** -[10.48550/arXiv.1805.02242](https://doi.org/10.48550/arXiv.1805.02242) -#Computer-Science---Machine-Learning, #Statistics---Machine-Learning, #Computer-Science---Computer-Vision-and-Pattern-Recognition - - -#ToRead - - ->[!Abstract] ->Verifying correctness of deep neural networks (DNNs) is challenging. We study a generic reachability problem for feed-forward DNNs which, for a given set of inputs to the network and a Lipschitz-continuous function over its outputs, computes the lower and upper bound on the function values. Because the network and the function are Lipschitz continuous, all values in the interval between the lower and upper bound are reachable. We show how to obtain the safety verification problem, the output range analysis problem and a robustness measure by instantiating the reachability problem. We present a novel algorithm based on adaptive nested optimisation to solve the reachability problem. The technique has been implemented and evaluated on a range of DNNs, demonstrating its efficiency, scalability and ability to handle a broader class of networks than state-of-the-art verification approaches.>[!note] Markdown Notes ->Comment: This is the long version of the conference paper accepted in IJCAI-2018. Github: https://github.com/TrustAI/DeepGO}>[!seealso] Related Papers -> - -# Annotations -## Notes -![[Paper Notes/Reachability Analysis of Deep Neural Networks with Provable Guarantees.md]] - -## Highlights From Zotero - -## Follow-Ups - diff --git a/Zettelkasten/Literature Notes/Runtime Safety Assurance Using Reinforcement Learning.md b/Zettelkasten/Literature Notes/Runtime Safety Assurance Using Reinforcement Learning.md deleted file mode 100644 index fa8c0b88..00000000 --- a/Zettelkasten/Literature Notes/Runtime Safety Assurance Using Reinforcement Learning.md +++ /dev/null @@ -1,164 +0,0 @@ ---- -authors: - - - "Lazarus, Christopher" - - - "Lopez, James G." - - - "Kochenderfer, Mykel J." - -citekey: "lazarusRuntimeSafetyAssurance2020" -publish_date: 2020-10-01 -pages: 1-9 -last_import: 2025-07-21 ---- - -# Indexing Information -Published: 2020-10 - -**DOI** -[10.1109/DASC50938.2020.9256446](https://doi.org/10.1109/DASC50938.2020.9256446) -#Control-systems, #Reinforcement-learning, #reinforcement-learning, #Safety, #Switches, #Aerospace-control, #Aircraft, #Atmospheric-modeling, #runtime-safety-assurance, #Unmanned-Aerial-Systems-UAS - - -#InSecondPass - - - ->[!Abstract] ->The airworthiness and safety of a non-pedigreed autopilot must be verified, but the cost to formally do so can be prohibitive. We can bypass formal verification of non-pedigreed components by incorporating Runtime Safety Assurance (RTSA) as mechanism to ensure safety. RTSA consists of a meta-controller that observes the inputs and outputs of a non-pedigreed component and verifies formally specified behavior as the system operates. When the system is triggered, a verified recovery controller is deployed. Recovery controllers are designed to be safe but very likely disruptive to the operational objective of the system, and thus RTSA systems must balance safety and efficiency. The objective of this paper is to design a meta-controller capable of identifying unsafe situations with high accuracy. High dimensional and non-linear dynamics in which modern controllers are deployed along with the black-box nature of the nominal controllers make this a difficult problem. Current approaches rely heavily on domain expertise and human engineering. We frame the design of RTSA with the Markov decision process (MDP) framework and use reinforcement learning (RL) to solve it. Our learned meta-controller consistently exhibits superior performance in our experiments compared to our baseline, human engineered approach.>[!seealso] Related Papers -> - -# Annotations -## Notes -![[Runtime Safety Assurance Using Reinforcement Learning-Note]] - -## Highlights From Zotero ->[!tip] Brilliant -> We can bypass formal verification of non-pedigreed components by incorporating Runtime Safety Assurance (RTSA) as mechanism to ensure safety. RTSA consists of a metacontroller that observes the inputs and outputs of a non-pedigreed component and verifies formally specified behavior as the system operates. When the system is triggered, a verified recovery controller is deployed. -> 2025-07-08 9:37 am -> - ->[!tip] Brilliant -> Recovery controllers are designed to be safe but very likely disruptive to the operational objective of the system, and thus RTSA systems must balance safety and efficiency. -> 2025-07-08 9:37 am -> - ->[!highlight] Highlight -> Unfortunately, the cost to formally verify a nonpedigreed or black-box autopilot for a variety of vehicle types and use cases is generally prohibitive. -> 2025-07-08 9:44 am -> - ->[!highlight] Highlight -> In order for this mechanism to work, the system needs to be able to distinguish between safe scenarios under which the operation should remain controlled by πn and scenarios that would likely lead to unsafe conditions in which the control should be switched to πr. We assume that a recovery controller πr is given and this work does not focus on its design or implementation. -> 2025-07-08 9:46 am -> - ->[!highlight] Highlight -> The problem that we address in this work is determining how to decide when to switch from the nominal controller πn to the recovery controller πr while balancing the trade-off between safety and efficiency. -> 2025-07-08 9:46 am -> - ->[!warning] Dubious -> We postulate that the task of navigating an aircraft from an origin to a destination by following a pre-planned path is far more complex than the task of predicting whether the aircraft is operating safely within a short time horizon of a given point. -> 2025-07-08 9:47 am -> - ->[!done] Important -> The goal of RTSA systems is to guarantee the safe operation of a system despite having black-box components as a part of its controller. Safe operation is specified by an envelope E ⊂ S which corresponds to a subset of the state space S within which the system is expected to operate ideally. RTSA continuously monitors the state of the system and switches to the recovery controller if and only if when not doing so, would lead the system to exit the safety envelope. -> 2025-07-08 9:50 am -> - ->[!warning] Dubious -> It must switch to the recovery control πr whenever the aircraft leaves the envelope. -> 2025-07-08 9:51 am -> -> *I mean really there is an envelope E_r \subset E \subset S that is the region within the safety envelope that is recoverable... no?* - - ->[!done] Important -> • Its implementation must be easily verifiable. This means it must avoid black box models that are hard to verify such as deep neural networks (DNNs)[3]. -> 2025-07-08 9:53 am -> - ->[!done] Important -> We model the evolution of the flight of an aircraft equipped with an RTSA system by defining the following MDP: M = (S, A, T, R) where the elements are defined below. • State space S ∈ Rp: a vector representing the state of the environment and the vehicle. • Action space A ∈ {deploy, continue}: whether to deploy the recovery system or let the nominal controller remain in control. • Transition T (s, a): a function that specifies the transition probability of the next state s′ given that action a was taken at step s, in our case this will be sampled from a simulator by querying f (s, a). • Reward R(s, a, s′), the reward collected corresponding to the transition. This will be designed to induce the desired behavior. -> 2025-07-08 9:56 am -> - ->[!done] Important -> In this model, the RTSA system is considered the agent while the states correspond to the position, velocity and other relevant information about the aircraft with respect to the envelope and the actions correspond to deploying the recovery controller or not. The agent receives a large negative reward for abandoning the envelope and a smaller negative reward for deploying the recovery controller in situations where it was not required. This reward structure is designed to heavily penalize situations in which the aircraft exits the safety envelope and simultaneously disincentivize unnecessary deployments of the recovery controller. The rewards at each step are weighted by a discount factor γ < 1 such that present rewards are worth more than future ones. -> 2025-07-08 9:59 am -> - ->[!done] Important -> Additionally, we consider the nominal controller to be a black box. All of these conditions combined lead us to operate under the assumption that the transition function is unknown and we do not have access to it. We do, however, have access to simulators from which we can query experience tuples (s, a, r, s′) by providing a state s and an action a and fetching the next state s′ and associated reward r. In this setting we can learn a policy from experience with RL. -> 2025-07-08 10:00 am -> - ->[!fail] This ain't right -> RL has successfully been applied to many fields [8]–[10]. -> 2025-07-08 10:00 am -> -> *Citation stash lmao* - - ->[!done] Important -> Q-learning as described above enables the estimation of tabular Q-functions which are useful for small discrete problems. However, cyber-physical systems often operate in contexts which are better described with a continuous state space. The problem with applying tabular Q-learning to these larger state spaces is not only that they would require a large state-action table but also that a vast amount of experience would be required to accurately estimate the values. An alternative approach to handle continuous state spaces is to use Q-function approximation where the state-action value function is approximated which enables the agent to generalize from limited experience to states that have not been visited before and additionally avoids storing a gigantic table. Policies based on value function approximation have been successfully demonstrated in the aerospace domain before [12]. -> 2025-07-08 11:14 am -> - ->[!warning] Dubious -> Instead, we will restrict our attention to linear value function approximation, which involves defining a set of features Φ(s, a) ∈ Rm that captures relevant information about the state and then use these features to estimate Q by linearly combining them with weights θ ∈ Rm×|A| to estimate the value of each action. In this context, the value function is represented as follows: Q(s, a) = m ∑ i=1 θiφi(s, a) = θT Φ(s, a) (9) Our learning problem is therefore reduced to estimating the parameters θ and selecting our features. Typically, domain knowledge will be leveraged to craft meaningful features Φ(s, a) = (φ1(s, a), φ2(s, a), ..., φm(s, a)), and ideally they would capture some of the geometric information relevant for the problem, e.g. in our setting, heading, velocity and distance to the geofence. The ideas behind the Q-learning algorithm can be extended to the linear value function approximation setting. Here, we initialize our parameters θ and update them at each transition to reduce the error between the predicted value and the observed reward. The algorithm is outlined below and it forms the basis of the learning procedure used in the experiments in Section III. -> 2025-07-08 11:18 am -> -> *This sounds like a constantly updating principal component analysis with some best fitting going on. Interesting, but if the reward is nonlinear (which seems likely?) isn't this problematic?* - - ->[!highlight] Highlight -> We restrict our function family to linear functions which can be easily understood and verified. A major drawback, however, is that linear functions are less expressive than DNNs, which makes their training more difficult and requires careful crafting of features. -> 2025-07-08 11:25 am -> - ->[!done] Important -> Despite the relative simplicity of linear value function approximators when compared to DNNs, we observed that they are able to capture relevant information about the environment and are well suited for this task. -> 2025-07-08 11:29 am -> - ->[!highlight] Highlight -> One approach to address this problem is to avoid or reduce the chance of random exploration. We dramatically increase the likelihood of observing episodes where the mission is completed successfully without exiting the envelope, but we also bias the learning process towards exploitation. It is well known that in order for a policy to converge under Q-learning, exploration must proceed indefinitely [15]. Additionally, in the limit of the the number of steps, the learning policy has to be greedy with respect to the Q-function [15]. Accordingly, avoiding or dramatically reducing random exploration can negatively affect the learning process and should be avoided. -> 2025-07-08 11:33 am -> - ->[!highlight] Highlight -> Instead of randomly initializing the parameters of the Qfunction approximation and then manually biasing the weights to decrease the chance of randomly deploying the recovery controller, we can use a baseline policy to generate episodes in which the RTSA system exhibited a somewhat acceptable performance. From these episodes, we learn the parameters in an offline approach known as batch reinforcement learning. It is only after we learn a good initialization of our parameters that we then start the training process of our policy πRT SA. For this purpose and to have a benchmark to compare our approach to, we define a baseline policy that consists of shrinking the safety envelope by specifying a distance threshold δ > 0. When the vehicle reaches a state that is less than δ distance away from exiting the envelope, the recovery controller is deployed. This naive approach serves both as a baseline for our experiments and also provides us with experience to initialize the weights of our policy before we do on-policy learning. -> 2025-07-08 11:36 am -> - ->[!highlight] Highlight -> We used configuration composed of a hexarotor simulator that models lift rotor aircraft features and includes a three dimensional Bezier curve trajectory definition module, nonlinear multi-rotor dynamics, input/output linearization, nested saturation, a cascade PID flight control model, and an extended Kalman filter estimation model. An illustration of the simulator environment in three dimensions is included in Figure 2 [17]. -> 2025-07-08 11:46 am -> -> *Notably, not really anything special with the controller setup. Shouldn't we be able to do math using the PID controller and set bounds? or perhaps it's a nonlinear issue? Probably the second thing.* - - ->[!fail] This ain't right -> deploying a parachute which was modeled using a simplified model that introduces a drag coefficient that only affects the z coordinates in the simulation. -> 2025-07-08 11:47 am -> - ->[!fail] This ain't right -> The state space in our simulation is comprised of more than 250 variables. Some correspond to simulation parameters 0246 0 1 2 3 −0−.040..200.02.4 0 1 2 3 path waypoints trajectory 0246 −0.4 −0.2 0.0 0.2 0.4 Fig. 3. Example of environment configuration and episode data with wind. such as sampling time, simulation time and physical constants. Another set of variables represent physical magnitudes such as velocity scaling factors, the mass of components of the hexarotor, distribution of the physical components of the hexarotor, moments of inertia and drag coefficients. Other variables represent maximum and minimum roll, pitch and yaw rates, rotor speed and thrust. The sensor readings, their biases, frequencies and other characteristics are also represented by other variables. Other variables represent the state of the controller and the actions it prescribes for the different actuators in the vehicle. And a few of them correspond to the position and velocity of the hexarotor during the simulation. Figure 4 shows the evolution of the position and velocity variables for a simulation episode corresponding to the example environment configuration. All of these variables are needed to completely specify the state of the world in the simulation and illustrate the high dimensional requirements of a somewhat accurate representation of flight dynamics in a simulator. In principle, all these variables would be needed to specify a policy for our RTSA system, but as discussed in Section II we can rely on value function approximation by crafting a set of informative features which significantly reduces the dimensionality of our problem. -> 2025-07-08 11:50 am -> -> *This has to be wrong. There's no way they need 250 states when many of these phenomena must be coupled. Drag coefficients for example are completely dependent on velocity and constants. That is a redundant state, less for the issue of it changing for the recovery controller. I'd still say that's a hybrid system thing.* - - ->[!highlight] Highlight -> In this work we restricted our attention to terminal recovery controllers. -> 2025-07-08 9:43 am -> - - -## Follow-Ups - diff --git a/Zettelkasten/Literature Notes/Safe Reinforcement Learning via Shielding under Partial Observability.md b/Zettelkasten/Literature Notes/Safe Reinforcement Learning via Shielding under Partial Observability.md deleted file mode 100644 index 7a0d3cf5..00000000 --- a/Zettelkasten/Literature Notes/Safe Reinforcement Learning via Shielding under Partial Observability.md +++ /dev/null @@ -1,43 +0,0 @@ ---- -authors: - - - "Carr, Steven" - - - "Jansen, Nils" - - - "Junges, Sebastian" - - - "Topcu, Ufuk" - -citekey: "carrSafeReinforcementLearning2023" -publish_date: 2023-06-26 -journal: "Proceedings of the AAAI Conference on Artificial Intelligence" -volume: 37 -issue: 12 -pages: 14748-14756 -last_import: 2025-05-12 ---- - -# Indexing Information -Published: 2023-06 - -**DOI** -[10.1609/aaai.v37i12.26723](https://doi.org/10.1609/aaai.v37i12.26723) -#General - - -#ToRead - - ->[!Abstract] ->Safe exploration is a common problem in reinforcement learning (RL) that aims to prevent agents from making disastrous decisions while exploring their environment. A family of approaches to this problem assume domain knowledge in the form of a (partial) model of this environment to decide upon the safety of an action. A so-called shield forces the RL agent to select only safe actions. However, for adoption in various applications, one must look beyond enforcing safety and also ensure the applicability of RL with good performance. We extend the applicability of shields via tight integration with state-of-the-art deep RL, and provide an extensive, empirical study in challenging, sparse-reward environments under partial observability. We show that a carefully integrated shield ensures safety and can improve the convergence rate and final performance of RL agents. We furthermore show that a shield can be used to bootstrap state-of-the-art RL agents: they remain safe after initial learning in a shielded setting, allowing us to disable a potentially too conservative shield eventually.>[!seealso] Related Papers -> - -# Annotations -## Notes -![[Paper Notes/Safe Reinforcement Learning via Shielding under Partial Observability.md]] - -## Highlights From Zotero - -## Follow-Ups - diff --git a/Zettelkasten/Literature Notes/Safe Reinforcement Learning via Shielding.md b/Zettelkasten/Literature Notes/Safe Reinforcement Learning via Shielding.md deleted file mode 100644 index 97dac89c..00000000 --- a/Zettelkasten/Literature Notes/Safe Reinforcement Learning via Shielding.md +++ /dev/null @@ -1,63 +0,0 @@ ---- -authors: - - - "Alshiekh, Mohammed" - - - "Bloem, Roderick" - - - "Ehlers, Rüdiger" - - - "Könighofer, Bettina" - - - "Niekum, Scott" - - - "Topcu, Ufuk" - -citekey: "alshiekhSafeReinforcementLearning2018" -publish_date: 2018-04-29 -journal: "Proceedings of the AAAI Conference on Artificial Intelligence" -volume: 32 -issue: 1 -last_import: 2025-05-15 ---- - -# Indexing Information -Published: 2018-04 - -**DOI** -[10.1609/aaai.v32i1.11797](https://doi.org/10.1609/aaai.v32i1.11797) -#Formal-Methods - - -#InFirstPass - - - ->[!Abstract] ->Reinforcement learning algorithms discover policies that maximize reward, but do not necessarily guarantee safety during learning or execution phases. We introduce a new approach to learn optimal policies while enforcing properties expressed in temporal logic. To this end, given the temporal logic specification that is to be obeyed by the learning system, we propose to synthesize a reactive system called a shield. The shield monitors the actions from the learner and corrects them only if the chosen action causes a violation of the specification. We discuss which requirements a shield must meet to preserve the convergence guarantees of the learner. Finally, we demonstrate the versatility of our approach on several challenging reinforcement learning scenarios.>[!seealso] Related Papers -> - -# Annotations -## Notes -![[Safe Reinforcement Learning via Shielding-Note]] - -## Highlights From Zotero - - - - ->[!highlight] Highlight -> . Increasing use of learning-based controllers inphysical systems in the proximity of humans strengthens theconcern of whether these systems will operate safely. -> 2025-05-13 4:28 pm - ->[!tip] Brilliant -> In this paper, we introduce shielded learning, a frame-work that allows applying machine learning to control sys-tems in a way that the correctness of the system’s executionagainst a given specification is assured during the learningand controller execution phases, regardless of how fast the learning process converges. The shield monitors the actionsselected by the learning agent and corrects them if and onlyif the chosen action is unsafe. -> 2025-05-13 4:29 pm - ->[!done] Important -> Last but not least, the shieldingframework is compatible with mechanisms such as functionapproximation, employed by learning algorithms in order to improve their scalability. -> 2025-05-13 4:31 pm - - -## Follow-Ups - diff --git a/Zettelkasten/Literature Notes/The Past, Present and Future of Cyber-Physical Systems - A Focus on Models.md b/Zettelkasten/Literature Notes/The Past, Present and Future of Cyber-Physical Systems - A Focus on Models.md deleted file mode 100644 index 0084d1d9..00000000 --- a/Zettelkasten/Literature Notes/The Past, Present and Future of Cyber-Physical Systems - A Focus on Models.md +++ /dev/null @@ -1,37 +0,0 @@ ---- -authors: - - - "Lee, Edward" - -citekey: "leePresentFutureCyberPhysical2015" -publish_date: 2015-02-26 -journal: "Sensors" -volume: 15 -issue: 3 -pages: 4837-4869 -last_import: 2025-05-12 ---- - -# Indexing Information -Published: 2015-02 - -**DOI** -[10.3390/s150304837](https://doi.org/10.3390/s150304837) - - - -#ToRead - - ->[!Abstract] ->This paper is about better engineering of cyber-physical systems (CPSs) through better models. Deterministic models have historically proven extremely useful and arguably form the kingpin of the industrial revolution and the digital and information technology revolutions. Key deterministic models that have proven successful include differential equations, synchronous digital logic and single-threaded imperative programs. Cyber-physical systems, however, combine these models in such a way that determinism is not preserved. Two projects show that deterministic CPS models with faithful physical realizations are possible and practical. The first project is PRET, which shows that the timing precision of synchronous digital logic can be practically made available at the software level of abstraction. The second project is Ptides (programming temporally-integrated distributed embedded systems), which shows that deterministic models for distributed cyber-physical systems have practical faithful realizations. These projects are existence proofs that deterministic CPS models are possible and practical.>[!seealso] Related Papers -> - -# Annotations -## Notes -![[The Past, Present and Future of Cyber-Physical Systems- A Focus on Models-Note]] - -## Highlights From Zotero - -## Follow-Ups - diff --git a/Zettelkasten/Literature Notes/A systematic classification of neural-network-based control.md b/Zettelkasten/Literature Notes/agarwalSystematicClassificationNeuralnetworkbased1997.md similarity index 88% rename from Zettelkasten/Literature Notes/A systematic classification of neural-network-based control.md rename to Zettelkasten/Literature Notes/agarwalSystematicClassificationNeuralnetworkbased1997.md index c4d1de56..ca7e913f 100644 --- a/Zettelkasten/Literature Notes/A systematic classification of neural-network-based control.md +++ b/Zettelkasten/Literature Notes/agarwalSystematicClassificationNeuralnetworkbased1997.md @@ -4,15 +4,18 @@ authors: - "Agarwal, M." citekey: "agarwalSystematicClassificationNeuralnetworkbased1997" +alias: "agarwalSystematicClassificationNeuralnetworkbased1997" publish_date: 1997-04-01 journal: "IEEE Control Systems Magazine" volume: 17 issue: 2 pages: 75-93 -last_import: 2025-07-21 +last_import: 2025-07-30 --- -# Indexing Information +# A systematic classification of neural-network-based control + +## Indexing Information Published: 1997-04 **DOI** @@ -28,11 +31,11 @@ Published: 1997-04 >Successful industrial applications and favorable comparisons with conventional alternatives have motivated the development of a large number of schemes for neural-network-based control. Each scheme is usually composed of several independent functional features, which makes it difficult to identify precisely what is new in the scheme. Help from available overviews is therefore often inadequate, since they usually discuss only the most important overall schemes. This work breaks the available schemes down to their essential functional features and organizes the latter into a multi-level classification. The classification reveals that similar schemes often get placed in different categories, fundamentally different features often get lumped into a single category, and proposed new schemes are often merely permutations and combinations of the well-established fundamental features. The classification has two main sections: neural network only as an aid; and neural network as controller.>[!seealso] Related Papers > -# Annotations -## Notes -![[A systematic classification of neural-network-based control-Note]] +## Annotations +### Notes +![[Zettelkasten/Literature Notes/Notes on Papers/A systematic classification of neural-network-based control-notes.md]] -## Highlights From Zotero +### Highlights From Zotero >[!highlight] Highlight > rigorous comparisons neural-network controllers have fared better than well- established conventional options when the plant characteristics are poorly known [2-61. > 2025-04-15 9:18 am @@ -64,5 +67,5 @@ Published: 1997-04 -## Follow-Ups +### Follow-Ups diff --git a/Zettelkasten/Literature Notes/Automation levels for nuclear reactor operations - A revised perspective.md b/Zettelkasten/Literature Notes/albertiAutomationLevelsNuclear2023.md similarity index 96% rename from Zettelkasten/Literature Notes/Automation levels for nuclear reactor operations - A revised perspective.md rename to Zettelkasten/Literature Notes/albertiAutomationLevelsNuclear2023.md index 288d404c..d0bbc49b 100644 --- a/Zettelkasten/Literature Notes/Automation levels for nuclear reactor operations - A revised perspective.md +++ b/Zettelkasten/Literature Notes/albertiAutomationLevelsNuclear2023.md @@ -12,6 +12,7 @@ authors: - "de Oliveira, Cassiano R. E." citekey: "albertiAutomationLevelsNuclear2023" +alias: "albertiAutomationLevelsNuclear2023" publish_date: 2023-03-01 journal: "Progress in Nuclear Energy" volume: 157 @@ -19,7 +20,9 @@ pages: 104559 last_import: 2025-07-30 --- -# Indexing Information +# Automation levels for nuclear reactor operations: A revised perspective + +## Indexing Information Published: 2023-03 **DOI** @@ -35,11 +38,11 @@ Published: 2023-03 >This work serves to propose updated levels of automation for nuclear reactor operations, as a result of considering long-term economic and commercial ambitions of the advanced reactor developer community. As in other fields such as road-going vehicles and aviation, reactor technologies can benefit from modern automation through the resulting reduction in operations and maintenance costs, while still maintaining the current industry standards regarding safety, resilience, reliability, overall performance, and the capacity for root-cause analysis. The current guidelines on automation levels, as published by the U.S. Nuclear Regulatory Commission in Section 9 of NUREG-0700, reflect outdated design principles that implicitly limit the potential of automation innovation for reactor operations, particularly in regard to advanced reactors intended to operate in remote locations or be used for off-grid applications. Motivated by the operational paradigms anticipated for future reactor designs, we propose a six-level approach that aligns with contemporary automation concepts as well as automation level definitions from other non-nuclear safety–critical industries. These levels build upon the current guidelines in order to enable next-generation nuclear reactor technologies to become increasingly economically competitive and commercially viable relative to competing power generation sources. Using a hypothetical heat removal reactor transient, we provide examples of how the human–machine interactions change at each level of automation, ranging from traditional operator control (Level 0) to operator-free unattended operations (Level 5)—the latter being one of the key attributes proposed at the Fission Battery Initiative led by Idaho National Laboratory. Finally, we critically examine the identified challenges, knowledge gaps, and enabling technologies to achieve advanced levels of automation.>[!seealso] Related Papers > -# Annotations -## Notes -![[Automation levels for nuclear reactor operations- A revised perspective - Note]] +## Annotations +### Notes +![[Zettelkasten/Literature Notes/Notes on Papers/Automation levels for nuclear reactor operations- A revised perspective-notes.md]] -## Highlights From Zotero +### Highlights From Zotero >[!highlight] Highlight > we propose a six-level approach that aligns with contemporary automation concepts as well as automation level definitions from other nonnuclear safety-critical industries. > 2025-07-24 9:42 am @@ -117,7 +120,7 @@ Published: 2023-03 -## Follow-Ups +### Follow-Ups >[!example] >In the present paradigm, much of this automation comes in the form of operator support. Examples include computerized operator support systems that assess various alarms and provide fault diagnoses to operators [26, 27, 28, 29], computer-based procedure systems that provide necessary data and procedures to assist operators by identifying tasks in real-time to foster safety goal achievement [30, 31, 32], and the automatic activation of primary safety systems (e.g., emergency core cooling systems) during severe accidents. diff --git a/Zettelkasten/Literature Notes/Remote nuclear microreactors - a preliminary economic evaluation of digital twins and centralized offsite control.md b/Zettelkasten/Literature Notes/bryanRemoteNuclearMicroreactors2023.md similarity index 89% rename from Zettelkasten/Literature Notes/Remote nuclear microreactors - a preliminary economic evaluation of digital twins and centralized offsite control.md rename to Zettelkasten/Literature Notes/bryanRemoteNuclearMicroreactors2023.md index 51ba1dca..3a8d5500 100644 --- a/Zettelkasten/Literature Notes/Remote nuclear microreactors - a preliminary economic evaluation of digital twins and centralized offsite control.md +++ b/Zettelkasten/Literature Notes/bryanRemoteNuclearMicroreactors2023.md @@ -10,18 +10,21 @@ authors: - "Browning, Jeren M." citekey: "bryanRemoteNuclearMicroreactors2023" +alias: "bryanRemoteNuclearMicroreactors2023" publish_date: 2023-12-21 journal: "Frontiers in Nuclear Engineering" volume: 2 -last_import: 2025-07-23 +last_import: 2025-07-30 --- -# Indexing Information +# Remote nuclear microreactors: a preliminary economic evaluation of digital twins and centralized offsite control + +## Indexing Information Published: 2023-12 **DOI** [10.3389/fnuen.2023.1293908](https://doi.org/10.3389/fnuen.2023.1293908) -#Economics, #Microreactor, #Digital-Twin, #fission-battery, #Remote-operation +#Economics, #Digital-Twin, #fission-battery, #Microreactor, #Remote-operation #InFirstPass @@ -32,11 +35,11 @@ Published: 2023-12 >The nuclear energy industry is looking to next-generation reactor designs to augment, diversify, and expand generation capacity in an increasingly complex and varied energy landscape. A key element in this objective is microreactors—small nuclear reactors which can provide flexible capacity at a reduced scale compared to traditional large-scale nuclear reactors. Specifically, microreactors could be used to provide clean, reliable combined heat and power to remote communities, worksites, or facilities. However, the construction and operations and maintenance costs to supply the required operator staffing and physical supporting assets, such as control rooms, could be a limiting factor for first adopters of the technology. Opportunities to reduce the cost of monitoring and control activities could enable early adoption, allowing economies of learning to take effect, spurring further adoption. A reduction in the number and cost intensity of control rooms and operators per deployed microreactor could significantly decrease the overall cost for a fleet of microreactors. To optimize microreactor economic competitiveness, one solution would be to establish an off-site operation facility for centralized monitoring and control (CM&C) of a fleet of microreactors. Leveraging advances in digital instrumentation and control systems could bolster the safety, reliability, and security of the remote communication architecture inherently required to operate remotely. Digital twins (DTs) are virtual replicas of physical assets which can be used for a variety of applications, including analyzing I&C signals against a validated model to perform several analysis and prediction functions. When implemented properly, DTs can potentially detect anomalies and component failures, and serve as a diagnostic tool for operators. These technologies can enhance operator understanding and awareness, reduce the management demand time on operators, and increase asset uptime by providing early alerts for failures alongside insights to aid in predictive maintenance. Furthermore, a DT system could enhance the secure and reliable communication architecture necessary for remote microreactor operation by verifying signals and suggesting or automating controls, thereby boosting their economic viability. This research examines the economic effects of various control strategies ranging from many individually and on-site controlled reactors to co-management of all microreactors in a system from a single, off-site control center. Results from the analysis are positive, revealing significant cost-reduction opportunities.>[!seealso] Related Papers > -# Annotations -## Notes -![[Remote nuclear microreactors- a preliminary economic evaluation of digital twins and centralized offsite control-Note]] +## Annotations +### Notes +![[Zettelkasten/Literature Notes/Notes on Papers/Remote nuclear microreactors- a preliminary economic evaluation of digital twins and centralized offsite control-notes.md]] -## Highlights From Zotero +### Highlights From Zotero >[!warning] Dubious > on-site human monitoring, control, and manual physical maintenance of microreactors can be costly–particularly > 2024-12-26 7:54 pm @@ -73,5 +76,5 @@ Published: 2023-12 > -## Follow-Ups +### Follow-Ups diff --git a/Zettelkasten/Literature Notes/Reluplex - An Efficient SMT Solver for Verifying Deep Neural Networks.md b/Zettelkasten/Literature Notes/katzReluplexEfficientSMT2017.md similarity index 93% rename from Zettelkasten/Literature Notes/Reluplex - An Efficient SMT Solver for Verifying Deep Neural Networks.md rename to Zettelkasten/Literature Notes/katzReluplexEfficientSMT2017.md index 04158b76..40ec4839 100644 --- a/Zettelkasten/Literature Notes/Reluplex - An Efficient SMT Solver for Verifying Deep Neural Networks.md +++ b/Zettelkasten/Literature Notes/katzReluplexEfficientSMT2017.md @@ -16,14 +16,17 @@ authors: - "Kunčak, Viktor" citekey: "katzReluplexEfficientSMT2017" +alias: "katzReluplexEfficientSMT2017" publish_date: 2017-01-01 publisher: "Springer International Publishing" location: "Cham" pages: 97-117 -last_import: 2025-05-15 +last_import: 2025-07-30 --- -# Indexing Information +# Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks + +## Indexing Information Published: 2017-01 **DOI** @@ -41,38 +44,43 @@ Published: 2017-01 >Deep neural networks have emerged as a widely used and effective means for tackling complex, real-world problems. However, a major obstacle in applying them to safety-critical systems is the great difficulty in providing formal guarantees about their behavior. We present a novel, scalable, and efficient technique for verifying properties of deep neural networks (or providing counter-examples). The technique is based on the simplex method, extended to handle the non-convex Rectified Linear Unit (ReLU) activation function, which is a crucial ingredient in many modern neural networks. The verification procedure tackles neural networks as a whole, without making any simplifying assumptions. We evaluated our technique on a prototype deep neural network implementation of the next-generation airborne collision avoidance system for unmanned aircraft (ACAS Xu). Results show that our technique can successfully prove properties of networks that are an order of magnitude larger than the largest networks verified using existing methods.>[!seealso] Related Papers > -# Annotations -## Notes -![[Reluplex- An Efficient SMT Solver for Verifying Deep Neural Networks-Note]] +## Annotations +### Notes +![[Zettelkasten/Literature Notes/Notes on Papers/Reluplex- An Efficient SMT Solver for Verifying Deep Neural Networks-notes.md]] -## Highlights From Zotero +### Highlights From Zotero >[!done] Important > The technique is basedon the simplex method, extended to handle the non-convex RectifiedLinear Unit (ReLU ) activation function, which is a crucial ingredientin many modern neural networks. The verification procedure tacklesneural networks as a whole, without making any simplifying assump-tions. We evaluated our technique on a prototype deep neural networkimplementation of the next-generation airborne collision avoidance sys-tem for unmanned aircraft (ACAS Xu). Results show that our techniquecan successfully prove properties of networks that are an order of mag-nitude larger than the largest networks verified using existing methods. > 2025-05-13 4:42 pm +> >[!done] Important > Past efforts at verifying properties of DNNs with ReLUs have had to make significant simplifying assumptions [3,10]—for instance, by considering only small input regions in which all ReLUs are fixed at either the activeor inactive state [3], hence making the problem convex but at the cost of beingable to verify only an approximation of the desired property > 2025-05-13 4:45 pm +> >[!tip] Brilliant > We propose a novel, scalable, and efficient algorithm for verifying propertiesof DNNs with ReLUs. We address the issue of the activation functions headon, by extending the simplex algorithm—a standard algorithm for solving LP instances—to support ReLU constraints. This is achieved by leveraging the piece-wise linear nature of ReLUs and attempting to gradually satisfy the constraintsthat they impose as the algorithm searches for a feasible solution. We call the algorithm Reluplex, for “ReLU with Simplex”. > 2025-05-13 4:46 pm +> >[!highlight] Highlight > The problem’s NP-completeness means that we must expect the worst-case performance of the algorithm to be poor. However, as is often the case with SAT and SMT solvers, the performance in practice can be quite reasonable; > 2025-05-13 4:47 pm +> >[!highlight] Highlight > Our contributions can be summarized as follows. We (i) present Reluplex,an SMT solver for a theory of linear real arithmetic with ReLU constraints; (ii) show how DNNs and properties of interest can be encoded as inputs to Reluplex; (iii) discuss several implementation details that are crucial to performance and scalability, such as the use of floating-point arithmetic, bound derivation for ReLU variables, and conflict analysis; and (iv) conduct a thorough evaluationon the DNN implementation of the prototype ACAS Xu system, demonstratingthe ability of Reluplex to scale to DNNs that are an order of magnitude largerthan those that can be analyzed using existing techniques. > 2025-05-13 4:48 pm +> -## Follow-Ups +### Follow-Ups >[!example] >are trained over a finiteset of inputs and outputs and are expected to generalize, i.e. to behave correctly for previously-unseen inputs. However, it has been observed that DNNs can react in unexpected and incorrect ways to even slight perturbations of their inputs [34]. diff --git a/Zettelkasten/Literature Notes/leePresentFutureCyberPhysical2015.md b/Zettelkasten/Literature Notes/leePresentFutureCyberPhysical2015.md new file mode 100644 index 00000000..604b67f2 --- /dev/null +++ b/Zettelkasten/Literature Notes/leePresentFutureCyberPhysical2015.md @@ -0,0 +1,69 @@ +--- +authors: + + - "Lee, Edward A." + +citekey: "leePresentFutureCyberPhysical2015" +alias: "leePresentFutureCyberPhysical2015" +publish_date: 2015-03-01 +journal: "Sensors" +volume: 15 +issue: 3 +pages: 4837-4869 +last_import: 2025-07-30 +--- + +# The Past, Present and Future of Cyber-Physical Systems: A Focus on Models + +## Indexing Information +Published: 2015-03 + +**DOI** +[10.3390/s150304837](https://doi.org/10.3390/s150304837) +#clock-synchronization, #cyber-physical-systems, #distributed-systems, #PRET-machines, #real-time-systems, #time-synchronization + + +#InFirstPass + + + +>[!Abstract] +>This paper is about better engineering of cyber-physical systems (CPSs) through better models. Deterministic models have historically proven extremely useful and arguably form the kingpin of the industrial revolution and the digital and information technology revolutions. Key deterministic models that have proven successful include differential equations, synchronous digital logic and single-threaded imperative programs. Cyber-physical systems, however, combine these models in such a way that determinism is not preserved. Two projects show that deterministic CPS models with faithful physical realizations are possible and practical. The first project is PRET, which shows that the timing precision of synchronous digital logic can be practically made available at the software level of abstraction. The second project is Ptides (programming temporally-integrated distributed embedded systems), which shows that deterministic models for distributed cyber-physical systems have practical faithful realizations. These projects are existence proofs that deterministic CPS models are possible and practical.>[!seealso] Related Papers +> + +## Annotations +### Notes +![[Zettelkasten/Literature Notes/Notes on Papers/The Past, Present and Future of Cyber-Physical Systems- A Focus on Models-notes.md]] + +### Highlights From Zotero + + + +>[!tip] Brilliant +> As an intellectual challenge, CPS is about the intersection, not the union, of the physical and the cyber. It combines engineering models and methods from mechanical, environmental, civil, electrical, biomedical, chemical, aeronautical and industrial engineering with the models and methods of computerscience. This paper argues that these models and methods do not combine easily and that theconsequently CPS constitutes a new engineering discipline that demands its own models and methods. +> 2025-05-09 1:50 pm +> + +>[!fail] This ain't right +> His control logic was effectively acomputation, albeit one carried out with analog circuits and mechanical parts, and therefore, cyberneticsis the conjunction of physical processes, computation and communication. +> 2025-05-09 1:52 pm +> + +>[!tip] Brilliant +> the fog (like the cloud, but closer to the ground) +> 2025-05-09 1:53 pm +> + +>[!highlight] Highlight +> Engineers often conflate the model with the thing being modeled. For example, electrical engineersmay refer to an ODE as “the system” and use it to assert, for example, that “the system is stable.”Such a statement, however, is not a valid statement about a physical system. It is a statement about a model of the physical system. Arguably, any definitive statement about a system (stability, determinism,timeliness, reliability, safety) is in fact a statement about a model and not a statement about the thingbeing modeled. I call this idea the “Kopetz principle,” after Hermann Kopetz, from whom I learned it. Emphasizing the need to avoid conflating the model with the thing being modeled, Solomon WolfGolomb famously stated “you will never strike oil by drilling through the map” [2]. +> 2025-04-30 9:23 pm +> + +>[!done] Important +> Ptides leverages network clock synchronization, which I believe will become ubiquitous +> 2025-05-09 1:56 pm +> + + +### Follow-Ups + diff --git a/Zettelkasten/Literature Notes/Economics and finance of Small Modular Reactors - A systematic review and research agenda.md b/Zettelkasten/Literature Notes/mignaccaEconomicsFinanceSmall2020.md similarity index 91% rename from Zettelkasten/Literature Notes/Economics and finance of Small Modular Reactors - A systematic review and research agenda.md rename to Zettelkasten/Literature Notes/mignaccaEconomicsFinanceSmall2020.md index 0dd308a7..c5ed646f 100644 --- a/Zettelkasten/Literature Notes/Economics and finance of Small Modular Reactors - A systematic review and research agenda.md +++ b/Zettelkasten/Literature Notes/mignaccaEconomicsFinanceSmall2020.md @@ -6,14 +6,17 @@ authors: - "Locatelli, G." citekey: "mignaccaEconomicsFinanceSmall2020" +alias: "mignaccaEconomicsFinanceSmall2020" publish_date: 2020-02-01 journal: "Renewable and Sustainable Energy Reviews" volume: 118 pages: 109519 -last_import: 2025-07-21 +last_import: 2025-07-30 --- -# Indexing Information +# Economics and finance of Small Modular Reactors: A systematic review and research agenda + +## Indexing Information Published: 2020-02 **DOI** @@ -21,18 +24,19 @@ Published: 2020-02 #Economics, #Finance, #Modularisation, #Modularity, #Small-modular-reactor, #SMR -#ToRead +#InFirstPass + >[!Abstract] >The interest toward Small Modular nuclear Reactors (SMRs) is growing, and the economic competitiveness of SMRs versus large reactors is a key topic. Leveraging a systematic literature review, this paper firstly provides an overview of “what we know” and “what we do not know” about the economics and finance of SMRs. Secondly, the paper develops a research agenda. Several documents discuss the economics of SMRs, highlighting how the size is not the only factor to consider in the comparison; remarkably, other factors (co-siting economies, modularisation, modularity, construction time, etc.) are relevant. The vast majority of the literature focuses on economic and financial performance indicators (e.g. Levelized Cost of Electricity, Net Present Value, and Internal Rate of Return) and SMR capital cost. Remarkably, very few documents deal with operating and decommissioning costs or take a programme (and its financing) rather than a “single project/plant/site” perspective. Furthermore, there is a gap in knowledge about the cost-benefit analysis of the “modular construction” and SMR decommissioning.>[!seealso] Related Papers > -# Annotations -## Notes -![[Economics and finance of Small Modular Reactors- A systematic review and research agenda-Note]] +## Annotations +### Notes +![[Zettelkasten/Literature Notes/Notes on Papers/Economics and finance of Small Modular Reactors- A systematic review and research agenda-notes.md]] -## Highlights From Zotero +### Highlights From Zotero >[!tip] Brilliant > Remarkably, very few documents deal with operating and decommissioning costs or take a programme (and its financing) rather than a “single project/plant/site” perspective. Furthermore, there is a gap in knowledge about the cost-benefit analysis of the “modular construction” and SMR decommissioning. > 2025-07-16 12:27 pm @@ -76,5 +80,5 @@ Published: 2020-02 > -## Follow-Ups +### Follow-Ups diff --git a/Zettelkasten/Literature Notes/Formal verification of neural network controlled autonomous systems.md b/Zettelkasten/Literature Notes/sunFormalVerificationNeural2019.md similarity index 79% rename from Zettelkasten/Literature Notes/Formal verification of neural network controlled autonomous systems.md rename to Zettelkasten/Literature Notes/sunFormalVerificationNeural2019.md index bd0930e0..18f94f18 100644 --- a/Zettelkasten/Literature Notes/Formal verification of neural network controlled autonomous systems.md +++ b/Zettelkasten/Literature Notes/sunFormalVerificationNeural2019.md @@ -8,14 +8,17 @@ authors: - "Shoukry, Yasser" citekey: "sunFormalVerificationNeural2019" +alias: "sunFormalVerificationNeural2019" publish_date: 2019-04-16 publisher: "Association for Computing Machinery" location: "New York, NY, USA" pages: 147–156 -last_import: 2025-05-12 +last_import: 2025-07-30 --- -# Indexing Information +# Formal verification of neural network controlled autonomous systems + +## Indexing Information Published: 2019-04 **DOI** @@ -33,59 +36,66 @@ Published: 2019-04 >In this paper, we consider the problem of formally verifying the safety of an autonomous robot equipped with a Neural Network (NN) controller that processes LiDAR images to produce control actions. Given a workspace that is characterized by a set of polytopic obstacles, our objective is to compute the set of safe initial states such that a robot trajectory starting from these initial states is guaranteed to avoid the obstacles. Our approach is to construct a finite state abstraction of the system and use standard reachability analysis over the finite state abstraction to compute the set of safe initial states. To mathematically model the imaging function, that maps the robot position to the LiDAR image, we introduce the notion of imaging-adapted partitions of the workspace in which the imaging function is guaranteed to be affine. Given this workspace partitioning, a discrete-time linear dynamics of the robot, and a pre-trained NN controller with Rectified Linear Unit (ReLU) non-linearity, we utilize a Satisfiability Modulo Convex (SMC) encoding to enumerate all the possible assignments of different ReLUs. To accelerate this process, we develop a pre-processing algorithm that could rapidly prune the space of feasible ReLU assignments. Finally, we demonstrate the efficiency of the proposed algorithms using numerical simulations with the increasing complexity of the neural network controller.>[!seealso] Related Papers > -# Annotations -## Notes -![[Formal verification of neural network controlled autonomous systems-Note]] +## Annotations +### Notes +![[Zettelkasten/Literature Notes/Notes on Papers/Formal verification of neural network controlled autonomous systems-notes.md]] -## Highlights From Zotero +### Highlights From Zotero >[!highlight] Highlight > our objective is to compute the set of safe initialstates such that a robot trajectory starting from these initial states is guaranteed to avoid the obstacles. > 2025-05-09 1:23 pm +> +>[!quote] Other Highlight +> we utilize a Satisfiability Modulo Convex (SMC) encoding to enumerate all the possible assignments of different ReLUs. +> 2025-05-12 11:29 am +> >[!done] Important > Toaccelerate this process, we develop a pre-processing algorithm thatcould rapidly prune the space of feasible ReLU assignments. > 2025-05-09 1:25 pm +> >[!highlight] Highlight > the safety and reliabilityof these AI-enabled CPS is still an under-studied problem. It is thenunsurprising that the failure of these AI-controlled CPS in several,safety-critical, situations leads to human fatalities [1]. > 2025-05-09 1:26 pm +> >[!tip] Brilliant > Representatives of the first class, namely testing of neural net-works, are the works reported in [9–18] in which the neural networkis treated as a white box, and test cases are generated to maximizedifferent coverage criteria. Such coverage criteria include neuroncoverage, condition/decision coverage, and multi-granularity test-ing criteria. On the one hand, maximizing test coverage gives systemdesigners confidence that the networks are reasonably free fromdefect. On the other hand, testing does not formally guarantee thata neural network satisfies a formal specification. > 2025-05-09 1:27 pm +> >[!highlight] Highlight > To take into consideration the effect of the neural network de-cisions on the entire system behavior, several researchers focusedon the falsification (or semi-formal verification) of autonomoussystems that include machine learning components [19–21]. Insuch falsification frameworks, the objective is to generate cornertest cases that forces a violation of system-level specifications > 2025-05-09 1:28 pm +> +>[!quote] Other Highlight +> Therefore, recent works focused en-tirely on verifying neural networks against simple input-output specifications [28–33]. Such input-output techniques compute aguaranteed range for the output of a deep neural network givena set of inputs represented as a convex polyhedron. +> 2025-05-12 11:29 am +> +>[!quote] Other Highlight +> For example, by using binary variables to en-code piecewise linear functions, the constraints of ReLU functions are encoded as a Mixed-Integer Linear Programming (MILP). Com-bining output specifications that are expressed in terms of Linear Programming (LP), the verification problem eventually turns to aMILP feasibility problem [32, 34]. +> 2025-05-12 11:29 am +> >[!highlight] Highlight > Unfortunately, the input-output range properties are simplistic and fail to capture the safety and reliability of cyber-physical systems when controlled by a neural network. Recent works showed how to perform reachability-based verification of closed-loop systems in the presence of learning components [38–40]. Reachabilityanalysis is performed by either separately estimating the output setof the neural network and the reachable set of continuous dynamics [38], or by translating the neural network controlled system into a hybrid system [39]. Once the neural network controlled system is translated into a hybrid system, off-the-shelf existing verificationtools of hybrid systems, such as SpaceEx [41] for piecewise affinedynamics and Flow∗ [42] for nonlinear dynamics, can be used to verify safety properties of the system. Another related technique is the safety verification using barrier certificates [43]. In suchapproach, a barrier function is searched using several simulationtraces to provide a certificate that unsafe states are not reachablefrom a given set of initial states. > 2025-05-09 1:33 pm +> >[!done] Important > Arguably, the ability of neural networks toprocess high-bandwidth sensory signals (e.g., cameras and LiDARs)is one of the main motivations behind the current explosion in theuse of machine learning in robotics and CPS. > 2025-05-09 1:35 pm +> -## Follow-Ups +### Follow-Ups ->[!example] - >we utilize a Satisfiability Modulo Convex (SMC) encoding to enumerate all the possible assignments of different ReLUs. - >- [x] #Follow-Up ✅ 2025-05-12 - ->[!example] - >Therefore, recent works focused en-tirely on verifying neural networks against simple input-output specifications [28–33]. Such input-output techniques compute aguaranteed range for the output of a deep neural network givena set of inputs represented as a convex polyhedron. - >- [x] #Follow-Up ✅ 2025-05-12 - ->[!example] - >For example, by using binary variables to en-code piecewise linear functions, the constraints of ReLU functions are encoded as a Mixed-Integer Linear Programming (MILP). Com-bining output specifications that are expressed in terms of Linear Programming (LP), the verification problem eventually turns to aMILP feasibility problem [32, 34]. - >- [x] #Follow-Up ✅ 2025-05-12 - diff --git a/Zettelkasten/Literature Notes/Enhancing Cyber-Physical System Dependability via Synthesis - Challenges and Future Directions.md b/Zettelkasten/Literature Notes/taylorEnhancingCyberPhysicalSystem2025.md similarity index 71% rename from Zettelkasten/Literature Notes/Enhancing Cyber-Physical System Dependability via Synthesis - Challenges and Future Directions.md rename to Zettelkasten/Literature Notes/taylorEnhancingCyberPhysicalSystem2025.md index d8ab07b5..614dcd54 100644 --- a/Zettelkasten/Literature Notes/Enhancing Cyber-Physical System Dependability via Synthesis - Challenges and Future Directions.md +++ b/Zettelkasten/Literature Notes/taylorEnhancingCyberPhysicalSystem2025.md @@ -6,12 +6,15 @@ authors: - "Amorim, Arthur" citekey: "taylorEnhancingCyberPhysicalSystem2025" +alias: "taylorEnhancingCyberPhysicalSystem2025" publish_date: 2025-06-23 location: "Naples, Italy" -last_import: 2025-05-12 +last_import: 2025-07-30 --- -# Indexing Information +# Enhancing Cyber-Physical System Dependability via Synthesis: Challenges and Future Directions + +## Indexing Information Published: 2025-06 @@ -24,18 +27,20 @@ Published: 2025-06 >[!seealso] Related Papers > -# Annotations -## Notes -![[Enhancing Cyber-Physical System Dependability via Synthesis- Challenges and Future Directions-Note]] +## Annotations +### Notes +![[Zettelkasten/Literature Notes/Notes on Papers/Enhancing Cyber-Physical System Dependability via Synthesis- Challenges and Future Directions-notes.md]] -## Highlights From Zotero +### Highlights From Zotero >[!done] Important > By formally designing safety and liveness requirements and synthesizing software that adheres to these specifications, unsafe behaviors can be prevented from the very beginning of system development. > 2025-05-06 4:37 pm +> >[!warning] Dubious > Preventing unsafe behaviors is achievable by meticulously engineering control software to prevent such behaviors. However, software often contains bugs that adversaries can exploit. Preventing bugs involves specifying the correct behavior of the system and proving that the software implementation adheres to the specification. However, these program verification-based approaches are challenging to apply [5], [9], [24]. > 2025-05-06 4:44 pm +> > *Bugs r bad. Basically the main point. @@ -43,5 +48,5 @@ These citations don't really support the claim that they're attached to.* -## Follow-Ups +### Follow-Ups diff --git a/Zettelkasten/Literature Notes/testing note.md b/Zettelkasten/Literature Notes/testing note.md deleted file mode 100644 index 0249f61d..00000000 --- a/Zettelkasten/Literature Notes/testing note.md +++ /dev/null @@ -1 +0,0 @@ -this is a testing note to see if autocomplete is finding this \ No newline at end of file