# ltlsynt

## 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)'

REALIZABLE
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
--BODY--
State: 0
[0&1&2] 0
[!0&!1 | !1&!2] 0
--END--


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 labeled 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'

UNREALIZABLE



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.

## TLSF

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 FILE can be synthesized using syfco and ltlsynt:

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


## Algorithm

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.