Auto sync: 2025-08-21 12:56:54 (4 files changed)

M  "Zettelkasten/Permanent Notes/20250818132022-temporal-logic.md"

M  "Zettelkasten/Permanent Notes/20250819103208-strix.md"

A  "Zettelkasten/Permanent Notes/20250821123741-syntcomp.md"

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

Zettelkasten/Permanent Notes/20250818132022-temporal-logic.md

@@ -3,7 +3,7 @@ id: 20250818132022
 title: Temporal Logic
 type: permanent
 created: 2025-08-18T17:20:22Z
-modified: 2025-08-18T20:49:51Z
+modified: 2025-08-21T16:42:25Z
 tags: []
 ---
 
@@ -58,3 +58,6 @@ states).
   - 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

Zettelkasten/Permanent Notes/20250819103208-strix.md

@@ -3,8 +3,29 @@ id: 20250819103208
 title: Strix
 type: permanent
 created: 2025-08-19T14:32:08Z
-modified: 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]]

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

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

@@ -1,9 +1,9 @@
 ---
 id: LIT-20250819112550
-title: Strix: Explicit Reactive Synthesis Strikes Back!
+title: Strix Explicit Reactive Synthesis Strikes Back!
 type: literature
 created: 2025-08-19T15:25:50Z
-modified: 2025-08-19T16:50:53Z
+modified: 2025-08-21T16:37:52Z
 citekey: meyerStrixExplicitReactive2018
 ---