Dane Sabo
be553ababb
M "Zettelkasten/Permanent Notes/Literature Notes/LIT-20250819112550-strix-explicit-reactive-synthesis-strikes-back.md"
58 lines
1.5 KiB
Markdown
58 lines
1.5 KiB
Markdown
---
|
|
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?**
|