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

id: LIT-20250819112550 title: Strix: Explicit Reactive Synthesis Strikes Back! type: literature created: 2025-08-19T15:25:50Z modified: 2025-08-19T16:50:53Z 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?