\section{Introduction}
\label{Sec:Intro}

Reactive synthesis is the automated construction, from a high-level description of its desired behavior, of a reactive system that continuously interacts with an uncontrollable external environment~\cite{church1957applications}. This declarative paradigm holds the promise of simplifying the task of designing provably correct reactive systems.

This work looks into the development of reactive synthesis from specifications in {Linear Temporal Logic over finite traces} ($\mathsf{LTLf}$), or \emph{$\mathsf{LTLf}$ synthesis}, for short. $\mathsf{LTLf}$ is a specification language that expresses rich and complex temporal behaviors over a {\em finite} time horizon~\cite{de2013linear}. This formalism has found application in specifying task plans in robotics~\cite{he2017reactive,lahijanian2015time}, safety-critical objectives~\cite{zhu2017symbolic}, business processes~\cite{PesicBA10}, and the like.

Seminal results have established that $\mathsf{LTLf}$ synthesis is 2$\mathsf{EXPTIME}$-complete~\cite{de2015synthesis}. Since then, several  undertakings have led to algorithmic solutions for  synthesis~\cite{de2015synthesis,camacho2018finite}. The current state-of-the-art reduces  synthesis to a reachability game played on a  deterministic finite-state automaton, or DFA~\cite{zhu2017ltlfsymbolic}. The DFA is obtained by converting the input $\mathsf{LTLf}$ specification into a DFA that recognizes the same language. This conversion has been identified as
a primary scalability bottleneck in synthesis \cite{zhu2017ltlfsymbolic}.
This is not surprising as the DFA is known to be double-exponential in the size of the specification in the worst case~\cite{kupferman1999model}. In order to be effective for synthesis the conversion must, in addition to being time and memory performant, also prevent state-space explosion, as recent investigations have discovered that the efficiency of solving the game on a DFA is strongly affected by the size of the state space~\cite{tabajara2019partition}. This work contributes towards the development of  $\mathsf{LTLf}$-to-DFA conversion techniques that are aimed at advancing the scalability of $\mathsf{LTLf}$ synthesis.

Prior works on $\mathsf{LTLf}$-to-DFA conversion have led to two contrasting algorithmic approaches. In the first approach \cite{zhu2017ltlfsymbolic}, the state-space of the DFA is represented explicitly, the construction is syntax driven, and the DFA is aggressively minimized. This approach first converts $\mathsf{LTLf}$ to an equivalent first-order-logic formula and then constructs a DFA for this formula using the $\mathsf{Mona}$ tool~\cite{henriksen1995mona}. The $\mathsf{Mona}$ algorithm first produces the binary syntax tree of the specification, then traverses the tree bottom-up while constructing the {\em minimal} DFA at each node. Consequently, it constructs the final DFA at the root of the tree in its canonical minimal form. Aggressive minimization can often prevent state-space explosion, as for many specifications arising from real-life situations the minimal DFAs are rarely more than exponential in the size of the specification, as opposed to double exponential~\cite{tabakov2012optimized}.
Yet, an exponential DFA might still be too large if the set of states is represented explicitly, and the overhead caused by aggressive DFA minimization grows rapidly with specification size.

The second approach, inspired by~\cite{tabajara2019partition}, represents the DFA state space symbolically, uses a compositional construction, and avoids minimizing the DFAs.
In compositional constructions,  the specification is decomposed into multiple smaller sub-specifications for which explicit DFA conversion is tractable. These intermediate DFAs are then composed to get the final DFA.
The symbolic representation  encodes the state space of a DFA in a logarithmic number of bits,
potentially achieving a polynomial representation even for an exponential-sized DFA, depending on the complexity of the DFA's structure.
The existing compositional approach takes advantage of this by representing the intermediate DFAs symbolically. In this case, the DFAs are composed by simply taking the symbolic product {\em without} performing minimization.
The problem with this, however, is that each symbolic product results in a DFA with a larger state space than its minimal DFA, as no minimization is performed. When the number of symbolic products is large, the overhead in the size of the state space magnifies.
Because of this, this approach ultimately produces a state space that is so enlarged that not even the succinct symbolic representation can compensate for the blow-up.

The key issue with both  approaches is that their critical operation is effective at small scale but becomes inhibitory at large scale. Explicit approaches aggressively perform minimization, which is efficient on small DFAs but expensive on larger ones. Meanwhile, symbolic approaches  perform symbolic products without minimization. While few symbolic products are manageable, too many products may lead to a large blow-up in the size of the state space.

This work proposes a novel compositional approach that is able to overcome the drawbacks of both existing approaches.
Our approach utilizes a {\em hybrid} state-space representation, i.e., at different times it uses both the explicit and symbolic state representations for the intermediate DFAs. The core idea is to use explicit-state representation for the intermediate DFAs as long as minimization is not prohibitively expensive, and to switch over to symbolic state representation as soon as that occurs. This way, our hybrid-representation approach applies explicit state representation to small DFAs, and also delays the point at which switch-over to symbolic representation occurs, thus ensuring that fewer symbolic products have to be performed to generate the final DFA.  Therefore, by finding a balance between the two representations, our hybrid appoach is able to extract their benefits and mitigate their weaknesses.

We have implemented our $\mathsf{LTLf}$-to-DFA conversion algorithm, and its extension to $\mathsf{LTLf}$ synthesis via reachability games, in tools called $\mathsf{Lisa}$ and $\mathsf{LisaSynt}$, respectively.
A comprehensive empirical analysis reveals the merits of the proposed hybrid compositional approach on both DFA conversion and $\mathsf{LTLf}$ synthesis, as each tool outperforms the current state-of-the-art in runtime and memory consumption. In addition, the DFAs generated from $\mathsf{Lisa}$ have size comparable to the minimal DFA and significantly smaller than those obtained from pure symbolic-state methods.

\section{Preliminaries}
\label{sec:preliminaries}

\subsection{Linear Temporal Logic over finite traces}

{Linear Temporal Logic over finite traces} ($\mathsf{LTLf}$)~\cite{baier2006planning,de2013linear} extends propositional logic with finite-horizon temporal operators. In effect, $\mathsf{LTLf}$  is a variant of $\mathsf{LTL}$~\cite{pnueli1977temporal} that is interpreted over a finite rather than infinite trace. The syntax of an $\mathsf{LTLf}$ formula over a finite set of propositions $\mathsf{Prop}$ is identical to $\mathsf{LTL}$, and defined as $\varphi:= a \in \mathsf{Prop} \mid \neg \varphi \mid \varphi \land \varphi \mid \varphi \lor \varphi \mid \mathsf{X} \varphi \mid \varphi \mathsf{U} \varphi \mid \mathsf{F} \varphi \mid \mathsf{G} \varphi$.
Here $\mathsf{X}$ (Next), $\mathsf{U}$ (Until), $\mathsf{F}$ (Eventually), $\mathsf{G}$ (Always) are temporal operators.
The semantics of $\mathsf{LTLf}$ can be found in~\cite{de2013linear}.
W.l.o.g., we assume that every $\mathsf{LTLf}$ formula $\varphi$ is written as a conjunction of $\mathsf{LTLf}$ subformulas i.e. $\varphi = \bigwedge_{i=1}^n \varphi_i$.
The language of an $\mathsf{LTLf}$ formula $\varphi$, denoted by $\L(\varphi)$, is the set of finite words over $2^{\mathsf{Prop}}$  that satisfy $\varphi$.

$\mathsf{LTLf}$ synthesis is formally defined as follows:

\begin{definition}[$\mathsf{LTLf}$ synthesis]
\label{def:ltlf-synthesis}

Let $\varphi$ be an $\mathsf{LTLf}$ formula over $\mathsf{Prop} = \varset{I} \cup \varset{O}$ where the set of input variables $\varset{I}$ and output variables $\varset{O}$ are two disjoint sets of propositions.
We say $\varphi$ is realizable if there exists a strategy $\gamma: (2^{\varset{I}})^{+} \rightarrow 2^{\varset{O}}$ such that for every infinite sequence $\lambda = I_{0}, I_{1}, \cdots \in (2^{\varset{I}})^{\omega}$ of interpretations over $\varset{I}$, there exists $m \geq 0$ such that $\rho = (I_{0} \cup \gamma(I_{0})), (I_{1} \cup \gamma(I_{0}, I_{1})), \cdots, (I_{m} \cup \gamma(I_{0}, \cdots, I_{m}))$ satisfies $\varphi$.
The problem of $\mathsf{LTLf}$ synthesis is to decide whether a given $\varphi$ is realizable and to construct such a strategy if so.
\end{definition}

Intuitively, $\mathsf{LTLf}$ synthesis can be perceived as  a game between an external environment and the desired system that take turns to assign values to input and output propositions, respectively. The system responds to the environment inputs using the strategy $\gamma$. The game is won by the system if its strategy is able to guarantee that the resultant input-output sequence will satisfy formula $\varphi$ after a finite number of turns. In our formulation of $\mathsf{LTLf}$ synthesis, like in~\cite{tabajara2019partition}, the environment plays first. Alternatively, the system may play first~\cite{zhu2017ltlfsymbolic}.
Solving the alternative formulation requires only slight changes to the algorithm presented in (\textsection~\ref{sec:synthesis}). We
adhere to the formulation in Definition~\ref{def:ltlf-synthesis}  in this paper as our benchmarks assume that formulation and all tools being compared support it.

\subsection{DFA and its representations}
A {\em deterministic finite automaton} (DFA)~\cite{thomas2002automata} is a tuple $D = ( \Sigma, S , \iota, \Delta, F )$ where
$\Sigma$ is a finite set of symbols (called an alphabet),
$S$ is a finite set of states,
$\iota \in S$ is the initial state,
$F \subseteq S$ is the set of accepting states and
$\Delta : S \times \Sigma \rightarrow S $ is the transition function. A finite word $w = w_0\dots w_n \in \Sigma^*$ has a {\em run} $\rho = s_0\dots s_{n+1} \in S^{+}$ in $D$ if for all $i\in \{0,\dots n\}$ we have that $s_{i+1} = \Delta(s_i, w_i)$ and $s_0 = \iota$. A run $\rho = s_0\dots s_{n+1}$ is an {\em accepting run} in $D$ if $s_{n+1} \in F$.
A word $w$ is in the language of  $D$, $\L(D)$, if $w$ has an accepting run in $D$.
A DFA is said to be {\em minimal} if the language represented by that DFA cannot be represented by another DFA with fewer states.

Every $\mathsf{LTLf}$ formula $\varphi$ over $\mathsf{Prop}$ can be converted into a DFA $D$ with alphabet $\Sigma = 2^\mathsf{Prop}$~\cite{de2013linear} such that $\L(D) = \L(\varphi)$.
If this DFA is constructed in a form that explicitly enumerates all DFA states, we call it an \emph{explicit-state} representation. A DFA over the alphabet $\Sigma = 2^\mathsf{Prop}$ can also be compactly represented \emph{symbolically}, by also encoding the state space using a logarithmic number of propositions. The \emph{symbolic-state} representation of a DFA $D = (2^\mathsf{Prop}, S , \iota, \Delta, F )$ is a tuple $\mathcal{D} = (\mathcal{S}(\varset{Z}), \mathcal{T}(\varset{Z}, \mathsf{Prop}, \varset{Z}'), \mathcal{F}(\varset{Z}))$. In this representation, $\varset{Z} = \{z_1,\dots z_n\}$ are propositions encoding the state space $S$, with $n = \lceil \log |S| \rceil$, and their primed counterparts $\varset{Z}' =  \{z'_1,\dots z'_n\}$ encode the next state.
Each state $s \in S$ corresponds to an interpretation $Z \in 2^\varset{Z}$ over propositions $\varset{Z}$. When representing the next state of the transition function, the same encoding is used for an interpretation $Z'$ over $\varset{Z}'$.
Then, $\mathcal{S}$, $\mathcal{T}$ and $\mathcal{F}$ are Boolean formulas representing $\iota$, $\Delta$ and $F$, respectively. $\mathcal{S}(\varset{Z})$ is satisfied only by the interpretation of the initial state $\iota$ over $\varset{Z}$. $\mathcal{T}(\varset{Z}, \mathsf{Prop}, \varset{Z}')$ is satisfied by interpretations $Z \in 2^\varset{Z}$, $P \in 2^\mathsf{Prop}$ and $Z' \in 2^{\varset{Z}'}$ iff $\Delta(s, P) = s'$, where $s$ and $s'$ are the states corresponding to $Z$ and $Z'$.
Lastly, $\mathcal{F}(\varset{Z})$ is satisfied by the interpretation $Z$ over $\varset{Z}$ corresponding to state $s\in S$ iff $s \in F$.
The intersection of two DFAs $D_1=(\mathcal{S}_1, \mathcal{T}_1, \mathcal{F}_1)$ and $D_2 = (\mathcal{S}_2, \mathcal{T}_2, \mathcal{F}_2)$, denoted $D_1 \wedge D_2$,   is given by $(\mathcal{S}_1\wedge \mathcal{S}_2, \mathcal{T}_1 \wedge \mathcal{T}_2, \mathcal{F}_1 \wedge \mathcal{F}_2)$. In this paper, all Boolean formulas, including $\mathcal{S}$, $\mathcal{T}$ and $\mathcal{F}$ of a symbolic DFA, will be encoded using {\em Reduced Ordered Binary Decision Diagrams} (BDDs)~\cite{bryant1986graph}.

\subsection{DFA game}
\label{subsec:dfa-game}

A \emph{DFA game} is a reachability game between two players, called the \emph{environment} and the \emph{system}, played over a DFA with alphabet $2^{\varset{I} \cup \varset{O}}$.
The environment player assigns values to the input variables $\varset{I}$, while the system assigns values to the output variables $\varset{O}$.
The DFA game starts at the initial state of the DFA.
At each round of the game, first the  environment chooses an assignment $I$ to the $\varset{I}$ variables, and then the system will choose an assignment $O$ to the $\varset{O}$ variables.
The combined assignment $I \cup O$ determines the unique state the game moves to according to the transition function of the DFA.
The system \emph{wins} the game if the game reaches an accepting state of the DFA.
{\em Solving a DFA game} corresponds to determining whether there exists a strategy for the system to always win the game.

DFA games are known to be solvable in polynomial time with respect to the number of states~\cite{mazala2002infinite}. The algorithm determines if the initial state is a {\em winning state}, i.e., a state that is either accepting or from which, for every assignment $I$ to the $\varset{I}$ variables, the system can always choose an assignment $O$ to the $\varset{O}$ variables that leads to a winning state. More details will be given in (\textsection~\ref{sec:synthesis}).
If the initial state is a winning state, then there exists a winning strategy that can be represented by a Mealy machine that
determines the output of the system given the current state and input. For more details, refer to~\cite{tabajara2019partition}.

\section{Related work}

\subsubsection{$\mathsf{LTLf}$ to DFA conversion}

There are two commonly used approaches for the conversion currently.
In the current state-of-the art approach,
the $\mathsf{LTLf}$ formula is translated into  first-order logic over finite traces, and then converted into a DFA by $\mathsf{Mona}$, a more general conversion tool from monadic second-order logic to DFA~\cite{henriksen1995mona}.
The first $\mathsf{LTLf}$ synthesis tool $\mathsf{Syft}$ utilizes this method for DFA generation~\cite{zhu2017ltlfsymbolic}.

An alternative approach, used by the tool $\mathsf{Spot}$~\cite{duret2016spot}, is to translate the $\mathsf{LTLf}$ formula into an $\mathsf{LTL}$ formula with equivalent semantics, convert this formula into a B\"{u}chi automaton~\cite{gerth1995simple}, and then transform this B\"{u}chi automaton into a DFA.
Both approaches generate a DFA in explicit state-space representation.

\subsubsection{DFA vs. NFA}
NFAs are more general than DFAs. In fact, NFAs can be constructed from an $\mathsf{LTLf}$ formula in a single-exponential blow-up as opposed to the double-exponential blow-up incurred for DFA construction.
Various approaches for $\mathsf{LTLf}$-to-NFA with single-exponential blow-up have been described such as
\cite{baier2006planning,de2015synthesis}.
Yet, in practice, single exponential NFA conversion tools do not perform as well as DFA conversion tools.
\cite{tabakov2012optimized} shows that minimal DFAs from $\mathsf{LTLf}$ formulas tend to be orders of magnitude smaller than their NFA counterparts constructed from implementations of the single-exponential algorithms.

\subsubsection{$\mathsf{LTLf}$ synthesis}
As aforementioned, current state-of-the-art tool $\mathsf{Syft}$~\cite{zhu2017ltlfsymbolic} uses $\mathsf{Mona}$ to construct an explicit-state DFA, then converts this DFA into a symbolic representation in order to solve the game using a symbolic fixed-point computation. The explicit-state DFA construction has been identified as the primary bottleneck to $\mathsf{Syft}$ as the length of the formula increases.
Therefore, recent attempts in synthesis have been made  to avoid the explicit DFA construction. We describe these attempts below.

A recent approach attempted to avoid the full construction by instead decomposing the specification into  conjuncts, then converting each conjunct to an individual DFA~\cite{tabajara2019partition}. Since these conjuncts are smaller formulas, their explicit-state DFAs can be constructed efficiently.
The smaller DFAs are then converted into a symbolic representation and the game is solved over this {\em decomposed symbolic representation}.
While
the construction was indeed more efficient in terms of time and memory, the resulting DFA had a much larger state space.  This severely decreased the performance of the game-solving algorithm, rendering a poorly scaling procedure for $\mathsf{LTLf}$ synthesis.

In another attempt to avoid explicit DFA construction, \cite{camacho2018finite} first constructs an NFA from the formula and then reduces  synthesis to fully-observable nondeterministic (FOND) planning. The NFA is determinized  on-the-fly during the  planning phase.
Even here, the specification is decomposed into conjuncts, which are separately converted to NFAs and used to encode to FOND.
Despite the generalization to NFAs, in practice FOND-based methods rely on DFA conversion tools since they are more competitive than existing NFA construction tools that incur a single-exponential blow up.
Previous experiments suggest the FOND-based approach is complementary with the approach based on explicit DFA construction, each being able to solve instances that the other cannot.

\subsubsection{Compositional techniques in temporal  synthesis}

Both \cite{tabajara2019partition} and \cite{camacho2018finite} benefit from compositional techniques as they both  decompose the input formula into conjuncts before construction of the respective automata.  Application-specific decomposition has also been shown to lead to an orders-of-magnitude improvement in $\mathsf{LTLf}$ synthesis for robotics~\cite{he2019efficient}.

A precedent for compositional techniques exists also in synthesis of $\mathsf{LTL}$ over infinite traces, including in several state-of-the-art tools such as $\mathsf{Strix}$~\cite{meyer2018strix} and $\mathsf{Acacia+}$~\cite{bohy2012acacia}.
$\mathsf{Strix}$ decomposes the formula semantically, i.e., it generates a subformula if it belongs to a restricted fragment of $\mathsf{LTL}$ such as safety $\mathsf{LTL}$ or co-safety $\mathsf{LTL}$. This way it benefits from constructing automaton using more efficient fragment-specific algorithms.
On the other hand, $\mathsf{Acacia+}$ decomposes the formula into conjuncts, which are each solved as a  separate safety game. The final solution is obtained by composing solutions from the separate safety games.

\section{Hybrid compositional DFA generation}
\label{sec:hybrid}

This section describes the primary contribution of this work. We present a novel compositional approach for $\mathsf{LTLf}$-to-DFA conversion.
Our approach is based on using a hybrid-state representation, i.e., at different times it uses both explicit and symbolic-state representations for intermediate DFAs, as opposed to prior works in which only one of the two state-representations is used~\cite{zhu2017ltlfsymbolic,camacho2018finite,tabajara2019partition}.
By diligent application of both representations, our hybrid approach is able to leverage their complementary strengths and render an algorithm that is not only competitive time- and memory-wise, but also  generates DFAs with small number of states.

Our compositional approach is comprised of two phases, called the {\em decomposition phase} and the {\em composition phase}.
In the decomposition phase, the input formula is first {\em decomposed} into smaller subformulas which are then converted into their equivalent DFAs using standard algorithms.
In the composition phase, the intermediate DFAs are {\em composed} to produce the final DFA.
We describe each phase for our hybrid approach in detail below.
The formal description of our algorithm has been deferred to the Appendix.

\subsection{Decomposition phase}

The decomposition phase is the first step in our algorithm. This phase receives the $\mathsf{LTLf}$ formula $\varphi$ as input.
We make an  assumption that the formula is given as the conjunction of multiple small $\mathsf{LTLf}$ subformulas, i.e., $\varphi = \bigwedge_{i=1}^n \varphi_i$ where each $\varphi_i$ is an $\mathsf{LTLf}$ formula in itself.
This assumption has been adopted as a standard practice in  synthesis domains as large specifications arising from applications tend to exhibit this form~\cite{filiot2010compositional,filiot2011antichains}.

We interpret formula $\varphi$ as an $n$-ary syntax tree as opposed to a binary-tree. Consequently, the input formula  $\varphi = \bigwedge_{i=1}^n \varphi_i$ is decomposed into  $n$-subformulas $\varphi_1, \dots ,\varphi_n$.
Then each of these subformulas $\varphi_i$ is converted into its minimal DFA $D_i$ in explicit-state representation.
This can be performed by an existing  tool~\cite{de2013linear,duret2016spot,henriksen1995mona,kupferman1999model}.  More advanced decomposition schemes could be adopted from~\cite{camacho2018finite}.

The  rationale behind this step is that existing explicit-state  tools are efficient in generating minimal DFA for small formulas. Since the subformulas are typically small in length, we are able to benefit from existing literature in this step.

\subsection{Composition phase}

The composition phase receives the minimal DFAs $D_i$ for subformulas $\varphi_i$ in the previous phase, which are represented with explicit states. Our goal in this phase is to construct a DFA corresponding to $\varphi$. In theory, this can be obtained by simply taking the intersection of DFAs $D_i$.
In practice, the intersection of $n$ DFAs may lead to state-space explosion since DFA intersection is done by performing their product construction.
Therefore, the main focus of the composition phase is about how to efficiently construct the intersection without incurring state explosion.
We discuss the salient features of our algorithm before describing it in detail.

Briefly speaking, we perform the composition of DFAs in iterations.
In each iteration, two DFAs are selected based on a {\em dynamic smallest-first heuristic}, which will be described below, and removed from the set.
A new DFA is formed by the product of the two selected DFAs. The new DFA will be minimized based on a {\em selective DFA heuristic}, which is also described below. The new DFA is then inserted back into the set. The new set is the input to the next iteration.
This continues until only one DFA remains, which is presented as the final DFA.
In the following, we denote by $S_j$ the set of DFAs at the $j$-th iteration. Then $S_1 = \{D_1, \dots, D_{n}\}$, and $S_{n} = \{D\}$ where $D$ is the final output DFA.

In contrast to prior works which either use explicit states or symbolic states, the central feature of our algorithm is that it uses hybrid representation for DFAs, i.e., in different iterations all DFAs in $S_j$ are either represented in explicit- or symbolic-state form. Initially,
all DFAs in $S_1$ are in explicit-state form.
This continues while the DFAs in $S_j$ have a small number of states, since the product and minimization of DFAs are efficient for small DFAs with explicit-state representation.
But as some DFAs in $S_j$ grow in size they require more memory and longer time to perform minimization.
So, as soon as some DFA in $S_j$ reaches a large number of states,  all DFAs in $S_j$ are converted into symbolic-state representation, in which the DFAs are represented more succinctly.
By this time, hopefully, we are left with few DFAs in the set $S_j$.
Here onwards, all DFAs are represented in symbolic form until the end of the algorithm. Therefore, fewer DFAs in $S_j$ implies fewer symbolic products need to be performed, and hence limits the blow-up in state-space of the final DFA.
 This way, our algorithm balances the strengths of both approaches, mitigates their individual drawbacks, and efficiently generates a small DFA, if not the minimal.

We now describe the two heuristics, namely
{\em dynamic smallest-first composition of DFAs} and {\em selective DFA minimization} abbreviated to DSF and SDM, respectively.

We first discuss DSF, which is used to decide which two DFAs should be composed in each iteration.
We observe that the order in which intersection of DFAs is performed does not affect the correctness of the final DFA since both Boolean conjunction and DFA intersection are associative and commutative operations.
In theory, we can design any criteria to select two DFAs to be composed at each iteration.
In practice, a careless choice of the two DFAs may produce an unnecessarily large intermediate DFA that causes the algorithm to fail at the composition phase due to the large memory footprint.
Therefore, we aim to find an order that can  optimize time and space in the composition phase.
To help with that we use DSF, which as the name suggests chooses the smallest two DFAs in each iteration.
The DFAs with explicit states are chosen based on the number of states, while the DFAs with symbolic-state representation are chosen based on the number of nodes in the BDD representation of the transition function.
The intuition behind this heuristic is that if the algorithm would fail on the composition of the smallest two DFAs in that iteration, then it would probably fail on the composition of all other pairs of DFAs as well.

Next we discuss SDM, which decides when it is beneficial to perform DFA minimization after the intersection of DFAs in each iteration.
DFA minimization has been proved to be critical to the performance of DFA generation in~\cite{henriksen1995mona} as it helps in maintaining a smaller number of states, which is also one of our critical parameters.
However, it is also an expensive operation.
Currently, the best known complexity for  minimization are $\mathcal{O}(n\log n)$ and  $\mathcal{O}(n^2)$ for explicit- and symbolic-state representations, respectively~\cite{hopcroft1971n,wimmer2006sigref}. Therefore, there is a tension between reducing the number of states and achieving efficiency.
To resolve this, we conducted an empirical study to evaluate the effect of  minimization. We observed that in most cases, minimization reduces the number of states by 2-3 times. While this is significant when the states are represented explicitly, in symbolic-state representation this leads to a reduction in 1-2 state variables only.
Therefore, we adhere to the SDM heuristic in which we minimize intermediate DFAs in explicit-state representation only.
There are two advantages to this.
First, since minimization is performed on explicit-state representation only, by virtue of our algorithm design this occurs only when the DFAs are small. For these, the time spent in minimization is so low that it is worth maintaining minimal DFAs.
Second, by maintaining minimal DFAs in the explicit-form, the algorithm delays the switch over to symbolic form as the DFA sizes take longer to reach the thresholds. This leads to fewer symbolic products, which results in curbing the amount of blow-up in state-space.

A semi-formal description of the steps of the algorithm are given below. The complete formal description has been deferred to the Appendix.

\vspace{-0.1cm}
\subsubsection{Step 0. (Initial)}

We are given input formula $\varphi = \bigwedge_{i=1}^n \varphi_i$, and {\em switch-over threshold values} $t_1, t_2 > 0$.
The parameters $t_1$ and $t_2$ correspond
to the thresholds for the numbers of states in an individual DFA and in the product of two DFAs, respectively, to trigger the symbolic representation.

\vspace{-0.1cm}
\subsubsection{Step 1. (Decomposition)}
Construct the minimal DFA $D_i$ in explicit-state representation for all $i \in \{1,\dots, n\}$.
Create the set $S_1 = \{D_1,\dots, D_n\}$.

\vspace{-0.1cm}
\subsubsection{Step 2. (Explicit-state composition)}

For $j \in \{1,\dots, n-1\}$, let $S_j = \{M_1,\dots, M_{n-j+1}\}$ be the set of DFAs in the $j$-th iteration.

If $S_j$ has only one DFA, return that as the solution.

Otherwise, if the DFAs in $S_j$  become too large, proceed to Step 3. Assume w.l.o.g. that $M_1$ and $M_2$ are the two DFAs chosen by the DSF heuristic. Let $|A|$ denote the number of states in a DFA $A$ represented in explicit-state form.
If $\min(|M_1|, |M_2|) > t_1$ or $(|M_1|\cdot |M_2|) > t_2$, move to Step 3.  Let $k$ be the iteration in which this occurs, i.e. when $j = k$.

Otherwise, as per SDM, construct DFA $P$ by minimization of $M_1 \cap M_2$. Then, create $S_{j+1} = \{P, M_3,\dots, M_n\}$ for the next iteration, and repeat Step 2.

\vspace{-0.1cm}
\subsubsection{Step 3. (Change state representation)}

Convert all DFAs in $S_k = \{M_1,\dots, M_{n-k+1}\}$ from explicit-state  to symbolic-state representation, and proceed to Step 4. Note that the state space of each DFA $M_i$ is encoded symbolically using a different set of state variables $\varset{Z}_i$, where all $\varset{Z}_i$ are disjoint. Since no more minimization occurs after this point, the total set of state variables $\varset{Z} = \varset{Z}_1 \cup \ldots \cup \varset{Z}_{n-k+1}$ defines the state space of the final DFA.

\vspace{-0.1cm}
\subsubsection{Step 4. (Symbolic-state composition)}
For $j \in \{k,\dots, n\}$, let $S_j = \{M_1,\dots, M_{n-i+1}\}$ be the set of DFAs in the $j$-th iteration.

If $S_j$ has only one DFA, return that DFA as the solution.

Otherwise, assume w.l.o.g. that $M_1$ and $M_2$ are the two DFAs chosen by the DSF  heuristic. Construct $P = M_1 \wedge M_2$. Recall that, since $M_1$ and $M_2$ are in symbolic form, we do not perform DFA minimization of $P$. Create $S_{i+1} = \{P, M_3,\dots, M_n\}$ for the next iteration, and repeat Step 4.

\section{$\mathsf{LTLf}$ synthesis}
\label{sec:synthesis}

$\mathsf{LTLf}$ synthesis can be reduced to solving a DFA game played on the DFA corresponding to the formula $\varphi$~\cite{de2015synthesis}. As explained in (\textsection~\ref{subsec:dfa-game}), this amounts to computing the set of winning states. If the initial state of the DFA is in this set, then the formula is realizable and a winning strategy can be constructed, otherwise not.

In this section, we describe the winning set computation algorithm on a DFA game when its states are represented symbolically. This is a standard least-fixed point algorithm for reachability games with symbolic state space, and is similar to~\cite{zhu2017ltlfsymbolic,tabajara2019partition}. For sake of completion, we summarize the algorithm here.

Let $\varphi$ be an $\mathsf{LTLf}$ formula over disjoint input and output propositions $\varset{I}$ and $\varset{O}$, respectively, and $\varset{G} = (\mathcal{S}(\varset{Z}), \mathcal{T}(\varset{Z}, \mathsf{Prop}, \varset{Z}'), \mathcal{F}(\varset{Z}))$ be a symbolic DFA for $\varphi$. The DFA game is played on $\varset{G}$. In our case, this DFA is obtained from our hybrid compositional approach (\textsection~\ref{sec:hybrid}), which we assume is in symbolic form, since explicit-state outputs can easily be converted to symbolic form.

To compute the winning set of $\varset{G}$, we compute the least-fixed point of a Boolean formula $W_{i}(\varset{Z})$ that denotes the set of states from which the system can win in at most $i$ steps of the DFA game.
Initially, $W_{0}(\varset{Z})$ is the set  $\mathcal{F}(\varset{Z})$ of accepting states.
At each iteration, the algorithm constructs $W_{i+1}(\varset{Z})$ from $W_{i}(\varset{Z})$ by adding those states from which the system is guaranteed to reach $W_{i}(\varset{Z})$ in one step. Formally,
\[
W_{i+1}(\varset{Z}) = W_{i}(\varset{Z}) \lor (\forall \varset{I}. \exists \varset{O}, \varset{Z}'. \mathcal{T}(\varset{Z}, \varset{I} \cup \varset{O}, \varset{Z}') \land W_{i}(\varset{Z}'))
\]
where $W_{i}(\varset{Z}')$ can be obtained from $W_{i}(\varset{Z})$ by substituting variables $\varset{Z}$ with $\varset{Z}'$.
 This continues until no more states can be added to $W_{i+1}(\varset{Z})$, i.e., until it encounters the first index $i$ such that  $W_{i+1}(\varset{Z}) \equiv W_{i}(\varset{Z})$.
 Since the number of states in the DFA is finite, the algorithm is guaranteed to terminate.
The initial state is present in the winning set, say $W_\mathsf{FP}(\varset{Z})$, if $\mathcal{S}(\varset{Z}) \implies W_\mathsf{FP}(\varset{Z})$ holds. Details on winning-strategy construction has been deferred to~\cite{tabajara2019partition}.

In this work, all Boolean formulas for $\varset{G}$ and all  $W_{i+1}(\varset{Z})$  are represented as BDDs. All boolean operations, quantification and variable substitution are available in standard BDD libraries. Finally, $\equiv$ is a constant time operation in BDDs.

The complexity of solving a DFA game is polynomial in the size of the state space.
Therefore, the efficiency of $\mathsf{LTLf}$ synthesis is heavily affected by the size of the constructed DFA.
Therefore, as our hybrid compositional approach generates small (if not minimal) DFAs, these are suitable for synthesis, as witnessed also by our experimental evaluation.

\section{Experimental evaluation}
\label{sec:exp-eval}

The goal of the empirical analysis is to examine  the performance of our hybrid approach in $\mathsf{LTLf}$-to-DFA generation and  $\mathsf{LTL}$ synthesis against existing tools and approaches

\subsection{Implementation details}
Our hybrid compositional $\mathsf{LTLf}$-to-DFA conversion procedure (\textsection~\ref{sec:hybrid}) has been implemented in a tool called $\mathsf{Lisa}$.
$\mathsf{Lisa}$ has been extended to $\mathsf{LisaSynt}$  to perform $\mathsf{LTLf}$ synthesis using the winning strategy computation described in (\textsection~\ref{sec:synthesis}).

$\mathsf{Lisa}$ takes an $\mathsf{LTLf}$ formula and switch-over thresholds  $t_1$, $t_2$ as inputs,  and outputs a corresponding DFA with symbolic states. The output may not be minimal.
For the same inputs, $\mathsf{LisaSynt}$ internally invokes $\mathsf{Lisa}$, solves the DFA game given by $\mathsf{Lisa}$'s output, and returns whether the formula is realizable. If so, it can also return a winning strategy.

$\mathsf{Lisa}$ and $\mathsf{LisaSynt}$ have been written in C++.
They employ $\mathsf{BuDDy}$~\cite{BuDDypakage} as their BDD library for the symbolic representations and operations on DFAs, and  take advantage of dynamic variable ordering for the BDDs.

To generate explicit-state minimal DFAs in the decomposition phase,
$\mathsf{Lisa}$ uses $\mathsf{Spot}$~\cite{duret2016spot} and the $\mathsf{Mona}$-based method~\cite{henriksen1995mona}.
It borrows the rich APIs from $\mathsf{Spot}$ to conduct DFA intersection and minimization in the explicit-state composition phase.
Per se, $\mathsf{Spot}$ APIs are available for $\omega$-automata (automata over infinite words). In order to use the $\mathsf{Spot}$ API for operations over DFAs, $\mathsf{Lisa}$
stores intermediate explicit DFAs as a {\em weak deterministic B\"uchi automata }(wDBA)~\cite{dax2007mechanizing}.
Intuitively, if the DFA accepts the language $\L$, then its wDBA accepts the language $\L\cdot(\{\mathsf{loop}\})^\omega$, where $\mathsf{loop}$ is a fresh variable not present in $\mathsf{Prop}$.
The wDBA can be constructed from the DFA for $\L$ by making the following changes (a) add a new state $\mathsf{sink}$, (b) for each accepting state in the DFA, add a transition from that state to $\mathsf{sink}$ on $\mathsf{loop}$, (c) add a transition from  $\mathsf{sink}$ to itself on $\mathsf{loop}$ , (d) make $\mathsf{sink}$ the only accepting state in the wDBA. This automaton accepts a word iff its run visits $\mathsf{sink}$ infinitely often.
Since wDBA is an $\omega$-automaton, we use $\mathsf{Spot}$ APIs for wDBAs to conduct intersection and minimization, both of which return a wDBA as output, in the similar complexity for those operations in a DFA~\cite{dax2007mechanizing,Kupferman18}.
Lastly, a wDBA for language $\L\cdot(\{\mathsf{loop}\})^{\omega}$ can be easily converted back to a DFA for language $\L$.

\subsection{Design and setup for empirical evaluation \footnote{The source code of our tool is publicly available at \url{https://github.com/vardigroup/lisa}}\footnote{Figures are best viewed online in color.}}

The evaluation has been designed to compare
the performance of $\mathsf{Lisa}$ and $\mathsf{LisaSynt}$ to their respective existing tools and approaches.
$\mathsf{LTLf}$-to-DFA conversion tools are compared on runtime, number of benchmarks solved, hardness of benchmarks solved (size of minimal DFA) and the number of state variables in the output DFA. $\mathsf{LTLf}$ synthesis tools are compared on runtime and the number of benchmarks solved.
We conduct our experiments on a benchmark suite curated from prior works, spanning classes of realistic and synthetic benchmarks. In total, we have 454 benchmarks split into four classes: random conjunctions (400 cases)~\cite{zhu2017ltlfsymbolic}, single counters (20 cases), double counters (10 cases) and Nim games (24 cases)~\cite{tabajara2019partition}. More details on each class can be found in the Appendix.

\begin{table}[t]
\centering

\begin{tabular}{c|c|c|c}
\hline
\multicolumn{1}{|c|}{
\multirow{ 2}{*}{
\textbf{\begin{tabular}[c]{@{}c@{}}\# States in \\ the minimal \\ DFA\end{tabular}}
}
}
& \multicolumn{3}{l|}{\textbf{Number of benchmarks solved}}                                                                                \\ \cline{2-4}
\multicolumn{1}{|c|}{}                                                                                & \textbf{\begin{tabular}[c]{@{}c@{}}Mona-\\ based\end{tabular}} & \textbf{\begin{tabular}[c]{@{}c@{}}Lisa-\\Explicit\end{tabular}} & \multicolumn{1}{c|}{\textbf{Lisa}} \\ \hline

\multicolumn{1}{c|}{$\geq$ 1K}   & 111 & 123 & 137 \\ \hline
\multicolumn{1}{c|}{$\geq$ 5K}   & 70 & 82 & 96 \\ \hline
\multicolumn{1}{c|}{$\geq$ 10K}   & 48 & 60 & 74 \\ \hline
\multicolumn{1}{c|}{$\geq$ 50K}   & 13 & 23 & 35 \\ \hline
\multicolumn{1}{c|}{$\geq$ 100K}   & 8 & 16 & 26 \\ \hline
\multicolumn{1}{c|}{$\geq$ 250K}   & 1 & 5 & 12 \\ \hline
\multicolumn{1}{c|}{$\geq$ 500K}   & 0 & 2 & 4 \\ \hline
\multicolumn{1}{c|}{$\geq$ 750K}   & 0 & 2 & 2 \\ \hline
\multicolumn{1}{c|}{Size unknown} & -- & -- & 21** \\ \hline
\multicolumn{1}{c|}{\textbf{Total solved}}   & \textbf{307} & \textbf{338} & \textbf{372} \\ \hline
\end{tabular}
\caption{DFA construction. Hardness of benchmarks is measured by the size of minimal DFA. **Note: There are 34 benchmarks that were solved only by $\mathsf{Lisa}$. Of these, we were able to identify the size of the minimal DFA of 13 benchmarks using a symbolic DFA minimization algorithm~\cite{wimmer2006sigref}. The 21 cases with unknown size are those that could not be minimized even after 24hrs with 190GB.}
\label{table:size}
\vspace{-0.2cm}
\end{table}

\begin{figure}[t]
\centering
\includegraphics[width=0.42\textwidth, trim=1cm 0.8cm 1cm 1cm]{cactusdfa.pdf}
\caption{DFA construction. Cactus plot indicating number of benchmarks each tool can solve for a given timeout.}
\vspace{-0.5cm}
\label{Fig:cactusdfa}
\end{figure}

A good balance between explicit- and symbolic-representation of states is crucial to the performance of $\mathsf{Lisa}$, i.e., it is crucial to carefully choose values of the switch-over thresholds $t_1$ and $t_2$. Recall the switch is triggered if either the smallest minimal DFA has more than $t_1$ states, or if the product of the number of states in the two smallest minimal DFAs is more than $t_2$. Intuitively, we want $t_1$ to be large enough that the switch is not triggered too soon but small enough that conversion of all DFAs from explicit- to symbolic-state representation is not too expensive.  Threshold $t_2$ is closely related to how effective minimization is, and hence depends on the benchmark class. If the benchmark class is such that minimization reduces the DFA size by only 2-3 times, then we would set $t_2$ to be a low value. But if the class is such that minimization reduces DFA size by orders of magnitude, as it does for the Nim game class, we set $t_2$ to a higher value to take advantage of minimization. Currently, these are determined empirically. We set $t_1$ and $t_2$ to 800 and 300000, respectively, for the Nim-game class and to 800 and 2500, respectively, for all other classes.

For experiments on $\mathsf{LTLf}$-to-DFA conversion, we compare $\mathsf{Lisa}$ to
the current-state-of-the-art  $\mathsf{Mona}$-based method ~\cite{zhu2017ltlfsymbolic,camacho2018finite} and two other derivations of $\mathsf{Lisa}$. Recall the $\mathsf{Mona}$-based method is a syntax-driven, explicit-state based approach that returns minimal DFAs. The first derivation is  $\mathsf{Lisa}$-$\mathsf{Explicit}$ which is adapted from $\mathsf{Lisa}$ by setting $t_1=t_2=\infty$.
Therefore, it is a purely explicit-state compositional approach. Like the $\mathsf{Mona}$-based method, it also generates the minimal DFA, but unlike the former it uses the smallest-first heuristic.
The second derivation is
 $\mathsf{Lisa}$-$\mathsf{Symbolic}$, adapted from $\mathsf{Lisa}$ by setting $t_1=t_2=0$.
 This corresponds to the compositional, symbolic-state approach referred to in (\textsection~\ref{Sec:Intro}).

 For experiments on $\mathsf{LTLf}$ synthesis, we compared $\mathsf{LisaSynt}$ to an enhanced version of $\mathsf{Syft}$ (a tool that uses the $\mathsf{Mona}$-based method for DFA conversion)~\cite{zhu2017ltlfsymbolic} that we call $\mathsf{Syft}+$, and the partitioned approach from~\cite{tabajara2019partition}, referred to as $\mathsf{Part}$.
 $\mathsf{Syft}+$ was created by enabling dynamic variable ordering in $\mathsf{Syft}$. This was necessary for a fair comparison as $\mathsf{Syft}$, unlike $\mathsf{LisaSynt}$ and $\mathsf{Part}$, uses static variable ordering. We observed that $\mathsf{Syft}+$ shows upto 75\% reduction in runtime compared to $\mathsf{Syft}$. Note that $\mathsf{Part}$ uses the same symbolic-state approach as $\mathsf{Lisa}$-$\mathsf{Symbolic}$ for constructing the DFAs, except that it skips the composition step, instead performing synthesis directly over the initial set of symbolic DFAs $S_1$.
 Ultimately, it still suffers from the state-space explosion, only in this case it happens during the
 winning-state computation.

All experiments were conducted on a single node of a high-performance cluster. Each node consists of four quad-core Intel-Xeon processor running at 2.6~GHz.
$\mathsf{LTLf}$-to-DFA conversion experiments were run for 1~hour with 8~GB each, $\mathsf{LTLf}$-synthesis experiments for 8~hours with 32~GB each.

\begin{figure}[t]
\centering
\includegraphics[width=0.42\textwidth, trim=1cm 0.8cm 1cm 1cm]{dcdfabar.pdf}
\caption{DFA construction. Runtime for double-counter benchmarks. Plots touching black line means time/memout.}
\vspace{-0.1cm}
\label{Fig:doubledfatime}
\end{figure}

\begin{figure}[!t]
\centering
\includegraphics[width=0.42\textwidth, trim=1cm 0.8cm 1cm 1cm]{dcvarsbar.pdf}
\caption{DFA construction. Number of variables needed to symbolically represent the  DFA's state-space for double-counter benchmarks. No bar indicates time/memout.}
\vspace{-0.5cm}
\label{Fig:doubledfavars}
\end{figure}

\subsection{Observations}

\subsubsection{$\mathsf{Lisa}$ and $\mathsf{Lisa}$-$\mathsf{explicit}$ scale better to larger benchmarks} than the $\mathsf{Mona}$-based method, not just solving more total benchmarks but also being able to handle instances of larger scale (Table~\ref{table:size}).
Between $\mathsf{Lisa}$-$\mathsf{Explicit}$ and $\mathsf{Mona}$, the former is more consistent in solving benchmarks with large minimal DFAs due to the DSF heuristic that enables low memory consumption in intermediate stages.
Finally, $\mathsf{Lisa}$ solves benchmarks with even larger minimal DFAsas it is designed to combine minimal DFAs of explicit state- and succinctness of symbolic-state representation to solve larger formulas.

\subsubsection{$\mathsf{Lisa}$ is the most efficient tool among all four options.} This is clear from the cactus plot in Fig.~\ref{Fig:cactusdfa}.
The plot may seem to indicate that $\mathsf{Lisa}$ only has a slight advantage over $\mathsf{Lisa}$-$\mathsf{Symbolic}$. But, on closer inspection we observe that $\mathsf{Lisa}$-$\mathsf{Symbolic}$ solves most random benchmarks but fares poorly on the realistic ones (see Fig~\ref{Fig:doubledfatime}). This is because they have more sub-specifications, resulting in a large number of symbolic products. The $\mathsf{Mona}$-based method is still the fastest in generating small DFAs (fewer than 50K states) but memouts soon due to explicit-state representation of DFAs. Finally, $\mathsf{Lisa}$-$\mathsf{Explicit}$ is a close second but does not scale as well as $\mathsf{Lisa}$ due to  minimization on very large DFAs. $\mathsf{Lisa}$  has been designed to overcome these deficiencies, and is supported by the current empirical evaluation as well.

\subsubsection{$\mathsf{Lisa}$ mitigates state-space explosion.} Even though $\mathsf{Lisa}$ may not generate the minimal DFAs, we observe that in most cases the state-space of the final DFA produced by $\mathsf{Lisa}$ is one or two variables more than that of the minimal DFA.
This is significantly lower than the number of state variables used by $\mathsf{Lisa}$-$\mathsf{Symbolic}$ (Fig.~\ref{Fig:doubledfavars}). Note that $\mathsf{Lisa}$-$\mathsf{Symbolic}$ fails to solve the double counter benchmarks for $i \geq 7$ (Fig~\ref{Fig:doubledfatime}). Yet we know the number of state variables immediately after Step 3 (\textsection~\ref{sec:hybrid}).
Analyzing the benchmarks, we observed that they were split into 3-200 sub-formulas, yet only 1-3 symbolic products were conducted to construct the DFA.
This demonstrates that our threshold-values are able to
delay the switch-over to symbolic representations and reduce blow-up by the product.
This is why the DFAs generated by $\mathsf{Lisa}$ have comparable sizes to the minimal DFAs.
An important future work, therefore, is to design mechanisms to determine the switch-over thresholds at runtime as opposed to relyng on user-expertise to  assign threshold values.

\subsubsection{$\mathsf{Lisa}$'s small DFAs improve synthesis performance.}
We evaluate for synthesis on non-random benchmarks only, i.e., sequential counters and nim games. We chose to disregard random benchmarks  as their winning set computation time is negligible, as in those benchmarks the fixed point is reached in 2-3 iteration irrespective of the DFA size.
Figure~\ref{Fig:doublesyntime}-\ref{Fig:cactussyn} show that $\mathsf{LisaSynt}$ solves most benchmarks and is the most efficient tool.
We observed that  $\mathsf{Syft}$+ fails because $\mathsf{Mona}$ memouts early, while $\mathsf{Part}$ suffers from state-space explosion. $\mathsf{LisaSynt}$ is resilient to both as $\mathsf{Lisa}$ consumes low memory by virtue of symbolic representation and small state space.

The time consumed inside the winning set computation during synthesis depends on the number of iterations before the fixed-point is reached. Yet, so far not much focus has been given to optimizing this step as the DFAs generated so far have not been large enough for the number of iterations to become an issue.
With $\mathsf{Lisa}$'s ability to construct large DFAs, we were able to observe that the single and double counter benchmarks can spend more than 90\% of the time  in the winning set computation, as the number of iterations is exponential in the number of bits (Appendix).
This provides concrete evidence of the importance of investigating the development of faster algorithms for winning set computation to improve game-based synthesis.

\begin{figure}[t]

\centering
\includegraphics[width=0.42\textwidth, trim=1cm 0.8cm 1cm 1cm]{casesynnonrandom.pdf}
\caption{Synthesis. Number of benchmarks synthesized from each non-random benchmark class.}
\label{Fig:doublesyntime}
\vspace{-0.0cm}
\end{figure}

\begin{figure}[t]

\centering
\includegraphics[width=0.42\textwidth, trim=1cm 0.8cm 1cm 1cm]{cactussyn.pdf}
\caption{Synthesis. Cactus plot  (non-random benchmarks).}
\label{Fig:cactussyn}
\vspace{-0.5cm}

\end{figure}

\section{Concluding remarks}

This work tackles the primary bottleneck in $\mathsf{LTLf}$ synthesis- $\mathsf{LTLf}$ to DFA conversion.
The central problem addressed in this work is the efficient and scalable construction of DFAs with small state space from $\mathsf{LTLf}$ specifications, as a step to $\mathsf{LTLf}$ synthesis.
To the best of our knowledge, ours is the {\em first} {hybrid} approach for DFA construction. Our approach combines explicit- and symbolic-state representations in a manner that effectively leverages their strengths and alleviates their individual shortcomings. Our empirical evaluations on DFA conversion and $\mathsf{LTLf}$ synthesis on $\mathsf{Lisa}$ and $\mathsf{LisaSynt}$ outperform the current states of the art, and demonstrate the merit of our hybrid approach. This indicates promise to further develop and explore hybrid approaches for automaton generation for other specification languages as well, and encourages similar investigations into the other building blocks in synthesis algorithms.

\section*{ Acknowledgments}
We thank A. Camacho, A. M. Wells and S. Zhu for their valuable inputs at different stages of the project. This work is partially supported by NSF grants IIS-1527668, CCF-1704883, IIS-1830549, the National Natural Science Foundation of China (Grant Nos. 61761136011, 61532019), the Guangdong Science and Technology Department (Grant No. 2018B010107004), and the Brazilian agency CNPq through the Ci\^{e}ncia Sem Fronteiras program.

\bibliographystyle{aaai}