diff --git a/.task/taskchampion.sqlite3 b/.task/taskchampion.sqlite3 index e2ff8bcdc..809cdd22d 100644 Binary files a/.task/taskchampion.sqlite3 and b/.task/taskchampion.sqlite3 differ diff --git a/Zettelkasten/Permanent Notes/20251223161108-andre-platzer.md b/Zettelkasten/Permanent Notes/20251223161108-andre-platzer.md new file mode 100644 index 000000000..143fbcf13 --- /dev/null +++ b/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. + diff --git a/Zettelkasten/Permanent Notes/20251223162450-web-of-science.md b/Zettelkasten/Permanent Notes/20251223162450-web-of-science.md new file mode 100644 index 000000000..0c980515d --- /dev/null +++ b/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]]. diff --git a/Zettelkasten/Permanent Notes/20251223162954-snowballing.md b/Zettelkasten/Permanent Notes/20251223162954-snowballing.md new file mode 100644 index 000000000..47bf6c154 --- /dev/null +++ b/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. diff --git a/Zettelkasten/Permanent Notes/20251223163648-deterministic-parity-automata.md b/Zettelkasten/Permanent Notes/20251223163648-deterministic-parity-automata.md new file mode 100644 index 000000000..278ddecfe --- /dev/null +++ b/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. diff --git a/Zettelkasten/Permanent Notes/20251223165340-mealy-machines.md b/Zettelkasten/Permanent Notes/20251223165340-mealy-machines.md new file mode 100644 index 000000000..8753144cf --- /dev/null +++ b/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]] + diff --git a/Zettelkasten/Permanent Notes/20251223170627-finite-state-machines.md b/Zettelkasten/Permanent Notes/20251223170627-finite-state-machines.md new file mode 100644 index 000000000..78374eb99 --- /dev/null +++ b/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 + + diff --git a/Zettelkasten/Permanent Notes/20251223171835-moore-machines.md b/Zettelkasten/Permanent Notes/20251223171835-moore-machines.md new file mode 100644 index 000000000..f1cdbaf75 --- /dev/null +++ b/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.