diff --git a/.obsidian/plugins/colored-tags/data.json b/.obsidian/plugins/colored-tags/data.json index 3ccdebcc..4bcfc6f7 100755 --- a/.obsidian/plugins/colored-tags/data.json +++ b/.obsidian/plugins/colored-tags/data.json @@ -226,7 +226,13 @@ "ToRead": 214, "dead": 215, "Computer-Science---Logic-in-Computer-Science": 216, - "Computer-Science---Programming-Languages": 217 + "Computer-Science---Programming-Languages": 217, + "clock-synchronization": 218, + "cyber-physical-systems": 219, + "distributed-systems": 220, + "PRET-machines": 221, + "real-time-systems": 222, + "time-synchronization": 223 }, "_version": 3 } \ No newline at end of file diff --git a/Literature Notes/A Review of Formal Methods applied to Machine Learning.md b/Literature Notes/A Review of Formal Methods applied to Machine Learning.md index d1bb865e..b88afe0d 100644 --- a/Literature Notes/A Review of Formal Methods applied to Machine Learning.md +++ b/Literature Notes/A Review of Formal Methods applied to Machine Learning.md @@ -7,13 +7,13 @@ authors: citekey: "urbanReviewFormalMethods2021" publish_date: 2021-04-21 -last_import: 2025-05-06 +last_import: 2025-05-12 --- # Indexing Information **DOI** [10.48550/arXiv.2104.02466](https://doi.org/10.48550/arXiv.2104.02466) -#Computer-Science---Logic-in-Computer-Science, #Computer-Science---Machine-Learning, #Computer-Science---Programming-Languages +#Computer-Science---Machine-Learning, #Computer-Science---Logic-in-Computer-Science, #Computer-Science---Programming-Languages #InFirstPass diff --git a/Literature Notes/Effectiveness and efficiency of search methods in systematic reviews of complex evidence - audit of primary sources.md b/Literature Notes/Effectiveness and efficiency of search methods in systematic reviews of complex evidence - audit of primary sources.md new file mode 100644 index 00000000..c20e9065 --- /dev/null +++ b/Literature Notes/Effectiveness and efficiency of search methods in systematic reviews of complex evidence - audit of primary sources.md @@ -0,0 +1,53 @@ +--- +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/Literature Notes/Formal verification of neural network controlled autonomous systems.md b/Literature Notes/Formal verification of neural network controlled autonomous systems.md index 15d4bffa..65a262c2 100644 --- a/Literature Notes/Formal verification of neural network controlled autonomous systems.md +++ b/Literature Notes/Formal verification of neural network controlled autonomous systems.md @@ -12,7 +12,7 @@ publish_date: 2019-04-16 publisher: "Association for Computing Machinery" location: "New York, NY, USA" pages: 147–156 -last_import: 2025-05-06 +last_import: 2025-05-12 --- # Indexing Information @@ -23,7 +23,8 @@ last_import: 2025-05-06 -#ToRead +#InFirstPass + >[!Abstract] @@ -35,6 +36,54 @@ last_import: 2025-05-06 ![[Paper Notes/Formal verification of neural network controlled autonomous systems.md]] ## 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 + + +>[!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 + + + + + + +>[!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 +>[!example] + >we utilize a Satisfiability Modulo Convex (SMC) encoding to enumerate all the possible assignments of different ReLUs. + >- [ ] #Follow-Up + +>[!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. + >- [ ] #Follow-Up + +>[!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]. + >- [ ] #Follow-Up + diff --git a/Literature Notes/The Past, Present and Future of Cyber-Physical Systems - A Focus on Models.md b/Literature Notes/The Past, Present and Future of Cyber-Physical Systems - A Focus on Models.md new file mode 100644 index 00000000..1d53a510 --- /dev/null +++ b/Literature Notes/The Past, Present and Future of Cyber-Physical Systems - A Focus on Models.md @@ -0,0 +1,59 @@ +--- +authors: + + - "Lee, Edward A." + +citekey: "leePresentFutureCyberPhysical2015a" +publish_date: 2015-03-01 +journal: "Sensors" +volume: 15 +issue: 3 +pages: 4837-4869 +last_import: 2025-05-12 +--- + +# Indexing Information +**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 +![[Paper Notes/The Past, Present and Future of Cyber-Physical Systems- A Focus on Models.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/Paper Notes/Formal verification of neural network controlled autonomous systems.md b/Paper Notes/Formal verification of neural network controlled autonomous systems.md new file mode 100644 index 00000000..fce9db6a --- /dev/null +++ b/Paper Notes/Formal verification of neural network controlled autonomous systems.md @@ -0,0 +1,31 @@ +# First Pass +**Category:** +Methods paper + +**Context:** +Using NN w/ LiDAR to say safety reliability claims using FM + +**Correctness:** +Assumptions seem good, other than anticipating LiDAR as a +continuous data stream. + +**Contributions:** +1. Framewok for formally proving safety properties of autonomous robots using LiDAR and NNs +2. Something something imaging-adapted partitions. A 'notion' + +**Clarity:** +Very well written and clear. + +# 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?**