diff --git a/Zettelkasten/Permanent Notes/20250818132022-temporal-logic.md b/Zettelkasten/Permanent Notes/20250818132022-temporal-logic.md index b735b8f9b..59e8eb5b4 100644 --- a/Zettelkasten/Permanent Notes/20250818132022-temporal-logic.md +++ b/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 diff --git a/Zettelkasten/Permanent Notes/20250819103208-strix.md b/Zettelkasten/Permanent Notes/20250819103208-strix.md index 73197949a..1b12c5db0 100644 --- a/Zettelkasten/Permanent Notes/20250819103208-strix.md +++ b/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]] diff --git a/Zettelkasten/Permanent Notes/20250821123741-syntcomp.md b/Zettelkasten/Permanent Notes/20250821123741-syntcomp.md new file mode 100644 index 000000000..cee5683b8 --- /dev/null +++ b/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. diff --git a/Zettelkasten/Permanent Notes/Literature Notes/LIT-20250819112550-strix-explicit-reactive-synthesis-strikes-back.md b/Zettelkasten/Permanent Notes/Literature Notes/LIT-20250819112550-strix-explicit-reactive-synthesis-strikes-back.md index 049cbbcd6..937d6d8b9 100644 --- a/Zettelkasten/Permanent Notes/Literature Notes/LIT-20250819112550-strix-explicit-reactive-synthesis-strikes-back.md +++ b/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 ---