Synthesizing Good-Enough Strategies for LTLf Specifications

1 Introduction

Reactive synthesis is the automated construction of a reactive system from a given specification ϕ [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 systemM such that for each infinite 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 satisfies ϕ, i.e., α⊗M(α) |= ϕ [Pnueli and Rosner, 1989]. The extracted systemM 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 controlling 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 ϕ unsatisfiable, 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 quantified; ∃Oϕ stands for ∃o1 · · · ∃okϕ, where O = {o1, . . . , ok} and k ≥ 1, and it has the same meaning as in standard first order logic. We refer to [Sistla et al., 1987] for more details of LTL with ∃ (existential) and ∀ (universal) quantifiers.

In recent years, the version of LTL over finite traces [Baier and McIlraith, 2006; De Giacomo and Vardi, 2013], or LTLf for short, emerged as another popular logic for specifications, because many settings, such as planning [Baier and McIlraith, 2006], assume that an execution stops after the specification 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 finite 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 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 finite words are easier and more efficient than those for building automata on infinite 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 specific 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 finite traces (LTLf ) [Baier and McIlraith, 2006; De Giacomo and Vardi, 2013], which is a variant of LTL [Pnueli, 1977] with the same syntax but it is interpreted over finite instead of infinite traces. The syntax of an LTLf formula over a finite set of propositions P is defined 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 finite traces. Note that X is a strong next operator such that Xϕ requires the tail of the finite trace to satisfy ϕ, while we use N to denote the weak next operator such that Nϕ demands that if the tail of the finite trace is not empty, then it satisfies ϕ. 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 infinite/finite words over 2P that satisfy ϕ.

2.2 NFA, DFA, DBA, and DPA

A nondeterministic finite automaton (NFA) is a tuple A = (Σ, S, ι,∆, F), where S is a finite 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 finite 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 definition of DFAs; the difference lies in the fact that a DBA only accepts infinite words. The run of B on u = u0u1 · · · un · · · ∈ Σω is the infinite 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 infinitely many times. B accepts an infinite word u if the run of B on u is accepting. The language L(B) of B is the set of all accepted infinite 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 defining the acceptance condition. The run ρ of P over u is accepting if the minimal color induced by p occurring infinitely 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 finite sets and α = a0, a1, · · · and β = b0, b1, · · · be two finite/infinite 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 suffix 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

γ : (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 α ⊗ γ(α).

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 finite prefix of α ⊗ γ(α) of length m + 1 that satisfies ϕ.

Definition 1 (Winning strategy). Let γ be a strategy. (1) γ is a winning strategy for an LTL formula ϕ if for every infinite word α = I0, I1, · · · ∈ (2I )ω of interpretations over I, the computation α ⊗ γ(α) satisfies ϕ. (2) γ is a winning strategy for an LTLf formula ϕ if for every infinite word α = I0, I1, · · · ∈ (2I )ω of interpretations over I, there exists an integer m ≥ 0 such that α[0..m] ⊗ γ(α)[0..m] satisfies ϕ.

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 infinite input-output sequence satisfies ϕ. 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 predefined 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 infinite word β ∈ (2O )ω such that α ⊗ β |= ϕ; for an LTLf formula ϕ, we say that α is ϕ-fhopeful if there exists an integer m ≥ 0 and a finite word β = O0 · · · Om ∈ (2O )+ such that α[0..m] ⊗ β |= ϕ.

The problem of good-enough (GE) LTL synthesis [Almagor and Kupferman, 2020] is to decide whether there ex-

Definition 2 (Good-enough (GE)-strategy). Let γ be a strategy. (1) γ is a GE-strategy for an LTL formula ϕ if for every ϕ-hopeful infinite 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] |= ϕ.

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.

Definition 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 finding 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 infinite word α ∈ (2I )ω , the computation α ⊗ γ(α) induced by the winning strategy γ for (∃Oϕ) =⇒ ϕ satisfies 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 finite 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 infinite words. Thus, the quantified LTL formula ∃Oϕ [Sistla et al., 1987], as an assumption, naturally allows us to focus only on the ϕ-hopeful infinite input words, while for LTLf formulas, the quantified LTLf formula ∃Oϕ is interpreted over finite words over 2I . In particular, the assumption ∃Oϕ restricts us to finite input words over 2I rather than the ϕ-f-hopeful words. The definition of GE-synthesis for LTLf formulas, however, is defined with respect to infinite 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 quantified 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 first 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 satisfiable if and only if t(ϕ) is satisfiable. That is, one can reduce the LTLf satisfiability of ϕ to the LTL satisfiability of t(ϕ). The variable tail is used to indicate when a finite word in L(ϕ) terminates. The resulting LTL formula t(ϕ) has the following language.

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.

Intuitively, given a finite word u ∈ L(ϕ), tail holds for the first |u| positions and ¬tail holds forever afterwards.

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 finite words, which are easier and more efficient in practice than those building automata on infinite 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 infinite 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 first 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 DBAConstruction

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 infinite input sequence, which clearly satisfy ϕ, we first 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.

Definition 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 defined as follows: (1) if ∆(q, a) = q′ , then

∆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 undefined for some state q ∈ S1 and assignment a ∈ (2P∪{tail} ). Intuitively, in Definition 4, we just use "tail" to mark when a finite 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 Definition 4. Then L(B1) = {λ ⊗ {tail}∗ | λ ∈ L(ϕ) } · (2P )ω and B1 has 22O(|ϕ|) states.

Construction of B2

We now construct the DBA B2 that accepts all infinite 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 modified 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 NBAAwith 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 infinite sequences α ∈ (2I )ω that are not ϕ-f-hopeful, i.e., no strategy at all can generate a computation for α that satisfies ϕ.

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 efficiently 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 specifications 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 first 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 efficiently.

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 confirms 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 modified version of BOSY [Faymonville et al., 2017] and of LTL- 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 modified BOSY first 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 modified LTLSYNT first 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 2020 1 ; 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 website 2 , resulting in 294 benchmark files. We then used SYFCO 3 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 files according to the strong/weak semantics of the X next operator (cf. Section 2), which are encoded in the benchmark files 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 BENCHEXEC 4 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 considerably 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.

1 http://www.syntcomp.org/syntcomp-2020-results/

2 https://syntcomp.react.uni-saarland.de/

3 https://github.com/reactive-systems/syfco/

4 https://github.com/sosy-lab/benchexec/

Comparison between LISA and LTLSYNT. In Figure 1we 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 finding 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 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 RelatedWork

The GE-synthesis problem for LTLf formulas can be seen as a synthesis problem for an LTLf formula ϕ under the quantified 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 specified 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 satisfied 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 confirmation of this conjecture. Note that the GE-synthesis problemwe consider here, though possibly identified 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 synthesis, 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 FutureWork

To the best of our knowledge, this is the first 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 specific 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 confirmed the merits of our specific 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 Office and the National Natural Science Foundation of China (Grants Nos. 61532019, 61761136011, 61572024).