vault backup: 2025-07-07 13:35:20

.obsidian/plugins/colored-tags/data.json

@@ -271,7 +271,14 @@
     "development-process": 259,
     "safety": 260,
     "static-analysis": 261,
-    "Computer-Science---Cryptography-and-Security": 262
+    "Computer-Science---Cryptography-and-Security": 262,
+    "deep-reinforcement-learning": 263,
+    "hybrid-automaton": 264,
+    "imitation-learning": 265,
+    "reachability-analysis": 266,
+    "Runtime": 267,
+    "Switches": 268,
+    "Vehicle-dynamics": 269
   },
   "_version": 3
 }

Literature Notes/Literature Note.md

@@ -97,7 +97,7 @@ Published: {{ date | format("YYYY-MM") }}
 
 # Annotations
 ## Notes
-![[Paper Notes/{{ title | replace(':', '-')  | replace('&', 'and')  | replace('<', '')  | replace('>', '')  | replace('#', '')  | replace('*', '')  | replace('(', '')  | replace(')', '')  | replace('[', '')  | replace(']', '')  }}.md]]
+![[Notes on Papers/{{ title | replace(':', '-')  | replace('&', 'and')  | replace('<', '')  | replace('>', '')  | replace('#', '')  | replace('*', '')  | replace('(', '')  | replace(')', '')  | replace('[', '')  | replace(']', '')  }}.md]]
 
 ## Highlights From Zotero
 {#- Process non-Purple highlights -#}

Literature Notes/On Using Real-Time Reachability for the Safety Assurance of Machine Learning Controllers.md

@@ -0,0 +1,107 @@
+---
+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
+![[Notes on Papers/On Using Real-Time Reachability for the Safety Assurance of Machine Learning Controllers]]
+
+## 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
+  

Notes on Papers/On Using Real-Time Reachability for the Safety Assurance of Machine Learning Controllers.md

@@ -0,0 +1,21 @@
+# First Pass
+**Category:** Experimental Results
+**Context:** They used a F1/10 model of an autonomous car to test out a simplex
+safety structure 
+**Correctness:** 
+**Contributions:** 
+**Clarity:** 
+
+# Second Pass
+**What is the main thrust?**
+
+**What is the supporting evidence?**
+
+**What are the key findings?**
+
+# Third Pass
+**Recreation Notes:**
+
+**Hidden Findings:**
+
+**Weak Points? Strong Points?**