Strix is a tool for reactive LTL synthesis combining a direct translation of LTL formulas into deterministic parity automata (DPA) and an efficient, multi-threaded explicit state solver for parity games. In brief, Strix (1) decomposes the given formula into simpler formulas, (2) translates these on-the-fly into DPAs based on the queries of the parity game solver, (3) composes the DPAs into a parity game, and at the same time already solves the intermediate games using strategy iteration, and (4) finally translates the wining strategy, if it exists, into a Mealy machine or an AIGER circuit with optional minimization. Strix has taken part in the synthesis competition SYNTCOMP since 2018 and taken first place in all LTL tracks each time, outperforming the tools ltlsynt, BoSy and Bowser.

It relies on Owl for the translation of LTL to deterministic automata.

Download and Installation

The latest release of Strix can be found on the GitHub releases for Strix. Both source releases and pre-compiled binaries for various systems are available.

Detailed build instructions can be found in BUILDING.md and usage instructions in USAGE.md. A description of the supported formats is contained in FORMATS.md. Older release can be found in the archive.

Awards

• First place in all LTL tracks of SYNTCOMP 2018:
  • Sequential Realizability
  • Parallel Realizability
  • Sequential Synthesis Quantity
  • Parallel Synthesis Quantity
  • Sequential Synthesis Quality
  • Parallel Synthesis Quality
• First place in all LTL tracks of SYNTCOMP 2019:
  • Sequential Realizability
  • Sequential Synthesis Quantity
  • Sequential Synthesis Quality
• First place in all LTL and Parity Game tracks of SYNTCOMP 2020:
  • Sequential LTL Realizability
  • Sequential LTL Synthesis Quantity
  • Sequential LTL Synthesis Quality
  • Sequential Parity Game Realizability
• First place in the following tracks of SYNTCOMP 2021:
  • Sequential LTL Realizability
  • Sequential LTL Synthesis
  • Parity Game Synthesis Quality

Contact

For feedback, comments and questions contact Philipp and Salomon.

Citing

If you want to cite Strix in an academic publication, please use the following references:

• Michael Luttenberger, Philipp J. Meyer, Salomon Sickert
  Practical Synthesis of Reactive Systems from LTL Specifications via Parity Games
  Acta Inf. (2019) : bibtex / view / preprint / submitted artifact

• Philipp J. Meyer, Salomon Sickert, Michael Luttenberger
  Strix: Explicit Reactive Synthesis Strikes Back!
  CAV (2018) : bibtex / view / preprint / slides

Acknowledgements

This project has received funding from the European Research Council (ERC) under the European Unions Horizon 2020 research and innovation programme under grant agreement No 787367 (PaVeS).