Dane Sabo
64f1617e9d
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"
32 lines
870 B
Markdown
32 lines
870 B
Markdown
---
|
|
id: 20250819103208
|
|
title: Strix
|
|
type: permanent
|
|
created: 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]]
|