Symbolic LTLf Synthesis

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 Jianwen Li∗ Rice University lijwen2748@gmail.com

∗Corresponding author

†Corresponding author

Moshe Y. Vardi

Rice University vardi@cs.rice.edu

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

⊤ 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 φ1Rφ2 ≡ ¬(¬φ1U¬φ2). Additionally, we define the abbreviations Fφ ≡ ⊤Uφ and Gφ ≡ ⊥Rφ. Standard boolean abbreviations, such as ∨ (or) and → (implies) are also used.

• ρ, i |= ⊤;
• ρ, i |= a iff a ∈ ρ[i];
• ρ, i ̸|= ⊥;
• ρ, i |= ¬φ iff ρ, i ̸|= φ;
• ρ, i |= Xφ, iff i + 1 < |ρ| and ρ, i + 1 |= φ;
• ρ, i |= φ1 ∧ φ2, iff ρ, i |= φ1 and ρ, i |= φ2;
• ρ, i |= φ1Uφ2, iff there exists j s.t. i ≤ j < |ρ| and ρ, j |= φ2, and for all k, i ≤ k < j, we have ρ, k |= φ1.

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 〈X, Y〉 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)).

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

Moreover, variables in X (Y) are called X- (Y-)variables.

2.2 DFAGames

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 × 2X → Q is the transition function such that ϱ(q, X) = δ(q, X ∪ Y ) and Y = ω(q);
• Q ⊆ S is the set of winning states;
• ω : 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.

3.1 DFAConstruction

SPOT [Duret-Lutz et al., 2016] is the state-of-the-art platform for conversion from LTL formulas to explicit Deterministic B¨uchi 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 folφ [Giacomo and Vardi, 2013]. Taking such a FOL formula folφ as input, MONA is able to generate the DFA for φ.

3.2 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 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′ chosen fromm atomic propositions. If v is an X-variable in φ, then v′ 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.

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

• Z is a set of ⌈log2 |S|⌉ new propositions such that every state s ∈ S corresponds to an interpretation Z ∈ 2Z ;
• X and Y are as defined for G;
• 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 ′ of the propositions of Z, such that if Z corresponds to a state s ∈ S then Z ′ corresponds to the state δ(s, X ∪ Y );

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.

• 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 .

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;
• ζ : 2Z × 2X → 2Z is the transition function such that ζ(Z, X) = η(X, Y, Z) and Y = τ (Z).
• τ is as defined above;

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:

Theorem1. If an LTLf formula φ is realizable with respect to 〈X , Y〉, 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 ∪ {Tail} where Tail 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 ∪{Tail} as the input and output variables of t(φ), respectively. Intuitively, the Tail 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 Tail being an output variable.

Theorem 2. φ is realizable with respect to 〈X , Y〉 if and only if t(φ) is realizable with respect to 〈X, Y ∪ {Tail}〉.

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 ) = s′ 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 s′ . 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 δ′ : 2Z × 2X × 2Y → S with ⌈log2 |S|⌉ 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 δ′ . (2) Decompose the MTBDD into a sequence of BDDs B = 〈B0, B1, ..., Bn-1〉, n = ⌈log2 |S|⌉, where each Bi, when evaluated on an interpretation (X ∪ Y ∪ Z), computes the i-th bit in the binary encoding of state δ′ (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 = 〈B0,B1, ...,Bn-1〉 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 = 〈Bt0 ,Bt1 , ...,Bti-1 ,Bti 〉 and W = 〈Bw0 ,Bw1 , ...,Bwi-1 ,Bwi 〉, 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 .

Our implementation uses the CUDD BDD library [Somenzi, 2016], where fundamental BDD operations are provided. In realizability checking, Bti+1 is constructed fromBwi 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 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 Section 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, widening 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 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 be applied to the construction of automata over infinite words, a key step in LTL synthesis.

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

Acknowledgments

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 Ciˆencia Sem Fronteiras program.