Auto sync: 2025-12-23 17:40:07 (8 files changed)

M  .task/taskchampion.sqlite3

A  "Zettelkasten/Permanent Notes/20251223161108-andre-platzer.md"

A  "Zettelkasten/Permanent Notes/20251223162450-web-of-science.md"

A  "Zettelkasten/Permanent Notes/20251223162954-snowballing.md"

A  "Zettelkasten/Permanent Notes/20251223163648-deterministic-parity-automata.md"

A  "Zettelkasten/Permanent Notes/20251223165340-mealy-machines.md"

A  "Zettelkasten/Permanent Notes/20251223170627-finite-state-machines.md"

A  "Zettelkasten/Permanent Notes/20251223171835-moore-machines.md"

Zettelkasten/Permanent 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.
+

Zettelkasten/Permanent 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]]. 

Zettelkasten/Permanent 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. 

Zettelkasten/Permanent 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.

Zettelkasten/Permanent 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]]
+

Zettelkasten/Permanent 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
+
+

Zettelkasten/Permanent 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:39:56Z
+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.