# synthesizing_goodenough_strategies_for_ltlf_specifications__6ff819d7.pdf

Synthesizing Good-Enough Strategies for LTLf Speciﬁcations

Yong Li1 , Andrea Turrini1,2 , Moshe Y. Vardi3 and Lijun Zhang1,2

1State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences 2Institute of Intelligent Software, Guangzhou 3Department of Computer Science, Rice University {liyong, turrini,zhanglj}@ios.ac.cn, vardi@cs.rice.edu

We consider the problem of synthesizing goodenough (GE)-strategies for Linear Temporal Logic (LTL) over ﬁnite traces or LTLf for short. The problem of synthesizing GE-strategies for an LTL formula ϕ over inﬁnite traces reduces to the problem of synthesizing winning strategies for the formula ( Oϕ) = ϕ, where O is the set of propositions controlled by the system. We ﬁrst prove that this reduction does not work for LTLf formulas. Then we show how to synthesize GE-strategies for LTLf formulas via the Good-Enough (GE)- synthesis of LTL formulas. Unfortunately, this requires to construct deterministic parity automata on inﬁnite words, which is computationally expensive. We then show how to synthesize GE-strategies for LTLf formulas by a reduction to solving games played on deterministic B uchi automata, based on an easier construction of deterministic automata on ﬁnite words. We show empirically that our specialized synthesis algorithm for GE-strategies outperforms the algorithms going through GE-synthesis of LTL formulas by orders of magnitude.

1 Introduction Reactive synthesis is the automated construction of a reactive system from a given speciﬁcation ϕ [Church, 1957], typically written as a Linear Temporal Logic (LTL) formula over a set of input signals I and a set of outputs O [Pnueli, 1977]. Reactive synthesis can be used to solve a number of different problems in AI, in particular planning. For instance, several variants of conditional planning problems with fully observability can be reduced to LTL synthesis problems, see, e.g., [Aminof et al., 2019; Camacho et al., 2019]. The task of synthesis is to construct a system M such that for each inﬁnite input sequence α (2I)ω, M is able to output, in a step-by-step fashion, an output sequence M(α) such that the combined input and output sequence satisﬁes ϕ, i.e., α M(α) |= ϕ [Pnueli and Rosner, 1989]. The extracted system M is a winning strategy. The synthesis problem of winning strategies for an LTL formula ϕ has been proved to be 2EXPTIME-complete and it is usually reduced to solving a game between the environment controlling the input signals and the system control-

ling the output, on a deterministic Parity automaton (DPA) representing ϕ [Pnueli and Rosner, 1989]. The requirement for constructing a system producing a satisfying computation of ϕ for each input sequence α is, however, sometimes too strong and unrealistic: there may be input sequences making ϕ unsatisﬁable, whatever the outputs are. Therefore, researchers have proposed [Almagor and Kupferman, 2020; Damm and Finkbeiner, 2011] to relax this requirement and focused on synthesizing a system that makes best effort to respond to the input signals from the environment, which is termed as the good-enough (GE) synthesis in [Almagor and Kupferman, 2020]. More precisely, for GEsynthesis, the synthesized system M is required to output a sequence M(α) such that α M(α) |= ϕ whenever possible. That is, if there does not exist an output sequence β such that α β |= ϕ, M can just respond with an arbitrary output sequence. We call such a system a good-enough (GE)-strategy. The synthesis problem of GE-strategies for LTL formulas has been reduced to the synthesis of winning strategies for the formula ( Oϕ) = ϕ [Almagor and Kupferman, 2020; Damm and Finkbeiner, 2011], where the assumption Oϕ restricts us to the input sequences that can be combined with an output sequence such that the resultant sequences satisfy ϕ. More precisely, given a formula ϕ with free input/environment variables I and free output/system variables O, Oϕ is the formula where only input variables in ϕ are left free, while output variables are existentially quantiﬁed; Oϕ stands for o1 okϕ, where O = {o1, . . . , ok} and k 1, and it has the same meaning as in standard ﬁrst order logic. We refer to [Sistla et al., 1987] for more details of LTL with (existential) and (universal) quantiﬁers. In recent years, the version of LTL over ﬁnite traces [Baier and Mc Ilraith, 2006; De Giacomo and Vardi, 2013], or LTLf for short, emerged as another popular logic for speciﬁcations, because many settings, such as planning [Baier and Mc Ilraith, 2006], assume that an execution stops after the speciﬁcation has been achieved; we refer to [De Giacomo and Vardi, 2013] for more applications of LTLf in AI. Later, synthesizing winning strategies for an LTLf formula ϕ was proved to be 2EXPTIME-complete and can be reduced to solving a game played on a deterministic ﬁnite automaton (DFA) accepting ϕ [De Giacomo and Vardi, 2015]. LTLf synthesis has since then found applications in specifying task plans in robotics [He et al., 2017; Lahijanian et al., 2015], business

Proceedings of the Thirtieth International Joint Conference on Artiﬁcial Intelligence (IJCAI-21)

processes [Pesic et al., 2010], and more. This work looks into the synthesis problem of GEstrategies for LTLf formulas. Our contributions are threefold and summarized as follows. First, we show that the reduction idea in the LTL setting to the synthesis of winning strategies for the formula ( Oϕ) = ϕ does not work for LTLf formulas. Second, we show that synthesizing GE-strategies for LTLf formulas can be reduced to the synthesis for LTL formulas. In practice, however, solving LTLf synthesis via a translation to LTL cannot compete with native approaches specialized for LTLf formulas, as shown in [Zhu et al., 2017; Wells et al., 2020]. This is because in practice, DFAs are expressive enough to accept the language of an LTLf formula and specialized algorithms for constructing automata on ﬁnite words are easier and more efﬁcient than those for building automata on inﬁnite words for an LTL formula [Zhu et al., 2017; Wells et al., 2020]. Moreover, LTL synthesis requires solving parity (DPA) games, while LTLf synthesis only depends on solving DFA games; it is known that solving a DFA game is much easier than solving a DPA game between the environment and the system, since DFA games are solvable in polynomial time [Mazala, 2002], while whether DPA game is doable in polynomial time is still an open problem [Calude et al., 2017]. Therefore, it is of importance to obtain a specialized algorithm for the synthesis of GE-strategies for LTLf formulas to achieve better scalability. Third, and our main contribution, we propose to synthesize GE-strategies for LTLf formulas by a reduction to solving a game played on deterministic B uchi automata, based on construction of DFAs. We also prove that the problem of synthesizing GEstrategies for LTLf formulas is 2EXPTIME-complete. Moreover, we conduct a comprehensive empirical evaluation on benchmarks from synthesis competitions and literature. We show that our speciﬁc synthesis algorithm for GE-strategies outperforms the algorithm going through GE-synthesis of LTL formulas by orders of magnitude, regarding the runtime and the number of solved cases.

2 Preliminaries

2.1 Linear Temporal Logic over Finite Traces We focus here on Linear Temporal Logic over ﬁnite traces (LTLf) [Baier and Mc Ilraith, 2006; De Giacomo and Vardi, 2013], which is a variant of LTL [Pnueli, 1977] with the same syntax but it is interpreted over ﬁnite instead of inﬁnite traces. The syntax of an LTLf formula over a ﬁnite set of propositions P is deﬁned as ϕ ::= a P | ϕ | ϕ ϕ | ϕ ϕ | Xϕ | ϕUϕ | Fϕ | Gϕ. Here X (strong Next), U (Until), F (Finally/Eventually), and G (Globally/Always) are temporal operators interpreted over ﬁnite traces. Note that X is a strong next operator such that Xϕ requires the tail of the ﬁnite trace to satisfy ϕ, while we use N to denote the weak next operator such that Nϕ demands that if the tail of the ﬁnite trace is not empty, then it satisﬁes ϕ. Consequently, Nϕ := X ϕ. The negation of an LTLf formula ϕ, i.e., ϕ is also an LTLf formula. As usual, true and false represent a tautology and a falsum, respectively. We denote by |ϕ| the length of ϕ, i.e., the number of temporal operators and connectives in ϕ. We refer interested readers to [Pnueli, 1977] and [De Giacomo

and Vardi, 2013] for the semantics of LTL and LTLf, respectively. The language of an LTL/LTLf formula ϕ, denoted as L(ϕ), is the set of inﬁnite/ﬁnite words over 2P that satisfy ϕ.

2.2 NFA, DFA, DBA, and DPA

A nondeterministic ﬁnite automaton (NFA) is a tuple A = (Σ, S, ι, , F), where S is a ﬁnite set of states, ι S is the initial state, : S Σ 2S is the nondeterministic transition function, and F S is the set of accepting states. A run of A on a word u = u0u1 un Σ is a sequence of states ρ = s0 sn+1 S+ such that s0 = ι and si+1 (si, ui) holds for all i {0, . . . , n}. The run ρ is accepting if sn+1 F. A accepts a word u if there is an accepting run of A on u. The language L(A) of A is the set of all accepted words. An NFA D is said to be a deterministic ﬁnite automaton (DFA) if for each s S and a Σ, | (s, a)| 1, i.e., we have : S Σ S. For an LTLf formula ϕ one can construct, with a singleexponential blow-up, an NFA A over the alphabet Σ = 2P from ϕ such that L(A) = L(ϕ) [De Giacomo and Vardi, 2013]. An NFA A can be converted into an equivalent DFA D with an exponential blowup by subset construction (see, e.g., [Hopcroft et al., 2007]). Consequently, an LTLf formula ϕ can be converted to a DFA D whose number of states is at most doubly exponential in the size of ϕ. A deterministic B uchi automaton (DBA) is a tuple B = (Σ, S, ι, , F) as in the deﬁnition of DFAs; the difference lies in the fact that a DBA only accepts inﬁnite words. The run of B on u = u0u1 un Σω is the inﬁnite sequence ρ = s0 sn+1 Sω of states such that s0 = ι and si+1 = (si, ui) holds for all i 0. ρ is accepting if ρ visits some state in F inﬁnitely many times. B accepts an inﬁnite word u if the run of B on u is accepting. The language L(B) of B is the set of all accepted inﬁnite words. A deterministic Parity automaton (DPA) is a tuple P = (Σ, S, ι, , p), where S, ι and are as in DBAs while p: S N is a function deﬁning the acceptance condition. The run ρ of P over u is accepting if the minimal color induced by p occurring inﬁnitely often in ρ is even. Note that one can construct a DPA P for every LTL formula ϕ such that L(P) = L(ϕ), while there exists an LTL formula ψ such that no DBA accepts L(ψ) [Baier and Katoen, 2008].

2.3 Winning and Good-Enough Strategies

Let A and B be two ﬁnite sets and α = a0, a1, and β = b0, b1, be two ﬁnite/inﬁnite words over 2A and 2B, respectively. We denote by α β the combined word (a0 b0), (a1 b1) over 2A B and by α β the reduced word (a0 \ b0), (a1 \ b1) over 2A\B, provided that α, β are of the same length. We denote by α[i] the element ai of α and we use α[i..k] to denote the subword of α between ai and ak, included, when i k and the empty word ε when i > k; lastly, we denote by α[i..] the sufﬁx of α starting from ai. In this work we consider LTL/LTLf formulas over P = I O, where I and O are two disjoint sets of propositions/variables. The set of input variables I is controlled by the environment while the set of output variables O is controlled by the system. A strategy γ is a total function

Proceedings of the Thirtieth International Joint Conference on Artiﬁcial Intelligence (IJCAI-21)

γ : (2I)+ 2O. For every word α = I0, I1, (2I)ω of interpretations over I, the strategy γ induces the word (I0 γ(I0)), (I1 γ(I0, I1)), . . . , (Im γ(I0, . . . , Im)) (2P)ω of interpretations over P, which we call the computation induced by γ on α, denoted as α γ(α). Deﬁnition 1 (Winning strategy). Let γ be a strategy. (1) γ is a winning strategy for an LTL formula ϕ if for every inﬁnite word α = I0, I1, (2I)ω of interpretations over I, the computation α γ(α) satisﬁes ϕ. (2) γ is a winning strategy for an LTLf formula ϕ if for every inﬁnite word α = I0, I1, (2I)ω of interpretations over I, there exists an integer m 0 such that α[0..m] γ(α)[0..m] satisﬁes ϕ. Intuitively, for an LTLf formula ϕ, the environment, controlling the input variables, provides an unbounded sequence of inputs α; a strategy γ, in order to be winning for ϕ, must generate an appropriate sequence of output variables γ(α) such that, once combined with α as α γ(α), there is a ﬁnite preﬁx of α γ(α) of length m + 1 that satisﬁes ϕ. We say that ϕ is realizable if there is a winning strategy for ϕ. The problem of LTL synthesis [Pnueli and Rosner, 1989] is to decide whether ϕ is realizable and construct a winning strategy if so. Intuitively, LTL synthesis can be regarded as a DPA game corresponding to ϕ [Pnueli and Rosner, 1989] played between an external environment and the desired system that take turns to assign values to input and output propositions, respectively. The game is won by the system if we can construct a winning strategy guaranteeing that the resultant inﬁnite input-output sequence satisﬁes ϕ. Similarly, the problem of LTLf synthesis is to decide whether the LTLf formula ϕ is realizable and to construct a winning strategy if so. Different from that of LTL formulas, LTLf synthesis for ϕ can be reduced to solving a game between the system and the environment played on a DFA accepting ϕ [De Giacomo and Vardi, 2015], rather than on a DPA. In practice, however, it is not always possible to construct a winning strategy for the system. For instance, let ϕ = Fi Fo where i and o are input and output variables, respectively. ϕ requires the computation to make both i and o eventually hold, in no predeﬁned order. There is no winning strategy since the environment can generate i all the time. As proposed in [Damm and Finkbeiner, 2011; Almagor and Kupferman, 2020], one can relax the goal for winning strategies and aim to obtain the best strategy we can get among all alternative strategies. We call such strategy a good-enough (GE)-strategy and extend this notion to LTLf. Let α (2I)ω: for an LTL formula ϕ, α is said to be ϕhopeful if there exists an inﬁnite word β (2O)ω such that α β |= ϕ; for an LTLf formula ϕ, we say that α is ϕ-fhopeful if there exists an integer m 0 and a ﬁnite word β = O0 Om (2O)+ such that α[0..m] β |= ϕ. Deﬁnition 2 (Good-enough (GE)-strategy). Let γ be a strategy. (1) γ is a GE-strategy for an LTL formula ϕ if for every ϕ-hopeful inﬁnite input word α (2I)ω, we have that α γ(α) |= ϕ. (2) γ is a GE-strategy for an LTLf formula ϕ if for every ϕ-f-hopeful input word α (2I)ω, there exists an integer m 0 such that α[0..m] γ(α)[0..m] |= ϕ. The problem of good-enough (GE) LTL synthesis [Almagor and Kupferman, 2020] is to decide whether there ex-

ists a GE-strategy γ for ϕ and construct γ if so. We say a strategy γ GE-realizes ϕ if γ is a GE-strategy for ϕ; we also say that ϕ is GE-realizable if there exists a GE-strategy for ϕ. Analogous notions extend to LTLf formulas as below.

Deﬁnition 3 (GE-synthesis for LTLf formulas). The goodenough (GE)-synthesis problem for LTLf formulas is to decide whether there exists a GE-strategy γ for a given LTLf formula ϕ and construct γ if so.

Clearly, a winning strategy is a GE-strategy; a GE-strategy, however, is not necessarily a winning strategy since, e.g., ϕ = Fi Fo is not realizable but has a GE-strategy that outputs o at least once. We have the following result about the synthesis of GE-strategies for LTL.

Theorem 1 ([Almagor and Kupferman, 2020]). The problem of the GE-synthesis for an LTL formula ϕ can be reduced to ﬁnding a winning strategy γ for the formula ( Oϕ) = ϕ. Moreover, we can construct a DPA accepting the language of the formula ( Oϕ) = ϕ with a doubly exponential blow-up with respect to |ϕ|.

Thus we can reduce the GE-synthesis problem for the LTL formula ϕ to the game played on a DPA for ( Oϕ) = ϕ. Intuitively, for each inﬁnite word α (2I)ω, the computation α γ(α) induced by the winning strategy γ for ( Oϕ) = ϕ satisﬁes either O ϕ or ϕ, i.e., either α is not ϕ-hopeful or α γ(α) |= ϕ when α is ϕ-hopeful, respectively. Consequently, a winning strategy γ for the formula ( Oϕ) = ϕ is a GE-strategy for ϕ.

3 Good-Enough Synthesis for LTLf Formulas

In this work, we study the problem of good-enough synthesis for LTLf formulas, i.e., synthesizing a GE-strategy for a given LTLf formula ϕ over P = I O, whenever possible.

3.1 Reduction to ( Oϕ) = ϕ Does Not Work for LTLf Formulas As aforementioned, the GE-synthesis problem for an LTL formula ϕ can be reduced to a game played on a DPA for the formula ( Oϕ) = ϕ. One may wonder whether the GE-synthesis problem for an LTLf formula ϕ can analogously be reduced to a game played on a DFA for the formula ( Oϕ) = ϕ. Unfortunately, this is not the case, since the ﬁnite trace semantics of LTLf can be exploited to synthesize a strategy γ for ( Oϕ) = ϕ that does not work for ϕ, as formalized by Theorem 2 below.

Theorem 2. There is an LTLf formula ϕ such that a winning strategy for the formula ( Oϕ) = ϕ is not necessarily a GE-strategy for ϕ.

For LTL formulas, the reduction to ( Oϕ) = ϕ works because LTL is interpreted over inﬁnite words. Thus, the quantiﬁed LTL formula Oϕ [Sistla et al., 1987], as an assumption, naturally allows us to focus only on the ϕ-hopeful inﬁnite input words, while for LTLf formulas, the quantiﬁed LTLf formula Oϕ is interpreted over ﬁnite words over 2I. In particular, the assumption Oϕ restricts us to ﬁnite input words over 2I rather than the ϕ-f-hopeful words. The deﬁnition of GE-synthesis for LTLf formulas, however, is deﬁned

Proceedings of the Thirtieth International Joint Conference on Artiﬁcial Intelligence (IJCAI-21)

with respect to inﬁnite sequences over 2I. Consequently, we cannot reduce the synthesis of a GE-strategy for the LTLf formula ϕ to the synthesis of the winning strategy for the quantiﬁed LTLf formula ( Oϕ) = ϕ. Example 1. An LTLf formula justifying Theorem 2 is ϕ = Fi Fo, where i and o are the input and output variables, respectively. There are GE-strategies for ϕ, such as the one outputting o on seeing the input i or the one continuously outputting o. There are, however, also winning strategies for Oϕ = ϕ that are not GE-strategies for ϕ, such as the one that outputs o/ o if the ﬁrst input is i/ i, respectively, and then only outputs o.

3.2 Good-Enough Synthesis as Reduction to LTL As shown by [De Giacomo and Vardi, 2013], given an LTLf formula ϕ over P, one can construct an LTL formula t(ϕ) over propositions P {tail} in linear time, where tail / P is a fresh variable, such that ϕ is satisﬁable if and only if t(ϕ) is satisﬁable. That is, one can reduce the LTLf satisﬁability of ϕ to the LTL satisﬁability of t(ϕ). The variable tail is used to indicate when a ﬁnite word in L(ϕ) terminates. The resulting LTL formula t(ϕ) has the following language. Lemma 1 ([De Giacomo and Vardi, 2013]). L(t(ϕ)) = { λ {tail} | λ L(ϕ) } (2P)ω. Intuitively, given a ﬁnite word u L(ϕ), tail holds for the ﬁrst |u| positions and tail holds forever afterwards. For synthesis, the fresh proposition tail / P is under the control of the system. It is further shown in [Zhu et al., 2017] that this reduction also works for LTLf realizability and synthesis, i.e., ϕ is realizable if and only if t(ϕ) is realizable; also, a winning strategy for t(ϕ) yields a winning strategy for the LTLf formula ϕ. We now show that this reduction works also for the GE-synthesis for LTLf formulas.

Lemma 2. Let ϕ be an LTLf formula and α (2I)ω. Then α is ϕ-f-hopeful if and only if α is t(ϕ)-hopeful. Lemma 3. Let ϕ be an LTLf formula. Then (1) ϕ is GErealizable iff t(ϕ) is GE-realizable; and (2) a GE-strategy γ for t(ϕ) is also a GE-strategy for ϕ. We present now the main result of this subsection, which is a direct consequence of Lemma 3. Theorem 3. The GE-synthesis problem for an LTLf formula ϕ with respect to I, O can be reduced to the GE-synthesis problem for the LTL formula t(ϕ) with respect to I, O {tail} . Thanks to Theorem 3, we can reduce the GE-synthesis problem for LTLf formulas to the GE-synthesis problem for LTL formulas. This reduction, however, is not computationally competitive when compared with our specialized synthesis algorithm for LTLf formulas, given below in Section 3.3, as experiments show (cf. Section 4).

3.3 Synthesizing GE-Strategies for LTLf Formulas via DBA Games By Theorem 2, for LTLf formulas, the problem of GEsynthesis for ϕ cannot be reduced to the classical synthesis problem for ( Oϕ) = ϕ. Nonetheless, due to

Lemma 3, we can just synthesize a winning strategy γ for (O {tail})t(ϕ) = t(ϕ), since γ is also a GE-strategy for the LTLf formula ϕ. The key issue with this approach is that one has to, directly or indirectly, construct a DPA for the formula (O {tail})t(ϕ) = t(ϕ), which is generally believed to be the main bottleneck of the synthesis procedure [Kupferman, 2012]. Our key observation for the synthesis of a GE-strategy for an LTLf formula is that we can construct a DBA accepting the language of (O {tail})t(ϕ) = t(ϕ) based on the construction of NFAs and DFAs from ϕ. This allows us to exploit algorithms, specialized for LTLf, for constructing automata on ﬁnite words, which are easier and more efﬁcient in practice than those building automata on inﬁnite words [Zhu et al., 2017; Wells et al., 2020]. In the remainder of the section we show how this is achieved; we start by formalizing the language of (O {tail})t(ϕ) = t(ϕ), following directly from Lemma 2 since t(ϕ) is an LTL formula and ( (O {tail})t(ϕ)) (O {tail}) t(ϕ) recognizes the inﬁnite words over I that are not t(ϕ)-hopeful. Lemma 4. Let ϕ be an LTLf formula; then it holds that L( (O {tail})t(ϕ) = t(ϕ)) = L(t(ϕ)) { α (2I)ω | α is not ϕ-f-hopeful }. In the following, we show that instead of constructing a DPA for L(t(ϕ)) { α (2I)ω | α is not ϕ-f-hopeful }, we can construct a DBA accepting it. Consequently, the problem of synthesizing a GE-strategy for ϕ is reduced to solving a game played on a DBA B rather than on a DPA, which is much easier to solve [Mazala, 2002]. In order to construct the desired DBA B, we ﬁrst build a DBA B1 for L(t(ϕ)), which accounts for the situation where a GE-strategy must generate a computation satisfying ϕ on a given ϕ-f-hopeful input sequence. Then we build a DBA B2 for { α (2I)ω | α is not ϕ-f-hopeful }. Finally, we take their union product B accepting exactly the computations for synthesizing GE-strategies. Theorem 4. Let γ be a winning strategy for the system that produces computations in L(B) = L(B1) L(B2). Then γ is a GE-strategy for ϕ.

3.4 DBA Construction We show how to construct the DBAs B1, B2, and B in detail.

Construction of B1 In order to construct the DBA B1 accepting all computations generated by a GE-strategy on a given ϕ-f-hopeful inﬁnite input sequence, which clearly satisfy ϕ, we ﬁrst construct a DFA D accepting L(ϕ), with a doubly exponential blowup [De Giacomo and Vardi, 2015]. Then we get the DBA B1 from D so that it accepts the language { λ {tail} | λ L(ϕ) = L(D) } (2P)ω, where tail is a fresh variable not present in P. Note that in the DBA game, the fresh variable tail is controlled by the system as an output variable. Deﬁnition 4. Let D = (2P, S, ι, , F) be the DFA for ϕ. Then the DBA B1 is the tuple (2P {tail}, S1, ι1, 1, F1), where S1 = S { } with / S being a fresh state, ι1 = ι is the initial state, F1 = { } is the set of accepting states, and 1 is deﬁned as follows: (1) if (q, a) = q , then

Proceedings of the Thirtieth International Joint Conference on Artiﬁcial Intelligence (IJCAI-21)

1(q, a {tail}) = q ; (2) if q F, then 1(q, a) = for each a 2P; and (3) 1( , a) = for each a 2P. Note that the transition function 1 may be undeﬁned for some state q S1 and assignment a (2P {tail}). Intuitively, in Deﬁnition 4, we just use tail to mark when a ﬁnite word in L(ϕ) terminates. Since the number of states in D is at most doubly exponential in the length of ϕ [De Giacomo and Vardi, 2015], we directly obtain the following result. Lemma 5. Let B1 be the DBA constructed in Deﬁnition 4. Then L(B1) = { λ {tail} | λ L(ϕ) } (2P)ω and B1 has 22O(|ϕ|) states.

Construction of B2 We now construct the DBA B2 that accepts all inﬁnite sequences λ (2I)ω for which no strategy can generate a computation satisfying ϕ. That is, L(B2) = { α (2I)ω | α is not ϕ-f-hopeful }. To construct the DBA B2, we take the following three steps. Step 1. Construct an NFA N accepting L(ϕ) with a single exponential blow-up [De Giacomo and Vardi, 2015] and then make all accepting states of N sink accepting states with a self-loop transition labeled with true = 2P {tail}. Thus we have that L(N) = L(ϕ) true and N has 2O(|ϕ|) states. Step 2. Existentially quantify out all O-variables on the transitions of N and let N be the resultant NFA. Let and be the transition functions of N and N , respectively. Then if q (q, a) for a 2P, then we have that q (q, a \ O). We then treat the modiﬁed NFA N as an NBA A. Intuitively, the NBA A accepts all input sequences α = I0, I1, (2I)ω that are ϕ-f-hopeful. That is, we have that L(A) = { α (2I)ω | α is ϕ-f-hopeful }. Then we just need to complement the NBA A at the next step since the desired DBA B2 accepts the complementary language of A. Note that all accepting states of A are sink states with a self-loop on true. Step 3. Determinize the NBA A with a standard subset construction [Hopcroft et al., 2007] and set all states that do not contain a sink accepting state of A as accepting states, which yields the DBA B2, which we assume without loss of generality to be complete. Since all accepting states of A are sink states, all states reachable from a nonaccepting state of B2 will also be nonaccepting, which makes it possible to complement the NBA A with a simple subset construction and then to reverse the set of accepting states. Note that complementing general NBAs is much more complicated and expensive [Vardi, 2007; Yan, 2008] than a subset construction. Intuitively, B2 accepts all inﬁnite sequences α (2I)ω that are not ϕ-f-hopeful, i.e., no strategy at all can generate a computation for α that satisﬁes ϕ. Lemma 6. Let B2 be the DBA constructed above for ϕ. Then L(B2) = { α (2I)ω | α is not ϕ-f-hopeful } and B2 has 22O(|ϕ|) states.

Construction of B The DBA B is then the union product of B1 and B2 such that L(B) = L(B1) L(B2). Since the accepting states in B1 and B2 are sink states, we can just compute the union product as

it is done for DFAs [Hopcroft et al., 2007]. Let B1 = (2P {tail}, S1, ι1, 1, F1) and B2 = (2I, S2, ι2, 2, F2). Then we have B = (2P {tail}, S1 S2, (ι1, ι2), 1 2, (S1 F2) (F1 S2)). We remark that this union product can be efﬁciently performed symbolically.

Strategy Extraction To extract a winning strategy for the system on the DBA B, we use a DBA game solving algorithm, working in polynomial time with respect to the number of states of B [Mazala, 2002]. The algorithm determines whether from the initial state the system is sure to win the game. In this case, a winning strategy is given as a Mealy machine producing the appropriate system s output for the current state and input. See [Mazala, 2002] for more details about solving DBA games and extracting winning strategies.

3.5 Correctness and Complexity Theorem 5. Let ϕ be an LTLf formula and B the DBA constructed in Section 3.4. (1) There exists a winning strategy for the DBA game played on B if and only if ϕ is GE-realizable. (2) A winning strategy γ for the DBA game played on B is also a GE-strategy for ϕ. It is clear that the LTLf GE-realizability/GE-synthesis problem is in 2EXPTIME. Similarly to [Rosner, 1991, Section 3.2] in the LTL setting, one can also construct from a given 2EXPTIME Turing machine M an LTLf formula ϕM that is realizable if and only if M accepts the empty tape, where all input sequences are ϕM-f-hopeful. Hence checking GErealizability of ϕM is equivalent to checking its realizability. Thus the 2EXPTIME-hardness result follows. Theorem 6. The synthesis problem of GE-strategies for LTLf speciﬁcations is 2EXPTIME-complete.

4 Experimental Evaluation 4.1 Implementation We have extended the LISA tool described in [Bansal et al., 2020] with an implementation of the synthesis algorithm described in Section 3; we used MONA [Henriksen et al., 1995] to construct DFAs and NFAs from an LTLf formula, as described in [Zhu et al., 2019]. The DFAs and NFAs are ﬁrst constructed explicitly, then encoded symbolically by means of well-known standard techniques (see, e.g., [Ferrara et al., 2005; Bansal et al., 2020]); this allows us to build their union product efﬁciently. We implemented two versions of the construction for the automaton B2 in LISA: one using NFAs as in Section 3 and one using only DFAs (without affecting the correctness of our algorithm). While this adds in theory an exponential blowup, in practice working with DFAs often yields better performance than with NFAs [Tabajara and Vardi, 2020]. The comparison between the two approaches given below in Section 4.3 conﬁrms this, so we use DFAs by default.

4.2 Evaluation Setting To evaluate the effectiveness of the strategy synthesis algorithm proposed in Section 3, we compared LISA with a modiﬁed version of BOSY [Faymonville et al., 2017] and of LTL-

Proceedings of the Thirtieth International Joint Conference on Artiﬁcial Intelligence (IJCAI-21)

Outcome LISA BOSY LTLSYNT strong weak strong weak strong weak

realizable 1840 1838 832 831 1123 1105 unrealizable 49 50 0 0 18 16

timeout 4 6 598 566 339 366 out of memory 9 8 70 66 4 3 other failures 9 9 411 448 427 421

Table 1: Summary of the outcomes of the experiments

SYNT, part of SPOT [Duret-Lutz et al., 2016], so to allow them to support GE-synthesis. Since BOSY and LTLSYNT do not support LTLf natively, we used SPOT to convert each LTLf formula ϕ as t(ϕ). The modiﬁed BOSY ﬁrst constructs a universal co-B uchi automaton accepting ( (O {tail})t(ϕ)) = t(ϕ) and then uses the built-in bounded synthesis techniques [Faymonville et al., 2017] on this automaton to synthesize the GE-strategy. The modiﬁed LTLSYNT ﬁrst constructs a DPA that accepts ( (O {tail})t(ϕ)) = t(ϕ) and then solves the DPA game with built-in solvers [Duret-Lutz et al., 2016]. LTLSYNT got the second place in SYNTCOMP 20201; we did not compare with the winner Strix [Meyer et al., 2018] since its architecture does not allow us to add support for GEsynthesis with reasonable effort, as we did for the other tools. As benchmarks, we collected all benchmarks available on the past SYNTCOMP competitions website2, resulting in 294 benchmark ﬁles. We then used SYFCO3 to translate them to the JSON format accepted by each tool. We considered also the 1617 benchmarks used in [Bansal et al., 2020], already in the appropriate JSON format, for a total of 1911 executions. We considered all formulas in the benchmarks as LTLf formulas and then generated two versions of the ﬁles according to the strong/weak semantics of the X next operator (cf. Section 2), which are encoded in the benchmark ﬁles by the operators X[!] and X, respectively. We performed our experiments on a desktop PC equipped with a 3.4 GHz Intel i7-6700 processor and 8 GB of RAM, of which 5 GB were assigned to the experiments; the operating system was Ubuntu 18.04. We used BENCHEXEC4 to trace the execution of the tools; we imposed a timeout of 10 minutes for each benchmark. We use the following conventions in the scatter plots presented in the remainder of this section: a mark placed on the horizontal/vertical dotted line at time 600 means that the corresponding tool went timeout; a mark on the dashed line, instead, stands for the tool went out of memory during the execution; a mark on the top/right border of the plot indicates that the tool failed for other motivations.

4.3 Experimental Results

Overview of the results. Table 1 summarizes the outcomes of the different tools on the two versions of the benchmarks. As we can see, LISA has been able to solve consider-

1http://www.syntcomp.org/syntcomp-2020-results/ 2https://syntcomp.react.uni-saarland.de/ 3https://github.com/reactive-systems/syfco/ 4https://github.com/sosy-lab/benchexec/

10 1 100 101 102 103

10 1 100 101 102 103

Lisa runtime (s)

ltlsynt runtime (s)

Weak semantics

10 1 100 101 102 103

10 1 100 101 102 103

Lisa runtime (s)

ltlsynt runtime (s)

Strong semantics

Figure 1: Comparison of LISA and LTLSYNT on the benchmarks

10 1 100 101 102 103

10 1 100 101 102 103

Lisa DFA runtime (s)

Lisa NFA runtime (s)

Weak semantics

10 1 100 101 102 103

10 1 100 101 102 103

Lisa DFA runtime (s)

Lisa NFA runtime (s)

Strong semantics

Figure 2: Comparison of LISA using DFA and NFA construction

ably more experiments than both BOSY and LTLSYNT; out of 1911 benchmarks, LISA failed only on less than 25; BOSY and LTLSYNT, instead, failed on more than 1000 and 750 experiments, respectively, of which roughly half caused by timeout. It is interesting to observe in Table 1 that BOSY has never returned unrealizable. This happens also for cases on which both LISA and LTLSYNT returned unrealizable; so it seems BOSY returns some wrong answer. Given these differences in the outcomes, we exclude BOSY from the remainder of our experimental evaluation.

Comparison between LISA and LTLSYNT. In Figure 1 we compare the execution running time of LISA and LTLSYNT; the left plot is relative to the strong X semantics while the right plot to the weak X semantics. As we can see, in both semantics LISA is almost always considerably much faster than LTLSYNT in either synthesizing a GE-strategy or ﬁnding that there is no GE-strategy, as indicated by the large majority of the points above the diagonal dotted line. There are few cases on which LISA crashed, corresponding to the points on the plot right border, as already mentioned in the summary of the experiments above.

Comparison of LISA using DFA and NFA construction. We also compared the running time of LISA when using a DFA instead of an NFA for the construction of the DBA B2 (cf. Sections 3.4 and 4.2); it is shown in Figure 2. As we can see from the plots, even though constructing the NFA is usually faster than generating the DFA, the latter gives a better overall performance, as indicated by the majority of the points above the diagonal, in particular for executions requiring more than 0.25 seconds. This can be motivated by the blowup caused

Proceedings of the Thirtieth International Joint Conference on Artiﬁcial Intelligence (IJCAI-21)

by the determinization step in the construction of the DBA B2 (cf. Section 3.4), which can be mitigated when working with DFAs from the beginning.

5 Related Work

The GE-synthesis problem for LTLf formulas can be seen as a synthesis problem for an LTLf formula ϕ under the quantiﬁed LTL assumption Ot(ϕ), though without explicitly giving the assumption. There are works [Camacho et al., 2018; Zhu et al., 2020; Giacomo et al., 2020] about the synthesis problem where assumptions are explicitly given as an LTL formula ψ; ψ is also used to restrict the synthesis problem to certain environment behaviours we care about: in [Zhu et al., 2020], the assumption is restricted to simple fairness and stability, which is then reduced to solving a so-called fair and stable DFA game, respectively. The assumption is further extended in [Giacomo et al., 2020] to the whole set of LTL formulas, which however relies on solving DPA games. In [Camacho et al., 2018], the assumption is speciﬁed as a conjunction of a safe LTL formula ψs and a co-safe LTL formula ψc, i.e., the LTL formula ψs ψc. Our work and the works in [Camacho et al., 2018; Zhu et al., 2020; Giacomo et al., 2020] consider a similar problem (i.e., the synthesis of a strategy so to satisfy a given LTLf formula given that the environment behaves nicely) in two different scenarios; the main difference is that the environment assumptions in their problems are given explicitly as LTL formulas, while our problem does not need to take an environment assumption as input. Even if we see the ϕ-f-hopeful sequences as an assumption, there is no trivial way to model them as an LTL formula from the given LTLf formula ϕ, so to formalize the concept of ϕ-f-hopeful sequence. Below we focus on a detailed comparison with [Camacho et al., 2018], where the LTLf synthesis problem for ϕ under the safe and co-safe assumption ψs ψc has also been reduced to solving a DBA game. Thus, they can use one DFA for ψs, one DFA for ψc and one DFA for ϕ, and then compose them via automata product operation to obtain the DBA game. In contrast, our constructed NFA and DFA are both obtained from the input LTLf formula ϕ, our only input. A synthesis problem for a kind of LTLf formulas with quality measures, denoted by LTLf[F], has been considered in [Camacho et al., 2018]: instead of a formula being either totally satisﬁed or totally violated by a computation, a value between 0 and 1 by the weight functions f F indicates its degree of satisfaction. Different strategies can then be compared according to the so called best guaranteed value (bgv), the minimum value among the values of the resultant computations induced by a strategy. A strongly bgv-optimal strategies for LTLf[F] is a strategy that desires to obtain the best worst-case value. We conjecture that strongly bgv-optimal strategies degenerate to our GE-strategies when the quality is set to one and the LTL assumption ψs ψc is discarded; we leave as future work the conﬁrmation of this conjecture. Note that the GE-synthesis problem we consider here, though possibly identiﬁed as a subclass of synthesis of strongly bgvoptimal strategies now, is still novel just like the interesting subclass called GR(1) [Bloem et al., 2012] of full LTL syn-

thesis, which allows for specialized and practical algorithms and draws a lot of researchers to work on it. We remark that the 2EXPTIME-completeness established in [Camacho et al., 2018] applies only to LTLf synthesis with safe and co-safe LTL assumptions and no such result is claimed for synthesizing strongly bgv-optimal strategies from LTLf formulas with explicit assumptions and quality measures. Our 2EXPTIME-completeness is for synthesizing GEstrategies only for LTLf formulas. We note, however, that, if the conjecture above is correct, then our hardness result extends to the synthesis of strongly bgv-optimal strategies.

6 Conclusion and Future Work

To the best of our knowledge, this is the ﬁrst time the problem of GE-synthesis for LTLf formulas has been considered. The main contribution of this work is that we proposed to solve the GE-synthesis problem for LTLf formulas by reducing it to a DBA game. Our speciﬁc GE-synthesis algorithm takes advantage of the construction of NFAs and DFAs, which is much easier than the direct or indirect construction of DPAs by going through LTL synthesis. The empirical evaluation on benchmarks from SYNTCOMP and literature conﬁrmed the merits of our speciﬁc approach. We observe that currently the bottleneck of our approach is the size of the DBAs, which invites for further improvement as future work.

Acknowledgements

We would like to thank the anonymous reviewers for their valuable suggestions and comments about this paper. Work supported in part by the Guangdong Science and Technology Department (Grant No. 2018B010107004), NSF grants IIS-1527668, CCF-1704883, IIS-1830549, an award from the Maryland Procurement Ofﬁce and the National Natural Science Foundation of China (Grants Nos. 61532019, 61761136011, 61572024).

References [Almagor and Kupferman, 2020] Shaull Almagor and Orna Kupferman. Good-enough synthesis. In CAV, pages 541 563, 2020. [Aminof et al., 2019] Benjamin Aminof, Giuseppe De Giacomo, Aniello Murano, and Sasha Rubin. Planning under LTL environment speciﬁcations. In ICAPS, pages 31 39, 2019. [Baier and Katoen, 2008] Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. [Baier and Mc Ilraith, 2006] Jorge A. Baier and Sheila Mc Ilraith. Planning with temporally extended goals using heuristic search. In ICAPS, pages 342 345, 2006. [Bansal et al., 2020] Suguman Bansal, Yong Li, Lucas M. Tabajara, and Moshe Y. Vardi. Hybrid compositional reasoning for reactive synthesis from ﬁnite-horizon speciﬁcations. In AAAI, pages 9766 9774, 2020. [Bloem et al., 2012] Roderick Bloem, Barbara Jobstmann, Nir Piterman, Amir Pnueli, and Yaniv Sa ar. Synthesis of

Proceedings of the Thirtieth International Joint Conference on Artiﬁcial Intelligence (IJCAI-21)

reactive(1) designs. J. Comput. Syst. Sci., 78(3):911 938, 2012. [Calude et al., 2017] Cristian S. Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan. Deciding parity games in quasipolynomial time. In STOC, pages 252 263, 2017. [Camacho et al., 2018] Alberto Camacho, Meghyn Bienvenu, and Sheila A. Mc Ilraith. Finite LTL synthesis with environment assumptions and quality measures. In KR, pages 454 463. AAAI Press, 2018. [Camacho et al., 2019] Alberto Camacho, Meghyn Bienvenu, and Sheila A. Mc Ilraith. Towards a uniﬁed view of AI planning and reactive synthesis. In ICAPS, pages 58 67, 2019. [Church, 1957] Alonzo Church. Applications of recursive arithmetic to the problem of circuit synthesis. J. Symbol. Logic, 28(4):289 290, 1957. [Damm and Finkbeiner, 2011] Werner Damm and Bernd Finkbeiner. Does it pay to extend the perimeter of a world model? In FM, pages 12 26, 2011. [De Giacomo and Vardi, 2013] Giuseppe De Giacomo and Moshe Y. Vardi. Linear temporal logic and linear dynamic logic on ﬁnite traces. In IJCAI, pages 854 860, 2013. [De Giacomo and Vardi, 2015] Giuseppe De Giacomo and Moshe Y. Vardi. Synthesis for LTL and LDL on ﬁnite traces. In IJCAI, pages 1558 1564, 2015. [Duret-Lutz et al., 2016] Alexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibaud Michaud, Etienne Renault, and Laurent Xu. Spot 2.0 a framework for LTL and ω-automata manipulation. In ATVA, pages 122 129, 2016. [Faymonville et al., 2017] Peter Faymonville, Bernd Finkbeiner, and Leander Tentrup. Bo Sy: An experimentation framework for bounded synthesis. In CAV, pages 325 332, 2017. [Ferrara et al., 2005] Andrea Ferrara, Guoqiang Pan, and Moshe Y. Vardi. Treewidth in veriﬁcation: Local vs. global. In LPAR, pages 489 503, 2005. [Giacomo et al., 2020] Giuseppe De Giacomo, Antonio Di Stasio, Moshe Y. Vardi, and Shufang Zhu. Two-stage technique for LTLf synthesis under LTL assumptions. In KR, pages 304 314, 2020. [He et al., 2017] Keliang He, Morteza Lahijanian, Lydia E. Kavraki, and Moshe Y. Vardi. Reactive synthesis for ﬁnite tasks under resource constraints. In IROS, pages 5326 5332, 2017. [Henriksen et al., 1995] Jesper G. Henriksen, Jakob Jensen, Michael Jørgensen, Nils Klarlund, Robert Paige, Theis Rauhe, and Anders Sandholm. Mona: Monadic secondorder logic in practice. In TACAS, pages 89 110, 1995. [Hopcroft et al., 2007] John E. Hopcroft, Rajeev Motwani, and Jeffrey D. Ullman. Introduction to automata theory, languages, and computation, 3rd Edition. Addison Wesley, 2007.

[Kupferman, 2012] Orna Kupferman. Recent challenges and ideas in temporal synthesis. In SOFSEM, pages 88 98, 2012. [Lahijanian et al., 2015] Morteza Lahijanian, Shaull Almagor, Dror Fried, Lydia E. Kavraki, and Moshe Y. Vardi. This time the robot settles for a cost: A quantitative approach to temporal logic planning with partial satisfaction. In AAAI, pages 3664 3671, 2015. [Mazala, 2002] Ren e Mazala. Inﬁnite games. In Automata, Logics, and Inﬁnite Games, pages 23 38. Springer, 2002. [Meyer et al., 2018] Philipp J. Meyer, Salomon Sickert, and Michael Luttenberger. Strix: Explicit reactive synthesis strikes back! In CAV, pages 578 586, 2018. [Pesic et al., 2010] Maja Pesic, Dragan Bosnacki, and Wil M. P. van der Aalst. Enacting declarative languages using LTL: Avoiding errors and improving performance. In SPIN, pages 146 161, 2010. [Pnueli and Rosner, 1989] Amir Pnueli and Roni Rosner. On the synthesis of a reactive module. In POPL, pages 179 190, 1989. [Pnueli, 1977] Amir Pnueli. The temporal logic of programs. In FOCS, pages 46 57, 1977. [Rosner, 1991] Roni Rosner. Modular synthesis of reactive systems. The Weizmann Institute of Science (Israel), 1991. Ph D thesis. [Sistla et al., 1987] A. Prasad Sistla, Moshe Y. Vardi, and Pierre Wolper. The complementation problem for b uchi automata with appplications to temporal logic. Theor. Comput. Sci., 49:217 237, 1987. [Tabajara and Vardi, 2020] Lucas M. Tabajara and Moshe Y. Vardi. LTLf synthesis under partial observability: From theory to practice. In GANDALF, pages 1 17, 2020. [Vardi, 2007] M. Y. Vardi. The B uchi complementation saga. In STACS, pages 12 22, 2007. [Wells et al., 2020] Andrew M. Wells, Morteza Lahijanian, Lydia E. Kavraki, and Moshe Y. Vardi. LTLf synthesis on probabilistic systems. In GANDALF, pages 166 181, 2020. [Yan, 2008] Qiqi Yan. Lower bounds for complementation of ω-automata via the full automata technique. Log. Methods Comput. Sci., 4(1:5), 2008. [Zhu et al., 2017] Shufang Zhu, Lucas M. Tabajara, Jianwen Li, Geguang Pu, and Moshe Y. Vardi. Symbolic LTLf synthesis. In IJCAI, pages 1362 1369, 2017. [Zhu et al., 2019] Shufang Zhu, Geguang Pu, and Moshe Y. Vardi. First-order vs. second-order encodings for LTLf-toautomata translation. In TAMC, pages 684 705, 2019. [Zhu et al., 2020] Shufang Zhu, Giuseppe De Giacomo, Geguang Pu, and Moshe Y. Vardi. LTLf synthesis with fairness and stability assumptions. In AAAI, pages 3088 3095. AAAI Press, 2020.

Proceedings of the Thirtieth International Joint Conference on Artiﬁcial Intelligence (IJCAI-21)