vault backup: 2026-01-14 13:42:21

Zettelkasten/Fleeting Notes/Meetings/20260106-Meeting-With-INL.md

@@ -0,0 +1,37 @@
+# Meeting with Ginger and Benjamin about Summer Internship
+
+Also not directly an interview, but rather a check-in and
+conversation. Good conversation about the thrust they would
+be interested in me working on. CIE-group. They want to do a
+push about how we define resilliency, especially when it
+comes to cyber control systems. Probabilism and defense in
+depth is not enough, or perhaps not the right approach.
+
+Ginger also brought up good points. We want to be able to
+have evidence for autonomous control systems for things like
+liability courts. If something goes wrong, we want to be
+able to say why the control system made the right choice,
+based on formal methods approaches to justify control
+actions. Also talk about *graded* responses and saying
+whether or not we can justify operation of a degraded
+system.
+
+16-wk on-site internship. Relocation help included. Spoke
+highly of Dan and continued collaboration is an option.
+
+Two main deliverables:
+- a kind of state of the art on what 'resilience' is and how
+  it is determined
+- a thrust or way forward of what new metrics for resilience
+  could look like. Sounds like an advanced proposal
+- Conference paper?
+
+Team: Ginger, Benjamin, a gentleman named John, other
+individuals.
+
+Benjamin has a reachability manifesto he wants to send us.
+Dan as INL-vetted will probably get an email about it.
+
+More to come in the next couple of weeks. Need to evaluate
+against Emerson opportunity. This seems to have more
+direction.

Zettelkasten/Fleeting Notes/Weekly/2026_02.md

@@ -0,0 +1,61 @@
+---
+id: 2026-02
+title: Weekly — 2026-01-07
+type: Weekly
+created: 2026-01-07T18:49:47Z
+modified: 2026-01-07T18:49:47Z
+tags: [weekly]
+---
+
+# Weekly - 2026 CW 02 (Wed 2026-01-07)
+
+## Accomplishments
+
+### Union
+- ✓ Talk to Jessica about getting a room for an event
+
+### Thesis
+- ✓ Find out what 10 CFR is. Specifically, 10 CFR 50.34 and 10 CFR 55.59. Emergency Operating Procedures?
+
+### Internship
+- INL internship meeting yesterday. Went very well. 
+
+## Pushed or Rescheduled
+
+- (Union) Follow up with Jessica about room booking
+- (Chair-Search) Read Clarks application and provide review scores
+- (Chair-Search) Read remaining two applicants and provide scores
+
+## Cancelled or Deleted
+
+No tasks were cancelled or deleted in the past 7 days.
+
+## To Do
+
+### Due This Week
+
+**Due in 10 hours:**
+- (Chair-Search) Read additional applican and provide scords
+
+**Due 2026-01-08:**
+- (Thesis) The Algorithmic Analysis of Hybrid Systems (1995) [Urgency: 14.6]
+- (Thesis) Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems (1993) [Urgency: 10.6]
+- (Thesis) Hamilton-Jacobi Reachability: A Brief Overview and Recent Advances (2017) [Urgency: 10.6]
+- (Chair-Search) Read Clarks application and provide review scores [Urgency: 9.15]
+- (Chair-Search) Read remaining two applicants and provide scores [Urgency: 9.15]
+- (ENGR1933) Complete RAMP training [Urgency: 9.15]
+
+**Due 2026-01-13:**
+- Fill out graduate student evaluation form [Urgency: 5.86]
+
+### High Priority
+
+- (Union) Follow up with Jessica about room booking [Urgency: 16.8]
+- (Thesis) Do FRET tutorials [Urgency: 13.1]
+- (zk) AIGER Circuits [Urgency: 3.22]
+- (zk) Reactive Synthesis [Urgency: 3.22]
+- (zk) Write about opp. chall. and res. needs for remote micro ope. [Urgency: 3.18]
+- (ERLM) Add research tasks to research approach section [Urgency: 2.48]
+- (Thesis) Hybrid Systems: Review and Recent Progress (2003) [Urgency: 2.41]
+- Have meeting with Dan about performance review
+- Internship items: Follow up with Emerson next week about paperwork

Zettelkasten/Permanent Notes/20260109155358-hybrid-automata.md

@@ -0,0 +1,17 @@
+---
+id: 20260109155358
+title: Hybrid Automata
+type: permanent
+created: 2026-01-09T20:53:58Z
+modified: 2026-01-09T21:08:30Z
+tags: []
+---
+
+# Hybrid Automata
+Hybrid automata are a framework for the formal modeling of
+computed systems. Hybrid automata are a generalization of
+[[timed automata]], where all states are governed by
+differential equations.
+
+## Relevant Sources
+[[hybrid-automata-an-algorithmic-approach-to-the-specification-and-verification-of-hybrid-systems]]

Zettelkasten/Permanent Notes/20260109155410-linear-hybrid-automata.md

@@ -0,0 +1,16 @@
+---
+id: 20260109155410
+title: Linear Hybrid Automata
+type: permanent
+created: 2026-01-09T20:54:10Z
+modified: 2026-01-09T21:11:18Z
+tags: []
+---
+
+# Linear Hybrid Automata
+Linear hybrid automata are [[hybrid-automata]] systems where
+'the rate of change with time is constant' for each
+variable, and the 'terms involved in the invariants, guards,
+and assignments are required to be linear'.
+
+A special case of linear hybrid automata are [[timed-automata]].

Zettelkasten/Permanent Notes/20260109155415-timed-automata.md

@@ -0,0 +1,27 @@
+---
+id: 20260109155415
+title: Timed Automata
+type: permanent
+created: 2026-01-09T20:54:15Z
+modified: 2026-01-09T21:13:51Z
+tags: []
+---
+
+# Timed Automata
+Timed automata are linear hybrid automata with the
+special condition that every continuously changing variable
+is a *clock*. That means that every variable varies one to
+one with time, just counting time.
+
+Timed automata have invariants and guards that compare time
+only with constants. There are no other continuous dynamics
+here. 
+
+An example of a timed automata is something like an alarm.
+Easy peasy, is time greater or less than a value. If it is,
+trigger the alarm! One might also have a constant setting
+whether or not an alarm is 'enabled'. But, there's no other
+dynamics than time itself.
+
+## Relevant Sources
+[[hybrid-automata-an-algorithmic-approach-to-the-specification-and-verification-of-hybrid-systems]]

Zettelkasten/Permanent Notes/20260109155838-reactive-programs.md

@@ -0,0 +1,23 @@
+---
+id: 20260109155838
+title: Reactive Programs
+type: permanent
+created: 2026-01-09T20:58:38Z
+modified: 2026-01-09T21:08:01Z
+tags: []
+---
+
+# Reactive Programs
+Reactive programs, or reactive systems, are those that have
+an output or state change controlled by the current state
+and input. These programs react to environmental changes in
+real time. Basically every relevant control system is a
+'reactive' system, but in computer science, reactive
+programs have a unique meaning. Reactive computer programs
+are those that have computation depending on external
+inputs, a.k.a. stuff from OUTSIDE of the computer's world.
+
+
+## Relevant Sources
+[[strix-explicit-reactive-synthesis-strikes-back]]
+[[hybrid-automata-an-algorithmic-approach-to-the-specification-and-verification-of-hybrid-systems]]

Zettelkasten/Permanent Notes/20260114132351-bayes-theorem.md

@@ -0,0 +1,48 @@
+---
+id: 20260114132351
+title: Bayes' Theorem
+type: permanent
+created: 2026-01-14T18:23:51Z
+modified: 2026-01-14T18:42:20Z
+tags: []
+---
+
+# Bayes' Theorem
+
+Suppose we know $P(x)$, *the prior*, and we get some data
+$Y$, and we want to know the probability $P(X|Y)$, which in
+English is *the probability of our model being correct given
+the data we've collected*.
+
+We can use Bayes' Theorem to find it!
+
+$$ P(X|Y) = \frac{P(Y|X) P(X)}{P(Y)} $$
+
+Where:
+- $P(X|Y)$ is called the *posterior*
+- $P(Y|X)$ is called the *likelihood*
+- $P(X)$ is called the *prior*
+- $P(Y)$ is called the *evidence*
+
+We can usually find the evidence by the following formula:
+
+$$ P(Y) = \sum P(Y|x_i) P(x_i) $$
+
+We can apply Bayes' Theorem to states in time too.
+
+$$ P(X_t|Y_t) = \frac{P(Y_t|X_t) P(X_t)}{P(Y_t)} $$
+
+where:
+- $ X_{t+1} = f(x_t, w_t) $
+- $ Y_{t} = f(x_t) + v_t $
+$w_t$ is process noise, while $v_t$ is measurement noise.
+
+Bayes' Rule is great for simulation and data-based
+approaches.
+
+## Related Ideas
+[[Expected Value]]
+
+## Sources
+Bayesian Signal Processing w/ Dan (1/12)
+

Zettelkasten/Permanent Notes/20260114133159-expected-value.md

@@ -0,0 +1,21 @@
+---
+id: 20260114133159
+title: Expected Value
+type: permanent
+created: 2026-01-14T18:31:59Z
+modified: 2026-01-14T18:41:57Z
+tags: []
+---
+
+# Expected Value
+Expected value is pretty much the mean of a function, but
+more specifically, it's the weighted average of all possible
+outcomes of a function:
+
+$$ \hat X = E{X} $$
+
+If we have an estimate of a posterior using [[Bayes'
+Theorem]], we can get the following result:
+
+$$ \hat X = \sum_i X^i \hat{Pr}(X^i|Y) $$
+

Zettelkasten/Permanent Notes/Literature Notes/LIT-20250819112550-strix-explicit-reactive-synthesis-strikes-back.md

@@ -3,7 +3,7 @@ id: LIT-20250819112550
 title: Strix Explicit Reactive Synthesis Strikes Back!
 type: literature
 created: 2025-08-19T15:25:50Z
-modified: 2025-08-21T16:37:52Z
+modified: 2026-01-09T21:08:06Z
 citekey: meyerStrixExplicitReactive2018
 ---
 
@@ -55,3 +55,6 @@ is also pretty good compared to other synthesizers.
 **Hidden Findings:**
 
 **Weak Points? Strong Points?**
+
+## Spawned Zettels
+[[Reactive Programs]]

Zettelkasten/Permanent Notes/Literature Notes/LIT-20260109152249-hybrid-automata-an-algorithmic-approach-to-the-specification-and-verification-of-hybrid-systems.md

@@ -0,0 +1,49 @@
+---
+id: LIT-20260109152249
+title: Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems
+type: literature
+created: 2026-01-09T20:22:49Z
+modified: 2026-01-09T21:14:05Z
+citekey: 
+---
+
+# Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems
+
+## First Pass
+**Category:** 
+New methods paper
+
+**Context:** 
+This paper was released in the early 1990's when formal
+methods was gaining some steam for proving algorithms. This
+paper talks about the challenges of hybrid systems, where
+there are discrete changes on top of continuous dynamics.
+
+**Correctness:** 
+It's an extremely well cited paper.
+
+**Contributions:** 
+The [[Hybrid Automata]]
+
+**Clarity:** 
+4/5. Dense. Mathematical.
+
+## 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?**
+
+## Spawned Zettels
+[[Hybrid Automata]]
+[[Linear Hybrid Automata]]
+[[Timed Automata]]
+[[reactive-programs]]