# partitioning_techniques_in_ltlf_synthesis__da7ab209.pdf

Partitioning Techniques in LTLf Synthesis

Lucas Martinelli Tabajara and Moshe Y. Vardi Rice University lucasmt@rice.edu, vardi@cs.rice.edu

Decomposition is a general principle in computational thinking, aiming at decomposing a problem instance into easier subproblems. Indeed, decomposing a transition system into a partitioned transition relation was critical to scaling BDD-based model checking to large state spaces. Since then, it has become a standard technique for dealing with related problems, such as Boolean synthesis. More recently, partitioning has begun to be explored in the synthesis of reactive systems. LTLf synthesis, a finite-horizon version of reactive synthesis with applications in areas such as robotics, seems like a promising candidate for partitioning techniques. After all, the state of the art is based on a BDD-based symbolic algorithm similar to those from model checking, and partitioning could be a potential solution to the current bottleneck of this approach, which is the construction of the state space.

In this work, however, we expose fundamental limitations of partitioning that hinder its effective application to symbolic LTLf synthesis. We not only provide evidence for this fact through an extensive experimental evaluation, but also perform an indepth analysis to identify the reason for these results. We trace the issue to an overall increase in the size of the explored state space, caused by an inability of partitioning to fully exploit state-space minimization, which has a crucial effect on performance. We conclude that more specialized decomposition techniques are needed for LTLf synthesis which take into account the effects of minimization.

1 Introduction

Decomposing problems into smaller tasks and recombining them to find a solution is a fundamental tool of computational thinking. A notable example in formal verification is the idea of decomposing a transition system using a partitioned transition relation. In this approach, the system is represented by the product of individual components, and the transition relation of the entire system can be ex-

pressed by the set of individual transition relations. Partitioning was critical to scaling BDD-based model checking to large state spaces [Burch et al., 1991], by producing a more compact and efficient representation for the transition relation of the system. Thanks to the success in model checking, partitioning has become a standard technique in symbolic and BDD-based algorithms, and was applied also to related problems such as symbolic Boolean satisfiability [Pan and Vardi, 2005] and Boolean synthesis [John et al., 2015; Tabajara and Vardi, 2017]. A problem that might seem to be a promising candidate for partitioning techniques is that of LTLf synthesis [De Giacomo and Vardi, 2015], an adaptation to finitehorizon semantics of the classic problem of synthesizing reactive systems from specifications in Linear Temporal Logic (LTL), which has promising applications in areas such as robotics [He et al., 2017]. The current state of the art for LTLf synthesis is based on a reduction to a reachability game played on a deterministic finite automaton (DFA), which is solved using a BDD-based symbolic fixpoint algorithm [Zhu et al., 2017], similar to those that benefited from partitioning in model checking. Furthermore, the main limiting factor of current approaches is the construction of the DFA, which can often be very large and in the worst case doubly-exponential in the size of the formula [Kupferman and Vardi, 2001]. This problem is amplified by the fact that state-of-the-art techniques use an explicit construction of the automaton state space, only later encoding it symbolically. Partitioning would allow the DFA to be represented as a product of smaller component DFAs that can be constructed much more efficiently than a single monolithic DFA, thus eliminating the bottleneck of DFA construction. In fact, previous efforts have already been made to apply similar decomposition techniques to reactive synthesis frameworks. Decomposition has been used successfully in explicit-state (infinite-horizon) LTL synthesis by the tool STRIX [Meyer et al., 2018], which won the 2018 reactive synthesis competition (SYNTCOMP). Decomposition has also been employed in [Camacho et al., 2018], where LTLf synthesis is reduced to FOND planning, though their results show that even using decomposition the FOND-planning approach does not always perform more efficiently than the standard BDD-based algorithm. A natural question to ask, then, is how such techniques perform when integrated into the BDD-based

Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence (IJCAI-19)

symbolic algorithm. It would be natural to assume that partitioning could be applied to symbolic LTLf synthesis to reap similar improvements as the ones obtained in model checking and related problems. In this work, however, we expose fundamental limitations of partitioning that hinder its application in symbolic LTLf synthesis. An extensive experimental evaluation shows that, although decomposing the LTLf formula avoids an initial overhead during DFA construction, this comes at a significant expense for computing the game s winning strategy. We follow this evaluation with an in-depth analysis of the algorithm s execution that traces the issue to an overall increase in the size of the explored state space. We are able to attribute this increase to the partitioned representation being unable to fully exploit state-space minimization when constructing the DFA. Although at the initial phases of the fixpoint computation the partitioned transition relation is able to provide a compact representation that mitigates this issue, as the fixpoint computation progresses BDD sizes increase significantly in relation to the monolithic version. Our analysis indicates that this increase cannot be contained by simply using better heuristics for processing the partitioned transition relation. These results suggest that, while DFA minimization is expensive, it is crucial to the success of LTLf-synthesis algorithms. Therefore, for a decomposition strategy to be effective for this problem, it must interact well with minimization, a property that partitioning lacks. The conclusion that we draw is that, while partitioning is an effective technique for symbolic model checking and other related problems, LTLf synthesis may require a different way of thinking and perhaps more powerful decomposition approaches.

2 Preliminaries 2.1 LTL over Finite Traces (LTLf) The syntax of LTLf is identical to that of LTL over infinite traces. We define it over a set of propositions P as follows:

ϕ ::= | | p | ϕ | ϕ1 ϕ2 | ϕ1 ϕ2 | Xϕ | ϕ1Uϕ2

We also define in the usual way additional temporal operators Fϕ Uϕ and Gϕ F ϕ. LTLf differs from LTL in its semantics, being interpreted over finite rather than infinite traces. A (finite) trace of length m is a sequence ρ = ρ[0], ρ[1], . . . , ρ[m 1] (2P ) , where each ρ[i] is an interpretation or assignment of the propositions in P, represented by the subset of the propositions that are true in instant i. In contrast, an infinite trace is a sequence ρ = ρ[0], ρ[1], . . . (2P )ω of infinite length. The semantics of LTLf are defined inductively through a relation ρ, i |= ϕ, which denotes that finite trace ρ satisfies ϕ at instant i. See [De Giacomo and Vardi, 2013] for the formal definition of ρ, i |= ϕ. We say that a trace ρ satisfies formula ϕ, denoted by ρ |= ϕ, if ρ, 0 |= ϕ. Definition 1 (LTLf Synthesis). Let ϕ be an LTLf formula over set of propositions P = X Y, for disjoint sets X and Y. X is the set of input variables and Y is the set of output variables. ϕ is realizable if there exists a function γ : (2X ) 2Y from histories of input variables

to output variables such that, for every infinite sequence X0, X1, . . . (2X )ω, there is m 0 such that ρ = (X0, γ(X0)), (X1, γ(X0, X1)), . . . , (Xm, γ(X0, . . . , Xm)) satisfies ϕ. The problem of LTLf synthesis is, given ϕ, to decide if ϕ is realizable, and if so to construct such a γ.

The function γ works as a model of a system whose traces always satisfy ϕ. The output of the system in the current instant depends on the entire history of the inputs received so far. It is worth noting that in this work we consider that the system is able to take the current input into account when choosing an output, rather than only past inputs. This accounts for the slight difference in the definition of γ from [Zhu et al., 2017]. We choose this formulation first because it is more natural for specifying the benchmarks in Section 4, and second because in the symbolic algorithm (see Section 3) the order of quantifiers is more amenable to partitioning. Yet, our results will show that even using this formulation LTLf synthesis is not able to benefit from partitioning.

2.2 DFA Game An instance of LTLf synthesis can be solved by reduction to a game played over a Deterministic Finite Automaton (DFA). A DFA is a tuple A = (S, Σ, ι, , F), where:

S is the set of states of the automaton.

Σ is a finite alphabet.

ι S is the initial state.

S Σ S is the (deterministic) transition relation.

F S is the set of accepting states.

The run of a finite trace on a DFA A is the sequence of states visited by the trace when starting from the initial state. The fact that is deterministic guarantees that the run of a trace is unique. A run is accepting if the last state is in F. The language of A, denoted L(A), is the set of traces for which the corresponding run is accepting. The product of DFAs A1, . . . , Ak over the same alphabet Σ is the DFA A1 . . . Ak = (S1 . . . Sk, Σ, (ι1, . . . , ιk), , F1 . . . Fk), where ((s1, . . . , sk), σ, (s 1, . . . , s k)) if and only if (s1, σ, s 1) i for all i. It is not hard to see that L(A1 . . . Ak) = L(A1) . . . L(Ak). Every LTLf formula ϕ can be translated into a DFA A over alphabet Σ = 2P such that ρ L(A) if and only if ρ |= ϕ [De Giacomo and Vardi, 2015]. A DFA game is a reachability game played using a DFA as the arena. The two players of the game represent the system and the environment. The game starts at the initial state of the DFA, and at every round the environment chooses an assignment to the X variables, while the system chooses an assignment to the Y variables. The combined assignment determines the state the game moves to. The system wins the game if it eventually reaches an accepting state of the DFA. We say that a state is a winning state if from that state the system can always make choices that will cause the game to reach an accepting state. A strategy for the system is represented by a transducer (specifically, a Mealy machine) T = (Q, 2X , 2Y, τ, ν) with

Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence (IJCAI-19)

state space Q, input and output alphabets 2X and 2Y, initial state τ and transition function ν : Q 2X 2Y Q. The state of the transducer stores information about the history of the game so far, with the transition function serving to choose what output to produce and how to update its state. A strategy is winning for the system if, starting from the initial state of the DFA, a system that follows the strategy wins regardless of the choices of the environment. A winning strategy for the DFA game implicitly defines a solution to the LTLf synthesis problem for the original formula ϕ [Zhu et al., 2017].

3 Partitioned LTLf Synthesis Integrating partitioning into LTLf synthesis requires having a way to construct a partitioned transition relation from an LTLf formula. This construction should also be more efficient than constructing the monolithic DFA. The fact that most specifications take the form of a conjunction of constraints gives a natural way to decompose the formula: translate each conjunct individually into a DFA, then take the transition relation of all DFAs together as a partitioned transition relation for their product. This approach, which we detail below, follows the same general idea employed for decomposing specifications in [Camacho et al., 2018] and [Meyer et al., 2018].

3.1 DFA of a Conjunctive Formula Let ϕ = ϕ1 . . . ϕk be an LTLf formula over input variables X and output variables Y. ϕ can be translated into a DFA A = (S, 2X Y, ι, , F) that accepts the language of traces that satisfy ϕ. We call this a monolithic DFA for ϕ. This is the DFA that is originally used in [Zhu et al., 2017]. Alternatively, each conjunct ϕi can be individually translated to a DFA Ai = (Si, 2X Y, ιi, i, Fi) that accepts the language of traces that satisfy ϕi. Although ϕi might depend on only a subset of the variables, for simplicity we interpret it as a formula over X Y. Under this interpretation, L(A) = L(A1) . . . L(Ak) = L(A1 . . . Ak). Therefore, A1 . . . Ak is also a DFA for ϕ. We call this a partitioned DFA for ϕ. Rather than explicitly computing the product state space S1 . . . Sk, a partitioned DFA can be represented simply by its individual components A1, . . . , Ak. In order to apply partitioned techniques, each component DFA Ai must be encoded symbolically. This can be done using the same symbolic DFA encoding of [Zhu et al., 2017]: The state space Si is encoded as a set of state variables Zi such that |Zi| = log2(|Si|). We create a copy z i of each variable zi Zi to use as a next-state variable, and denote this set by Z i. The initial state ιi is represented by an assignment Ii 2Zi of the state variables. The transition relation i is represented by a boolean formula δi over Zi, X, Y and Z i. The set of accepting states Fi is represented by a boolean formula fi over Zi. A symbolic representation of the product DFA can then be obtained from the representation of the individual components, by taking Z = Sk i=1 Zi, Z = Sk i=1 Z i, I =

I1 . . . Ik, δ = δ1 . . . δk and f = f1 . . . fk. As in [Zhu et al., 2017], BDDs can be used to represent the boolean formulas. In the case of a partitioned DFA, however, rather than constructing a single BDD for the conjunctions δ and f, it is possible to instead construct one BDD for each individual component δi and fi, which can be expected to be much smaller. Next, we describe how to adapt the symbolic algorithm of [Zhu et al., 2017] to a partitioned representation.

3.2 Solving a DFA Game over a Partitioned DFA The algorithm of [Zhu et al., 2017] is based on a least fixpoint that expands at every iteration an under-approximation of the set W of winning states (for the system) of the DFA for ϕ. The initial under-approximation, W0, is simply the set of accepting states. After that, every iteration expands Wj into a larger under-approximation Wj+1, until no more states can be added. At this point, we know that the current set is the entire set of winning states, and the system can win the game if and only if the initial state is in the set. It is also possible to stop as soon as the initial state is added to the set, since at this point we already know that the system can win from the initial state. When using a partitioned DFA as described in Section 3.1, Wi can be defined recursively as follows:

W0 = F1 . . . Fk Wj+1 = Wj {(s1, . . . , sk) S1 . . . Sk |

X 2X . Y 2Y. s 1, . . . , s k.

i=1 ((si, X, Y, s i) i) (s 1, . . . , s k) Wj}

Note that every iteration adds to Wj+1 those states of the form (s1, . . . , sk) from which, for every input X, the system can choose an output Y that moves the game into a state in Wj (which is already known to be winning). When Wj+1 = Wj, we know that no more winning states exist. Just as the DFA is represented symbolically, so can the sets W0, W1, . . ., as formulas w0, w1, . . . over the state variables Z. The fixpoint algorithm above can then be implemented symbolically as follows, where for a formula α and a variable set V {Z, X, Y, Z } the notation α(V) defines formula α over the variables in V:

w0(Z) = f1(Z) . . . fk(Z)

wj+1(Z) = wj(Z) X. Y. Z .

i=1 δi(Z, X, Y, Z ) wj(Z )

As mentioned in Section 3.1, each fi and δi can be represented as a BDD, and similarly for wj. BDDs implement all the common boolean operations used in the computation, such as , , universal and existential quantification, and variable substitution. Furthermore, they are canonical representations of boolean functions, allowing logical equivalence to be performed in constant time. This is useful to perform the test wj+1 wj of whether the fixpoint has been reached. To compute the intermediate BDD for the formula Y. Z . Vk i=1 δi(Z, X, Y, Z ) wj(Z ), the straightforward option would be to simply take the conjunction of all the

Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence (IJCAI-19)

individual BDDs of each δi and wj, and then existentially quantify the Y and Z variables. This approach, however, would fail to take full advantage of the partitioned representation. When existentially quantifying a variable v over a conjunction of formulas, the quantifier need not be applied to those conjuncts where v does not appear. This allows some variables to be quantified early, before conjoining all the subformulas. For example, consider a variable z Z k. Then, z only appears in δk and wj. Therefore, z . Vk i=1 δi(Z, X, Y, Z ) wj(Z ) Vk 1 i=1 δi(Z, X, Y, Z ) ( z .δk(Z, X, Y, Z ) wj(Z )). Quantification of output variables that only appear in some of the conjuncts can be pushed inside in a similar way. Although the final BDD is the same, when using early quantification the intermediate BDDs can be significantly smaller, as the existential quantification tends to reduce their size before their conjunction becomes too large. Several heuristics can be used to decide in which order to perform conjunctions and quantification [Geist and Beer, 1994; Pan and Vardi, 2005]. In Section 4, however, we show that using better heuristics does not improve the performance of partitioning in LTLf synthesis.

3.3 Computing a Winning Strategy When existentially quantifying a variable v from a Boolean formula ψ, it is also possible to compute, as a side product, a function from an assignment of the free variables of ψ to an assignment of v that satisfies ψ whenever possible. This process is known, among other names, as Boolean synthesis [Fried et al., 2016]. Then, when computing Y. Z . Vk i=1 δi(Z, X, Y, Z ) wj(Z ) at iteration j+1, we can also construct a Boolean function gj+1 : 2Z 2X 2Y 2Z representing the choice for output variables and next state at that iteration. If the game is solved in m iterations, then the collection of functions g1, . . . , gm encodes a winning strategy. If the first move is chosen according to gm, the second according to gm 1, and so on, then the move chosen according to g1 is guaranteed to reach an accepting state of the DFA. As can be seen in [Tabajara and Vardi, 2017], Boolean synthesis can be performed even if Y. Z . Vk i=1 δi(Z, X, Y, Z ) wj(Z ) is computed using early quantification, as we propose in Section 3.2. Therefore, we can compute a winning strategy while still taking advantage of the benefits of a partitioned transition relation.

4 Experimental Evaluation After describing how partitioning can be integrated into symbolic LTLf synthesis, we proceed to perform an experimental evaluation to point out the limitations of partitioning in this context1. We compare the performance of the partitioned approach with the original monolithic approach and show that partitioning introduces a significant overhead into the computation of the winning strategy. We follow these results with a thorough analysis that identifies the source of the overhead to be an enlargement of the DFA game s state space, and explain the reason for this phenomenon.

1Supplemental data in https://bitbucket.org/ijcai2816/ijcai-2816/

Following standard practice in LTLf-synthesis literature [Zhu et al., 2017; Camacho et al., 2018], we convert LTLf to first-order logic and use the tool MONA [Henriksen et al., 1995] to translate FOL formulas to DFAs. For the partitioned version of the algorithm, we decompose the LTLf specification into its top-level conjuncts and convert them individually to FOL, and then to DFAs using MONA. All measured times are end-to-end, including translation to FOL, construction of the DFA and computation of the winning strategy. It is important to note that MONA produces canonical DFAs, meaning that they are the DFAs of minimum size for their formulas. In the monolithic approach, the monolithic DFA is minimized, while in the partitioned approach each component DFA is minimized. Because of this, even though the partitioned representation makes the size of the transition relation smaller, the number of state variables in the partitioned approach will be larger. As will be seen later in this section, this fact turns out to have a large impact on the performance of the partitioned approach. All experiments were performed on a cluster consisting of 2304 processor cores in 192 Westmere nodes (12 processor cores per node) at 2.83 GHz with 48 GB of RAM per node (4 GB per core). Although we partition the DFA game, the partitioned algorithm is not easily parallelizable because every iteration of the fixpoint consists of sequentially combining components into a monolithic BDD. Therefore, the different cores were used only for running multiple experiments in parallel. Every instance had a timeout of 8 hours.

4.1 Evaluation on LTLf Benchmarks As a fairly recent problem, LTLf synthesis lacks the extensive sets of benchmarks that exist for LTL synthesis. This forces us to construct our own set of benchmarks to use in our experimental evaluation. We initially considered benchmarks in the style of the ones used in [Zhu et al., 2017] and [Camacho et al., 2018], formed by random conjunctions of smaller base cases taken from the lilydemo LTL benchmark suite from [Jobstmann and Bloem, 2006] interpreted with LTLf semantics. In these benchmarks, the partitioned approach did outperform the monolithic one. The DFA games produced by these benchmarks, however, were very easy to solve, having very shallow winning strategies. All realizable instances could be won in at most 2 moves by the system. This is likely due partly to their random nature and partly to the fact that the base cases were formulas designed for infinite-horizon LTL, which can often become trivial when interpreted with finitehorizon semantics. We therefore conclude that these benchmarks are not an appropriate basis of comparison for LTLf synthesis, and proceed to construct more suitable benchmark families by encoding finite-horizon games in LTLf. Each of the three families below can be scaled based on one or more parameters which, unlike the case of random conjunctions, also increase the number of moves to win the game. The first two families deal with counters, which are important non-trivial components of many synthesis problems. Counters can model, for example, the spatial position of robots in a grid, or the amount of resources available to complete a task. The third family is based on a real game that has been extensively studied and requires complex strategic reasoning.

Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence (IJCAI-19)

1 2 3 4 5 6 7 8 9 10

Number of bits (n)

Monolithic Partitioned

Figure 1: Running time of Single-Counter benchmarks. Plots are in log scale. Missing points mean that the instance either timed out or ran out of memory. The results show that running time increases significantly when partitioning is used.

Single Counter. The first benchmark family is a simple example where the behavior of the system is completely determined by the actions of the environment. Therefore, the challenge in this family lies mostly in proving that the specification is realizable. The system stores an n-bit counter (where n is the scaling parameter) which it must increment upon a signal by the environment. The system wins if the counter eventually overflows to 0. To guarantee that the game is winning for the system, the specification assumes that the environment will send the increment signal at least once every two timesteps.

Double Counters. This family of benchmarks is similar to the previous one, except that in this case there are two n-bit counters, one incremented by the environment and another by the system. The goal of the system is for its counter to eventually catch up with the environment s counter. To guarantee that this is achievable, the specification assumes that the environment cannot increment its counter twice in a row.

Nim. This family of benchmarks describes a generalized version of the game of Nim [Bouton, 1901] with n heaps of m tokens each. The environment and the system take turns removing any number of tokens from one of the heaps, and the player who removes the last token loses.

The LTLf encoding of the benchmarks above take the form of conjunctions of several subformulas describing the possible actions and goal of the system. These formulas were given as specifications, with increasing values of n and m, to the monolithic and partitioned versions of the algorithm. We tried numerous different combinations of earlyquantification heuristics, as well as variable ordering heuristics for the BDDs. For all of them, the same general results were obtained, showing a stark contrast with previous applications of partitioning. The best performance for both the partitioned and monolithic versions was achieved by using dynamic variable reordering for the BDDs. Figure 1 shows these results for the Single-Counter benchmarks when n varies from 1 to 10, using the Bucket-Elimination heuristic [Mc Mahan et al., 2004] for early quantification. Results

Monolithic Partitioned n = 1, m = 1 0.09 30.7 n = 1, m = 2 0.16 31.9 n = 1, m = 3 0.32 326.37 n = 1, m = 4 0.06 - n = 2, m = 1 0.1 - n = 2, m = 2 0.15 - n = 2, m = 3 0.32 - n = 2, m = 4 0.63 - n = 3, m = 1 0.1 - n = 3, m = 2 0.59 - n = 3, m = 3 2.51 - n = 3, m = 4 6.62 -

Table 1: Running time, in seconds, of the Nim benchmarks for different values of n and m. Missing values for the partitioned version indicate that the instance either timed out or ran out of memory.

Monolithic Partitioned n = 1, m = 1 4 67 n = 1, m = 2 7 107 n = 1, m = 3 10 176 n = 1, m = 4 10 445 n = 2, m = 1 10 200 n = 2, m = 2 14 3047 n = 2, m = 3 20 3782 n = 2, m = 4 16 15457 n = 3, m = 1 6 423 n = 3, m = 2 14 2394 n = 3, m = 3 15 42175 n = 3, m = 4 17 472323

Table 2: Number of nodes of the BDD for the winning states of the Nim benchmarks for different values of n and m. For easier visualization, we show only the initial size of the BDD. In the monolithic version BDD sizes remain relatively constant during the computation, reaching around 60 nodes at most, while in the partitioned version most instances fail after one or two iterations.

for the Double-Counter benchmarks, as well as for other heuristics, follow a similar trend. Table 1 shows the same comparison for the Nim benchmarks. In our experiments, unlike the case for model checking and other problems, symbolic LTLf synthesis was not able to benefit from partitioning. In fact, despite making DFA construction more feasible as expected (construction of the partitioned DFA always finished in under a second), partitioning created a massive overhead during computation of the winning strategy that lead to an orders-of-magnitude increase in running time. This overhead was large enough to nullify all benefits from the partitioned DFA construction, as in all cases where the monolithic version failed during construction, the partitioned version failed during the fixpoint computation. In the next section we provide an analysis of this phenomenon.

4.2 Analysis of the Results Explaining the disparity between the above results and previous applications of partitioning requires a more in-depth look into the behavior of the fixpoint algorithm in the mono-

Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence (IJCAI-19)

1 10 100 1000 10000

Size (BDD nodes)

Iteration (j)

n=1 n=2 n=3 n=4 n=5 n=6 n=7 n=8 n=9 n=10

1 10 100 1000

Size (BDD nodes)

Iteration (j)

n=1 n=2 n=3 n=4 n=5 n=6 n=7 n=8 n=9 n=10

Figure 2: Node count of the BDD for the winning states per iteration of the fixpoint algorithm on the Single-Counter benchmarks, using the (a) Monolithic or (b) Partitioned approach. For better visualization, one or both axes are in log scale in each of the plots.

lithic and partitioned cases. For this purpose, we proceeded to monitor the size of the BDD wj representing the set of winning states across iterations of the fixpoint. Figure 2 displays these measurements for the Single-Counter benchmark family, again using dynamic variable reordering and Bucket Elimination, with every line representing a different value for the number of bits n. Figure 3 and Table 2 show analogous results for the Double-Counters and Nim families. It is clear from the plots that there is a notable difference between the behavior of the monolithic and partitioned approaches. In the monolithic version, the BDD sizes change very little during the fixpoint computation (the changes are even smaller when dynamic variable reordering is not used). In the partitioned version, however, although the BDD sizes are initially small, they increase rapidly in the first few iterations of the fixpoint computation. By the time it becomes relatively constant, BDD size is already several orders of magnitude larger than in the monolithic version. Interestingly, in the case of the Single-Counter benchmarks, even though the state space is exponential, the initial BDD sizes of the monolithic version increase linearly with n, indicating that a good symbolic encoding is achieved. This

1 10 100 1000

Size (BDD nodes)

Iteration (j)

n=1 n=2 n=3 n=4 n=5 n=6

Size (BDD nodes)

Iteration (j)

n=1 n=2 n=3 n=4 n=5 n=6 n=7 n=8 n=9 n=10

Figure 3: Node count of the BDD for the winning states per iteration of the fixpoint algorithm on the Double-Counters benchmarks, using the (a) Monolithic or (b) Partitioned approach. Plots are in log-log scale. The monolithic DFA could not be constructed for n > 6.

is not the case, for example, in the Double-Counter benchmarks, where the initial BDD sizes are exponential in n for the monolithic version, while being linear for the partitioned version. Even in the Double-Counter case, however, the BDDs in the partitioned version quickly grow exponentially to surpass the ones in the monolithic version. These measurements of BDD growth allow us to conclude that the issue is not caused by inefficiencies in processing the partitioned transition relation during each iteration, but rather by a massive increase in BDD sizes during the course of the fixpoint computation. An important conclusion that can be drawn from this observation is that better early-quantification schemes are not enough to solve this problem: since BDDs are canonical data structures, the BDD computed at each iteration will be the same regardless of the order in which conjunctions and quantification are performed. At the same time, this observation also helps explain why the partitioned approach performed well on the random conjunctions mentioned in the beginning of Section 4.1, since those benchmarks can be solved in only one or two iterations. If the game can be solved in a single iteration, for example, then it is essentially equivalent to an instance of Boolean synthe-

Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence (IJCAI-19)

sis, where partitioning is already known to work [Tabajara and Vardi, 2017]. The blowup in BDD sizes for the partitioned version can be explained by the fact that, although the partitioned transition relation provides a more compact representation of a DFA game, the underlying state space can be significantly larger than for the monolithic version, leading to a major increase in the representation of the set of winning states. For example, in the Single-Counter benchmarks the number of state variables is in the order of n for the monolithic DFA, and 7n for the partitioned DFA. The large difference in size of the state spaces is due to the fact that MONA constructs canonical DFAs, and therefore the state space of the monolithic DFA is as small as possible. In the partitioned version, while the individual DFAs are minimized, the full state space of their product can be much larger than the canonical DFA, to the point that not even the symbolic representation can handle. A reasonable question to ask is if it would be possible to find a balance between minimization and partitioning by constructing each DFA from the conjunction of multiple subformulas, rather than a single subformula. In this case, the individual DFAs might be more complex, but MONA would be able to perform more aggressive minimization. We tried both selecting which formulas to combine manually and using clustering heuristics from previous applications of partitioning such as [Pan and Vardi, 2005]. In either case, the running time and BDD sizes were smaller than in the fullypartitioned version, but still larger than the monolithic version, suggesting that performance decreases proportionally to the degree of partitioning. The results of our experiments reveal critical issues that prevent the effective application of classic partitioned approaches to LTLf synthesis. Although such approaches might seem to be a promising solution to the current bottleneck of synthesis algorithms, i.e. DFA construction, this benefit is invalidated by the increased complexity of the resulting game.

5 Discussion

Ultimately, our results show that, despite having seen widespread use in related problems, partitioning has crucial weaknesses when it comes to LTLf synthesis. Partitioning does not interact effectively with DFA construction and minimization, giving rise to a compact representation of the transition relation but an enlarged representation of state sets. Although our evaluation encompasses only a few benchmark families, these families illustrate common elements of synthesis problems, such as counters and strategic reasoning. Therefore it is not unreasonable to believe that our results extend to other interesting cases. At the very least, we have shown that partitioning is not a simple general solution, as one might have expected. Its applicability, if any, is likely to be limited to specific cases and might require domain knowledge to partition the problem in a way that still allows some degree of minimization. The role that minimization plays in LTLf synthesis accounts for the crucial difference with partitioning in model checking. In the latter we have no access to a canonical transition system in the same sense as in the former. Instead, the

model is already provided with a fixed state space, and the transition relation is partitioned along the already-existing set of state variables. Therefore, unlike in LTLf synthesis, partitioning in model checking produces no overhead on the statespace representation. Our evaluation focused on LTLf due to the attention that this variant has recently attracted in the field of AI, and we cannot answer conclusively yet whether similar approaches would be effective or not in synthesis algorithms for the standard, infinite-horizon LTL. LTLf does have the distinction, however, that DFAs can be fully minimized. This favors the monolithic approach, that can benefit more from minimization than the partitioned approach. Nevertheless, it would not be surprising if a similar state-space explosion occurred also in the infinite-horizon case, even if to a lesser degree due to the smaller role of minimization. Therefore, the results of our evaluation should be considered if one intends to apply similar partitioning techniques to LTL synthesis. Note that the LTL-synthesis tool STRIX [Meyer et al., 2018] mentioned in the introduction also uses a similar type of decomposition, with successful results. The main difference is that rather than using symbolic techniques, STRIX maintains an explicit representation of the state space throughout, allowing the algorithm to compute states of the product on-the-fly as they are needed. This means that the explored state space needs to grow only as much as necessary to compute the winning strategy, and therefore the full size of the state space matters less than in symbolic approaches. We cannot rely solely on explicit-state approaches for synthesis, however, since they will necessarily need to use exponential space when the winning strategy requires an exponential number of states, while symbolic techniques might be able to compute the same strategy in polynomial space. Yet, our results indicate that to improve current symbolic LTLf synthesis approaches, it might be necessary to look beyond classic partitioning towards more sophisticated decomposition techniques. Alternative decomposition approaches to partitioning have been proposed for Boolean relations in the context of Boolean synthesis [Akshay et al., 2017; Chakraborty et al., 2018], and it is possible that some of these ideas can be leveraged to LTLf synthesis as well, although further research is necessary to determine exactly how. The work of [Fried et al., 2018] has also explored several novel notions of decomposition, both of relations and of DFAs. Given that minimization has shown itself to have a crucial effect on the performance of LTLf synthesis, finding a decomposition approach that will display good results for this problem will require carefully considering how the decomposition can exploit minimization as much as possible, and the ultimate effect that it has on the explored state space.

Acknowledgements

Work partially supported by NSF Grant no. IIS-1830549, by the Brazilian agency CNPq through the Ciˆencia Sem Fronteiras program, and by the Data Analysis and Visualization Cyberinfrastructure funded by NSF under grant OCI0959097 and Rice University. The authors thank Dror Fried for his helpful comments and feedback on the paper.

Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence (IJCAI-19)

References [Akshay et al., 2017] S. Akshay, Supratik Chakraborty, Ajith K. John, and Shetal Shah. Towards Parallel Boolean Functional Synthesis. In Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Proceedings, Part I, pages 337 353, 2017. [Bouton, 1901] Charles L Bouton. Nim, a game with a complete mathematical theory. Annals of Mathematics, 3(1/4):35 39, 1901. [Burch et al., 1991] Jerry R. Burch, Edmund M. Clarke, and David E. Long. Representing Circuits More Efficiently in Symbolic Model Checking. In Proceedings of the 28th Design Automation Conference, pages 403 407, 1991. [Camacho et al., 2018] Alberto Camacho, Jorge A. Baier, Christian J. Muise, and Sheila A. Mc Ilraith. Finite LTL Synthesis as Planning. In Proceedings of the Twenty Eighth International Conference on Automated Planning and Scheduling, ICAPS 2018, pages 29 38, 2018. [Chakraborty et al., 2018] Supratik Chakraborty, Dror Fried, Lucas M. Tabajara, and Moshe Y. Vardi. Functional Synthesis via Input-Output Separation. In 2018 Formal Methods in Computer Aided Design, FMCAD 2018, pages 1 9, 2018. [De Giacomo and Vardi, 2013] Giuseppe De Giacomo and Moshe Y. Vardi. Linear Temporal Logic and Linear Dynamic Logic on Finite Traces. In IJCAI 2013, Proceedings of the 23rd International Joint Conference on Artificial Intelligence, pages 854 860, 2013. [De Giacomo and Vardi, 2015] Giuseppe De Giacomo and Moshe Y. Vardi. Synthesis for LTL and LDL on Finite Traces. In Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, pages 1558 1564, 2015. [Fried et al., 2016] Dror Fried, Lucas M. Tabajara, and Moshe Y. Vardi. BDD-Based Boolean Functional Synthesis. In Computer Aided Verification - 28th International Conference, CAV 2016, Proceedings, Part II, pages 402 421, 2016. [Fried et al., 2018] Dror Fried, Axel Legay, Jo el Ouaknine, and Moshe Y. Vardi. Sequential Relational Decomposition. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, pages 432 441, 2018. [Geist and Beer, 1994] Daniel Geist and Ilan Beer. Efficient Model Checking by Automated Ordering of Transition Relation Partitions. In Computer Aided Verification, 6th International Conference, CAV 94, Proceedings, pages 299 310, 1994. [He et al., 2017] Keliang He, Morteza Lahijanian, Lydia E. Kavraki, and Moshe Y. Vardi. Reactive Synthesis for Finite Tasks under Resource Constraints. In 2017 IEEE/RSJ International Conference on Intelligent Robots and Systems, IROS 2017, pages 5326 5332, 2017.

[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 Tools and Algorithms for Construction and Analysis of Systems, First International Workshop, TACAS 95, Proceedings, pages 89 110, 1995. [Jobstmann and Bloem, 2006] Barbara Jobstmann and Roderick Bloem. Optimizations for LTL Synthesis. In Formal Methods in Computer-Aided Design, 6th International Conference, FMCAD 2006, pages 117 124, 2006. [John et al., 2015] Ajith K. John, Shetal Shah, Supratik Chakraborty, Ashutosh Trivedi, and S. Akshay. Skolem Functions for Factored Formulas. In Formal Methods in Computer-Aided Design, FMCAD 2015, pages 73 80, 2015. [Kupferman and Vardi, 2001] Orna Kupferman and Moshe Y. Vardi. Model Checking of Safety Properties. Formal Methods in System Design, 19(3):291 314, 2001. [Mc Mahan et al., 2004] Benjamin J. Mc Mahan, Guoqiang Pan, Patrick Porter, and Moshe Y. Vardi. Projection Pushing Revisited. In Advances in Database Technology - EDBT 2004, 9th International Conference on Extending Database Technology, Proceedings, pages 441 458, 2004. [Meyer et al., 2018] Philipp J. Meyer, Salomon Sickert, and Michael Luttenberger. Strix: Explicit Reactive Synthesis Strikes Back! In Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, Flo C 2018, Proceedings, Part I, pages 578 586, 2018. [Pan and Vardi, 2005] Guoqiang Pan and Moshe Y. Vardi. Symbolic Techniques in Satisfiability Solving. J. Autom. Reasoning, 35(1-3):25 50, 2005. [Tabajara and Vardi, 2017] Lucas M. Tabajara and Moshe Y. Vardi. Factored Boolean Functional Synthesis. In 2017 Formal Methods in Computer Aided Design, FMCAD 2017, pages 124 131, 2017. [Zhu et al., 2017] Shufang Zhu, Lucas M. Tabajara, Jianwen Li, Geguang Pu, and Moshe Y. Vardi. Symbolic LTLf Synthesis. In Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, pages 1362 1369, 2017.

Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence (IJCAI-19)