Symbolic LTLf Synthesis
Shufang Zhu
East China Normal University

Lucas M. Tabajara
Rice University

arXiv:1705.08426v2 [cs.LO] 21 Sep 2017

Geguang Pu†
East China Normal University
Abstract
LTLf synthesis is the process of finding a strategy
that satisfies a linear temporal specification over finite traces. An existing solution to this problem relies on a reduction to a DFA game. In this paper, we
propose a symbolic framework for LTLf synthesis
based on this technique, by performing the computation over a representation of the DFA as a boolean
formula rather than as an explicit graph. This approach enables strategy generation by utilizing the
mechanism of boolean synthesis. We implement
this symbolic synthesis method in a tool called Syft,
and demonstrate by experiments on scalable benchmarks that the symbolic approach scales better than
the explicit one.

1

Introduction

The problem of synthesis from temporal specifications can be
used to model a number of different problems in AI, in particular planning. Linear Temporal Logic, or LTL, is the standard
formalism to describe these specifications, but while LTL is
classically interpreted over infinite runs, many planning problems have a finite horizon, since they assume that execution
stops after a specific goal is achieved. This context leads to
the emergence of a version of LTL with alternative semantics
over finite traces, called LTLf . Some of the planning problems which can be reduced to LTLf synthesis include several
variants of conditional planning with full observability [Bacchus and Kabanza, 2000; Gerevini et al., 2009]. A general
survey of applications of LTLf in AI and CS can be found
in [Giacomo and Vardi, 2013].
LTL synthesis in infinite-horizon settings has been well investigated in theory since [Pnueli and Rosner, 1989], but the
lack of good algorithms for the crucial step of automata determinization is prohibitive for finding practical implementations [Fogarty et al., 2013]. In addition, usual approaches rely
on parity games [Thomas, 1995], for which no polynomialtime algorithm is known. In contrast, in the finite-horizon
setting the specification can be represented by a finite-state
∗
†

Corresponding author
Corresponding author

Jianwen Li∗
East China Normal University
& Rice University
Moshe Y. Vardi
Rice University

automaton, for which determinization is practically feasible [Tabakov et al., 2012] and the corresponding game can be
solved in polynomial time on the number of states and transitions of the deterministic automaton. This opens the possibility for theoretical solutions to be implemented effectively.
A solution to the LTLf synthesis problem was first proposed in [De Giacomo and Vardi, 2015], based on DFA
games. Following this method, an LTLf specification can be
transformed into a DFA with alphabet comprised of propositional interpretations of the variables in the formula. A winning strategy for the game defined by this DFA is then guaranteed to realize the temporal specification.
In this paper, we present the first practical implementation
of this theoretical framework for LTLf synthesis, in the form
of a tool called Syft. Syft follows a symbolic approach based
on an encoding of the DFA using boolean formulas, represented as Binary Decision Diagrams (BDDs), rather than an
explicit representation through the state graph. We base the
choice of a symbolic approach in experiments on DFA construction from an LTLf specification. We compared between
two methods for DFA construction: one symbolic using the
tool MONA [Henriksen et al., 1995], receiving as input a
translation of the LTLf specification to first-order logic, and
one explicit using SPOT [Duret-Lutz et al., 2016]. Although
both methods display limited scalability, the results show that
the symbolic construction scales significantly better.
Using a symbolic approach allows us to leverage techniques for boolean synthesis [Fried et al., 2016] in order to
compute the winning strategy. Our synthesis framework employs a fixpoint computation to construct a formula that expresses the choices of outputs in each state that move the
game towards an accepting state. By giving this formula as
input to a boolean synthesis procedure we can obtain a winning strategy whenever one exists.
Further experiments comparing the performance of the Syft
tool with an explicit implementation E-Syft again display better scalability for the symbolic approach. Furthermore, a
comparison with a standard LTL synthesis tool confirms that
restricting the problem to finite traces allows for more efficient techniques to be used. Finally, the results show DFA
construction to be the limiting factor in the synthesis process.

2

Preliminaries

2.1

LTLf

Basics

Linear Temporal Logic (LTL) over finite traces, i.e. LTLf ,
has the same syntax as LTL over infinite traces introduced in
[Pnueli, 1977]. Given a set of propositions P , the syntax of
LTLf formulas is defined as follows:
φ ::= > | ⊥ | a | ¬φ | φ1 ∧ φ2 | Xφ | φ1 U φ2

> and ⊥ represent true and false respectively. a ∈ P is
an atom, and we define a literal l to be an atom or the negation of an atom. X (Next) and U (Until) are temporal operators. We also introduce their dual operators, namely Xw
(Weak Next) and R (Release), defined as Xw φ ≡ ¬X¬φ and
φ1 Rφ2 ≡ ¬(¬φ1 U ¬φ2 ). Additionally, we define the abbreviations F φ ≡ >U φ and Gφ ≡ ⊥Rφ. Standard boolean
abbreviations, such as ∨ (or) and → (implies) are also used.
A trace ρ = ρ[0], ρ[1], . . . is a sequence of propositional
interpretations (sets), in which ρ[m] ∈ 2P (m ≥ 0) is the
m-th interpretation of ρ, and |ρ| represents the length of ρ.
Intuitively, ρ[m] is interpreted as the set of propositions which
are true at instant m. Trace ρ is an infinite trace if |ρ| =
∞, which is formally denoted as ρ ∈ (2P )ω ; otherwise ρ
is a finite trace, denoted as ρ ∈ (2P )∗ . LTLf formulas are
interpreted over finite traces. Given a finite trace ρ and an
LTLf formula φ, we inductively define when φ is true for ρ
at step i (0 ≤ i < |ρ|), written ρ, i |= φ, as follows:
• ρ, i |= >;
• ρ, i 6|= ⊥;

• ρ, i |= a iff a ∈ ρ[i];

• ρ, i |= ¬φ iff ρ, i 6|= φ;

• ρ, i |= φ1 ∧ φ2 , iff ρ, i |= φ1 and ρ, i |= φ2 ;

• ρ, i |= Xφ, iff i + 1 < |ρ| and ρ, i + 1 |= φ;

• ρ, i |= φ1 U φ2 , iff there exists j s.t. i ≤ j < |ρ| and
ρ, j |= φ2 , and for all k, i ≤ k < j, we have ρ, k |= φ1 .

An LTLf formula φ is true in ρ, denoted by ρ |= φ, if and
only if ρ, 0 |= φ. We next define the LTLf synthesis problem.

Definition 1 (LTLf Synthesis). Let φ be an LTLf formula and
X , Y be two disjoint atom sets such that X ∪ Y = P . X is the
set of input variables and Y is the set of output variables. φ is
realizable with respect to hX , Yi if there exists a strategy g :
(2X )∗ → 2Y , such that for an arbitrary infinite sequence λ =
X0 , X1 , . . . ∈ (2X )ω of propositional interpretations over X ,
we can find k ≥ 0 such that φ is true in the finite trace ρ =
(X0 ∪g()), (X1 ∪g(X0 )), . . . , (Xk ∪g(X0 , X1 , . . . , Xk−1 )).
Moreover, variables in X (Y) are called X- (Y-)variables.

2.2

DFA Games

The traditional way of performing LTLf synthesis is by a
reduction to corresponding Deterministic Finite Automaton
(DFA) games. According to [De Giacomo and Vardi, 2015],
every LTLf formula can be translated in 2EXPTIME to a DFA
which accepts the same language as the formula.
Let the DFA G be (2X ∪Y , S, s0 , δ, F ), where 2X ∪Y is
the alphabet, S is the set of states, s0 is the initial state,
δ : S × 2X ∪Y → S is the transition function, and F is the set

of accepting states. A game on G consists of two players, the
controller and the environment. X is the set of uncontrollable
propositions, which are under the control of the environment,
and Y is the set of controllable propositions, which are under
the control of the controller. The DFA game problem is to
check the existence of winning strategy for the controller and
generate it if exists. A strategy for the controller is a function g : (2X )∗ → 2Y , deciding the values of the controllable
variables for every possible history of the uncontrollable variables. To define a winning strategy for the controller, we use
the definition of winning state below.
Definition 2 (Winning State). Given a DFA G =
(2X ∪Y , S, s0 , δ, F ), s ∈ S is a winning state if s ∈ F is
an accepting state, or there exists Y ∈ 2Y such that, for every X ∈ 2X , δ(s, X ∪ Y ) is a winning state. Such Y is the
winning output of winning state s.
A strategy g is a winning strategy if, given an infinite
sequence λ = X0 , X1 , X2 , . . . ∈ (2X )ω , there is a finite trace ρ = (X0 ∪ g()), (X1 ∪ g(X0 )), . . . , (Xk ∪
g(X0 , X1 , . . . , Xk−1 )) that ends at an accepting state. If the
initial state s0 is a wining state, then a winning strategy exists. After obtaining a DFA from the LTLf specification, we
can utilize the solution to the DFA game for LTLf synthesis.
Formally, the winning strategy can be represented as a deterministic finite transducer, defined as below.
Definition 3 (Deterministic Finite Transducer). Given a DFA
G = (2X ∪Y , S, s0 , δ, F ), a deterministic finite transducer
T = (2X , 2Y , Q, s0 , %, ω, F ) is defined as follows:
• Q ⊆ S is the set of winning states;
• % : Q × 2X → Q is the transition function such that
%(q, X) = δ(q, X ∪ Y ) and Y = ω(q);
• ω : Q → 2Y is the output function such that ω(q) is a
winning output of q.

2.3

Boolean Synthesis

In this paper, we utilize the boolean synthesis technique proposed in [Fried et al., 2016]. The formal definition of the
boolean synthesis problem is as follows.
Definition 4 (Boolean Synthesis [Fried et al., 2016]). Given
two disjoint atom sets X , Y of input and output variables,
respectively, and a boolean formula ξ over X ∪Y, the boolean
synthesis problem is to construct a function γ : 2X → 2Y
such that, for all X ∈ 2X , if there exists Y ∈ 2Y such that
X ∪ Y |= ξ, then X ∪ γ(X) |= ξ. The function γ is called
the implementation function.
We treat boolean synthesis as a black box, using the implementation function construction in the LTLf synthesis to
obtain the output function of the transducer. For more details
on techniques and algorithms for boolean synthesis we refer
to [Fried et al., 2016].

3

Translation from LTLf Formulas to DFA

Following [De Giacomo and Vardi, 2015], in order to use
DFA games to solve the synthesis problem, we need to first
convert the LTLf specification to a DFA. This section focuses
on DFA construction. Given an LTLf formula φ, the corresponding DFA can be constructed explicitly or symbolically.

DFA Construction

3.2

350
300
250
200
150
100
50
0

1

2

3

4

5

6

Length of the formula

Figure 1: Comparison of scalability between SPOT and
MONA on the length of formulas
SPOT

MONA

220

Evaluations

It is unnecessary to compare the outputs of SPOT and MONA
in terms of size, since both tools return a minimized DFA.The
key point is to test them in scalability. LTL and LTLf have
the same syntax, so we construct our benchmarks from 20
basic cases, half of which are realizable, from the LTL literature [Jobstmann and Bloem, 2006]. Regarding the LTL
benchmarks, the semantics of LTL formulas is not, in general
preserved, when moving to the finite-trace setting.
Since these basic cases are too small to be used individually to evaluate the DFA construction tools, we use a class of
random conjunctions over basic cases [Daniele et al., 1999].
Note that real specifications typically consist of many temporal properties, whose conjunction ought to be realizable. Formally, a random
V conjunction formula RC(L) has the form:
RC(L) = 1≤i≤L Pi (v1 , v2 , ..., vk ), where L is the number of conjuncts, or the length of the formula, and Pi is a
randomly selected basic case (out of the 20 ones). Variables
v1 , v2 , ..., vk are chosen randomly from a set of m candidate
variables. Given L and m (the size of the candidate variable
set), we generate a formula RC(L) in the following way: (1)
Randomly select L basic cases; (2) For each case φ, substitute every variable v with a random new variable v 0 chosen
from m atomic propositions. If v is an X-variable in φ, then
v 0 is also an X-variable in RC(L). The same applies to the
Y-variables.
Each candidate variable may be chosen multiple times, so
the number of variables in the formula varies. We generate 50
random formulas for each configuration (L, m), adding up to
4500 instances in total. Formula lengths L range from 1 to
10, and m varies in increments of 50 from 100 to 500. The
platform used in the experiments is a computer cluster consisting of 2304 processor cores in 192 Westmere nodes (12
processor cores per node) at 2.83 GHz with 4GB of RAM per
core, and 6 Sandy Bridge nodes of 16 processor cores each,
running at 2.2 GHz with 8GB of RAM per core. Time out
was set to 120 seconds. Cases that cannot generate the DFA
within 120 seconds fail even if the time limit is extended, due
to running out of memory.

SPOT
MONA

400
Number of converted cases

SPOT [Duret-Lutz et al., 2016] is the state-of-the-art platform for conversion from LTL formulas to explicit Deterministic Büchi Automaton (DBA). The reduction rules from an
LTLf formula φ to an LTL formula φe are proposed in [Giacomo and Vardi, 2013], and are already implemented in
SPOT. Thus by giving an LTLf formula to SPOT, it returns
the DBA De for φe . De can be trimmed to a DFA that
recognizes the language of the LTLf formula φ. For more
details on this reduction, we refer to [Dutta et al., 2013;
Dutta and Vardi, 2014].
MONA [Henriksen et al., 1995] is a tool that translates
from the Weak Second-order Theory of One or Two successors (WS1S/WS2S) to symbolic DFA. First Order Logic
(FOL) on finite words, which is a fragment of WS1S, has the
same expressive power as LTLf , so an LTLf formula φ can be
translated to a corresponding FOL formula f olφ [Giacomo
and Vardi, 2013]. Taking such a FOL formula f olφ as input,
MONA is able to generate the DFA for φ.

450

Number of converted cases

3.1

200
180
160
140
120
100
80
100

150

200

250

300

350

400

450

500

Number of candidate variables

Figure 2: Comparison of scalability between SPOT and
MONA on the number of variables
Here we consider the number of successfully converted
cases for scalability evaluation. The results are summarized
in Figure 1 and 2, which present the scalability of SPOT
and MONA on L and m respectively. As L grows, MONA
demonstrates greater scalability, since SPOT cannot handle
cases for L > 4. We conjecture that the poor scalability on L
of SPOT is due to the bad handling of conjunctive goals. In
the comparison of scalability on m, MONA is able to solve
around twice as many cases than SPOT for each m. Given
these results, we adopt MONA for the DFA construction process and pursue a symbolic approach for LTLf synthesis.

4

Symbolic LTLf Synthesis

From an explicit automaton, the DFA game can be solved
following the approach described in [De Giacomo and Vardi,
2015], by searching the state graph to compute the set of winning states and choosing for each winning state a winning
output. The winning states and outputs can then be used to
construct a transducer that implements the winning strategy.
To solve a DFA game symbolically, we first use MONA
to construct a symbolic representation of the DFA. Then, we
perform a fixpoint computation over this symbolic representation to obtain a boolean formula encoding all winning states
of the DFA along with their corresponding winning outputs.
Finally, if the game is realizable, we can synthesize a winning
strategy from this formula with the help of a boolean synthe-

sis procedure. In the rest of this section we describe each of
these steps in more detail.
We start by defining the concept of symbolic automaton:
Definition 5 (Symbolic Automaton). Given a DFA G =
(2X ∪Y , S, s0 , δ, F ), the corresponding symbolic automaton
F = (X , Y, Z, Z0 , η, f ) is defined as follows:
• X and Y are as defined for G;
• Z is a set of dlog2 |S|e new propositions such that every
state s ∈ S corresponds to an interpretation Z ∈ 2Z ;
• Z0 ∈ 2Z is an interpretation of the propositions in Z
corresponding to the initial state s0 ;
• η : 2X × 2Y × 2Z → 2Z is a boolean function mapping
interpretations X, Y and Z of the propositions of X , Y
and Z to a new interpretation Z 0 of the propositions of
Z, such that if Z corresponds to a state s ∈ S then Z 0
corresponds to the state δ(s, X ∪ Y );
• f is a boolean formula over the propositions in Z, such
that f is satisfied by an interpretation Z iff Z corresponds to a final state s ∈ F .
Intuitively, the symbolic automaton represents states by
propositional interpretations, the transition function by a
boolean function and the set of final states by a boolean formula.
To solve the realizability problem over a symbolic automaton we compute a boolean formula w over Z that is satisfied exactly by those interpretations that correspond to winning states. The specification is realizable if and only if Z0
satisfies w. To solve the synthesis problem, we compute a
boolean function τ : 2Z → 2Y such that for any sequence
(X0 , Y0 , Z0 ), (X1 , Y1 , Z1 ), . . . that satisfies: (1) Z0 is the initial state; (2) For every i ≥ 0, Yi = τ (Zi ); (3) For every
i ≥ 0, Zi+1 = η(Xi , Yi , Zi ) there exists an i such that Zi
satisfies f . In other words, starting from the initial state, for
any sequence of uncontrollable variables, if the controllable
variables are computed by τ and the next state is computed
by η, the play eventually reaches an accepting state.

4.1

Realizability and Synthesis over Symbolic
Automata

We can compute w and τ through a fixpoint computation over
two boolean formulas: wi , over the set of propositions Z, and
ti , over Z ∪ Y. These formulas encode winning states and
winning outputs in the following way: every interpretation
Z ∈ 2Z such that Z |= wi corresponds to a winning state, and
every interpretation (Z, Y ) ∈ 2Z × 2Y such that (Z, Y ) |= ti
corresponds to a winning state together with a winning output
of that state. When we reach a fixpoint, wi should encode all
winning states and ti all pairs of winning states and winning
outputs.
In the procedure below, we compute the fixpoints of wi and
ti starting from w0 and t0 . We assume that we are able to perform basic Boolean operations over the formulas, as well as
substitution, quantification and testing for logical equivalence
of two formulas.
In the first step of the computation, we initialize
t0 (Z, Y ) = f (Z) and w0 (Z) = f (Z), since every accepting state is a winning state. Note that t0 is independent of the

propositions from Y, since once the play reaches an accepting state the game is over and we don’t care about the outputs anymore. Then we construct ti+1 and wi+1 as follows:
ti+1 (Z, Y ) = ti (Z, Y ) ∨ (¬wi (Z) ∧ ∀X.wi (η(X, Y, Z))),
wi+1 (Z) = ∃Y.ti+1 (Z, Y )
An interpretation (Z, Y ) ∈ 2Z × 2Y satisfies ti+1 if either: (Z, Y ) satisfies ti ; or Z was not yet identified as a winning state, and for every input X we can move from Z to an
already-identified winning state by setting the output to Y .
Note that it is important in the second case that Z has not yet
been identified as a winning state, because it guarantees that
the next transition will move closer to the accepting states.
Otherwise, it would be possible, for example, for ti+1 to accept an assignment to Y that moves from Z back to itself,
making the play stuck in a self loop.
From ti+1 , we can construct wi+1 by existentially quantifying the output variables. This means that wi+1 is satisfied
by all interpretations Z ∈ Z that satisfy ti+1 for some output, ignoring what the output is. The computation reaches a
fixpoint when wi+1 ≡ wi (≡ denoting logical equivalence).
At this point, no more states will be added, and so all winning
states have been found. By evaluating wi on Z0 we can know
if there exists a winning strategy. If that is the case, ti can be
used to compute this strategy. This can be done through the
mechanism of boolean synthesis.
By giving ti as the input formula to a boolean synthesis
procedure, and setting Z as the input variables and Y as the
output variables, we get back a function τ : 2Z → 2Y such
that (Z, τ (Z)) |= ti if and only if there exists Y ∈ 2Y such
that (Z, Y ) |= ti .
Using τ , we can define a symbolic transducer H corresponding to the winning strategy of the DFA game.
Definition 6 (Symbolic Transducer). Given a symbolic automaton F = (X , Y, Z, Z0 , η, f ) and a function τ : 2Z →
2Y , the symbolic transducer H = (X , Y, Z, Z0 , ζ, τ, f ) is as
follows:
• X , Y, Z, Z0 and f are as defined for F;
• τ is as defined above;

• ζ : 2Z × 2X → 2Z is the transition function such that
ζ(Z, X) = η(X, Y, Z) and Y = τ (Z).
Note that τ selects a single winning output for each winning state. Such a transducer is a solution to the DFA game,
and therefore to the LTLf synthesis problem.
The following theorem states the correctness of the entire
synthesis procedure:
Theorem 1. If an LTLf formula φ is realizable with respect to
hX , Yi, the symbolic transducer H corresponds to a winning
strategy for φ.
Proof. The translation from LTLf to FOL is correct from [Giacomo and Vardi, 2013]. Correctness of the construction of
the symbolic DFA from the FOL formula follows from the
correctness of MONA [Henriksen et al., 1995]. The winning
state computation is correct due to being an implementation
of the algorithm in [De Giacomo and Vardi, 2015]. The synthesis of τ is correct from the definition of boolean synthesis.

4.2

LTLf

Synthesis via LTL Synthesis

An alternative procedure to LTLf synthesis can be obtained
by a reduction to LTL synthesis. This reduction allows tools
for general LTL synthesis to be used in solving the LTLf synthesis problem. The reduction works as follows. 1) Given an
LTLf formula φ over propositions P , there is an LTL formula
t(φ) over propositions P ∪ {T ail} where T ail is a new variable, and φ is satisfiable iff t(φ) is satisfiable (see [Giacomo
and Vardi, 2013; Li et al., 2014]). 2) If P = X ∪ Y, and X
and Y are the set of input and output variables of φ, respectively, set X and Y ∪ {T ail} as the input and output variables
of t(φ), respectively. Intuitively, the T ail variable is an output variable that indicates when the finite trace should end.
As such, when the LTLf property is satisfied, the controller
can set this variable to true. The result of solving the LTL
synthesis problem for t(φ) corresponds to solving the LTLf
synthesis problem for φ. The correctness of the reduction
is guaranteed by the following theorem, which follows from
the construction in [Giacomo and Vardi, 2013] together with
T ail being an output variable.
Theorem 2. φ is realizable with respect to hX , Yi if and only
if t(φ) is realizable with respect to hX , Y ∪ {T ail}i.
In Section 6, we use this reduction to compare our LTLf
synthesis implementation with tools for standard LTL synthesis over infinite traces.

5

Implementation

We implemented the symbolic synthesis procedure described
in Section 4 in a tool called Syft, using Binary Decision Diagrams (BDDs) to represent the boolean formulas. For comparison, we also implemented the explicit version in a tool
called E-Syft. Both were implemented in C++11, and Syft
uses CUDD-3.0.0 as the BDD library.
Each tool consists of two parts: DFA construction and the
synthesis procedure. Based on the evaluations of the performance of DFA construction in Section 3, we adopt MONA
to construct the DFA to be given as input to the synthesis
procedure. The DFA is given by MONA as a Shared Multiterminal BDD (ShMTBDD) [Bryant, 1992; Morten et al.,
1996], which represents the function δ : S × 2X ∪Y → S.
A ShMTBDD is a binary decision diagram with |S| roots and
m terminal nodes (m ≤ |S|) representing states in the automaton. Formally speaking, δ(s, X ∪ Y ) = s0 is a transition
in the DFA if and only if starting from the root representing
state s and evaluating the interpretation X ∪ Y leads to the
terminal representing state s0 . To evaluate an interpretation
X ∪ Y on a ShMTBDD, take the high branch in every node
labeled by a variable v ∈ X ∪ Y and the low branch otherwise. We next describe how we preprocess the DFA given by
MONA.

5.1

Preprocessing the DFA of MONA

From ShMTBDD to Explicit DFA. Each root in an
ShMTBDD corresponds to an explicit state in the DFA.
Moreover, a root of the ShMTBDD includes the information
about if the state is initial or accepting, thus enabling s0 and
F to be easily extracted for the explicit DFA. To construct the

transition function, we enumerate all paths in the ShMTBDD,
each path from s (root) to t (terminal node) corresponding to
one transition from state s to t in the DFA. Note that the size
of the explicit DFA may be exponential on the size of the
ShMTBDD.
From ShMTBDD to BDD. Following Section 4, we can
construct a symbolic automaton in which the transition function η is in form of a (multi-rooted) BDD that describes a
boolean function η : 2X × 2Y × 2Z → 2Z . Thus we need to
first generate the BDD for the given ShMTBDD.
The basic idea is as follows: (1) From the ShMTBDD
of δ, construct a Multi-Terminal BDD (MTBDD) for δ 0 :
2Z × 2X × 2Y → S with dlog2 |S|e new boolean variables
encoding the states, where every path through the state variables, representing an interpretation Zs , leads to the node under the root s in the ShMTBDD. Then, for each transition in δ,
there exists an equivalent transition in δ 0 . (2) Decompose the
MTBDD into a sequence of BDDs B = hB0 , B1 , ..., Bn−1 i,
n = dlog2 |S|e, where each Bi , when evaluated on an interpretation (X ∪ Y ∪ Z), computes the i-th bit in the binary
encoding of state δ 0 (X, Y, Z).
The idea of splitting the ShMTBDD into BDDs is illustrated on Figure 3. As shown in this example, bits b0 , b1
are used to denote the four states s0 , s1 , s2 , s3 . In step (1),
root s0 is substituted by Zs0 that corresponds to the formula (¬b0 ∧ ¬b1 ). After replacing all roots with corresponding interpretations, the MTBDD is produced. In step
(2), s0 , s1 , s2 , s3 can be represented by 00, 01, 10, 11 respectively, where b0 denotes the leftmost bit. Bit b0 for both s0
and s1 is 0. So by forcing all paths that proceed to terminals
s0 and s1 in the MTBDD to reach terminal node 0, and all
paths to terminals s2 and s3 to reach terminal node 1, BDD
B0 is generated. BDD B1 is constructed in an analogous way
for bit b1 .

5.2

Implementing the Synthesis Algorithms

Explicit Synthesis. Following [De Giacomo and Vardi,
2015], the main algorithm for explicit synthesis is as follows:
starting from accepting states in F , iteratively expand the set
of winning states. For every state s that is not yet a winning
state, if we find an assignment Y such that for all assignments X of input variables, δ(s, X ∪ Y ) is a winning state,
then Y is set to be the winning output of the new winning
state s. All assignments of Y have to be enumerated in the
worst case. Fixpoint checking is accomplished by checking
that no new winning state was added during each iteration.
The transducer is generated according to Definition 3.
Symbolic Synthesis. The input here is a symbolic automaton F, in which the transition relation η is represented by a
sequence B = hB0 , B1 , ..., Bn−1 i of BDDs, where each Bi
corresponding to bit bi , and the formula f for the accepting
states, is represented by BDD Bf . We separate the DFA game
into two phases, realizability and strategy construction.
Following the theoretical framework in Section 4, from
the accepting states Bf , we construct two BDD sequences
T and W, such that T = hBt0 , Bt1 , ..., Bti−1 , Bti i and
W = hBw0 , Bw1 , ..., Bwi−1 , Bwi i, where Bti and Bwi are
the BDDs of the boolean formulas ti and wi respectively. The
fixpoint computation terminates as soon as Bwi+1 ≡ Bwi .

Symbolic

MTBDD

Explicit

200
180
Number of solved cases

b0
ShMTBDD
s0

x0

s1

s1

s3

s2

x1

x1

s2

⇒

s3

b0

x0

b1

x1

b1

+

s1

s2

s3

01

10

11

b1

x0

x1
1

0

BDD B0

x1
0

1
BDD B1

Figure 3: Transformation from ShMTBDD to BDD
Our implementation uses the CUDD BDD library [Somenzi, 2016], where fundamental BDD operations
are provided. In realizability checking, Bti+1 is constructed
from Bwi by first substituting each bit bi of the binary encoding of the state with the corresponding BDD Bi . The BDD
operation Compose is used for such substitution. CUDD also
provides the operations UnivAbstract and ExistAbstract for
universal and existential quantifier elimination respectively.
For fixpoint checking, we use canonicity of BDDs, which
reduces equivalence checking to constant-time BDD equality
comparison. To check realizability, the fixpoint BDD Bwi is
evaluated on interpretation Z0 of state variables, returning 1
if realizable.
Since veision 3.0.0, CUDD includes a built-in boolean synthesis method SolveEqn, which we can use to generate the
function τ . From τ , the symbolic transducer can be constructed according to Definition 6.

6

120
100

60

b1

x0

140

80

x1

b0

b1

⇒

b1

160

Experiments

The experiment was divided into two parts and resulted in two
major findings. First, we compared the symbolic approach
against the explicit method and showed that the symbolic approach is clearly superior to the explicit one. Second, we
evaluated our LTLf synthesis implementation against the reduction to LTL synthesis presented in Section 4.2, and again
show our approach to be more efficient.
We carried out experiments on the same platform as Sec-

1

2

3

4

5

6

7

8

9

10

Length of the formula

Figure 4: Comparison of scalability of Symbolic against Explicit on the length of formula
tion 3. For the synthesis experiments, besides the original 20
basic cases we also collected 80 instances from the LTL synthesis tool Acacia+ [Bohy et al., 2012], making 100 cases in
total. In this section, L denotes the length of the formulas and
N denotes the approximate number of variables. Due to the
construction rules of the formula, as described in Section 3,
each variable is chosen randomly and may be chosen multiple
times. Thus, the exact number of variables in a formula for a
given N varies in the range (N − 5, N + 5].

6.1

Symbolic vs Explicit

We aim to compare the results on two aspects: 1) the scalability of each approach; 2) the performance on each procedure
(automata construction/safety game) of LTLf synthesis.
Scalability on the length of formulas. We evaluated the
scalability of Syft and E-Syft on 2000 benchmarks where the
formula length L ranges from 1 to 10 and N = 20, as MONA
is more likely to succeed in constructing the DFA for this
value of N . Each L accounts for 200 of the 2000 benchmarks.
Figure 4 shows the number of cases the tools were able to
solve for each L. As can be seen, the symbolic method can
handle a larger number of cases than the explicit one, which
demonstrates that the symbolic method outperforms the explicit approach in scalability on the length of the formula.
Scalability on the number of variables. In this experiment,
we compared the scalability over the number of variables N ,
which varies from 10 to 60, where L is fixed as 5. As can be
seen in Figure 5, for smaller cases the two approaches behave
similarly, since they succeed in almost all cases. The same
happens for larger cases, because MONA cannot construct the
DFAs. For intermediate values the difference is more noticeable, showing better performance by the symbolic tool. The
number of cases that the explicit method can solve sharply declines when N = 30. However, the symbolic tool can handle
more than 40 variables. Both methods tend to fail for N > 50
at the DFA conversion stage.
Synthesis vs DFA Construction. In this experiment we
studied the effect of N on the time consumed by DFA construction and synthesis. The percentage of time consumed by
each is shown in Figure 6. We observe that for large cases,
DFA construction dominates the running time. As the size
of the DFA increases, DFA construction takes significantly
longer, while synthesis time increases more slowly, widen-

Symbolic

Explicit
Syft
Acacia+

200

200
Number of solved cases

Number of solved cases

180
160
140
120
100
80
60
40

150

100

50

20
0

10

20

30

40

50

0

60

1

Number of variables

Percentage of time consumed

80
70

50
40
30
20
10
10

20

30

40

50

60

Number of variables

Figure 6: Comparison of scalability of Symbolic against Explicit on the number of variables
ing the gap between the two. This result allows us to conclude that the critical performance limitation of synthesis is
the DFA construction process rather than synthesis itself.

6.2

Comparison with Standard LTL Synthesis

Here we adopted Acacia+ [Bohy et al., 2012], in which
LTL2BA [Gastin and Oddoux, 2001] is the automaton constructor, as the LTL synthesis tool and SPOT [Duret-Lutz et
al., 2016] as the translator to convert from LTLf formulas
to LTL formulas, as presented in Section 4.2. We evaluated
the effectiveness of each approach in terms of the number of
solved cases. Figure 7 shows the number of solved cases as
the length of the formula grows. As shown in the figure, Acacia+ is only able to solve a small fraction of the instances that
Syft can solve. The evidence here confirms that restricting the
problem to finite traces allows more efficient techniques to be
used for synthesis.

6.3

5

Figure 7: Comparison of scalability of Symbolic approach
against Acacia+ on the length of the formula

7

60

0

4

be applied to the construction of automata over infinite words,
a key step in LTL synthesis.

Synthesis process
DFA construction

90

3
Length of the formula

Figure 5: Comparison of scalability of Symbolic against Explicit on the number of variables
100

2

Discussion

The symbolic synthesis method scales better than the explicit
approach both on the length of LTLf formulas and the number
of variables. The performance of the symbolic method, however, relies critically on the DFA-construction process, making this the bottleneck of LTLf synthesis. Comparing with the
reduction from LTLf synthesis to LTL synthesis, the advantage of our approach is that the DFA construction can leverage
techniques developed for finite-state automata, which cannot

Conclusion

We presented here the first realization of a symbolic approach
for LTLf synthesis, based on the theoretical framework of
DFA games. Our experimental evaluation shows that these
techniques are far more efficient than a reduction to standard
LTL synthesis. Furthermore, our experiments on DFA construction and synthesis have shown that a symbolic approach
to this problem has advantages over an explicit one. In both
cases, however, the limiting factor for scalability was DFA
construction. When the DFA could be constructed, the symbolic procedure was able to synthesize almost all cases, but
for larger numbers of variables DFA construction is not able
to scale.
These observations suggest the need for more scalable
methods of symbolic DFA construction. A promising direction would also be to develop techniques for performing synthesis “on the fly” during the construction of the DFA, rather
than waiting for the entire automaton to be constructed before
initiating the synthesis procedure.
In [Giacomo and Vardi, 2013] an alternative formalism for
finite-horizon temporal specifications is presented in the form
of Linear Dynamic Logic over finite traces, or LDLf . LDLf is
strictly more expressive than LTLf , but is also expressible as a
DFA. Therefore, given a procedure to perform the conversion
from LDLf to DFA, our approach can be used in the same
way. This would allow synthesis to be performed over a larger
class of specifications.

8

Acknowledgment

Work supported in part by NSFC Projects No. 61572197
and No. 61632005, MOST NKTSP Project 2015BAG19B02,
STCSM Project No.16DZ1100600, project Shanghai Collaborative Innovation Center of Trustworthy Software for Internet of Things (ZF1213), NSF grants CCF-1319459 and IIS1527668, NSF Expeditions in Computing project “ExCAPE:
Expeditions in Computer Augmented Program Engineering”
and by the Brazilian agency CNPq through the Ciência Sem
Fronteiras program.

References
[Bacchus and Kabanza, 2000] Fahiem Bacchus and Froduald Kabanza. Using Temporal Logics to Express Search
Control Knowledge for Planning. Artif. Intell., 116(12):123–191, 2000.
[Bohy et al., 2012] Aaron Bohy, Véronique Bruyère, Emmanuel Filiot, Naiyong Jin, and Jean-François Raskin.
Acacia+, a Tool for LTL Synthesis. In CAV, 2012.
[Bryant, 1992] Randal E. Bryant. Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams. ACM
Comput. Surv., 24(3):293–318, 1992.
[Daniele et al., 1999] Marco Daniele, Fausto Giunchiglia,
and Moshe Y. Vardi. Improved Automata Generation for
Linear Temporal Logic. In CAV, 1999.
[De Giacomo and Vardi, 2015] Giuseppe De Giacomo and
Moshe Y. Vardi. Synthesis for LTL and LDL on Finite
Traces. In IJCAI, 2015.
[Duret-Lutz et al., 2016] Alexandre Duret-Lutz, Alexandre
Lewkowicz, Amaury Fauchille, Thibaud Michaud, Etienne Renault, and Laurent Xu. Spot 2.0 — A Framework
for LTL and ω-automata Manipulation. In ATVA, 2016.
[Dutta and Vardi, 2014] Sonali Dutta and Moshe Y. Vardi.
Assertion-based flow monitoring of SystemC models. In
MEMOCODE, pages 145–154, 2014.
[Dutta et al., 2013] Sonali Dutta, Moshe Y. Vardi, and Deian
Tabakov. CHIMP: A Tool for Assertion-Based Dynamic
Verification of SystemC Models. In the Second International Workshop on Design and Implementation of Formal
Tools and Systems, 2013.
[Fogarty et al., 2013] Seth Fogarty, Orna Kupferman,
Moshe Y. Vardi, and Thomas Wilke. Profile Trees for
Büchi Word Automata, with Application to Determinization. In GandALF, 2013.
[Fried et al., 2016] Dror Fried, Lucas M. Tabajara, and
Moshe Y. Vardi. BDD-Based Boolean Functional Synthesis. In CAV, 2016.
[Gastin and Oddoux, 2001] Paul Gastin and Denis Oddoux.
Fast LTL to Büchi Automata Translation. In CAV, 2001.
[Gerevini et al., 2009] Alfonso Gerevini, Patrik Haslum,
Derek Long, Alessandro Saetti, and Yannis Dimopoulos.
Deterministic planning in the fifth international planning
competition: PDDL3 and experimental evaluation of the
planners. Artif. Intell., 173(5-6):619–668, 2009.
[Giacomo and Vardi, 2013] Giuseppe De Giacomo and
Moshe Y. Vardi. Linear Temporal Logic and Linear
Dynamic Logic on Finite Traces. In IJCAI, 2013.
[Henriksen et al., 1995] Jesper G. Henriksen, Jakob L.
Jensen, Michael E. Jørgensen, Nils Klarlund, Robert
Paige, Theis Rauhe, and Anders Sandholm. Mona:
Monadic Second-order Logic in Practice. In TACAS, 1995.
[Jobstmann and Bloem, 2006] Barbara Jobstmann and Roderick Bloem. Optimizations for LTL synthesis. In FMCAD, 2006.

[Li et al., 2014] Jianwen Li, Lijun Zhang, Geguang Pu,
Moshe Y. Vardi, and Jifeng He. LTLf Satisfiability Checking. In ECAI, 2014.
[Morten et al., 1996] Biehl Morten, Klarlund Nils, and
Rauhe Theis. Mona: decidable arithmetic in practice
(demo). In FTRTFT, 1996.
[Pnueli and Rosner, 1989] Amir Pnueli and Roni Rosner. On
the Synthesis of a Reactive Module. In POPL, 1989.
[Pnueli, 1977] A. Pnueli. The temporal logic of programs.
pages 46–57, 1977.
[Somenzi, 2016] Fabio Somenzi. CUDD: CU Decision Diagram Package 3.0.0. Universiy of Colorado at Boulder.
2016.
[Tabakov et al., 2012] D. Tabakov, K.Y. Rozier, and M. Y.
Vardi. Optimized temporal monitors for SystemC. Formal
Methods in System Design, 41(3):236–268, 2012.
[Thomas, 1995] Wolfgang Thomas. On the Synthesis of
Strategies in Infinite Games. In STACS, 1995.

