ltlfsynt
Table of Contents
Reactive synthesis is the problem of synthesizing a controller that produces output signals based on a history of input signals, under the constraint of some specification that relates the input and output signals over time.
ltlfsynt
solves this problem when the specification is an LTLf
formula (i.e., LTL interpreted over finite traces). It can either
decide realizability (i.e., decide if a controller satisfying the
formula exist) or synthesize a reactive controller as an And-Inverter
Graph (AIG).
Consider a set \(I\) of input atomic propositions, a set \(O\) of output atomic propositions, and an LTLf formula φ over the propositions in \(I \cup O\). This tool can build controllers using two different semantics:
- Mealy controller
- A Mealy controller is a function \(c: (2^{I})^+\to 2^O\). A Mealy controller realizes \(\varphi\) if for any ω-word \((u_i)_{i \in \mathbb{N}} \in (2^I)^\omega\) over the input propositions, there exists some position \(k>0\) such that the (nonempty) word \((u_i \cup c(u_0 \dots u_{i-1}, u_i))_{0 \le i \le k}\in (2^{I\cup O})^k\) satisfies φ.
- Moore controller
- A Moore controller is a function \(c: (2^{I})^*\to 2^O\). A Moore controller realizes \(\varphi\) if for any ω-word \((u_i)_{i \in \mathbb{N}} \in (2^I)^\omega\) over the input propositions, there exists some position \(k>0\) such that the (nonempty) word \((u_i \cup c(u_0 \dots u_{i-1}))_{0 \le i \le k}\in (2^{I\cup O})^k\) satisfies φ.
In other words, a Mealy controller should decide the outputs for the current instant based on the history of all inputs as well as the current inputs. A Moore controller should decide outputs without knowing the current inputs, it only knows about past inputs. In either semantics, the controller should ensure that φ is satisfied after a finite number of steps. Once φ has been satisfied, the output of the controller is unconstrained.
Example
Here is an example LTLf specification generated by genltl
:
f=`genltl --tv-counter-mealy=2` echo "$f" | sed 's/(*G/\n&/g'
(init0 <-> ob0) & (init1 <-> ob1) & G(inc <-> oc0) & G((X[!]ob0 -> (ob0 xor oc0)) & (X[!]!ob0 -> (ob0 <-> oc0))) & G(oc1 <-> (ob0 & oc0)) & G((X[!]ob1 -> (ob1 xor oc1)) & (X[!]!ob1 -> (ob1 <-> oc1))) & (G(!inc -> X[!]inc) -> F(!ob0 & !ob1))
Output variables ob0
and ob1
encode a 2-bit counter. Input
variables init0
and init1
specify the initial value of this
counter, as encoded on the first line.
When the input variable inc
is set, the counter should be
incremented by one on the next step. This is encoded on the next four
lines, by using to extra output variables to represent carries
(oc0
and oc1
), and ensuring that, if a next step exist, the next
value of the counter (X[!]ob0
and X[!]ob1
) will be set according
to its current value and to that of the carries.
X[!]
is Spot's notation for the strong next operator of LTLf. The
weak next is simply noted X
. Since we are working with finite
words, a strong next ensure that the current instant is not the last
one. A weak next is always satisfied on the last instant.
The last implication is something we would like to confirm under the
above rules, and regardless of the initial value of the counter.
Assuming the input variable inc
is raised at least every other step
(G(!inc -> X[!]inc)
), we claim that the counter will eventually wrap
back to zero F(!ob0 & !ob1)
.
We show that the answer is positive by passing this formula to
ltlfsynt
. (Notice that in this formula, input and output variables
start with i
and o
respectively, so ltlfsynt
can tell them apart
automatically.)
ltlfsynt --semantic=Mealy -f "$f" --realizability
REALIZABLE
This specification is realizable.
Without the --realizability
switch, ltlfsynt
will additionally
print a Mealy machine representing the controller, in the HOA format.
ltlfsynt --semantic=Mealy -f "$f"
REALIZABLE HOA: v1 States: 5 Start: 0 AP: 7 "init0" "init1" "inc" "ob0" "ob1" "oc1" "oc0" acc-name: all Acceptance: 0 t properties: trans-labels explicit-labels state-acc deterministic controllable-AP: 3 4 5 6 --BODY-- State: 0 [!0&!1&!2&!3&!4&!5&!6 | !0&!1&2&!3&!4&!5&6 | !0&1&!2&!3&4&!5&!6 | 0&!1&!2&3&!4&!5&!6 | 0&1&!2&3&4&!5&!6] 1 [!0&1&2&!3&4&!5&6] 2 [0&!1&2&3&!4&5&6] 3 [0&1&2&3&4&5&6] 4 State: 1 [!2&!6 | 2&6] 1 State: 2 [!2&3&4&!5&!6] 1 [2&3&4&5&6] 4 State: 3 [!2&!3&4&!5&!6] 1 [2&!3&4&!5&6] 2 State: 4 [!2&!3&!4&!5&!6 | 2&!3&!4&!5&6] 1 --END--
We can hide the REALIZABLE
line with --hide
, and print the Mealy
machine in GraphViz's format as follows:
ltlfsynt --semantic=Mealy -f "$f" --hide --dot=strategy
Remember that unlike ltlsynt
, we are working with finite semantics
here. The controller will read a sequence of input assignments of
infinite size, but that sequence should have at least one position
such that the combination of inputs and outputs up to that point
satisfy the specification. Once the specification has been satisfied,
the controller is free to output anything. This is why the values of
ob0
, ob1
, oc1
are not specified on the transition leaving the
rightmost state: that state is reached either when the counter wrapped
to zero, or when the input signal do not satisfy our assumption
(G(!inc -> X[!]inc)
), so at that point the specification has been
satisfied and the output variable can be chosen freely.
The reason we still force the value of oc0
to be equal to that of
inc
on the last state is because of an optimization in ltlfsynt
:
since the specification contains G(inc <-> oc0)
, the formula can be
simplified by replacing all occurrences of oc0
by inc
. ltlfsynt
does this to reduce the number of variables it has to deal with, and
only adds the oc0
variable back at the very end, before presenting
results.
The controller may be output as an And-Inverter-Graph in AIGER format
using the --aiger
option:
ltlfsynt --semantic=Mealy -f "$f" --aiger
REALIZABLE aag 59 3 3 4 53 2 4 6 8 83 10 109 12 119 25 35 45 6 14 10 13 16 9 14 18 9 13 20 2 18 22 3 16 24 21 23 26 8 14 28 19 27 30 4 29 32 5 14 34 31 33 36 6 16 38 6 18 40 2 38 42 3 36 44 41 43 46 10 12 48 8 13 50 9 47 52 49 51 54 11 13 56 8 54 58 9 11 60 57 59 62 6 61 64 7 53 66 63 65 68 11 12 70 9 68 72 57 71 74 6 73 76 65 75 78 4 77 80 5 67 82 79 81 84 6 26 86 9 54 88 27 87 90 6 89 92 4 90 94 5 84 96 93 95 98 4 84 100 5 90 102 99 101 104 2 103 106 3 97 108 105 107 110 4 38 112 5 36 114 111 113 116 2 115 118 43 117 i0 init0 i1 init1 i2 inc o0 ob0 o1 ob1 o2 oc1 o3 oc0
Here is a graphical representation of the And-Inverter Graph for this controller:
ltlfsynt --semantic=Mealy -f "$f" --hide --dot=aig
The input signals are shown at the bottom in blue triangles. The
output signals are shown at that top in red triangles. Three latches
(1-bit registers), represented with orange rectangles are used to
remember the state of the controller. Latches are all false
initially. The L*_out
nodes emit the current latch value, and the
L*_in
receive the value of the latch for the next step. All round
nodes correspond to binary AND gates. Black dots invert a signal.
Invoking ltlfsynt
The specification can be supplied in three ways:
- as an LTLf formula, supplied on the command-line:
-f formula
. - as an LTLf formula, stored in a file:
-F FILENAME
. - as a file in the TLSF v1.2 format:
--tlsf FILENAME
.
When receiving an LTLf formula with -f
or -F
, ltlfilt
needs to
know which atomic propositions are input or output. This can be
specified with options --ins
, --outs
, or with --part-file
. See
ltlfsynt's documentation of those options. Without any such option,
ltlfsynt
assumes that variables starting with i
are inputs, and
those starting with o
are output.
Similarly, the semantics also have to be specified using
--semantics=Mealy
(the default) or --semantics=Moore
. When
comparing ltlfsynt
to other tools, beware that they may have not
have the same semantics by default.
When the specification is passed as a TLSF file with the --tlsf
option, the syfco
tool is automatically invoked to transform the
specification into LTLf, to retrieve the lists of input/output
variables, and to obtain the semantics to use.
Fine-tuning
ltlfsynt
operates in several phases as follows:
- preprocess the specification
- translate the LTLf specification into two-player game
- solve the two-player game
- extract a winning strategy as a Mealy machine
- encode the Mealy machine in AIG
Steps 2 & 3 are optionally merged together.
Preprocessing
Various optimizations are enabled by default.
- Variables that always appear with the same polarity in the
specification can be changed into constants and removed from the
specification. This optimization can be disabled with
--polarity=no
. - Group of variables that are specified as equivalent can be replaced
by a unique variable of that group. This can be disabled with
--global-equivalence=no
. - The specification can be decomposed into multiple output-disjoint
specifications that can be solved independently. This decomposition
can be disabled with
--decompose=no
. - The formula is simplified with some cheap rewriting rules. This is
especially important when decomposition is used, because the
decomposition sometimes need to distribute subformulas to favor
decompositions. This can be disabled with
--simplify=no
.
Translation & Game solving
By default those two steps are combined and performed on-the-fly.
This gives the best results. ltlfilt
supports alternative
approaches. In all approaches, the DFA that is constructed is
represented using multi-terminal binary decision diagrams (MTBDD).
Off-line approaches
In these approaches, first a DFA is built, then it is interpreted
as a game and solved. The why the DFA is built is controlled by
the --translation
option:
--translation=full
: a full DFA is created for the input specification; this is a direct translation from LTLf to MTBDD-based DFA.--translation=compositional
: a full DFA is created for the input specification, but the translation is compositional. The specification will be split on top-level Boolean operators, then subformulas will be translated separately, and finally the resulting automata will be combined.--translation=restricted
builds a restricted version of the DFA in which accepting states are replaced by accepting sinks. This is a direct translation as well.
The restricted
translation is always faster than the full
translation. The compositional
translation is usually faster than
the full
translation as well (provided intermediate automata are
minimized). restricted
is usually better than compositional
on
meaningful specifications, and compositional
is often than
restricted
or specifications built from random combination
specifications.
The automaton that is built can be minimized. This is controlled with
the --minimize=yes
and --minimize=no
options. By default,
minimization is only turned on for --translation=compositional
,
because minimization is what makes the compositional translation fast.
For other approaches, minimization is not recommended, because solving
the unminimized automaton is faster than minimizing it.
The MTBDD-based DFA is interpreted as game that can be solved in two ways:
--backprop=nodes
: solve the game by backpropagation at the level of the MTBDD nodes. This is a linear algorithm.--backprop=states
: solve the game by backpropagation but at the level of the MTDFA states. This uses less memory, but the algorithm may require quadratic time.
On-the-fly approaches
The DFA can be built on-the-fly. Thiss build the equivalent of the "restricted" automaton from above and solve the game as it is constructed.
The order in which states are explored can be controlled with
--translation=dfs
or --translation=bfs
.
The DFS on-the-fly translation is the default. Compared to the BFS, it allows an extra optimization: when a state is backtracked, we know that all its successors have been explored, so if it has not been decided that the state was winning, we can mark it as losing (and this information can be backpropagated).
An extra optimization that is enabled by default in on-the-fly
approaches is one-step (un)realizability where the formula α
for the current step is rewritten into two formulas Boolean formulas
\(\alpha_r\) and \(\alpha_u\) such that if \(\alpha_r\) is realizable then
\(\alpha\) is realizable, and if \(\alpha_u\) is unrealizable, then
\(\alpha\) is unrealizable. There are some specifications where this
optimization is a huge help. Conversely, for some specifications
where this does not help, this is just an unnecessary overhead. You
may disable it with --one-step-preprocess=no
.
Realizability
Use the --realizability
to interrupt the process once the game has
been solved.