Table of Contents

Basic usage

This tool synthesizes controllers from LTL/PSL formulas.

Consider a set \(I\) of input atomic propositions, a set \(O\) of output atomic propositions, and a PSL formula φ over the propositions in \(I \cup O\). A controller realizing φ is a function \(c: 2^{I \cup O} \times 2^I \mapsto 2^O\) such that, for every ω-word \((u_i)_{i \in N} \in (2^I)^\omega\) over the input propositions, the word \((u_i \cup c(u_0 \dots u_{i-1}, u_i))_{i \in N}\) satisfies φ.

ltlsynt has three mandatory options:

  • --ins: a comma-separated list of input atomic propositions;
  • --outs: a comma-separated list of output atomic propositions;
  • --formula or --file: a LTL/PSL specification.

The following example illustrates the synthesis of a controller acting as an AND gate. We have two inputs a and b and one output c, and we want c to always be the AND of the two inputs:

ltlsynt --ins=a,b --outs=c -f 'G (a & b <=> c)'
HOA: v1
States: 1
Start: 0
AP: 3 "b" "c" "a"
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc deterministic
State: 0
[0&1&2] 0
[!0&!1 | !1&!2] 0

The output is composed of two parts:

  • the first one is a single line REALIZABLE or UNREALIZABLE;
  • the second one is an automaton describing the controller (if the input specification is realizable). In this example, the controller has a single state, with two loops labelled by a & b & c and (!a | !b) & !c.

If a controller exists, then one with finite memory exists. Such controllers are easily represented as automata (or more specifically as I/O automata or transducers). In the automaton representing the controller, the acceptance condition is irrelevant and trivially true.

The following example illustrates the case of an unrealizable specification. As a is an input proposition, there is no way to guarantee that it will eventually hold.

ltlsynt --ins=a --outs=b -f 'F a'

By default, the controller is output in HOA format, but it can be output as an AIGER circuit thanks to the --aiger flag. This is the output format required for the SYNTCOMP competition.

The generation of a controller can be disabled with the flag --realizability. In this case, ltlsynt output is limited to REALIZABLE or UNREALIZABLE.


ltlsynt was made with the SYNTCOMP competition in mind, and more specifically the TLSF track of this competition. TLSF is a high-level specification language created for the purpose of this competition. Fortunately, the SYNTCOMP organizers also provide a tool called syfco which can translate a TLSF specification to an LTL formula.

The following four steps show you how a TLSF specification called spec.tlsf can be synthesized using syfco and ltlsynt:

LTL=$(syfco FILE -f ltlxba -m fully)
IN=$(syfco FILE -f ltlxba -m fully)
OUT=$(syfco FILE -f ltlxba -m fully)
ltlsynt --formula="$LTL" --ins="$IN" --outs="$OUT"


The tool reduces the synthesis problem to a parity game, and solves the parity game using Zielonka's recursive algorithm. The full reduction from LTL to parity game is described in the following paper:

  • Reactive Synthesis from LTL Specification with Spot, Thibaud Michaud, Maximilien Colange. In Proc. of SYNT@CAV'18. to appear.

You can also ask ltlsynt to print to obtained parity game into PGSolver format, with the flag --print-pg. Note that this flag deactivates the resolution of the parity game, which is to be deferred to one of the solvers from PGSolver.