UP | HOME

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) &
oc0) &
(ob0 xor oc0)) & (X[!]!ob0 -> (ob0 <-> oc0))) &
(ob0 & oc0)) &
(ob1 xor oc1)) & (X[!]!ob1 -> (ob1 <-> oc1))) &
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 exists, 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 ensures 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 --semantics=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 --semantics=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 --semantics=Mealy -f "$f" --hide --dot=strategy

Sorry, your browser does not support SVG.

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 signals 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 --semantics=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 --semantics=Mealy -f "$f" --hide --dot=aig

Sorry, your browser does not support SVG.

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 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:

  1. Preprocess the specification.
  2. Translate the LTLf specification into two-player game.
  3. Solve the two-player game.
  4. Extract a winning strategy as a Mealy machine.
  5. Encode the Mealy machine in AIG.

Steps 2 & 3 are optionally merged together and performed on-the-fly.

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.

The easiest way to track what is going on with these options is to run ltlfsynt with the --verbose options.

ltlfsynt --semantics=Mealy -f "$f" --verbose --realizability

Here we see that the oc0 was replaced by inc (such replacement occur because of --global-equiv is enabled by default), that the formula could not be decomposed (--decompose=yes is the default), and the result of --simplify=yes (the default) is shown before starting the translation.

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 MTDFA (that Spot's name for MTBDD-encoded DFA) resulting from these translations, and that will be used directly as a reachability game, can be displayed with --dot=game. Here is the output for the full translation (the compositional translation would give the same output on this example). See this page if you need an introduction to MTDFAs. The MTDFA is interpreted as a game in which round node are player by the environment, diamond nodes are played by the controller, and the controller want to force the game to reach an accepting state.

ltlfsynt --trans=full --semantics=Mealy -f "$f" --hide --dot=game

Sorry, your browser does not support SVG.

For comparison, here is MTDFA output by the restricted translation. Note how all accepting states have been merged into the true BDD node, and the game have been simplified already.

ltlfsynt --trans=restrict --semantics=Mealy -f "$f" --hide --dot=game

Sorry, your browser does not support SVG.

In the above case, we are lucky that the result of this translation is already a strategy: each diamond node has exactly one child that is the false BDD node, so the strategy is to always take the other child. Generally, the result of the translation may not be a strategy; that will be computed in a second step.

The automaton that has been 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 a 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. This builds the equivalent of the "restricted" automaton from above and solves the game as it is constructed.

The order in which states are explored can be controlled with --translation=dfs or --translation=bfs.

The BFS on-the-fly translation is the default, because it had a very slight advantage over DFS in a benchmark we did.

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.

The option --dot=game still works with on-the-fly approaches, but in that case it can only display the strategy that results from creating the game and solving it on-the-fly. If this is combined with --realizability (discussed below), the strategy returned by the on-the-fly approach is simplified to true or false, so there is not much to see.

Realizability

Use the --realizability to interrupts the process once the game has been solved.

In addition to our test-suite, we have run ltlfsynt --realizability on benchmarks from the LTLf tracks of the Synthesis Competition, and ensured that all results where consistent between various configurations of ltlfsynt and with several other LTLf realizability tools.

In contrast, the generation of controllers in any form (HOA, AIG) has not yet been thoroughly tested and should be regarded as highly experimental.

AIG encoding

ltlfsynt shares its AIG encoder with ltlsynt, so see ltlsynt's –aiger option.