PV2 ⊧ Strixsynthesises a controller for an LTL formula

Tool for reactive LTL synthesis

Application domain/field

• Synthesis
• LTL synthesis
• Reactive synthesis
• Deterministic parity automata (DPA)
• Controller synthesis

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:

• Mealy/Moore machine (HOA format)
• AIGER circuit
• BDD (dot format with CUDD interpretation)
• Parity game (PGSolver format)

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