PV2 Strixsynthesises a controller for an LTL formula

Tool for reactive LTL synthesis

Application domain/field

Type of tool

LTL synthesis tool

Expected input

LTL formula(s)

Format:

Owl format, see https://gitlab.lrz.de/i7/owl/blob/master/doc/FORMATS.md

Expected output

REALIZABLE or UNREALIZABLE. If realizable, then it also outputs a controller in one of the following formats:

Internals

Uses Speculoos, MeMin, ABC. Given an LTL formula, it synthesizes a controller. I.e. it tries to find a matching implementation, e.g. a Mealy machine, for an LTL formula. To achieve this, it takes the following steps:
  1. Decompose the given formula into simpler formulas
  2. Translate these formulas on-the-fly into DPAs based on the queries of the parity game solver
  3. Compose the DPAs into a parity game, and at the same time solve the intermediate games using strategy iteration
  4. Translate the winning strategy, if it exists, into a Mealy machine or an AIGER circuit
Automaton LTL Synthesis

Links

Related papers

Strix: Explicit Reactive Synthesis Strikes Back! (CAV '18)

Last publication date

18 July 2018

Related tools

Compared to in the CAV '18 paper: PARTY, BoSy, LTLSYNT

ProVerB specific



ProVerB is a part of SLEBoK. Last updated: February 2023.