file sync

2026-02-06 20:19:24 -05:00 · 2026-02-06 20:19:24 -05:00 · 72d1d5a770
commit 72d1d5a770
parent 048b521a5d
112 changed files with 4104 additions and 0 deletions
--- a/.DS_Store
+++ b/.DS_Store
--- a/Notes/.DS_Store
+++ b/Notes/.DS_Store
--- a/Notes/Class/.DS_Store
+++ b/Notes/Class/.DS_Store
--- a/Processing/.DS_Store
+++ b/Processing/.DS_Store
--- a/Processing/20260112.pdf
+++ b/Processing/20260112.pdf
--- a/Processing/20260114.pdf
+++ b/Processing/20260114.pdf
--- a/Processing/20260121.md
+++ b/Processing/20260121.md
@ -0,0 +1,105 @@
 # BSP - Random Variables
 ## Discrete Random Variables
 Imagine two sets, A and B. 
 There is A+B, which the set of elements in A or B,
 and $AB = A \union B$, which is the elements in A and B.
 Suppose our set S is {1, 2, 3, 4, 5, 6} where A is the evens,
 and B is less than 5. AB is {2, 4}, while A+B is {1, 2, 3,
 4, 6}.
 Sometimes  -A is known as NOT A, or $\bar A$.
 $\bar S = {}$.
 ## Probability and Random Variables
 Set $\Omega$ is the set of all possible outcomes of an
 experiment.
 Events of some subset of outcomes are called 
 $\omega = {odd, even}$
 A trial is a single performance of an experiment (single
 sample).
 An experiment is to observe an single outcome $\zeta_i$.
 Experiment E means a set S of outcomes $\zeta$, certain
 subsets of S can be considered events.
 The space S is the certain event. Basically if it's in S, it
 happened. The null space is events that are impossible. E.g.
 can't get a 7 on a six-sided die.
 If event $\zeta_i$ consists of a single outcome then it is
 an elementary event. 
 Events A and B are mutually exclusive if they have no common
 elements (AB = null space)
 **Defining exactly what the events and outcomes are is super
 important**. It's very easy to get paradoxical results if
 careful choice of outcome and event is not chosen.
 ### Example
 Assign each event a number $A \rightarrow P(A)$
 Axioms:
 1. $P(A) \geq 0$
 2. $P(S) = 1$
 3. if $AB = 0$ then $P(A+B) = P(A) + P(B)$
 Corollaries:
 1. $P(0) = 0$
 2. $P(A) = 1 - P(\bar A) \leq 1$
 *fundamentally the probability of an event is some number
 between 1 and 0*
 3. If $A$ and $B$ are not mutually exclusive, then 
 $P(A+B) = P(A) + P(B) - P(AB) \leq P(A) + P(B)$
 4. If $B \subset A \rightarrow P(A) = P(B) + P(\bar A B)
   \geq P(B)$
 ## Conditional Probability
 Given an event $B: P(B)\geq 0$, we define conditional
 probability as $P(A|B) = \frac{P(AB)}{P(B)}$.
 Sometimes people write *joint probability* as $P(A,B)$ which
 is exactly the same as $P(AB)$.
 Given $n$ mutually exclusive events $A_i,...,A_n$ where $A_1
 + A_2 + ... + A_n = S$. For an arbitrary event $B$, 
 $P(B) = \sum_i P(A_i, B)$
 $P(B) = \sum_i P(B | A_i) P(A_i)$
 We know $B = BS = B(A_1+...+A_n)$. With some rearranging
 knowing each of the A's are independent, $BA_i$ and $BA_j$
 are independent for all $i\neq j$. 
 Thus, $P(B) = P(BA_1) + ... + P(BA_n)$ but we showed earlier
 there's a different way to find $P(B)$.
 if $B = S$, $P(S|A_i) = 1$, then $P(S) = 1 = \sum_i P(A_i)$
 if $B = A_i$, $P(A_j|A_i) = 1$ when i = j, 0 otherwise
 > [!important] Development of Bayes' Theorem
 >
 > Bayesian statistics are a way of thinking about a **degree
 > of belief** in a probability, not an estimation of the
 > probability from a number of experiments.
 > 
 > We know:
 >
 > $P(AB) = P(A|B)P(B) = P(B|A)P(A)$
 >
 > Then Bayes Theorem becomes
 > $$P(A|B) = \frac{P(B|A) P(A)}{P(B)}$$
 >
 > and then when events $A_i$ are mutually exclusive...
 >
 > $$P(A_i|B) = \frac{P(B|A_i) P(A_i)}{\sum_i P(B|A_i) P(A_i)}$$
 > 
--- a/Notes/Daily/2025-08-15.md
+++ b/Notes/Daily/2025-08-15.md
@ -0,0 +1,23 @@
 ---
 id: 2025-08-15
 title: Daily — 2025-08-15
 type: daily
 created: 2025-08-15T21:38:18Z
 modified: 2025-08-15T21:41:25Z
 tags: [daily]
 ---
 # Daily — 2025-08-15
 ## Quick capture
 - Today I didn't really do anything! But I made a bit more
 progress on my Zettelkasten. It actually exists now and I
 made commands to use it.
 - I also made git pushing commands.
 ## Tasks
 - [ ] 
 ## Notes
--- a/Notes/Daily/2025-08-18.md
+++ b/Notes/Daily/2025-08-18.md
@ -0,0 +1,43 @@
 ---
 id: 2025-08-18
 title: Daily — 2025-08-18
 type: daily
 created: 2025-08-18T17:12:19Z
 modified: 2025-08-19T13:43:54Z
 tags: [daily]
 ---
 # Daily — 2025-08-18
 ## Quick capture
 - Installed VimTex and got latex working on my laptop with
 neovim
 - Zettled more about Strix and logic
 - Meeting with Babay's group in the INFSCI building.
 - Signed up for Strava. Considering doing a run club. Could
  be coool!!!
 ## Tasks
 - 
 ## Notes
 Notes from Babay meeting:
 Emerson is going to upgrade the Ovation system in Cole's
 group. We're looking for controllers and things to use.
 Ideas from Babay's group:
 - Protocols: MODBUS and DNP3, HART protocol. Highway
 Addressable Remote something something. Similar to MODBUS
 and DNP3 in principal. 
 - Instrument light panel.
 - Testbed before Energy Innovation Center (EIC)? What tests can we do before going to
 EIC?
--- a/Notes/Daily/2025-08-19.md
+++ b/Notes/Daily/2025-08-19.md
@ -0,0 +1,58 @@
 ---
 id: 2025-08-19
 title: Daily — 2025-08-19
 type: daily
 created: 2025-08-19T14:31:15Z
 modified: 2025-08-19T19:06:40Z
 tags: [daily]
 ---
 # Daily — 2025-08-19
 ## Quick capture
 Goals for today:
 - Write powerpoint for Strix
 - Write heilmeir paragraphs for thesis idea
 - Tour new gym
 - Get details on dSPACE and speedgoat systems
 ## Tasks
 - [ ] 
 ## Notes
 Here is a list of I/O we can use in the PLC Cabinet:
 1. MODBUS compatibility (Babay / Cole)
    - Over Ethernet is ideal, but other mediums would also
    be nice to have.
 2. DNP3 (Babay)
 3. HART (Babay)
 4. Analog Inputs / Outputs
    - +/- 10 V for dSPACE (Maximum range)
    - +/- 10 V for TQ Equipment (Ball and Beam)
    - 0-1.8V for BeagleBone Black
    - IO101 from Speedgoat can use all of above (and +/- 5
    V, +/- 3.3V)
 5. Digital Inputs / Outputs
    - 10 V dSPACE and related
    - 3.3 V for BeagleBone Black
    - 5 V for Arduino
    - IO101 can use all of above
 6. OPC UA, don't need right now but could be useful for
   historians and working with data later.
 Obviously for digital signals we can use voltage regulators
 if required but it would definitely be nice to have 3.3V
 capability for the BeagleBone, and 5V for an Arduino.
--- a/Notes/Daily/2025-08-20.md
+++ b/Notes/Daily/2025-08-20.md
@ -0,0 +1,18 @@
 ---
 id: 2025-08-20
 title: Daily — 2025-08-20
 type: daily
 created: 2025-08-20T13:54:13Z
 modified: 2025-08-22T15:06:52Z
 tags: [daily]
 ---
 # Daily — 2025-08-20
 ## Quick capture
 - Workin in the morning on Strix presentaiton
 - Cole Group Meeting 10am - 11am
 - Write down weekly plan 11am+
 ## Notes
--- a/Notes/Daily/2025-08-22.md
+++ b/Notes/Daily/2025-08-22.md
@ -0,0 +1,24 @@
 ---
 id: 2025-08-22
 title: Daily — 2025-08-22
 type: daily
 created: 2025-08-22T15:41:02Z
 modified: 2025-08-22T16:03:15Z
 tags: [daily]
 ---
 # Daily — 2025-08-22
 ## Quick capture
 - Got to work kind of late. Feeling sicky af. Probably no
 darts tonight with PSM.
 - Working on moving all my notes into zettels
 - Lunch w AS today
 - Okay i'm starting to feel a little better (12:03PM)
 ## Tasks
 - [ ] 
 ## Notes
--- a/Notes/Daily/2025-08-25.md
+++ b/Notes/Daily/2025-08-25.md
@ -0,0 +1,29 @@
 ---
 id: 2025-08-25
 title: Daily — 2025-08-25
 type: daily
 created: 2025-08-25T16:02:00Z
 modified: 2025-08-26T13:56:53Z
 tags: [daily]
 ---
 # Daily — 2025-08-25
 ## Quick capture
 - Got in a little later today, but the bike is here! Gotta
 text Alisa about it.
 - I have 2 classes today (grumble grumble grumble). 
    - ME 3100 ERLM is Monday and Wednesday at 1PM-2:15PM
    - NUCE 2101 - Nuclear Core Dynamics is tonight
    6PM-8:30PM, like usual
 - I also enrolled in my health insurance.
 ## Tasks
 - [ ] 
 ## Notes
--- a/Notes/Daily/2025-08-26.md
+++ b/Notes/Daily/2025-08-26.md
@ -0,0 +1,19 @@
 ---
 id: 2025-08-26
 title: Daily — 2025-08-26
 type: daily
 created: 2025-08-26T15:05:38Z
 modified: 2025-08-26T15:06:58Z
 tags: [daily]
 ---
 # Daily — 2025-08-26
 ## Quick Capture
 - I started this morning doing some email
 - Now I'm hangin out in starbucks doing some work for the
 quad chart n'at
 - First, what the fuck is a quad chart??
 ## Notes
--- a/Notes/Daily/2025-08-27.md
+++ b/Notes/Daily/2025-08-27.md
@ -0,0 +1,32 @@
 ---
 id: 2025-08-27
 title: Daily — 2025-08-27
 type: daily
 created: 2025-08-27T18:33:33Z
 modified: 2025-08-28T17:57:53Z
 tags: [daily]
 ---
 # Daily — 2025-08-27
 ## Quick capture
 COLE GROUP MEETING
 Accomplishments:
 - Quad chart
 - writing more about LTL and building out some notes from
 papers
 - Found resources about temporal logic
 - first nuce class has happened. Codes and standards were
 cancelled
 to do:
 - Write goals and outcomes
 - Write more about approach. This is squishtastic
 - Actually finalize some outcomes. How do i navigate the
 fact that within switching mechanisms there is dynamics
 happening
 - I didn't say anything about what a hybrid system is.
 That's kind of the whole point of the thing.
 ## Notes
--- a/Notes/Daily/2025-08-29.md
+++ b/Notes/Daily/2025-08-29.md
@ -0,0 +1,39 @@
 ---
 id: 2025-08-29
 title: Daily — 2025-08-29
 type: daily
 created: 2025-08-29T14:23:06Z
 modified: 2025-08-29T15:44:16Z
 tags: [daily]
 ---
 # Daily — 2025-08-29
 ## Quick capture
 Yesterday I wrapped up a couple small things I needed to get
 done. First, I sold my bike to Alisa for 250! Pretty good
 deal for me, I made 30 on the sale. Then, I went to Harbor
 Freight and got some critical tools for working on the bike.
 It turns out, it's actually really hard to put a dirt bike
 on a stand. Heavy as all hell. But today, I'll get the sumo
 wheels on the bike!
 - [?] What tire pressure should I use for these new wheels?
 For work stuff, I've got to answer more Heilmeier questions
 and start writing a goals and outcomes section. The G&O
 should likely be a LaTeX document.
 The Emerson guys were here today too to fix up the ovation
 system. They told us they took the top off, affixed the
 power strip to the upper right side, and finally they told
 use we can totally take all the doors off if we wanted. They
 also said no 3.3V, they do all 24V stuff so they just don't
 carry the modules that go that low in power.
 ## Tasks
 - [ ] 
 ## Notes
--- a/Notes/Daily/20250331_Should_I_Continue.md
+++ b/Notes/Daily/20250331_Should_I_Continue.md
@ -0,0 +1,122 @@
 # What should I do about my PhD?
 ---
 The quick brown fox jumps over the lazy dog. The dog stays blissfully asleep. :)
 This time, I'm actually going to begin writing a journal. I feel like I have a 
 lot of thoughts that I let swim around, without doing much about them. To quote
 *the Happiness Lab* episode that I listened to today: 
 "Good intentions mean nothing if they don't translate into actions."
 So I'll take Dan's advice, and use writing to do thinking. I also think that 
 writing this journal can improve my writing skills. 
 So what's going on today?
 Well as I'm writing this, I'm on the 61D on my way into school listening to 
 *Spanish Pipedream* by John Prine. But what I really want to tell you about is
 the decision I'm trying to make about whether or not to finish my PhD here at 
 Pitt with Dan. Last Friday, I had a meeting with Dan about an idea I was 
 interested in pursuing that at the core involved working with a real, tangible
 system. That idea was politely dismissed, and I was 'nudged' back towards formal
 methods for critical infrastructure. My immediate impression is that formal
 methods for our lab is a crock of shit. 
 Dan means well and is genuinely looking out for my best interest, but that 
 doesn't translate into belief into his mission. Formal methods are an intense
 mathematical pursuit in order to prove 'correctness' of something to something 
 else. Formal methods experts may disagree with that characterization, but 
 ultimately that second 'something' can be a lot of things, such as a model of a
 plant, a written specification, or anything that can be logically defined. Dan
 wants to use formal methods to prove things about physical systems. His idea is
 aligned with what Manyu just finished up: can we use formal methods to prove that
 certain systems adhere to requirements using formal methods? This is connected
 in part to the HARDENS report, which tried to use formal methods tools at several 
 layers of abstraction to prove that a written requirement can be translated into 
 a proof for a determined plant design. There is certainly work to be done there.
 But is that work that I want to do? My brain says I could do it, but my gut 
 screams out a vehement no. This is the core issue--I know I could do it, but 
 once I would finish, where does that leave me? The answer: a formal methods 
 expert. Formal methods experts are highly sought after, but it is an intensely
 theoretical oriented field. When I think about what I want to do in my career 
 and what my values are, they are not only working through a computer (despite
 my aptitude for such). I want to build real things, works you can touch, and
 that interact with the world. A formal methods proof about a reactor that *might*
 get built is not in that alignment. 
 So what the hell do I do? As I write this, it seems pretty clear the relationship
 between myself and the Cole Lab's work is fractured. Going forward, I see three
 main options:
 1) Find another PhD advisor at Pitt. Bajaj is an obvious choice.
 2) Master out and go find a job.
 3) Go find another PhD opportunity somewhere else. Yichen did this.
 Pros and cons of each situation:
 1) Find another PhD advisor at Pitt
    + I would be able to keep my NRC Fellowship
    + I know people here already
    + I've already passed the qualifying exam
    - Money is garbage
    - I don't think anyone is actually doing work that I really want to do
    - Have to stay in Pittsburgh
    - NRC debt keeps growing
 2) Master out and go find a job
    + I would immediately make much more money
    + Can move somewhere else (Boston?)
    + NRC commitment is only a year
    + Could find an interesting R&D job?
    + Could get a second publication out for Bajaj's project
    + Could pick up PhD again in a year or so. Work on projects to make 
    myself super competitive 
    - Dr. Sabo is on hold
    - No thesis!
 3) Master out and start a PhD at another school
    + Dr. Sabo is slightly delayed
    + Could go work in Boston
    + Could go work on something I feel passionate about
    + Better degree diversity
    + Teaching plan could still work out
    - Slightly longer timeline
    - Have to take another qualifying exam
    - Still have the NRC commitment likely
    - Would not make much money
 I think the smartest thing is to master out, find a job for a year that will
 satisfy the NRC requirement, and then if I want to, restart the PhD somewhere
 else. This would put me finishing sometime in 2030 or so. That's certainly a lot.
 If I went to find a PhD now, I would finish somewhere in 2029 or so, then have
 the 1-year NRC commitment. Hmmm. 
 I checked my current progress in my degree, and learned that I satisfy the controls
 track masters degree after this semester. I would need to negotiate two things:
 either ME 2046 or ME 2150 would need to count as a DSC elective, and NUCE 2100 
 would have to be accepted as a ME elective (it is cross listed as ME 2100, so 
 shouldn't be impossible to argue for). The next thing I need to do for this would
 to be to talk to Dan about it. 
 Thinking about stopping with the Master's feels good. I think I should seriously 
 pursue this, and maybe talk to Rachel and my family about it.
 ## Chat w/ Pat
 Patrick and I got lunch today. He was generally pretty supportive and gave me 
 some sound advice that I can use. He asked me "have you read some literature 
 reviews?" And the answer to that is no, not really. He also advised to "just do
 something", which perhaps will help me feel like I'm actually getting something
 built. I think that is helpful. Going forward, I'm going to really try and do
 two things:
 1) Read at least 3 literature reviews by Friday
 2) Get ARCADE and I2C working by next Monday
    [Could be interesting](https://www.adafruit.com/product/2264?gQT=0)
 I really don't know what I should do. This certainly is not a one day decision.
 Honestly, I may like the idea of option 3 the best, but I do need to do some work.
 I've got it in the works to:figure out how to get the MS along the way with Antoine,
 so we'll see how that happens. I think the earliest things would happen would be at
 the end of the summer.
--- a/Notes/Daily/20250409_horsenoises.md
+++ b/Notes/Daily/20250409_horsenoises.md
@ -0,0 +1,50 @@
 The quick brown fox jumps over the lazy dog. The dog stays blissfully asleep. :)
 Since last time, I have found a bit more resolve on what I'm going to do about 
 this whole PhD thing. I have decided I am going to earnestly try to find a topic
 that fits with the lab's formal methods bend--at least for the rest of the 
 spring and into the beginning of the summer. I am taking action to try and find
 a topic, like trying to read more surveys and actually doing things. This past 
 week was not necessarily super successful in that regard, but on the margins was
 an improvement. Oh, well.
 There is a couple reasons I think this is the right move. First, I am already 
 here. Any other route that ends with my PhD will add extra time before I am 
 finished. Any job search right now is also probably not a great idea, since 
 Trump and his merry men are starting a trade war, and consequently likely a 
 recession. I am in a good position right now, and there is value in taking stock
 of the opportunity that I have. 
 Robert also lended some helpful advice: certainly the topic of my PhD does not
 pigeon hole me into a field for the rest of my career. I think this is true in 
 a restricted sense, but not in the general sense. For my sake, this means if I 
 do something formal methods adjacent, it does not mean I need to be stuck in 
 formal methods forever, but also I should be careful that the work I do also
 lends itself to another field I find interesting. One such area is perhaps using
 formal methods with artificial intelligence to leverage these tools to create
 explainable AI based control. 
 I need to read more to really understand what that can be. Update to come.
 Now for a slight change of pace, some more personal details.
 The pursuit of an apartment for Amber and I continues to be a contentious topic.
 Amber was quite upset coming back from her trip that I 'did not take care of
 myself'--her accusation is that I did not eat balanced meals or in general act
 with personal motivation to do things that are good for me. This also compounded
 with my food habits with my night classes. I have eaten out a lot recently before
 class instead of cooking food at home the night before or so. Amber attributes 
 this to lazyness. This argument culminated in her saying that she feels more 
 like a mom than a girlfriend. That makes me really upset.
 Do I think she is right? Well, in terms of food, sure. She has a good point. I 
 could certainly eat better, and this past weekend I see what she is saying about
 balanced meals. Fair point and this is something I must correct. Something that
 does make me worried however is this idea that she is like my mom rather than 
 my girlfriend, and more broadly that she feels I make changes because she tells
 me so rather than because I want to on my own. This is a frustrating catch-22 in
 my opinion. If I do not learn what is upsetting her, I cannot change that 
 behavior. But, if she tells me and I do change that behavior, she takes credit 
 for it and gets upset anyways. Honestly, it makes me feel like damned in a way.
 I'll try and change nonetheless, but it is incredibly demotivating to think 
 she will believe it is just because 'she told me so'. 
--- a/Notes/Daily/2025_07_30.md
+++ b/Notes/Daily/2025_07_30.md
@ -0,0 +1,23 @@
 ---
 ---
 # 2025-07-30
 ## Morning Brief
 Today's goal is to finish writing up some thesis ideas. I
 need to have 6 of them for a meeting with Dan. I used
 ChatGPT to help me brainstorm some ideas, but I need to go
 over them and format them in a way that is more
 approachable.
 On the other hand, I've been working on leaving my phone
 behind. I'm trying a new technique of just leaving it out of
 my reach. I can feel the itch in my brain that yearns for
 it... that's definitely an addiction I have to kick. 
 Anyways, here's the goals for today:
 - [ ] Write down 6 ideas for a thesis: [[thesis-ideas]]
 - [ ] Review literature notes, and organize my notes
 - [ ] Finish [[automation-levels-for-nuclear-reactor-operations-a-revised-perspective]]
--- a/Notes/Daily/2025_07_31.md
+++ b/Notes/Daily/2025_07_31.md
@ -0,0 +1,22 @@
 ---
 ---
 # 2025-07-31
 ## Morning Brief
 Yesterday I wrote 2 thesis ideas and started a third. Today,
 we finish them! I'm struggling to write outcomes but we'll
 get there over time. I can do this.
 I started the morning with an hour of doomscrolling. I
 really have to sort that out.
 Tasks are the same from [[2025-07-30|yesterday]]. Maybe I
 should make a centralized page for tasks.
 - [ ] Make task page #admin
 ## Lunch Brief
 ## Note for tomorrow
--- a/Notes/Daily/2025_08_01.md
+++ b/Notes/Daily/2025_08_01.md
@ -0,0 +1,11 @@
 ---
 ---
 # 2025-08-01
 ## Morning Brief
 Yesterday I finished two additional thesis ideas and got
 some more reading done 
 - [ ] Fill out health insurance enrollment
--- a/Notes/Daily/2025_08_04.md
+++ b/Notes/Daily/2025_08_04.md
@ -0,0 +1,17 @@
 ---
 ---
 # 2025-08-04
 ## Morning Brief
 I didn't do shit. But I emailed Dan that I'd be OOO
 Wednesday and Thursday for the motorcycle course.
 I'm finishing those fucking thesis ideas today. ON GOD.
 [[thesis-ideas-2025-07-30]]
 I'm' also supposed to have a date with Miranda today, but
 she hasn't texted me back. Interesting. Jackie also
 complimented my socks and show combo. That was nice. I
 showed her and Natan [Angus](ourcowangus.com).
--- a/Notes/Daily/2025_08_05.md
+++ b/Notes/Daily/2025_08_05.md
@ -0,0 +1,22 @@
 ---
 ---
 # 2025-08-05
 ## Morning Brief
 I didn't finish the thesis ideas from yesterday. Oopsie!
 Today is different though. Curently, I'm working from
 home^*, which really means I'm working in a coffee shop on
 Washington road. I'm at the Orbis Cafe, where I purchased a
 cinnamon roll and a cappucino. The caffeine has yet to hit,
 but when it does, I'll be cooking I'm sure. This is a nice
 spot and it's very relaxing to get things done while other
 people are around. I like this a lot, and perhaps I should
 do this more often while I'm at school too. 
 Anyways, Dan is OOO taking time off while he can before the
 fall semester. Who can blame him?
 Patrick and I discussed more PINN stuff yesterday. I should
 make a simple PINN demonstration.
--- a/Notes/Daily/2025_08_06.md
+++ b/Notes/Daily/2025_08_06.md
@ -0,0 +1,23 @@
 ---
 ---
 # 2025-08-06
 Today was the first day of the motorcycle safety course. It was
 good! I felt like I was honestly the best rider there. That being
 said, tomorrow is a new day and we'll see how it goes. Jackie
 looked like she had fun too.
 I had a great date yesterday. Miranda is very, very cool. She
 loves facebook marketplace, mac.bid, camping, and said her
 favorite book was *Dune*. My jaw just about fell open when I
 heard that. We're potentially going to go look at a van on
 Saturday. 
 I missed the Jumet Financial Open House. I slept right through
 that mf after getting back from the course. Whoops. I feel bad
 about it as Sam gave me a call right in the middle. No voicemail.
 Yikes. I'll see how that works out.
 Then, last thing today is getting some final writing done to say
 that I did any work today. No group meeting this week it looks
 like.
--- a/Notes/Daily/2025_08_07.md
+++ b/Notes/Daily/2025_08_07.md
@ -0,0 +1,11 @@
 ---
 ---
 # 2025-08-07
 Today I have not gotten too much done, but I did get here
 early today. Today, I'll sell the truck and work on Sam's
 car. I saw Patrick today too, which was nice. Robert's stuff
 is all gone.
 My main focus for today is to finish the thesis ideas and
 tune up the writing. That'll be enough.
--- a/Notes/Daily/2025_08_11.md
+++ b/Notes/Daily/2025_08_11.md
@ -0,0 +1,8 @@
 ---
 ---
 # 2025-08-11
 Today I'm finishing the thesis ideas, for real this time.
 I'm also going to get a model of a heat exchanger working.
--- a/Notes/Daily/2025_08_12.md
+++ b/Notes/Daily/2025_08_12.md
@ -0,0 +1,10 @@
 ---
 ---
 # 2025-08-12
 Yesterday I finished my thesis ideas! Hooray! It feels
 really good to actually have some writing finished. Today,
 I'm making a model for a simple heat exchanger in python.
 Then, I'm going to train a physics informed neural network
 on it and start fucking with parameters.
--- a/Notes/Daily/2025_08_13.md
+++ b/Notes/Daily/2025_08_13.md
@ -0,0 +1,67 @@
 ---
 ---
 # 2025-08-13
 Today is August 13th, 2025, otherwise known as judgment
 day. Just kidding, but today I have my meeting with Dan
 about my topic ideas. I feel anxious, but pretty good in
 general. I saw Dan this morning and he seems to be in good
 spirits. I can do this!
 My eye doctor appointment was also today. The results? My
 prescription is pretty much the same. I also do not have
 glaucoma it looks like. Doc was surprised I wear glasses at
 all, figuring the binocular detriment of glasses in my case.
 Honestly, he's right, I should wear contacts more often.
 I'll try to make a point to do that. Now that I have this
 new prescription, I can get on ordering more contacts from
 Costco. Dr. Clermont also recommend to try and stay around
 twelve hours of usage a day to minimize hydration issues. He
 said pushing 16 some times is okay. 12 hours would be 7-7
 (duh), while 16 would be 7-11pm. We also discussed LASIK,
 and he said honestly I'd be a great candidate. He gave me a
 note with a number to call.
 Today is also our group meeting. Apparently it's a
 'standup' now. 
 ## Personal 
 Personally I'm doing pretty okay. I'm trying to focus on
 framing things in a more positive way. I think it is working
 somewhat; there's moments where things click in a way I
 don't feel as anxious about. 
 On the lady front, I finally hit app-burnout. I was reading
 a text and the typos just made me angry. Like, c'mon, read
 your message! This isn't rational, however, as any number of
 things can create a typo and it really isn't a big deal.
 There's no reason I should get so frustrated at something so
 small like that.
 Anyways, here's the roster and relevant updates:
 **Miranda**:
 Miranda is cool and I like her a good bit. She's funny,
 seems somewhat interested in me, and is a great time to be
 around. That being said, I need to be careful. I'm getting
 somewhat infatuated with her but there isn't really a super
 strong connection there yet. This is one that I need to
 really step off the brakes with and see how things develop.
 She is going on vacation with her family next Friday, and
 then going solo camping after that. Then, I'm really going
 to try and let her set something up.
 **Katarina**:
 Katarina is a recent match and is interesting as a prospect.
 She seems pretty nice and is a bioengineering PhD student in
 her 5th year. So almost done maybe? I'll get more details on
 Thursday night!
 **Abby:** 
 Abby is a nurse who I've had an interesting conversation
 with about religion. She has 'catholic' in her profile but
 is apparently not very religious actually. She has a dog
 named Goose! We're meeting up on Sunday to take Goosey-boy
 for a walk.
--- a/Notes/Daily/2025_08_14.md
+++ b/Notes/Daily/2025_08_14.md
@ -0,0 +1,78 @@
 ---
 ---
 # 2025-08-14
 ## Work
 Yesterday Dan and I had our meeting about
 [[thesis-ideas-2025-07-30 | topic ideas]]. The results were
 as follows:
 5. Integrating Shielding in Nuclear Power
 3. Formally Verified NN CTRL of CRS
 1. Temporal Logic Specifications for Autonomous Control
   Synthesis.
 1. Formally Verified Runtime Monitoring and Fallback
 6. High Assurance Fault Detection with Digital Twins
 4. Verified Adaptive Control.
 The final topic result? 
 *Hybrid Controller Synthesis from Temporal Logic
 Specifications* 
 The research will be basically a mix of the third and fourth
 idea. More work to come on this one.
 I also got roped into making a presentation about Strix for
 next week's meeting. So I must learn about that!
 ## Reading
 Yesterday I read more of *The Power of Habit* and I learned
 about the **craving**. A craving is what actually makes the
 habit loop work. It was explained to me that the brain
 releases a spike in activity at first when it recognizes the
 reward. Once the cue and routine are associated with the
 reward, the brain over time will deliver the activity spike
 as an anticipation of the reward *earlier and earlier*. The
 result is that the brain gets the activity spike as soon as
 it sees the cue, anticipates the reward, and is thus
 motivated to do the routine. The craving is what makes
 habits easy. 
 ## Personal 
 Finally my personal info. I feel pretty good today. I didn't
 get a lot done this morning but I'm steady cooking now that
 I'm working in a Starbucks on campus. I've been
 peoplewatching as people slowly move in for the fall
 semester. It's fun to see all the different kinds of people
 walking around and to see the connection between kids and
 parents. The kids definitely look more nervous on average
 than the parents. And I get it, the parents know what to
 expect, but for the kids, this is the transition to the deep
 end. They'll be fine.
 On the lady front, here's today's update:
 **Miranda:** 
 Honestly I'm getting a little bored. I think it might just
 be a texting issue, or perhaps the infatuation wearing off.
 That's okay though, she's really busy this week som maybe
 that has something to do with it.
 **Abby:** 
 No update!
 **Katarina:** 
 Also no update, but I'm excited for our date tonight. We'll
 see how it goes.
 I made some updates to my hinge profile to make things sound
 more serious and better indicate what I want / who I am.
 Maybe this'll stand out more. Honestly, I tried to write the
 profile like one I'd be looking for. 
--- a/Notes/Daily/template.md
+++ b/Notes/Daily/template.md
@ -0,0 +1,10 @@
 ---
 ---
 # 2025-08-14
 ## Work
 ## Reading
 ## Personal 
--- a/Notes/Internship-spots.md
+++ b/Notes/Internship-spots.md
@ -0,0 +1,42 @@
 # Internship Locations
 This is a short list of internship spots I am considering.
 The goal is to find an internship that starts next summer,
 and maybe can eventually be parlay'd into a job.
 ## National Laboratories
 **Idaho National Laboratory**
 - Contacted Greg with research statement. 
 - He's talking about it with Wayne and Simon Pemblott.
 **Sandia National Laboratory**
 - Sent research statement to Lee. He liked it and offered
 comments.
 - There's a fellowship internship opportunity. I should
 check that out
 ## Nuclear Companies
 **Westinghouse**
 - Is there any opportunities here? Maybe, maybe not. They
 seem pretty humdrummy
 **Oklo**
 - Do they have opportunities? Must find a recruiter.
 ## Other Companies
 **Anduril**
 - Hehe cool robotics military tech
 - find a recruiter. They've got lots of jobs open
 **CIA**
 - Do they have internships?
 **Lockheed Martin**
 - Any cool advanced military gigs?
 **Applied Physics Lab**
 - We know Chris D'Angelo there
 **Loonwerks**
 - Spoke to Daren Cofer at NASA FM conference. Any
 opportunities there?
--- a/Notes/Meetings/20260106-Meeting-With-INL.md
+++ b/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.
--- a/Notes/Meetings/CISA_training.md
+++ b/Notes/Meetings/CISA_training.md
@ -0,0 +1,11 @@
 # CISA ICS Training Notes
 ## Russ' Quiz
 % data breaches involving phishing --- 15%
 % of all breaches involving human error --- 68%
 % financially motivated incidents that involve ransomware or
 extrotion --- 92%
 Year the PLC was invented? --- 1968
--- a/Notes/Meetings/INL.md
+++ b/Notes/Meetings/INL.md
@ -0,0 +1,7 @@
 # Notes from INL Internship Meeting
 **Attendees:** 
 - Dane
 - DGC
 - Greg Shannon
 - Wayne Austad
--- a/Notes/Meetings/emerson.md
+++ b/Notes/Meetings/emerson.md
@ -0,0 +1,17 @@
 # Meeting With Emerson about Internship 
 ## Attendees
 Dan
 Myself
 Rick
 ## 
 ## Questions I have:
 - What does the day to day work you'd have me working on
 look like?
 - Size of the team?
 - On site in cranberry?
 - Next steps? When should I hear from you?
--- a/Notes/Processed/hehe.md
+++ b/Notes/Processed/hehe.md
--- a/Notes/Random
+++ b/Notes/Random
@ -0,0 +1,2 @@
 [Vim for MATLAB](https://github.com/daeyun/vim-matlab)
--- a/Notes/Weekly/2025_34.md
+++ b/Notes/Weekly/2025_34.md
@ -0,0 +1,32 @@
 ---
 id: 2025-34
 title: Weekly — 2025-08-20
 type: Weekly
 created: 2025-08-20T13:54:13Z
 modified: 2025-08-20T19:10:24Z
 tags: [weekly]
 ---
 # Weekly - 2025 CW 34 (Aug 18 - Aug 22)
 ## Accomplishments
 1. Met with Babay's group and collected their needs for the
   new ovation system stuff. The notes are in [[daily-2025-08-18]]
 2. Learned about logic. Started with propositional logic,
   then did predicate logic, now am working on temporal
 logic.
 3. Made a presentation about Strix, and learned about parity
   games. Strix uses determnistic parity games to do
 synthesis, and yields automata that are very small relative
 to competition. They're old though--2017 was the first Strix
 paper.
 ## This week's plan
 1. Write heilmeir paragraphs for thesis topic
 2. Make Quad chart for ERLM
 3. Find and keep working on an LTL book
--- a/Notes/Weekly/2025_35.md
+++ b/Notes/Weekly/2025_35.md
@ -0,0 +1,18 @@
 ---
 id: 2025-35
 title: Weekly — 2025-08-20
 type: Weekly
 created: 2025-08-20T13:54:13Z
 modified: 2025-08-20T19:10:33Z
 tags: [weekly]
 ---
 # Weekly - 2025 CW 35 (Aug 25 - Aug 30)
 ## Last week's plan
 1. Write heilmeir paragraphs for thesis topic
 2. Make Quad chart for ERLM
 3. Find and keep working on an LTL book
--- a/Notes/Weekly/2025_36.md
+++ b/Notes/Weekly/2025_36.md
@ -0,0 +1,27 @@
 ---
 id: 2025-36
 title: Weekly — 2025-09-02
 type: Weekly
 created: 2025-08-20T13:54:13Z
 modified: 2025-09-03T18:59:44Z
 tags: [weekly]
 ---
 # Weekly - 2025 CW 36 (Aug 25 - Aug 30)
 ## Accomplishments
 - Wrote the goals and outcomes, went up to V4.
 - Goal was flubbed but have new content
 - started thinking about how continuous dynamics need to be
  included. 
 - Tried to watch a video about hybrid system verification.
 Made fun of 'trajectories' nomenclature instead of
 executions and then shit really went off the rails fast.
 Lots of pretty figures but I have to be honest I have no
 idea what the fuck he was talking about.
 - Had crises about intellectual mert
 ## To Do
 - Rewrite GO
 - SOTA. Start writing. 
 - look up cones for math
--- a/Notes/Weekly/2025_46.md
+++ b/Notes/Weekly/2025_46.md
@ -0,0 +1,62 @@
 ---
 id: 2025-46
 title: Weekly — 2025-11-12
 type: Weekly
 created: 2025-11-11T13:55:31-05:00
 modified: 2025-11-12T15:43:57-05:00
 tags: [weekly]
 ---
 # Weekly - 2025 CW 46 (Wed 2025-11-12)
 ## Accomplishments
 ### Internship
 - ✓ Write cover letter for INL Application
 - ✓ Apply for INL Internship
 - ✓ Submit INL Application on Taleo
 ### class.NUCE2-101.Exam2
 - ✓ Problem 1
 - ✓ Problem 2
 - ✓ Problem 3
 - ✓ Problem 4
 - ✓ Problem 5
 - ✓ Problem 6
 - ✓ Submit Exam 2
 ### ERLM
 - ✓ Assertion-Evidence - do in lieu of class
 ### General
 - ✓ Get Dan's approval for course
 - ✓ Create updated plan of study document
 ## Pushed or Rescheduled
 ### ERLM
 - Mock Peer Review Assignment (rescheduled)
 - Make data management plan (rescheduled)
 - Make biographical sketch (rescheduled)
 - Make facilities section (rescheduled)
 - Add more tasks for this week (rescheduled)
 - Draft Presentations (rescheduled)
 - Tune up state of the art for Proposal (rescheduled)
 - Final Presentations (rescheduled)
 ## Cancelled or Deleted
 No tasks were cancelled or deleted this week.
 ## To Do
 ### Immediate (Due within 24 hours)
 None
 ### Due Saturday, November 16 (4 days)
 - Submit enrollment form to Antoine
 - Mock Peer Review Assignment (ERLM)
 - Create ORCID account (ERLM)
 - Make data management plan (ERLM)
 - Make biographical sketch (ERLM)
 - Make facilities section (ERLM)
--- a/Notes/Weekly/2025_47.md
+++ b/Notes/Weekly/2025_47.md
@ -0,0 +1,58 @@
 ---
 id: 2025-47
 title: Weekly — 2025-11-19
 type: Weekly
 created: 2025-11-19T14:34:56-05:00
 modified: 2025-11-19T14:34:56-05:00
 tags: [weekly]
 ---
 # Weekly - 2025 CW 47 (Wed 2025-11-19)
 ## Accomplishments
 ### ERLM
 - ✓ Assertion-Evidence --- do in lieu of class
 - ✓ Read Proposal 1
 - ✓ Read Proposal 2
 - ✓ Read Proposal 6
 - ✓ Create ORCID account
 - ✓ Make data management plan
 - ✓ Make biographical sketch
 - ✓ Make facilities section
 - ✓ Mock Peer Review Assignment
 - ✓ Add more tasks for this week
 ### General
 - ✓ Get Dan's approval for course
 - ✓ Create updated plan of study document
 ## Pushed or Rescheduled
 No tasks were rescheduled during this period.
 ## Cancelled or Deleted
 No tasks were cancelled or deleted during this period.
 ## To Do
 ### Due This Week (Nov 19-26)
 **ERLM**
 - Draft Presentations (due 2025-11-21) [urgency: 8.75]
 ### High Priority
 **ERLM**
 - Tune up state of the art for Proposal (due in 2 weeks) [urgency: 3.44]
 - Final Presentations (due in 2 weeks) [urgency: 3.44]
 **Zettelkasten (zk)**
 - Write zettels about Andre Platzer and differential dynamic logic [urgency: 3.19]
 - Write zettels about webofscience database [urgency: 3.19]
 - Deterministic Parity Automata [urgency: 2.95]
 - Mealy Machines [urgency: 2.95]
 - AIGER Circuits [urgency: 2.95]
 - Reactive Synthesis [urgency: 2.95]
 - Write about opp. chall. and res. needs for remote micro ope. [urgency: 2.92]
--- a/Notes/Weekly/2025_49.md
+++ b/Notes/Weekly/2025_49.md
@ -0,0 +1,76 @@
 ---
 id: 2025-49
 title: Weekly — 2025-12-03
 type: Weekly
 created: 2025-12-03T21:01:29-05:00
 modified: 2025-12-03T21:01:29-05:00
 tags: [weekly]
 ---
 # Weekly - 2025 CW 49 (Wed 2025-12-03)
 ## Accomplishments
 ### ERLM
 - ✓ Draft Presentations
 ### Chair-Search
 - ✓ Make list of tasks for contact about student groups
 ## Pushed or Rescheduled
 The following tasks had their due dates modified during the past week:
 - Review and edit Goals and Outcomes section
 - Review and edit State of the Art section
 - Review and edit Research Approach section
 - Review and edit Metrics of Success section
 - Review and edit Risks and Contingencies section
 - Review and edit Broader Impacts section
 - Review and edit Budget section
 - Review and edit Schedule section
 - Verify RFP compliance for all sections
 - Final proofread and polish entire proposal
 - Review and edit Literature Review section
 - Review and edit Methodology Details section
 - Review and edit Expected Contributions section
 - Review and edit Timeline and Milestones section
 - Review and edit Team Qualifications section
 - Review and edit References section
 - Review and edit Appendices
 ## Cancelled or Deleted
 No tasks were cancelled or deleted during this period.
 ## To Do
 ### Due This Week (Dec 4-10)
 **ERLM Project - Editing Tasks (Due Tomorrow: Dec 4)**
 All of the following editing tasks are due tomorrow and are high priority:
 - Review and edit Goals and Outcomes section (Urgency: 22.1) ⚡ ACTIVE
 - Review and edit State of the Art section (Urgency: 22.1) ⚡ ACTIVE
 - Review and edit Research Approach section (Urgency: 18.1)
 - Review and edit Metrics of Success section (Urgency: 18.1)
 - Review and edit Risks and Contingencies section (Urgency: 18.1)
 - Review and edit Broader Impacts section (Urgency: 18.1)
 - Review and edit Budget section (Urgency: 18.1)
 - Review and edit Schedule section (Urgency: 18.1)
 - Verify RFP compliance for all sections (Urgency: 18.1)
 - Final proofread and polish entire proposal (Urgency: 18.1)
 - Review and edit Literature Review section (Urgency: 18.1)
 - Review and edit Methodology Details section (Urgency: 18.1)
 - Review and edit Expected Contributions section (Urgency: 18.1)
 - Review and edit Timeline and Milestones section (Urgency: 18.1)
 - Review and edit Team Qualifications section (Urgency: 18.1)
 - Review and edit References section (Urgency: 18.1)
 - Review and edit Appendices (Urgency: 18.1)
 - Update abstract based on final content (Urgency: 18.1)
 - Compile final PDF submission (Urgency: 18.1)
 ### High Priority
 All high-priority tasks are already listed above in the "Due This Week" section.
--- a/Notes/Weekly/2025_50.md
+++ b/Notes/Weekly/2025_50.md
@ -0,0 +1,58 @@
 ---
 id: 2025-50
 title: Weekly — 2025-12-17
 type: Weekly
 created: 2025-12-17T20:56:30Z
 modified: 2025-12-17T20:56:30Z
 tags: [weekly]
 ---
 # Weekly - 2025 CW 50 (Wed 2025-12-17)
 ## Accomplishments
 ### Chair-Search
 - ✓ Review Zbeeb, Khaled application
 - ✓ Review Christopher, Gordon application
 - ✓ Review Robles Hernandez, Francisco Carlos application
 - ✓ Review Asmatulu, Ramazan application
 - ✓ Review Gupta, Sanju application
 - ✓ Review Yang, Xiaodong application
 - ✓ Review Kim, Harrison application
 - ✓ Review Makhlouf, Abdelsalam application
 - ✓ Review Gouma, Pelagia application
 - ✓ Review Akkus, Ozan application
 - ✓ Review Narayan, Roger application
 ### Internship
 - ✓ Tune up presentation for Emerson... digital twins
 ## Pushed or Rescheduled
 No tasks were rescheduled during this period.
 ## Cancelled or Deleted
 No tasks were cancelled or deleted during this period.
 ## To Do
 ### Due This Week
 **Due within 24 hours:**
 - **Union** — Talk to Jessica about getting a room for an event (Due: 1d, Urgency: 9.23)
 ### High Priority
 **Zettelkasten (zk):**
 - Write zettels about Andre Platzer and differential dynamic logic (Urgency: 3.34)
 - Write zettels about webofscience database (Urgency: 3.34)
 - Deterministic Parity Automata (Urgency: 3.1)
 - Mealy Machines (Urgency: 3.1)
 - AIGER Circuits (Urgency: 3.1)
 - Reactive Synthesis (Urgency: 3.1)
 - Write about opp. chall. and res. needs for remote micro ope. (Urgency: 3.07)
 **Other Projects:**
 - **ERLM** — Add research tasks to research approach section (Urgency: 2.36)
 - **Thesis** — The Algorithmic Analysis of Hybrid Systems (1995) [reading] (Urgency: 2.3)
--- a/Notes/Weekly/2026_02.md
+++ b/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
--- a/Notes/Weekly/2026_03.md
+++ b/Notes/Weekly/2026_03.md
@ -0,0 +1,82 @@
 ---
 id: 2026-03
 title: Weekly — 2026-01-14
 type: Weekly
 created: 2026-01-14T18:46:24Z
 modified: 2026-01-14T19:21:41Z
 tags: [weekly]
 ---
 # Weekly - 2026 CW 03 (Wed 2026-01-14)
 ## Accomplishments
 - Finished FRET tutorial I was working on. I've still got
 weird dependency things I need to figure out. Moving to a
 mac has caused some interesting quirks but I'm working them
 out.
 - Read Hybrid Automata: An Algorithmic Approach to
 Specification and Verification of Hybrid Systems
 - Did 2 interviews for chair search and read additional
 applicants stuff. 
 - Bob asked me for help for ENGR 1933. I completed my RAMP
 training to get recertified. 
 - Completed the review form.
 - Did maneuvering with Emerson to get them moving on an
 offer. INL sent me a formal offer letter.
 ### Chair-Search
 - ✓ Read additional applican and provide scords
 - ✓ Read Clarks application and provide review scores
 - ✓ Read remaining two applicants and provide scores
 ### Thesis
 - ✓ Do FRET tutorials
 ## Pushed or Rescheduled
 ### Thesis
 - The Algorithmic Analysis of Hybrid Systems (1995) — rescheduled
 - Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems (1993) — rescheduled
 - Hamilton-Jacobi Reachability: A Brief Overview and Recent Advances (2017) — rescheduled
 ### Other
 - Investigate DICE conference — rescheduled
 ## Cancelled or Deleted
 No tasks were cancelled or deleted this week.
 ## To Do
 - Decide on an internship
 - Additional interviews this week
 - Review meeting is this week.
 - Re-outline research approach. Identify the holes
 - Plan out a prelim problem. Maybe a simple version of what
  HARDENS did. Just initiating scram?
 - Follow up with IT about what the hell is sending packets
 from the ARCADE puter.
 ### Due This Week
 No tasks are due in the next 7 days.
 ### High Priority
 **Thesis (reading)**
 - The Algorithmic Analysis of Hybrid Systems (1995) — Urgency: 17.8 (overdue by 5 days)
 - Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems (1993) — Urgency: 13.8 (overdue by 5 days)
 - Hamilton-Jacobi Reachability: A Brief Overview and Recent Advances (2017) — Urgency: 13.8 (overdue by 5 days)
 - Hybrid Systems: Review and Recent Progress (2003) — Urgency: 2.45
 - Multiple Lyapunov Functions and Other Analysis Tools for Switched and Hybrid Systems (1998) — Urgency: 2.45
 **Other**
 - Investigate DICE conference — Urgency: 15.8
 **ERLM (editing/writing)**
 - Add research tasks to research approach section — Urgency: 2.51
 **Zettelkasten**
 - AIGER Circuits — Urgency: 3.25
 - Reactive Synthesis — Urgency: 3.25
 - Write about opp. chall. and res. needs for remote micro ope. — Urgency: 3.22
--- a/Notes/Weekly/2026_05.md
+++ b/Notes/Weekly/2026_05.md
@ -0,0 +1,78 @@
 ---
 id: 2026-05
 title: Weekly — 2026-01-28
 type: Weekly
 created: 2026-01-28T18:38:10Z
 modified: 2026-01-28T18:45:48Z
 tags: [weekly]
 ---
 # Weekly - 2026 CW 05 (Wed 2026-01-28)
 ## Accomplishments
 **Thesis**
 - ✓ Edit research approach some
 - ✓ The Algorithmic Analysis of Hybrid Systems (1995) (reading, overdue from 2026-01-09)
 - ✓ Edit research approach
 - Set up the ARCADE computer and got the undergrads an
 account
 - Couple of the last interviews for the chair search. Things
  are looking really good and should wind down in intensity
  for a bit
 **General**
 - ✓ Write email to INL about rejecting offer
 - ✓ Make groupchat for Sam's bachelor party
 ## Pushed or Rescheduled
 **Poker**
 - Make development plan (overdue by 3 days)
 - Make plan about table layout (overdue by 3 days)
 **Thesis**
 - Write: Define hybrid systems and requirements (tablesetting intro) (overdue by 13 hours)
 - Write: Requirements mapping to system components (operational vs strategic) (overdue by 13 hours)
 - Write: Requirements extraction and discrete abstraction (overdue by 13 hours)
 - Write: Reactive synthesis implementation and tools (LTL, FRET) (overdue by 13 hours)
 - Write: Continuous components intro and mode types overview (overdue by 13 hours)
 - Write: Transitory modes (entry/exit, reachability verification) (overdue by 13 hours)
 - Write: Stabilizing modes (barrier certificates) (overdue by 13 hours)
 - Write: Expulsory modes (failure detection, ...) (overdue by 13 hours)
 ## Cancelled or Deleted
 No tasks were cancelled or deleted in the past week.
 ## To Do
 Finish writing about research approach. Redo risks and
 contingencies section based on research approach. For
 example, risk of continuous discrete abstraction being not
 good, risk of how much system variation is needed? Can only
 really do parametric uncertainty. Unless?
 **Due This Week**
 No tasks with explicit due dates in the next 7 days.
 **High Priority**
 These tasks are overdue and require immediate attention:
 **Thesis (urgency 14.5)**
 - Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems (1993) (reading, overdue by 2 weeks)
 - Hamilton-Jacobi Reachability: A Brief Overview and Recent Advances (2017) (reading, overdue by 2 weeks)
 **Poker (urgency 11.4)**
 - Make development plan (overdue by 3 days)
 - Make plan about table layout (overdue by 3 days)
 **Thesis Writing (urgency 10.9)**
 - Write: Define hybrid systems and requirements (tablesetting intro) (overdue by 13 hours)
 - Write: Requirements mapping to system components (operational vs strategic) (overdue by 13 hours)
 - Write: Requirements extraction and discrete abstraction (overdue by 13 hours)
 - Write: Reactive synthesis implementation and tools (LTL, FRET) (overdue by 13 hours)
 - Write: Continuous components intro and mode types overview (overdue by 13 hours)
 - Write: Transitory modes (entry/exit, reachability verification) (overdue by 13 hours)
--- a/Notes/HUB-20250818131731-logics.md
+++ b/Notes/HUB-20250818131731-logics.md
@ -0,0 +1,38 @@
 ---
 id: HUB-20250818131731
 title: Logics
 type: hub
 created: 2025-08-18T17:17:31Z
 modified: 2025-08-18T19:44:30Z
 tags: [hub]
 aliases: []
 ---
 # Logics
 > Logic is a way of transforming ideas in a plain language
 > into precise mathematical statements. There are a bunch of
 > different types of logic, as linked below, but in all of
 > them there's an emphasis on precision.
 ## Contents (map of notes)
 - [[Propositional Logic]]  
 - [[Predicate Logic]]  
 - [[Temporal Logic]]  
 ## Permanent seeds (key ideas)
 - [[ ]]  
 ## Related hubs
 - [[]]  
 ## Sources / Literature
 - 
 ## Open questions / Next actions
 - [ ] 
--- a/Notes/HUB-20250822135454-formal-methods.md
+++ b/Notes/HUB-20250822135454-formal-methods.md
@ -0,0 +1,38 @@
 ---
 id: HUB-20250822135454
 title: Formal Methods
 type: hub
 created: 2025-08-22T17:54:54Z
 modified: 2025-08-22T17:57:39Z
 tags: [hub]
 aliases: []
 ---
 # Formal Methods
 > The purpose of this hub is to make a high level hub of
 > everything formal methods related (which is a lot!!!)
 ## Related hubs
 - [[formal-methods-in-machine-learning]]  
 ## Related Zettels
 ### Topics
 [[Abstract Interpretation for Formal Methods]]
 [[Satisfiability Modulo Theory]]
 [[Mixed Integer Linear Programming]]
 [[Complete vs. Incomplete Formal Methods]]
 ### Tools
 [[Strix]]
 ## Sources / Literature
 - [[a-review-of-formal-methods-applied-to-machine-learning]]
 ## Open questions / Next actions
 - [ ] 
--- a/Notes/20250815170942-zettelkasten.md
+++ b/Notes/20250815170942-zettelkasten.md
@ -0,0 +1,20 @@
 ---
 id: 20250815170942
 title: Zettelkasten
 type: permanent
 created: 2025-08-15T21:09:42Z
 modified: 2025-08-15T21:18:21Z
 tags: []
 ---
 # Zettelkasten
 Zettelkasten is a note taking system that uses a series of
 single idea notes to build connections between notes. There
 are different kinds of zettelkasten notes:
 1. [[permanent-notes]]
 2. [[literature-notes]]
 3. [[hub-notes]]
 and 
 4. [[fleeting-notes]]
--- a/Notes/20250815171141-permanent-notes.md
+++ b/Notes/20250815171141-permanent-notes.md
@ -0,0 +1,10 @@
 ---
 id: 20250815171141
 title: Permanent Notes
 type: permanent
 created: 2025-08-15T21:11:41Z
 modified: 2025-08-15T21:11:56Z
 tags: []
 ---
 # Permanent Notes
--- a/Notes/20250815171436-literature-notes.md
+++ b/Notes/20250815171436-literature-notes.md
@ -0,0 +1,22 @@
 ---
 id: 20250815171436
 title: Literature Notes
 type: permanent
 created: 2025-08-15T21:14:36Z
 modified: 2025-08-15T21:20:37Z
 tags: []
 ---
 # Literature Notes
 Literature notes are notes that reference research. They
 should be like fleeting notes almost, where they only have
 one real connection--the resource used to derive the notes.
 From that point, the individual thoughts should be moved
 into permanent notes that are focused on each idea rather
 than the resource itself.
 I've created two folders in my literature notes: Processed
 and the root folder. This is pretty self explanatory, but
 for thoroughness, once lit notes are processed into
 zettels they move into the processed folder.
--- a/Notes/20250815171449-hub-notes.md
+++ b/Notes/20250815171449-hub-notes.md
@ -0,0 +1,21 @@
 ---
 id: 20250815171449
 title: Hub Notes
 type: permanent
 created: 2025-08-15T21:14:49Z
 modified: 2025-08-15T21:22:59Z
 tags: []
 ---
 # Hub Notes
 Hub notes are a way to systemitize knowledge. They include
 mostly links to other things that are derivatives or subsets
 of the hub note topic. Here's an example:
 A hub note might contain 'Functional Programming Languages'
 and link to several language topics 'Haskell', 'F*', etc.
 where each of those might also be a hub note.
 Hub notes are supposed to be a map in a sense of all the
 notes they contain.
--- a/Notes/20250815171459-fleeting-notes.md
+++ b/Notes/20250815171459-fleeting-notes.md
@ -0,0 +1,19 @@
 ---
 id: 20250815171459
 title: Fleeting Notes
 type: permanent
 created: 2025-08-15T21:14:59Z
 modified: 2025-08-15T21:24:24Z
 tags: []
 ---
 # Fleeting Notes
 Fleeting Notes are notes that are similar to unprocessed
 notes in [[literature-notes]], but they are not connected to
 a resource like a literature note is. They are notes that
 won't often get revisited (if at all). Daily notes are
 pretty much the quintessential example of a fleeting note,
 but also random ideas are a thing for fleeting notes too. I
 have a processed folder in my fleeting notes to do a similar
 process as lit notes.
--- a/Notes/20250818132007-propositional-logic.md
+++ b/Notes/20250818132007-propositional-logic.md
@ -0,0 +1,38 @@
 ---
 id: 20250818132007
 title: Propositional Logic
 type: permanent
 created: 2025-08-18T17:20:07Z
 modified: 2025-08-18T19:52:42Z
 tags: []
 ---
 # Propositional Logic
 Propositional logic makes statements saying things like 'if
 x, then y'. They are statements that are either **true or
 false**, and have binary variables (P, Q, R, X, Y, etc...)
 Here's some examples:
 *If x, then y.* 
 $$x\rightarrow y$$
 *If x and y, then z.* 
 $ (x \wedge y) \rightarrow z $
 *Either the pump is on or the power is out.*
 $ Pump \oplus \neg Power $ 
 The pump is on and water is flowing if and only if the power
 is on.
 $( Pump \wedge Water) \leftrightarrow Power$
 Propositional logic is expanded upon by 
 [[predicate-logic]].
--- a/Notes/20250818132018-predicate-logic.md
+++ b/Notes/20250818132018-predicate-logic.md
@ -0,0 +1,63 @@
 ---
 id: 20250818132018
 title: Predicate Logic
 type: permanent
 created: 2025-08-18T17:20:18Z
 modified: 2025-08-18T20:20:03Z
 tags: []
 ---
 # Predicate Logic
 Predicate logic extends propositional logic by using
 predicates and quantifiers. 
 - **Predicates** express properties or relations (e.g., 
 $Pump(x)$ or $Connected(v,c)$).
 - **Quantifiers** let us say something about *all* or *some*
 in the domain.
    - $\forall$ = for all 
    - $\exists$ = exists, at least one
    - $\exists!$ = there exists exactly one
 Predicates kind of look like functions: $Pump(x)$ means $x$ is
 a pump.
 **Relational Predicates** have two inputs:
 $Connected(x,y)$ means pump $x$ is connected to valve $y$
 ## Examples
 Predicate logic requires you to *introduce the
 variable first*. This feels weird at first, but is
 mathematically explicit. The predicate does not define the
 input, it only defines the property! 
 Here's an example:
 $\forall x (Pump(x) \rightarrow Working(x))$
 Means that 'every pump works'. But, we define first a set x,
 then specify it is a pump for all x, and that they all of x,
 which are all pumps, work.
 What if we have one pump that doesn't work?
 $\exists x(Pump(x) \wedge \neg Working(x))$
 ## Nested Qualifiers
 We can stack qualifiers and do some nifty things. 
 How do we say: There exists one controller that stabilizes
 every plant?
 $ \exists k \forall G (Plant(G) \rightarrow Stabilizes(k,G))$
 This is obviously not possible. So how do we say the
 opposite, that for any plant there exists at least one
 stabilizing controller:
 $ \forall G \exists k (Plant(G) \rightarrow (Controller(k)
 \wedge Stabilizes(k,G)))$
--- a/Notes/20250818132022-temporal-logic.md
+++ b/Notes/20250818132022-temporal-logic.md
@ -0,0 +1,63 @@
 ---
 id: 20250818132022
 title: Temporal Logic
 type: permanent
 created: 2025-08-18T17:20:22Z
 modified: 2025-08-21T16:42:25Z
 tags: []
 ---
 # Temporal Logic
 ## What is Temporal Logic?
 An extension of **predicate logic** that allows reasoning
 about how statements evolve over **time**.  
 - Used heavily in **formal verification**, **model
 checking**, and **control systems safety**.  
 - Reasoning is over **infinite traces** (sequences of
 states).  
 ---
 ## Core Temporal Operators
 | Symbol | LaTeX | Name | Meaning |
 |--------|-------|------|---------|
 | X φ | `X \varphi` | Next | φ holds in the **next** state |
 | F φ | `\Diamond \varphi` | Eventually | φ will hold at some time in the **future** |
 | G φ | `\Box \varphi` | Globally (Always) | φ holds at **all future times** |
 | φ U ψ | `\varphi \, U \, \psi` | Until | φ must hold until ψ holds |
 ---
 ## Example Specifications
 1. **Safety:**  
   *“The reactor temperature never exceeds 600°C.”*  
   $G\,(temp < 600)$
 2. **Liveness:**  
   *“The pump will eventually turn on.”*  
    $F(PumpOn)$
 3. **Response:**  
   *“Whenever a request occurs, it will eventually be granted.”*  
   $G\,(request \rightarrow F\,grant)$
 4. **Stability:**  
   *“If the valve opens, it stays open until pressure is safe.”*  
    $G\,(ValveOpen\rightarrow (ValveOpen\;U\;PressureSafe))$
 ## Why It Matters
 - **Formal Methods:** Express constraints on **system behaviors over time**.  
 - **Model Checking:** Tools like SPIN, NuSMV, Spot verify LTL specs.  
 - **Engineering Applications:**  
  - Ensure control systems obey safety invariants.  
  - Specify liveness goals for controllers (e.g., “eventually stabilize temperature”).  
  - Used in **TLA+**, runtime monitoring, and shield synthesis.
 ## Related Notes
 [[strix]] - a reactive synthesis tool using temporal logic
 specs
--- a/Notes/20250818164800-safety-properties.md
+++ b/Notes/20250818164800-safety-properties.md
@ -0,0 +1,22 @@
 ---
 id: 20250818164800
 title: Safety Properties
 type: permanent
 created: 2025-08-18T20:48:00Z
 modified: 2025-08-18T20:54:35Z
 tags: []
 ---
 # Safety Properties
 Safety properites say that nothing bad ever happens. They
 often are specified as such using some formal requirement. 
 In [[Temporal Logic | LTL]], they can look like this:
 *The traffic light will never been red and green at the same
 time.* 
 $G \neg (green \wedge red)$
 A sort of opposite of safety proprerties is [[liveness-properties]].
--- a/Notes/20250818165010-liveness-properties.md
+++ b/Notes/20250818165010-liveness-properties.md
@ -0,0 +1,22 @@
 ---
 id: 20250818165010
 title: Liveness Properties
 type: permanent
 created: 2025-08-18T20:50:10Z
 modified: 2025-08-18T20:54:38Z
 tags: []
 ---
 # Liveness Properties
 Liveness properties are kinda the dual of
 [[safety-properties]], but instead they say that something
 good will eventually happen.
 Here's an example:
 *If there's someone waiting, the light will eventually turn
 green:* 
 $ G(request \rightarrow F\, green)$
--- a/Notes/20250819103208-strix.md
+++ b/Notes/20250819103208-strix.md
@ -0,0 +1,31 @@
 ---
 id: 20250819103208
 title: Strix
 type: permanent
 created: 2025-08-19T14:32:08Z
 modified: 2025-08-21T16:42:39Z
 tags: []
 ---
 # Strix
 Strix is a reactive synthesis tool that takes linear
 temporal logic specifications and turns them into
 implementations using Mealy machines or AIGER circuits.
 Strix does this using deterministic parity automata (DPA).
 With these, they can use much more efficient parity game
 algorithms as opposed to using symbolic methods.
 Strix was debuted after SYNTCOMP2017, to great success.
 Their automata at the time were much smaller than
 competitive models, and their solve times were on average
 much faster. They also solved some benchmarks that other
 tools previously had been unable to solve.
 ## Related Notes
 [[Temporal Logic]]
 [[SYNTCOMP]]
 [[Deterministic Parity Automata]]
 [[Mealy Machines]]
 [[AIGER Circuits]]
 [[Reactive Synthesis]]
--- a/Notes/20250821123741-syntcomp.md
+++ b/Notes/20250821123741-syntcomp.md
@ -0,0 +1,21 @@
 ---
 id: 20250821123741
 title: SYNTCOMP
 type: permanent
 created: 2025-08-21T16:37:41Z
 modified: 2025-08-21T16:42:25Z
 tags: []
 ---
 # SYNTCOMP
 SYNTCOMP, otherwise known as the Reactive Synthesis
 Competition, is a yearly competition for reactive synthesis
 tools to compete against one another to try and solve
 synthesis benchmarks.
 SYNTCOMP has been around since 2014. Usually, they run all
 the code on their own machines to ensure fairness. 
 SYNTCOMP is a satelite event of CAV, the International
 Conference on Computer-Aided Verification.
--- a/Notes/20250822134355-formal-methods-in-machine-learning.md
+++ b/Notes/20250822134355-formal-methods-in-machine-learning.md
@ -0,0 +1,10 @@
 ---
 id: 20250822134355
 title: Formal Methods in Machine Learning
 type: permanent
 created: 2025-08-22T17:43:55Z
 modified: 2025-08-22T17:43:55Z
 tags: []
 ---
 # Formal Methods in Machine Learning
--- a/Notes/20250822135802-abstract-interpretation-for-formal-methods.md
+++ b/Notes/20250822135802-abstract-interpretation-for-formal-methods.md
@ -0,0 +1,15 @@
 ---
 id: 20250822135802
 title: Abstract Interpretation for Formal Methods
 type: permanent
 created: 2025-08-22T17:58:02Z
 modified: 2025-08-25T16:01:46Z
 tags: []
 ---
 # Abstract Interpretation for Formal Methods
 Abstract interpretation in a formal methods context takes
 something about a system and makes an approximation of it in
 order to make reasoning about it easier.
--- a/Notes/20250826111220-quad-charts.md
+++ b/Notes/20250826111220-quad-charts.md
@ -0,0 +1,58 @@
 ---
 id: 20250826111220
 title: Quad Charts
 type: permanent
 created: 2025-08-26T15:12:20Z
 modified: 2025-08-26T15:20:50Z
 tags: []
 ---
 # Quad Charts
 Quad charts are the briefest of research proposals, and are
 a way of conveying a research idea in just one
 slide. 
 The audience for a quad chart is usually non-technical. The
 content should reflect this.
 Quad charts consist of quadrants:
 ## Quadrant 1 (Upper Left): Goals and Objectives
 This quadrant states the goal of the research in a single
 sentence, and lists the outcomes underneath it. Often you
 can start with "The goal of this research is to..."
 Then, the outcomes follow: "If this research is
 successful, we should be able to do the following:
 1. ...
 2. ...
 3. ...
 (4.?)
 It is critical that no jargon is used here. It is very
 tempting to do so.
 ## Quadrant 2 (Bottom Left): Research Approach
 This quadrant answers the question: "What's new in your
 approach?"
 ## Quadrant 3 (Top Right): Pretty Picture
 This is a break for the reader, and likely the first thing
 they'll actually look at on the chart. This figure should
 illustrate a key idea about the work that you want the
 reader to take away.
 No personal information should be included.
 ## Quadrant 4 (Bottom Right): Impact and Contact Info
 This quadrant answers the question of "Who cares? What
 difference will it make if you're successful?"
 This quadrant should also contain contact info of the
 principal investigator, and if applicable, their advisor.
--- a/Notes/20250826114550-heilmeier-catechism.md
+++ b/Notes/20250826114550-heilmeier-catechism.md
@ -0,0 +1,40 @@
 ---
 id: 20250826114550
 title: Heilmeier Catechism
 type: permanent
 created: 2025-08-26T15:45:50Z
 modified: 2025-08-26T16:02:59Z
 tags: []
 ---
 # Heilmeier Catechism
 George Heilmeier was a program manager at the Defense
 Advanced Research Projects Administration (DARPA) who was
 flummoxed with research proposals for artificial
 intelligence. In order to quickly sort through the
 proposals, he developed an 8 question system to quickly cut
 through the muck.
 This is the Heilmeier Catechism:
 1. What are you trying to do? Articulate your research with
   absolutely no jargon.
 2. How is it done today and what are the limits of current
   practice?
 3. What's new in your approach and why will you be
   successful?
 4. Who cares? If you're successful, what difference will it
   make?
 5. What are the risks?
 6. How long will it take?
 7. How much will it cost?
 8. What are the midterm and final exams? How will you
   measure success?
--- a/Notes/20250829114522-hybrid-systems.md
+++ b/Notes/20250829114522-hybrid-systems.md
@ -0,0 +1,57 @@
 ---
 id: 20250829114522
 title: Hybrid Systems
 type: permanent
 created: 2025-08-29T15:45:22Z
 modified: 2025-09-11T21:46:53Z
 tags: []
 ---
 # Hybrid Systems
 I'm borrowing a lot from
 [[multiple-lyapunov-functions-and-other-analysis-tools-for-swtiched-and-hybrid-systems]].
 Hybrid systems are those that combine continuous and
 discrete dynamics together. This is usually some sort of
 finite automata + differential equations.
 Hybrid systems can be written like:
 $$\dot{x}(t) = \xi(t), \quad t\geq 0$$
 where $x(t)$ is the continuous component of the state.
 $\xi(t)$ is a vector field that depends on $x(t)$ and the
 hybrid dynamics.
 Switching between modes (aka discontinuities in $\xi(\cdot)$)
 can happen in one of two ways:
 1. **Autonomous Switching** - Autonomous switches happen
   depending on state values of $x(t)$.
 2. **Controlled Switching** - $\xi(\cdot)$ changes abruptly
   in response to a control command.
 One may write a continuous time autonomous hybrid system
 like this:
 $$\dot{x}(t) = f(x(t), q(t))$$
 $$q(t) = \nu(x(t), q(t^-))$$
 where:
 - $x(t) \in R^n$
 - $q(t) \in Q \simeq {1,...,N}$
 - $f(\cdot,q): R^n \rightarrow R^n,q \in Q$, with each
 [[lipschitz-continuous]]. These are the *continuous
 dynamics*.
 - $\nu: R^n \times Q \rightarrow Q$ is the *finite dynamics*
 A controlled system might be written as:
 $$\dot{x}(t) = f(x(t), q(t), u(t))$$
 $$q(t) = \nu(x(t), q(t^-), u(t))$$
 where:
 - $u(t) \in R^m$
--- a/Notes/20250911165736-switched-systems.md
+++ b/Notes/20250911165736-switched-systems.md
@ -0,0 +1,35 @@
 ---
 id: 20250911165736
 title: Switched Systems
 type: permanent
 created: 2025-09-11T20:57:36Z
 modified: 2025-09-11T21:09:55Z
 tags: []
 ---
 # Switched Systems
 Switched systems are those that mix continuous and discrete
 dynamics. They are systems that are 'multimodal'. This means
 that they can have different continuous dynamic modes.
 I'm borrowing form
 [[multiple-lyapunov-functions-and-other-analysis-tools-for-swtiched-and-hybrid-systems]],
 but here's a short description of how they work.
 A prototypical switched system is as follows:
 $$\dot{x}(t)=f_i ( x(t)), \quad i \in Q \simeq {1,...,N}$$
 with two conditions:
 1. Each $f_i$ is globally [[Lipschitz Continuous]]
 2. The i's are picked in a way that there are finite
   switches in finite time.
 There's also this thing called a *continuous switched
 system*. A continuous switched system is one that does not
 change continuous states when a switch occurs. That is to
 say when switching from $i$ to $i'$:
 $$f_i(x(t_i),t_i) = f_{i'}(x(t_{i'}),t_{i'})$$
--- a/Notes/20250911170650-lipschitz-continuous.md
+++ b/Notes/20250911170650-lipschitz-continuous.md
@ -0,0 +1,24 @@
 ---
 id: 20250911170650
 title: Lipschitz Continuous
 type: permanent
 created: 2025-09-11T21:06:50Z
 modified: 2025-09-16T16:32:37Z
 tags: []
 ---
 # Lipschitz Continuous
 Lipschitz continuous functions are a special case of
 continuous functions. Lipschitz continuity means that a cone
 can be created with slope less than some real number
 $K$. 
 Fora a real valued function in one dimension, Lipschitz
 continuity is defined as:
 $$| f(x_1) - f(x_2)| \leq K|x_1 - x_2|$$
 Lipschitz continuity can be expanded to vector fields. From
 here, we can say that ODE trajectories do NOT intersect, and
 that every trajectory is unique. 
--- a/Notes/20251030141457-nuclear-operating-procedures.md
+++ b/Notes/20251030141457-nuclear-operating-procedures.md
@ -0,0 +1,20 @@
 ---
 id: 20251030141457
 title: Nuclear Operating Procedures
 type: permanent
 created: 2025-10-30T18:14:57Z
 modified: 2025-10-30T18:19:21Z
 tags: []
 ---
 # Nuclear Operating Procedures
 Nuclear operating procedures are big books of procedures
 that reactor operators use to perform control of reactors.
 Operating procedures are built on a per-plant basis, but are
 also designed with the general plant architecture in mind
 [[nureg899]]. 
 Operating procedures have different categories:
 1. Regular operating procedures
 2. [[Emergency Operating Procedures]]
 3. Theres ones about severe accidents too.
--- a/Notes/20251030141936-emergency-operating-procedures.md
+++ b/Notes/20251030141936-emergency-operating-procedures.md
@ -0,0 +1,40 @@
 ---
 id: 20251030141936
 title: Emergency Operating Procedures
 type: permanent
 created: 2025-10-30T18:19:36Z
 modified: 2025-10-30T19:30:12Z
 tags: []
 ---
 # Emergency Operating Procedures
 Emergency operating procedures for nuclear power are special
 procedures that are used when off-normal conditions are
 present. They are for when 'shit hits the fan'. 
 EOPs have defining regulations. Most notably [[nureg899]].
 NUREG899 is a writers guide to emergency operating
 procedures.
 EOPs should be 'function-oriented'. This means operators
 should not need to know a root cause to start performing
 control operations in an emergency. Critical functions in an
 emergency are usually:
 1. [[Containment Integrity]]
 2. [[Reactivity Control]]
 3. [[Heat Removal]]
 4. [[Reactor Coolant Inventory Control]]
 If each of these are maintained, the reactor can be 'safe',
 and the risk of environmental release is minimized. [[nureg899]]
 EOPs should minimize cross referencing because it increases
 decision time and is disruptive changing between documents
 [[nureg899]].
 EOPs today are reveiwed with simulation exercises,
 control-room walkthroughs, seminars, and numerical analysis
 [[nureg899]].
--- a/Notes/20251223161108-andre-platzer.md
+++ b/Notes/20251223161108-andre-platzer.md
@ -0,0 +1,22 @@
 ---
 id: 20251223161108
 title: Andre Platzer
 type: permanent
 created: 2025-12-23T21:11:08Z
 modified: 2025-12-23T21:53:21Z
 tags: []
 ---
 # Andre Platzer
 Andre Platzer is a computer scientist who is a professor at
 both Carnegie Mellon and the Karlsruhe Institute of
 Technology. Platzer is a leading researcher in 
 [[differential dynamic logic]] and [[cyber-physical
 systems]]. He has helped to create
 software like [[KeYmaera X]]. 
 He has also written a book, called "Logical Foundations of
 Cyber-Physical Systems." Manyu worked with KeYmaera X some
 and was inspired by his work.
--- a/Notes/20251223162450-web-of-science.md
+++ b/Notes/20251223162450-web-of-science.md
@ -0,0 +1,17 @@
 ---
 id: 20251223162450
 title: Web of Science
 type: permanent
 created: 2025-12-23T21:24:50Z
 modified: 2025-12-23T21:29:48Z
 tags: []
 ---
 # Web of Science
 Web of Science is a citation aggregator and database. Web of
 Science has both forward and backward citation sources, and
 other tools for doing source analysis. It is good to find
 resources, but also to connect resources to one another.
 This is useful in [[snowballing]]. 
--- a/Notes/20251223162954-snowballing.md
+++ b/Notes/20251223162954-snowballing.md
@ -0,0 +1,21 @@
 ---
 id: 20251223162954
 title: Snowballing
 type: permanent
 created: 2025-12-23T21:29:54Z
 modified: 2025-12-23T21:31:23Z
 tags: []
 ---
 # Snowballing
 Snowballing is a form of source discovery. Snowballing means
 to start with a source, and travel forwards and backwards
 in time with respect to citations. From this, one can find
 closely related papers to an original source without too
 much effort. 
 Snowballing has been found in the literature to be an
 efficient source of collecting relevant sources given a
 certain topic. One needs to find the first bit of snow (a
 good first resource), to start the snowball. 
--- a/Notes/20251223163648-deterministic-parity-automata.md
+++ b/Notes/20251223163648-deterministic-parity-automata.md
@ -0,0 +1,27 @@
 ---
 id: 20251223163648
 title: Deterministic Parity Automata
 type: permanent
 created: 2025-12-23T21:36:48Z
 modified: 2025-12-23T21:40:09Z
 tags: []
 ---
 # Deterministic Parity Automata
 Deterministic parity automata are a type of automata where
 the environment and the system play against one another, and
 describes the interactions therein. DPA are exhaustive, and
 end up with a result determining which player 'wins'. 
 DPA's have a scoring mechanism that results in an even or
 odd final score. An even final score indicates that the
 'controller' wins the game. There is no input from the
 environment that can't be controlled by the controller. All
 traces end up in a favorable state, with no infinite loops.
 An odd score means the opposite. There exists some limit
 cycle where the controller can't reach a desired mode and
 stay there. 
 DPA's are used in [[strix]]. They're how Strix does it's
 generation from temporal logics to a final automaton.
--- a/Notes/20251223165340-mealy-machines.md
+++ b/Notes/20251223165340-mealy-machines.md
@ -0,0 +1,49 @@
 ---
 id: 20251223165340
 title: Mealy Machines
 type: permanent
 created: 2025-12-23T21:53:40Z
 modified: 2025-12-23T22:38:18Z
 tags: []
 ---
 # Mealy Machines
 Mealy machines are a formalization of a system that has
 states drawn as nodes and transitions drawn from state to
 state. 
 From Wikipedia:
 ```
    A mealy machine is a finite state machine whose
 output values are determined by both its current state, and
 the current inputs.
 ```
 Mealy machines can also be defined as a six-tuple:
 $$(S, S_0, \Sigma, \Lambda, T, G)$$
 where 
 - S is the finite set of states
 - S_0 is the start state
 - $\Sigma$ is the input alphabet
 - $\Lambda$ is the output alphabet
 - $T : S \times \Sigma \rightarrow S$ is the state
 transition function
 - $G : S \times \Sigma \rightarrow \Lambda$ is the output
 function
 Mealy machines have the advantage that they generally can
 produce smaller sized automata (aka less states). This is
 because transitions themselves in a Mealy machine are states
 in a Moore machine. The state of 'opening' in a Moore
 machine is the transition itself in a Mealy machine. Outputs
 aren't just based on state, so it isn't necesary to create a
 state to produce an output like a Moore machine. An output
 action can be created with the current state AND the input
 together.
 ## Related
 [[Finite State Machines]]
--- a/Notes/20251223170627-finite-state-machines.md
+++ b/Notes/20251223170627-finite-state-machines.md
@ -0,0 +1,49 @@
 ---
 id: 20251223170627
 title: Finite State Machines
 type: permanent
 created: 2025-12-23T22:06:27Z
 modified: 2025-12-23T22:39:00Z
 tags: []
 ---
 # Finite State Machines
 Finite State Machines are a computer science term for
 machines that have a finite number of states, with clearly
 defined transitions between them. Sometimes, FSM are
 referred to simply as *state machines*. 
 FSM are an abstraction of a computational system. FSM are
 heavily used in systems that have clearly defined discrete
 states. Examples include traffic lights, elevators,
 combination locks, or others.
 FSM have **actions**. Actions are the unabstractified
 version of whatever the execution is. For physical systems,
 it might be something like turning a motor on.
 FSM can be categorized into two main categories:
 ## Acceptors (or 'detectors' or 'recognizers') Acceptors are
 a type of FSM that produce binary output, recognizing
 whether or not a given input is accepted. Examples of
 systems that are acceptors include things like ready-commit
 systems, or a password checker. These systems have an input,
 and reach a state that determines the input is acceptable,
 or incorrect. 
 ## Transducers
 Transducers are a set of finite state machines that produce
 an output based on input or state using *actions*. Actions
 in this case represent a transition between state that
 also has some external change. A finite state machine of an
 elevator would have actions of the elevator changing between
 floors, for example.
 Transducers with respect to control have two different
 types:
 [[mealy-machines]] -- these have output depend on state and input
 [[moore-machines]] -- these have output depend on state ONLY
--- a/Notes/20251223171835-moore-machines.md
+++ b/Notes/20251223171835-moore-machines.md
@ -0,0 +1,39 @@
 ---
 id: 20251223171835
 title: Moore Machines
 type: permanent
 created: 2025-12-23T22:18:35Z
 modified: 2025-12-23T22:52:38Z
 tags: []
 ---
 # Moore Machines
 Moore machines are a type of finite state machine whose
 output only depends on output state. Moore machines are
 useful because they simplify the behavior of a system to the
 simplest behaviours possible. They can be defined as a
 six-tuple:
 $$(S, S_0, \Sigma, \Lambda, T, G)$$
 where 
 - S is the finite set of states
 - S_0 is the start state
 - $\Sigma$ is the input alphabet
 - $\Lambda$ is the output alphabet
 - $T : S \times \Sigma \rightarrow S$ is the state
 transition function
 - $G : S \rightarrow \Lambda$ is the output
 function
 Moore machines do not have exit actions. They can only
 change their output based on a change of state. This means
 for systems with physical characteristics, such as a door
 opening or closing system, the intermediate states of
 opening and closing have to exist in a Moore machine. It is
 not possible to go from Open to Closed directly, because
 Open can't generate the output Closed. Instead, Open + the
 input 'open_door' or similar goes to the state 'closing',
 which can then create an action of 'motor_on' or similar,
 and then finally get to the final state Closed.
--- a/Notes/20260109155358-hybrid-automata.md
+++ b/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]]
--- a/Notes/20260109155410-linear-hybrid-automata.md
+++ b/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]].
--- a/Notes/20260109155415-timed-automata.md
+++ b/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]]
--- a/Notes/20260109155838-reactive-programs.md
+++ b/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]]
--- a/Notes/20260114132351-bayes-theorem.md
+++ b/Notes/20260114132351-bayes-theorem.md
@ -0,0 +1,49 @@
 ---
 id: 20260114132351
 title: Bayes' Theorem
 type: permanent
 created: 2026-01-14T18:23:51Z
 modified: 2026-01-14T18:43: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)
--- a/Notes/20260114133159-expected-value.md
+++ b/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) $$
--- a/Notes/20260114153529-random-number-generation.md
+++ b/Notes/20260114153529-random-number-generation.md
@ -0,0 +1,39 @@
 ---
 id: 20260114153529
 title: Random Number Generation
 type: permanent
 created: 2026-01-14T20:35:29Z
 modified: 2026-01-14T20:46:35Z
 tags: []
 ---
 # Random Number Generation (RNG)
 Random number generation is all about getting random
 numbers, and is easily defined as picking a number from a
 uniform distribution. Generally, there's two types:
 ## True RNG
 True RNG is systems that are truly random. Random systems
 are almost always derived from [[chaotic systems]], which
 technically are deterministic, but as so final state
 sensitive they're basically intractable and 'random' values
 can be extracted. Sometimes lava lamps (turbulence) is used,
 sometimes isotope decay is the thing.
 ## Pseudo RNG
 Computers can't really do true RNG. They just can't handle
 non-deterministic outcomes. In addition, true RNG is *slow*. 
 As such computers build PRNG. 
 >[!definition] Pseudo Random Number Generator
 > 
 > $\text{Struct}(S, \mu, f, U, g)$
 >
 > Where:
 > - $S$ is a finite set of states 
 > - $\mu$ is a distribution on S for the initial state (seed!)
 > - $f:S \rightarrow S$, the state transition function
 > - $U$ is the output space [0,1), or perhaps {0,...,m-1}
 > - $g:S \rightarrow U$, the output function
 > 
--- a/Notes/LIT-20250819112550-strix-explicit-reactive-synthesis-strikes-back.md
+++ b/Notes/LIT-20250819112550-strix-explicit-reactive-synthesis-strikes-back.md
@ -0,0 +1,60 @@
 ---
 id: LIT-20250819112550
 title: Strix Explicit Reactive Synthesis Strikes Back!
 type: literature
 created: 2025-08-19T15:25:50Z
 modified: 2026-01-09T21:08:06Z
 citekey: meyerStrixExplicitReactive2018
 ---
 # Strix: Explicit Reactive Synthesis Strikes Back!
 Authors:
 1. [[Phillipp Meyer]]
 2. [[Salomon Sickert]]
 3. [[Michael Luttenberger]]
 ## First Pass
 **Category:** Design paper. They made a new LTL synthesizer
 **Context:** 
 Strix is a response to other reative LTL syntehsizer
 competition entries.
 **Correctness:** 
 Seems good to me! They have data to back up their stuff.
 **Contributions:** 
 They contribute Strix, a tool that uses Determinstic Parity
 Automata (DPA) to simplify synthesis. DPA helps Strix solve
 problems faster by using parity game solvers as opposed to
 symbolic or bounded methods currently used.
 **Clarity:** 
 Easy to read!
 ## Second Pass
 **What is the main thrust?**
 The main thrust is their new tool, Strix.
 **What is the supporting evidence?**
 They make a testing suite that is supposed to be similar to
 the SYNTCOMP2017 testing setup, and run their solver
 through the same trials that the competition included. They
 achieve pretty good results: much much faster solve times
 while also keeping automata size small.
 **What are the key findings?**
 Strix is pretty good. The use of DBAs seems effective. Their
 'quality', a measure of automata size vs specification size,
 is also pretty good compared to other synthesizers.
 ## Third Pass
 **Recreation Notes:**
 **Hidden Findings:**
 **Weak Points? Strong Points?**
 ## Spawned Zettels
 [[Reactive Programs]]
--- a/Notes/LIT-20250822120822-a-review-of-formal-methods-applied-to-machine-learning.md
+++ b/Notes/LIT-20250822120822-a-review-of-formal-methods-applied-to-machine-learning.md
@ -0,0 +1,97 @@
 ---
 id: LIT-20250822120822
 title: A Review of Formal Methods applied to Machine Learning
 type: literature
 created: 2025-08-22T16:08:22Z
 modified: 2025-08-22T16:11:25Z
 citekey: 
 ---
 # A Review of Formal Methods applied to Machine Learning
 **Category:** This is a review paper. 
 **Context:** This paper tries to keep up with where formal
 methods are for machine learning based systems. It is not
 necessarily a controls paper, but a broader machine learning
 paper in general.
 **Correctness:** Really well written on the first pass. Easy
 to understand and things seem well cited.
 **Contributions:** Great citations showing links to
 different papers and also provides nice spots for forward
 research. Talks about how verification needs to be done
 along the whole pipeline: from data prep to training to
 implementation. There needs to be more work on proving
 things about model behavior, but in general this review has
 a positive outlook on the field. 
 **Clarity:** Very well written, easy to understand. Except,
 what is abstractification of a network?
 ## Second Pass
 This review gives an overview of formal
 methods applied to machine learning. Formal methods has been
 used for ML to test for robustness for various perturbations
 on inputs. They start by talking about several types of
 formal methods, including deductive verification, design by
 refinement, proof assistants, model checking, and semantic
 static analysis, and then finally, abstract interpretation
 of semantic static analysis. The last one has been used the
 most in FM of ML.
 A large part of the paper focuses on formal methods for
 neural network perturbation robustness. They split up the
 methods into two types: complete and incomplete formal
 methods. Complete formal methods are *sound* and *complete*.
 This means they do not have false positives or false
 negatives. These methods generally do not apply well to
 large networks (beyond hundreds gets rough), but give the
 highest level of assurance. Here, there are two more
 subcategories: SMT based solvers and MILP-based solvers.
 SMT solvers are Satisfiability Modulo Theory solvers. These
 solvers a set of constraints and check to see whether or not
 all of the constraints can be satisfied. Safety conditions
 are encoded as the *nA Review of Formal Methods applied to Machine Learningegation* of the safety constraint. That
 way, if a safety condition is violated, the SMT solver will
 pick it up as a counter example. 
 MILP based solvers are Mixed Integer Linear Programming
 solvers. MILPs use linear programming where certain
 constraints are integers to reduce the solving space.
 Instead of having an explicity satisffiability condition on
 safety or not, MILPs instead can use a minimizing function
 to generate counter examples. For example, a MILP saftey
 condition might be formalized as: $$ \text{min}\space
 \bf{x}_n$$ where a negative value of $\bf{x}_n$ is 'a valid
 counter example'.
 There are also 'incomplete formal methods'. These incomplete
 methods are sound, meaning they will not produce false
 negatives, but they may not be complete, meaning they may
 produce false positives. They scale better, but the false
 positives can be pretty annoying.
 One of the main incomplete methods is abstract
 interpretation. Things get very weird very fast--this is all
 about zonotopes and using over approximation of sets to say
 things about stability. There is weird stuff going on with
 cell splitting and merging that seems like a to grasp. But,
 apparently it works. 
 Next, they spend some time talking about other machine
 learning methods and the formal methods that have been
 applied to them. Of particular interest to me is the formal
 method application to support vector machines and decision
 trees. There are some useful methods for detecting
 robustness to adversarial inputs, and knowing what the
 nearest misclassification adversarial case is.
 ## Third Pass
 **Recreation Notes:**
 **Hidden Findings:**
 **Weak Points? Strong Points?**
--- a/Notes/LIT-202509012125-how-to-choose-a-good-scientific-problem.md
+++ b/Notes/LIT-202509012125-how-to-choose-a-good-scientific-problem.md
@ -0,0 +1,42 @@
 ---
 id: LIT-20250819112550
 title: How To Choose a Good Scientific Problem
 type: literature
 created: 2025-08-19T15:25:50Z
 modified: 2025-09-02T01:41:17Z
 citekey: 
 ---
 # How to Choose a Good Scientific Problem
 ## Authors
 [[Uri Alon]]
 ## Notes
 Uri is all about the 'nuturing lab', which means a lab's
 goal is not just to advance knowledge, but to nurture future
 scientists. 
 He describes problems on two axes: interest and difficulty.
 Interest here means how much knowledge we gain from solving
 the problem. He says grad students should choose easy
 problems, with ideally low interest, then postdocs move to
 high interest and easy (to save time), and finally new
 professors move towards the hard problems with high impact,
 as they have time to do so. 
 Uri also argues that taking time to find a good topic is
 time well spent. It can save a lot of time down the line.
 The inner and outer voices can lead to different ideas.
 Outer voices are those of peers, the department, or speakers
 at a conference-- but the inner voice is the more valuable
 voice. That is your own voice. Uri descirbes the inner voice
 is often something that needs nurtured, but can lead to
 less laborious science, and more self expression.
 Finally Uri talks about the schema that should be considered
 during research. It is not useful to think students will go
 from A->B taking the shortest path. There must be room to
 wander, as that is where new problems can be best found.
 This is what really lets students grow.
--- a/Notes/LIT-20250911143337-multiple-lyapunov-functions-and-other-analysis-tools-for-swtiched-and-hybrid-systems.md
+++ b/Notes/LIT-20250911143337-multiple-lyapunov-functions-and-other-analysis-tools-for-swtiched-and-hybrid-systems.md
@ -0,0 +1,52 @@
 ---
 id: LIT-20250911143337
 title: Multiple Lyapunov Functions and Other Analysis Tools for Swtiched and Hybrid Systems
 type: literature
 created: 2025-09-11T18:33:37Z
 modified: 2025-09-16T17:23:17Z
 citekey: 
 ---
 # Multiple Lyapunov Functions and Other Analysis Tools for Swtiched and Hybrid Systems
 ## First Pass
 **Category:** 
 Theoretical methods paper. This paper introduces a couple of
 new ways to work with hybrid systems and also does
 introduction of a lot of terms.
 **Context:** 
 Branicky is doing a lot of work with hybrid systems. He
 defines what a switched system is, what a hybrid system is,
 what a continuous switched system is and also included
 definitions of autonomy in there too
 **Correctness:** 
 Been cited like 2000 times.
 **Contributions:** 
 Multiple Lyapunov theory and Stability via Iterated Function
 Systems.
 **Clarity:** 
 Complex ideas written simply. Easy to read.
 ## 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?**
 ## Zettels Created
 [[Switched Systems]]
 [[hybrid-systems]]
 [[lipschitz-continuous]]
--- a/Notes/LIT-20251023125758-nureg899.md
+++ b/Notes/LIT-20251023125758-nureg899.md
@ -0,0 +1,66 @@
 ---
 id: LIT-20251023125758
 title: NUREG899
 type: literature
 created: 2025-10-23T16:57:58Z
 modified: 2025-10-30T18:20:30Z
 citekey: 
 ---
 # NUREG899
 Emergency operating procedures should be
 *function-oriented*. That means that operators 'do not have
 to immediately diagnose an event... to maintain the plant in
 a safe configuration." Critical functions are cited as:
 1. Containment integrity
 2. Reactivity Control
 3. Heat Removal
 4. Reactor coolant inventory control
 Functions  are maintained by 'tasks'. Tasks are specific
 actions that are taken to maintain or achieve a function.
 This doc says EOPs are verified and validated by:
 1. Excercising EOPs on simulators
 2. Control room walk-throughs
 3. Desk top reviews
 4. Seminars
 5. Computer modeling and analysis
 OPs should minimize the use of cross referencing because it
 increases decision times and increases the chance of human
 error. It's 'disruptive'.
 Operator Aids are things like flowcharts or graphs that can
 help an operator learn things more quickly and clearly than
 text alone can provide. They should be easily learned and
 retained, while being precise and not cluttered.
 Interpretability is paramount.
 EOPs have segments:
 1. Cover page
 2. Table of contents if applicable
 3. Scope
 4. A set of entry conditions
 5. Automatic actions that happen by automated systems
 6. What the operator should do immediately
 7. Things the operator should do afterwards based on
   reference to written procedures
 8. Relevant supporting material.
 Control rooms should have a sufficient number of EOP
 handbooks such that everyone can use one, they're easy to
 get to, and also be located such that they don't interfere
 with workstations or cover up controls. If there's multiple
 control rooms that share a common area, each control room
 should have it's own set of EOPs. They should not be sharing
 copies, essentially.
 Appendix B talks about logical statements. They're written
 strangely like program control flow, underlined, and
 capitalized:
 IF RPS scram has not initiated,
 THEN initiate SLC and isolate RWCU
--- a/Notes/LIT-20260109152249-hybrid-automata-an-algorithmic-approach-to-the-specification-and-verification-of-hybrid-systems.md
+++ b/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]]
--- a/Notes/to_process/A
+++ b/Notes/to_process/A
@ -0,0 +1,77 @@
 # First Pass
 **Category:** 
 This is a review paper. 
 **Context:** 
 This paper tries to keep up with where formal methods are for machine 
 learning based systems. It is not necessarily a controls paper, but a broader
 machine learning paper in general.
 **Correctness:** 
 Really well written on the first pass. Easy to understand and things seem 
 well cited.
 **Contributions:** 
 Great citations showing links to different papers and also provides nice spots
 for forward research. Talks about how verification needs to be done along the
 whole pipeline: from data prep to training to implementation. There needs to 
 be more work on proving things about model behavior, but in general this
 review has a positive outlook on the field. 
 **Clarity:** 
 Very well written, easy to understand. Except, what is abstractification of a 
 network?
 # Second Pass
 This review gives an overview of formal methods applied to machine learning.
 Formal methods has been used for ML to test for robustness for various 
 perturbations on inputs. They start by talking about several types of formal 
 methods, including deductive verification, design by refinement, proof 
 assistants, model checking, and semantic static analysis, and then finally, 
 abstract interpretation of semantic static analysis. The last one has been 
 used the most in FM of ML.
 A large part of the paper focuses on formal methods for neural network 
 perturbation robustness. They split up the methods into two types: complete
 and incomplete formal methods. Complete formal methods are *sound* and 
 *complete*. This means they do not have false positives or false negatives. 
 These methods generally do not apply well to large networks (beyond 
 hundreds gets rough), but give the highest level of assurance. Here, there
 are two more subcategories: SMT based solvers and MILP-based solvers.
 SMT solvers are Satisfiability Modulo Theory solvers. These solvers a set
 of constraints and check to see whether or not all of the constraints can be 
 satisfied. Safety conditions are encoded as the *negation* of the safety constraint.
 That way, if a safety condition is violated, the SMT solver will pick it up as a 
 counter example. 
 MILP based solvers are Mixed Integer Linear Programming solvers. MILPs use
 linear programming where certain constraints are integers to reduce the
 solving space. Instead of having an explicity satisffiability condition on safety
 or not, MILPs instead can use a minimizing function to generate counter
 examples. For example, a MILP saftey condition might be formalized as:
 $$ \text{min}\space \bf{x}_n$$
 where a negative value of $\bf{x}_n$ is 'a valid counter example'.
 There are also 'incomplete formal methods'. These incomplete methods are
 sound, meaning they will not produce false negatives, but they may not be
 complete, meaning they may produce false positives. They scale better, but
 the false positives can be pretty annoying.
 One of the main incomplete methods is abstract interpretation. Things get very
 weird very fast--this is all about zonotopes and using over approximation of sets
 to say things about stability. There is weird stuff going on with cell splitting 
 and merging that seems like a to grasp. But, apparently it works. 
 Next, they spend some time talking about other machine learning methods and
 the formal methods that have been applied to them. Of particular interest to me
 is the formal method application to support vector machines and decision 
 trees. There are some useful methods for detecting robustness to adversarial 
 inputs, and knowing what the nearest misclassification adversarial case is.
 # Third Pass
 **Recreation Notes:**
 **Hidden Findings:**
 **Weak Points? Strong Points?**
--- a/Notes/to_process/A
+++ b/Notes/to_process/A
@ -0,0 +1,32 @@
 # First Pass
 **Category:**
 This paper is a literature review
 **Context:** 
 Mukul says that there are a whole bunch of thrusts out there about neural 
 network based controllers, and that there needs to be a better way to 
 parse what research is what
 **Correctness:** 
 Looks good to me I suppose.
 **Contributions:** 
 Here's the most important figure in the whole thing:
 ![[Pasted image 20250721095146.png]]
 **Clarity:** 
 Well written.
 # 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?**
--- a/Notes/to_process/An
+++ b/Notes/to_process/An
@ -0,0 +1,59 @@
 ---
 alias: tee-hee-hee
 ---
 # An autonomous control framework for advanced reactors notes
 ## First Pass
 **Category:** 
 This is a vision-like paper.
 **Context:** 
 Dr. Wood is a professor of nuclear engineering at the University of Tennesse.
 He started working at UT after working at ORNL for 20+ years where he was
 a senior researcher. He works on common cause failures.
 **Correctness:** 
 There are not many citations, and a lot of the paper seems like it is off-the-cuff. 
 This was an invited article though in the *Nuclear Engineering and Technology* 
 journal. He's also got quite the resume.
 **Contributions:** 
 Dr. Wood gives a good overview of where we are (automated control), and
 where we need to go (autonomous control). Comparisons are made to other 
 industries, and how they've addressed these challenges. Clarifications are made
 with respect to how the nuclear industry is unique.
 **Clarity:** 
 Well written and clear, but a bit wordy at times. Examples are used but 
 sometimes it just feels like a mouthful.
 ## Second Pass
 **What is the main thrust?**
 Wood talks a lot about what it means for a system to be autonomous. He 
 actually starts with a etymological argument- "*automatos* means self-acting,
 whereas *autonomos* means independent." The point of an autonomous system 
 is that it must be able to make intelligent decisions that a human would 
 otherwise make. Knowing how to handle degraded or faulty sensors or 
 actuators, switching controller trains, and knowing when scramming is
 necessary are all decisions that an autonomous system would make, that
 a simple automated system could not. The key is in the decision making.
 **What is the supporting evidence?**
 Dr. Wood compares a lot to NASA control systems for the Mars rovers. These
 systems use two tiers of controllers: a decision layer and a functionality layer. 
 The functionality layer does what you think--it manages the physical 
 functioning. The decision layer is different. It decides on controller modes and 
 works instead with operational level goals.
 **What are the key findings?**
 The biggest findings are that an autonomous control system for a nuclear
 power plant is possible, but by far the biggest roadblock is a high assurance 
 decision making system. 
 ## Third Pass
 **Recreation Notes:**
 **Hidden Findings:**
 **Weak Points? Strong Points?**
--- a/Notes/to_process/Automation
+++ b/Notes/to_process/Automation
@ -0,0 +1,36 @@
 # First Pass
 **Category:** 
 This is a paper following a workshop. It is kind of a big picture / idea 
 type paper.
 **Context:** 
 This paper was written after a workshop took place to talk about recent NRC
 regulations. They talk about how different industries categorize the level
 of autonomy in systems, and create autonomous levels of reactor control.
 **Correctness:** 
 Vivek Agarwal chaired ANS in Chicago this past year. He's the real deal
 **Contributions:** 
 They contribute a first thought on how to go about creating milestones for
 autonomous systems, and give us a language to use when describing what level
 of autonomy a system is gunning for.
 **Clarity:** 
 Clearly written. Very nice!
 # 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?**
 <!The quick brown fox jumps over the lazy dog. The dog takes a nice nap. :)>
--- a/Notes/to_process/Economics
+++ b/Notes/to_process/Economics
@ -0,0 +1,32 @@
 # First Pass
 **Category:** 
 Systematic Review
 **Context:** 
 This paper is from the civil engineering school at the University of Leeds. 
 They are doing an overview of economics and finance research of small
 modular reactors.
 **Correctness:** 
 Can not say. Is a review!
 **Contributions:** 
 They do a good break down of the research we have done ('what we know') and
 what needs done ('what we do not know'). They point out a big discrepancy that we do not have a lot of research on operations and maintenance costs. 
 **Clarity:** 
 Nicely written. Easy to understand.
 # 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?**
--- a/Notes/to_process/Enhancing
+++ b/Notes/to_process/Enhancing
@ -0,0 +1,33 @@
 # First Pass
 **Category:** This paper is an experimental paper. 
 **Context:** The context of this paper is using a couple different techniques 
 synthesize control programs using different formal methods tools.
 **Correctness:** I trust Max's integrity. Some of the citations were funky and
 the intro was fluffy though.
 **Contributions:** 
 This paper shows that using LTL and other formal methods still struggles to 
 generate controllers for significantly challenging systems. The high bay 
 warehouse used to create this paper had to be simplified. Then, they introduce
 an SMT solver based method to try to generate code.
 **Clarity:** 
 The intro and conclusion do not provide very strong clarity on what they 
 actually did other than "high assurance is high difficulty", and that we're not 
 really there yet on HACPS.
 # 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?**
--- a/Notes/to_process/Evaluating
+++ b/Notes/to_process/Evaluating
@ -0,0 +1,42 @@
 # First Pass
 **Category:** 
 This is a methods paper. 
 **Context:** 
 This paper proposes a way of using mixed integer linear programming (MILP)
 to  evaluate properties of neural networks.
 **Correctness:** 
 Formal
 **Contributions:** 
 They do nifty things with bounds tightening and presolving that makes their
 solver very fast compared to the state of the art or Reluplex. They also talk 
 about stable and unstable neurons.
 **Clarity:** 
 They have a really good explanation of what a MILP problem is and how one
 might encode a neural network as one.
 # Second Pass
 **What is the main thrust?**
 The main thrust is their new solving method of MILPs for neural networks.
 With their method, neural networks can have their neurons analyzed to 
 prove whether or not the network is robust to input perturbations. This is 
 especially important for classifiers, who need to know if there are sneaky
 nonlinearities that can be harmful to a built system (like a glitch). This 
 method of bounds tightening and MILP usage makes their solver much faster
 and therein more capable to handle large networks.
 **What is the supporting evidence?**
 They have a whole bunch of experimental results.
 **What are the key findings?**
 MILPs and bound tightening is very good!
 # Third Pass
 **Recreation Notes:**
 **Hidden Findings:**
 **Weak Points? Strong Points?**
--- a/Notes/to_process/Formal
+++ b/Notes/to_process/Formal
@ -0,0 +1,31 @@
 # First Pass
 **Category:** 
 This is a weird one. This paper is essentially just a 'state-of-the-FRET' paper
 **Context:** 
 FRET comes from NASA and is a tool to line up requirements in a temporal
 language.
 **Correctness:** 
 Formal. But they don't really go into details.
 **Contributions:** 
 Really I don't think they contribute much here than an explanation of what's
 going on.
 **Clarity:** 
 Easy to read. 
 # 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?**
--- a/Notes/to_process/Formal
+++ b/Notes/to_process/Formal
@ -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?**
--- a/Notes/to_process/Hardware
+++ b/Notes/to_process/Hardware
@ -0,0 +1,50 @@
 ---
 creation date: 2024-08-08
 modification date: Thursday 8th August 2024 09:57:16
 tags:
  - Research
  - "#Survey"
 ---
 # Preamble
 ### Notable Links
 [[ARCADE Implementation at the University of Pittsburgh]]
 [[1. A shortlist of ARCADE Experiments]]
 ## What are we doing?
 Collecting and organizing papers about HiTL testing. Making notes about 'em. Stuff like that.
 ## Why are we doing it?
 08-08-2024: I'm writing a paper for [[2. (SR-CIST) Workshop on Security and Resiliency of Critical Infrastructure and Space Technologies]] and really need to know about hardware in the loop testing. 
 ## Who cares?
 Me. Andrew, probably. Dan, a lot.
 # Papers
 ## Summary Table
 ```dataview
 table without id
 link(file.path, title) as "Title", year as "Year", authors as "Authors", readstatus as "Read Status"
 from outgoing([[]])
 where readstatus or readstatus=False 
 sort readstatus desc, year desc
 ```
 ## Papers about ARCADE
 [[maccaroneADVANCEDREACTORCYBER]]
 [[chenFullscopeHighfidelitySimulatorbased2024]]
 ## Hardware In The Loop Papers
 [[mihalicHardwareintheLoopSimulationsHistorical2022]]
 [[bullockHardwareintheloopSimulation2004]]
 [[puysHardwareInTheLoopLabsSCADA2021]]
 [[choiRealTimeHardwareintheLoopHIL2021]]
 ## Cybersecurity of OT Papers
 [[sunSoKAttacksIndustrial2021]]
 [[mclaughlinControllerawareFalseData2014]]
 [[chekoleEnforcingMemorySafety2018]]
 [[kushnerRealStoryStuxnet2013]]
 [[CyberAttackGerman2015]]
 [[sguegliaFederalOfficialsInvestigating2023]]
 ## Formal Methods and PLCs
 [[fernandezadiegoApplyingModelChecking2015]]
 [[lopez-miguelPLCverifStatusFormal2022]]
 [[kleinFormallyVerifiedSoftware2018]] -- Littlebird paper
 ## Kry10
 [[Kry10TechnicalOverview]]
--- a/Show More
+++ b/Show More
		`@ -0,0 +1,2 @@`
							`[Vim for MATLAB](https://github.com/daeyun/vim-matlab)`