Best-Effort Synthesis: Doing Your Best Is Not Harder Than Giving Up

1 Introduction

We study best-effort synthesis under environment assumptions in Linear-time Temporal Logic (LTL), the most used logic for dynamic system specifications in Verification [Baier et al., 2008]. Given an LTL specification of the possible behaviors of the environment (i.e., an assumption on the strategies that the environment can enact), and an LTL specification of the task (or goal) for the agent acting in such environments, our aim is to synthesize a strategy for the agent [Church, 1963; Pnueli and Rosner, 1989; Finkbeiner, 2016] that accomplishes the task against all the relevant strategies of the environment [D'Ippolito et al., 2018; De Giacomo and Rubin, 2018; Camacho et al., 2018; Aminof et al., 2019].

What do synthesis procedures return when the agent cannot always achieve its task even by exploiting the assumption on the environment? Typically, the algorithms "give up" declaring the task un-realizable. Here, instead, we synthesize a strategy ensuring that the agent will do nothing that would needlessly prevent it from achieving its task -which we call a best-effort strategy. The importance of such strategies is clear if the environment is not purely adversarial. This happens, e.g., when the assumptions over-approximate the environment (i.e., include environment strategies that are not possible in reality) or when environments are agnostic to the agent. See, e.g., [Faella, 2009; Bloem et al., 2014].

Observe that quantitative approaches based on optimization, such as MDPs, also always return strategies (or memoryless policies, in case of MDPs), that are in a sense "optimal", e.g., wrt expected rewards [Bertsekas, 2005]. Here, we focus on synthesis purely from logical specifications. We do not have external information about the probabilities of certain environment reactions, nor of utilities of taking certain actions. We do however have a logical specification which qualitatively defines the possible environment behaviors.

The main result of this paper is that best-effort synthesis under environment assumptions has exactly the same computational complexity as standard synthesis: 2EXPTIMEcomplete. Hence, "doing your best is not harder than giving up"! While it was already known that best-effort synthesis under environment assumptions was decidable [Aminof et al., 2020], its complexity appeared to be much higher than standard synthesis: e.g., if one was to express this problem naturally in Strategy Logic [Mogavero et al., 2014], one would get a 4EXPTIME upper-bound. Our algorithm employs a novel technique based on simultaneously playing multiple games with different objectives on the same arena. Then, by combining the different winning strategies, we get the desired best-effort strategy. We apply this technique to LTL specifications on infinite traces, as well as to LTLf specifications on finite traces [De Giacomo and Vardi, 2013; De Giacomo and Vardi, 2015]. The latter is particularly well suited for implementation, since it is based on manipulation of finite automata, for which a key step, determinization, while exponential in the worst case is often polynomial in practice [Tabakov and Vardi, 2005; Zhu et al., 2017; Zhu et al., 2020; Tabajara and Vardi, 2020].

Interestingly, best-effort synthesis under environment assumptions separates the traditional trace-based approach to synthesis [Pnueli and Rosner, 1989; Bloem et al., 2014], and the strategy-based approach [Mogavero et al., 2014; Kupferman et al., 2001; Aminof et al., 2019; Aminof et al., 2020]. We discuss this point further in Section 6.

2 Synthesis under Environment Assumptions Linear-time Temporal Logic (LTL)

Given a finite set AP of atomic propositions, formulas of LTL over AP are defined by the following BNF (where p ∈ AP ):

We use the usual abbreviations, ϕ ⊃ ϕ′ .= ¬ϕ∨ϕ′ , true .= p∨ ¬p, Fϕ .= trueUϕ, Gϕ .= ¬F¬ϕ. The size |ϕ| of a formula ϕ is the number of symbols in it. A trace τ is an infinite sequence of valuations of the atoms, i.e., τ ∈ (2AP )ω . For n ≥ 0, write τn for the valuation at position n. A history h is a finite prefix of a trace. Given a trace τ , an integer n, and an LTL formula ϕ, the satisfaction relation (τ, n) |= ϕ, stating that ϕ holds at step n of the sequence τ , is defined as follows: (τ, n) |= p iff p ∈ τn; (τ, n) |= ϕ1 ∨ ϕ2 iff (τ, n) |= ϕ1 or (τ, n) |= ϕ2; (τ, n) |= ¬ϕ iff (τ, n) |= ϕ does not hold; (τ, n) |= Xϕ iff (τ, n + 1) |= ϕ; and (τ, n) |= ϕ1 Uϕ2 iff there exists m ≥ n such that (τ,m) |= ϕ2 and (τ, j) |= ϕ1 for all n ≤ j < m. We write τ |= ϕ if (τ, 0) |= ϕ and say that τ satisfies ϕ and that τ is a model of ϕ.

Reactive Synthesis

(Reactive) synthesis concerns constructing the behaviors of an agent that achieve a given goal (aka task) while interacting with its environment. We specify goals as well as environment assumptions by LTL formulas. Formally, let X and Y be disjoint finite sets of Boolean variables, called the environment variables and agent variables respectively, and let AP .= X ∪ Y . A trace is then written as (X0 ∪ Y0)(X1 ∪ Y1) . . . where Xi ⊆ X, Yi ⊆ Y for all i.

An agent strategy is a function σag : (2X )+ → 2Y that maps a non-empty environment history to the next valuation of the agent variables. Similarly, an environment strategy is a function σenv : (2Y )∗ → 2X mapping agent histories to the next valuation of the environment variables. Note that the domain of σenv includes the empty sequence λ since the environment makes the first move. A trace (Xi ∪ Yi)i is σagconsistent if σag(X0X1 · · ·Xj) = Yj for every j ≥ 0; and is σenv-consistent if σenv(λ) = X0 and σenv(Y0Y1 · · · Yj) = Xj+1 for every j ≥ 0. We write PLAY(σag, σenv) for the unique trace consistent with both strategies.

Let ϕ be an LTL formula over X ∪ Y . An agent strategy σag enforces ϕ, written σag ▷ ϕ, if PLAY(σag, σenv) |= ϕ for every environment strategy σenv. In this case we say that ϕ is agent enforceable. Environment enforceability is defined similarly: σenv ▷ ϕ if ∀σag. PLAY(σag, σenv) |= ϕ. The synthesis problem is, given an LTL formula ϕ, find (if there is one) an agent strategy σ that enforces ϕ.

Theorem 1. [Pnueli and Rosner, 1989] The LTL synthesis problem is 2EXPTIME-complete.

Reactive Synthesis under Environment Assumptions

In most AI scenarios the agent has some knowledge of how the environment works, which it can exploit in order to enforce the goal. We specify this knowledge by an LTL formula E. Following [Aminof et al., 2018; Aminof et al., 2019], we view E as specifying the set of environment strategies that enforce it. Moreover, for it to be useful, we require this set to be nonempty, i.e., that E is environment-enforceable. In this case, we call E an environment assumption.

There is a weaker way to interpret LTL environment specifications (cf. [Bloem et al., 2014]), i.e., E directly restricts the traces (instead of the strategies) of interest to the ones that satisfy E. In that case, synthesis amounts to devising a strategy of the agent that enforces the implication E ⊃ ϕ. While these two ways of interpreting environment specifications are distinct, their synthesis problems are inter-reducible [Aminof et al., 2019]. Although we will exploit this fact in our algorithms, the trace-based approach falls short when dealing with the more general problem of best-effort synthesis under environment assumptions. We discuss this in Section 6.

Given an LTL formula ϕ and an LTL environment assumption E, the synthesis under environment assumptions problem [Aminof et al., 2019] is to find (if there is one) a strategy σag such that:

Such a strategy is said to enforce ϕ under E. Reactive synthesis is the special case taking E = true. Furthermore, it can be shown that most forms of planning with LTL goals, including on nondeterministic domains, are special cases of this synthesis problem [Aminof et al., 2019].

Theorem2. [Aminof et al., 2019] Solving LTL synthesis under environment assumptions is 2EXPTIME-complete.

3 Best-effort Strategies

To formalize the notion of best-effort strategies, we first recall what it means for an agent strategy to be better than another. Let E be an environment assumption, and let ϕ be an agent goal. Define a binary relation ≥ϕ|E on agent strategies:

Definition 1 (Dominance). σ1 ≥ϕ|E σ2 iff for every σenv ▷ E, PLAY(σ2, σenv) |= ϕ implies PLAY(σ1, σenv) |= ϕ.

This notion can be defined also when there is no assumption involved, by simply taking E = true. As usual, write σ1 >ϕ|E σ2 iff σ1 ≥ϕ|E σ2 and σ2 ≱ϕ|E σ1. If σ1 >ϕ|E σ2 we say that σ1 strictly dominates σ2 (for goal ϕ under environment assumption E). The relation ≥ϕ|E is a preorder, and >ϕ|E is a strict partial order.

Intuitively, σ1 >ϕ|E σ2 means that σ1 does at least as well as σ2 against every environment strategy enforcing E, and strictly better against at least one such strategy. In particular, if σ2 is not maximal, say σ1 strictly dominates it, then an agent that uses σ2 is not doing its "best" to achieve the goal: if it used σ1 instead, it could achieve the goal against a strictly larger set of environment strategies. Within this framework, maximal strategies do a "best-effort" to achieve the goal.

Remark 1. Enforcing strategies dominate all others. In particular, ϕ is agent-enforceable under E iff every maximal strategy wrt ≥ϕ|E enforces ϕ under E.

Definition 2 (Best-effort). An agent strategy σ2 is maximal, or best-effort, for the goal ϕ under the environment assumption E, iff there is no agent strategy σ1 such that σ1 >ϕ|E σ2.

When there is no environment assumption, i.e., E = true, we simply say that σ2 is best-effort for the goal ϕ. The problem of best-effort synthesis under assumption is:

Definition 3. Given an LTL goal ϕ and an LTL environment assumption E, the best-effort synthesis problem under environment assumptions is to find an agent strategy that is besteffort for ϕ under E.

Example 1. Suppose X = {r}, Y = {g}, and ϕ = G(r ⊃ F(g∧¬ X r)) and E = (¬r∧X r∧X X r) ⊃ X X X r. We think of the environment as issuing "requests" (r) and the agent as issuing "grants" (g). A best-effort strategy for ϕ under E has no obligation to do anything against a strategy that has produced the sequence ¬r, r, r, ¬r (and thus violated E). A strategy σ is best-effort iff, if such a sequence was not produced so far, then the strategy ensures that (i) every request is followed at some point in time by a grant, and (ii) there is no grant immediately following the sequence ¬r, r, r.

The realizability problem, i.e., deciding if such agent strategies exist, is trivial since they always exist:

Theorem 3. [Berwanger, 2007; Aminof et al., 2020] Given an LTL goal ϕ and an LTL environment assumption E, there is an agent strategy that is best-effort for the goal ϕ under E.

The main problem addressed in this work is to establish the exact complexity and algorithms for finding such strategies.

We end with a remark regarding environment assumptions in the context of best-effort synthesis. Consider two agent strategies σ1 ag and σ2 ag , and two environment strategies σ1 env and σ2 env , such that PLAY(σiag , σj env ) |= ϕ iff i = j. Observe that σ1 ag and σ2 ag are incomparable in the dominance order. Intuitively, lacking information regarding the relative importance of σ1 env and σ2 env , we have no way to rank σ1 ag and σ2 ag . Environment assumptions are one way of providing such information: in case only one of σ1 env and σ2 env enforces the assumption, the choice between σ1 ag and σ2 ag becomes clear.

4 Solving Games on Automata

In section 5 we give a 2EXPTIME algorithm for finding besteffort strategies under environment assumptions. The building blocks for this algorithm are games played on automata.

Deterministic Transition Systems

A deterministic transition system D = (Σ,Q, ι, δ) consists of a finite input alphabet Σ (typically, Σ = 2AP ), a finite set Q of states, an initial state ι ∈ Q, and a transition function δ : Q×Σ→Q. The size of D is the number of its states.

Let α = α0α1 · · · denote a finite or infinite sequence over the alphabet Σ. The run (aka path) induced by α is the sequence q0q1 · · · of states where q0 = ι and qi+1 = δ(qi, αi) for every i < |α|. We extend δ to the function Q × Σ∗ → Q as follows: δ(q, λ) = q, and for n > 0, if qn = δ(q, α0 · · · αn-1) then δ(q, α0α1 · · · αn) = δ(qn, αn).

Definition 4. The product of two transition systems Di = (Σ,Qi, ιi, δi) (for i = 1, 2) over the same input alphabet is the transition system D1×D2 = (Σ, Q, ι, δ) where Q = Q1× Q2; ι = (ι1, ι2); and δ((q1, q2), x) = (δ(q1, x), δ(q2, x)). The product D1 × D2 × · · · × Dn can be similarly defined for any finite sequence D1,D2, · · · ,Dn of transition systems over the same input alphabet Σ.

Parity Automata

Automata can be seen as transition-systems with an acceptance condition. To handle LTL, we use the parity acceptance condition. A Deterministic Parity Word automaton (DPA) A = (D, c) consists of a deterministic transition system D and a coloring function c : Q → Z. The index of A is the number of integers in the image of c, i.e., |{n ∈ Z | c-1 (n) ̸= ∅}|. An infinite run ρ = q0q1 · · · satisfies c (alternatively, accepted) iff the smallest n such that c(qi) = n for infinitely many i is even. An infinite string α ∈ Σω is accepted by A = (D, c) iff its run satisfies c. The set of infinite strings accepted by A is the language of A.

Theorem 4 (LTL to DPA). (cf. [Vardi, 1995]) Given an LTL formula ϕ, one can build a DPA Aϕ accepting exactly the models of ϕ, whose size is at most 2EXP in |ϕ| and whose index is at most EXP in |ϕ|.

If Ai = (Di, ci) are DPAs, and D is the product transitionsystem, we can lift the winning conditions ci to the product by ignoring the other components:

Definition 5. For DPAs Ai = (Di, ci) and writing D for the product of their transition systems D1, · · · ,Dk, define the lifting of ci to D to be the coloring function di : Q → Z defined by di(q1, · · · , qk) .= ci(qi).

Note that (D, di) is a DPA, and its language is the same as the language of the DPA (Di, ci).

Games on Deterministic Automata

It is known that solving synthesis (without environment assumptions) for an LTL goal ϕ can be reduced to solving a two-player game of perfect information on the DPA corresponding to ϕ. We describe this process below since we will later generalize it. This section is an adaptation of material on parity games [Apt and Gr¨adel, 2011] to our setting.

Informally, the current position in the game is a state q of the DPA, first the environment moves by setting X′ ⊆ X, then the agent follows by setting Y ′ ⊆ Y , and the position in the game is updated to the state δ(q, (X′ ∪ Y ′ )). This interaction generates an infinite run, and the agent is declared the winner if the run satisfies the parity condition. Formally, a DPA-game is played on a DPA A = (D, c) in which Σ = 2X∪Y , by the two players, agent and environment. The transition system D = (Σ,Q, ι, δ) is called the arena of the game, and c is called the objective of the game. An agent strategy σag : (2X )+ → 2Y is winning if for every strategy σenv of the environment, the trace PLAY(σag, σenv) is accepted by the DPA A (i.e., the run on the trace satisfies c). Similarly, a strategy σenv : (2Y )∗ → 2X for the environment is winning if for every strategy σag of the agent, the trace PLAY(σag, σenv) is not accepted by the DPA A (thus, the objective c of the game is from the agent's point of view). A player's winning region in the DPA-game on A is the set of states q for which that player is winning in the DPA-game on (Σ, Q, q, δ, c), i.e., starting from q. A strategy for a player that is winning from every state in her winning region is called uniform winning.

If the agent makes its moves just by looking at the current environment move and the current state of the DPA (instead of the exact full history of environment moves), then we say that the agent is using a positional strategy. Formally, a function fag : Q × 2X → 2Y induces the positional agent strategy σag: σag(X0) = fag(ι,X0), and for n > 0, σag(X0X1 · · ·Xn) = fag(qn,Xn) where qn .= δ(ι, α) and α is the finite sequence played up until now, i.e., α = (X0 ∪ σag(X0))(X1 ∪ σag(X0X1)) · · · (Xn-1 ∪ σag(X0X1 · · ·Xn-1)). We can similarly define environment positional strategies as functions fenv : Q→ 2X .

The relevant computational problem associated with a DPA-game is to compute, for a given player, that player's winning region W, as well as a uniform winning positional strategy for that player. We call this solving the game.

Theorem 5. DPA-games can be solved in time polynomial in the size of A and exponential in the index of A.

We also consider the case where the agent and environment co-operate. Formally, a pair of strategies σag, σenv is cooperatively winning if the trace PLAY(σag, σenv) is accepted by the DPA A. The co-operative winning region W ′ of a DPA-game A is the set of states q for which there is a pair of strategies that are co-operatively winning in the game played on (Σ, Q, q, δ, c), i.e., starting from q. Solving a co-operative DPA-game on A means to find the set W ′ , as well as a pair of uniform positional strategies (although we will only use the agent's) that co-operatively win from every state in W ′ . Note that this amounts to solving the emptiness problem for A.

Theorem 6. Co-operative DPA-games can be solved in time polynomial in both the size and index of the given DPA A.

We will sometimes need a way to limit the environment to moves that do not leave a given set of states Q′ . We do this by introducing a sink-state, and redirecting to it moves of the environment that start in Q′ and for which some response of the agent leaves Q′ :

Definition 6. Let D = (Σ, Q, ι, δ) be an arena and let Q′ ⊆ Q be a set of states. The environment-restriction of D to Q′ is the arena (Σ,Q ∪ {sink}, ι, δ′ ), where δ′ agrees with δ except that δ′ (q, (X′ ∪ Y ′ )) = sink in case q = sink, or q ∈ Q′ and δ(q, (X′ ∪ Z)) ̸∈ Q′ for some Z ⊆ Y .

5 Computing Best-Effort Strategies

In this section we establish the main result of the paper:

Theorem 7. Best-effort synthesis under environment assumptions (for LTL goals and assumptions) is 2EXPTIMEcomplete.

The main implication of this theorem is that it provides the following alternative approach to synthesis, with or without assumptions: instead of trying to solve reactive synthesis - which in case the formula ϕ is not agent-enforceable returns no strategy (i.e., gives up) - one can for the same cost search for a best-effort strategy which always exists and, in case ϕ is agent-enforceable, enforces ϕ.

The lower-bound is achieved by a reduction from reactive synthesis (without environment assumptions), which is 2EXPTIME-complete [Pnueli and Rosner, 1990]. In the remainder of this section we provide an algorithm for the upperbound. The idea is to reduce the problem to computing suitable winning and co-operatively winning strategies of certain DPA-games. Note that the case without environment assumption was solved in [Faella, 2009]. One can recover this case from our algorithm simply by setting E = true.

Algorithm A. Given LTL formulas ϕ and E:

1. For every ξ ∈ {¬E, E ⊃ ϕ, E ∧ ϕ} compute the DPAs Aξ = (Dξ, cξ) (Theorem 4).
2. Form the product D = D¬E ×DE⊃ϕ ×DE∧ϕ, and denote the lifted priority functions on D by d¬E , dE⊃ϕ and dE∧ϕ (Definitions 4 and 5).
3. In the DPA-game on (D, dE⊃ϕ), compute a uniform positional winning agent strategy fag for dE⊃ϕ (Theorem 5). Let W ⊆ Q be the agent's winning region.
4. In the DPA-game on (D, d¬E), compute the environment's winning region V ⊆ Q (Theorem 5). Thus, the environment can ensure E holds from every state in V .
5. Compute the environment-restriction of D to the set V , and call the resulting transition systemD′ (Definition 6). Form the DPA-game (D′ , dE∧ϕ) where the parity of the new sink state is given an odd color smaller than all even colors in D.
6. In the DPA-game (D′ , dE∧ϕ), find a uniform positional strategy gag that is co-operatively winning (Theorem 6).
7. Return the agent strategy induced by the positional strategy kag : Q× 2X → 2Y : kag(q,X′ ) = fag(q,X′ ) if q ∈ W, and kag(q, X′ ) = gag(q, X′ ) otherwise.

Correctness of Algorithm A

The correctness of Algorithm A uses the notion of a value val(h) of a history h: the value is "winning" if the player can enforce the goal under the environment assumption starting from h; "losing" if all plays extending h, that are consistent with an environment strategy that enforces the assumption, violate the goal; and "pending" otherwise. This allows one to characterize best-effort strategies as those that witness the value val(h) of every history h consistent with it [Berwanger, 2007; Aminof et al., 2020]. Here is a formalization of the main considerations. For a joint history h ∈ (2X∪Y )∗ , let E(h, σag) be the set of all environment strategies σenv that enforce E and for which h is consistent with σag, σenv; and let H(σag) be the set of all h for which E(h, σag) ̸= ∅. Define:

• val(σag, h) := +1 (winning) if PLAY(σag, σenv) |= ϕ for every σenv ∈ E(h, σag);
• val(σag, h) := -1 (losing) if PLAY(σag, σenv) |= ¬ϕ for every σenv ∈ E(h, σag);
• val(σag, h) := 0 (pending) otherwise.

Let val(h) be the maximum of val(σ, h) where σ varies over all agent-strategies for which h ∈ H(σ). 1 The next theorem follows from the cited characterization of dominance:

Theorem 8. An agent strategy σ is best-effort iff val(σ, h) = val(h) for every history h ∈ H(σ).

Example 2. To see that σ in Example 1 is best-effort use Theorem 8. To that end, let h ∈ H(σ). First note that val(h) < 1 since the environment strategy that always requests, except where not specified in h, enforces E and ¬ϕ. Second, note that ϕ can be violated by a history that contains r and then (possibly at the same time) a g immediately followed by r. If h is such a history, then val(h) = -1, and thus val(σ, h) = val(h). So, suppose h is not such a history. Let σenv be the environment strategy that never requests, except where specified in h and immediately after h. Note that σenv enforces E, and thus val(h) > -1 since an agent can safely respond to any outstanding requests. Since, in particular, σ safely responds to any outstanding request, also val(σ, h) > -1, and thus also in this case val(σ, h) = val(h) = 0.

The correctness of Algorithm A follows immediately from:

Theorem 9. Let σA be the agent-strategy produced by Algorithm A, and let h ∈ H(σ). Then val(σA, h) = val(h).

Intuitively, the strategy σA returned by Algorithm A has the property that histories that lead to states in W are winning

1 We use val(h) only in cases where h ∈ H(σ) for some σ.

(from these states the agent can enforce E ⊃ ϕ, and thus in particular can enforce ϕ assuming E), histories that lead to states in W ′ \ W, where W ′ is the co-operatively winning region from step 6 in the game (D′ , dE∧ϕ), are pending (from these states there is an environment strategy σenv enforcing E such that PLAY(σA, σenv) |= ϕ), and the rest are losing.

6 Strategy-based vs. Trace-based Approaches

While this paper adopts a strategy-based approach to synthesis [Mogavero et al., 2014; Kupferman et al., 2001; Aminof et al., 2019; Aminof et al., 2020], traditional synthesis follows a trace-based approach [Pnueli and Rosner, 1989; Bloem et al., 2014; Camacho et al., 2018]: synthesis for ϕ using the environment assumption E is solved by finding an agent strategy that enforces E ⊃ ϕ against all environment strategies, i.e., the assumption E is pushed into the goal formula instead of being used to limit the set of environment strategies. Unfortunately, while this works when synthesizing enforcing strategies, the example below clearly shows that it is inadequate when looking for best-effort strategies.

Consider a Star-Wars setting where the droid C-3PO is captured and made to work at a space port, loading boxes onto a cargo vessel. At every time-step, a few new boxes, of varying weights, may be added to the pending pile. Being a protocol droid, C-3PO is not very strong, and can load at most 30 kilograms in one time step. With the help of R2-D2, C-3PO learns that the space-port works under the following strict protocol: if at the time the cargo vessel has to leave, the loading is not finished, he will be declared inefficient and dismantled for parts in the next time step. He is otherwise safe except that, if he ever stops loading when there are pending boxes, he will be declared lazy and dismantled in the next time step. C-3PO thus forms the assumption E on the environment by taking the rules above conjuncted with the fact that if he sees Luke Skywalker then he will be rescued after two time steps.

For obvious reasons, C-3PO has the following goal ϕ: ¬dismantledUrescued. Unfortunately, the vessel's departure time, the new boxes that may be added at each time step, and Luke Skywalker's timing, are not under his control, making it impossible for him to have a winning strategy.

It is not hard to see that a best-effort strategy for ϕ under the assumption E will result in C-3PO continuously loading boxes unless there are no boxes to load, or the cargo vessel has to leave, or he previously saw Luke Skywalker. Indeed, any other strategy cannot be maximal since it is guaranteed, by the assumption E, to get C-3PO dismantled.

On the other hand, when considering the implication E ⊃ ϕ, any strategy σag that loads nothing on the first step is not dominated by any strategy σ′ag that does! To see that, consider an environment strategy σenv that operates as follows: it starts with 40 kilograms of boxes in the pile; if C-3PO loads nothing in the first time step then do nothing in the next step; otherwise, declare that it is time for the vessel to leave, and dismantle C-3PO in the next step. Hence, against σenv, the strategy σag achieves the implication, whereas σ′ag does not. Obviously, σenv is irrelevant since it blatantly violates E. However, when synthesizing for E ⊃ ϕ (unlike synthesizing for ϕ under E) it is still considered. Hence, by taking a maximal element from the set of strategies σag that load nothing on the first step, we get a best-effort strategy for E ⊃ ϕ that is a guaranteed suicide: it is an unconditionally losing strategy for the goal under E, and it never achieves the goal on any trace that satisfies E!

7 Best-Effort Synthesis in LTLf

Although many environment assumptions are naturally expressed in LTL (e.g., fairness assumptions), other classic ones such as planning domains and safety can be expressed in LTLf . In this section we show that the framework for LTL also applies to LTLf . The main difference is that in the this case we can give an algorithm for finding best-effort strategies that only uses classic simple graph-algorithm building blocks, such as breadth-first search, fixed-point algorithms, and subset constructions for determinization. In other words, the algorithm in this section lends itself to implementation.

Linear-time Temporal Logic on Finite Traces (LTLf )

LTLf has the same syntax as LTL but is interpreted on finite traces τ ∈ (2AP )+ [De Giacomo and Vardi, 2013] 2 . For the semantics, only the temporal operators are reinterpreted. This is done as follows. For n < |τ |:

• (τ, n) |= Xϕ iff n+1 < len(τ) and (τ, n+1) |= ϕ;
• (τ, n) |= ϕ1 Uϕ2 iff there exists i with n ≤ i < len(τ) such that (τ, i) |= ϕ2 and for all i ≤ j < n, (τ, j) |= ϕ1.

Let ˜X be the dual of X, i.e., ˜X .= ¬X¬ϕ. Semantically, (τ, n) |= ˜Xϕ iff n + 1 < len(τ ) implies (τ, n + 1) |= ϕ.

Thus, the main difference is that while in LTL the X operator is its own dual (i.e., ¬X¬ϕ ≡ Xϕ), this is not true in LTLf , where the dual of X has a different meaning to X.

An important computational advantage of LTLf is that it can be translated into ordinary finite-state automata. A Deterministic Finite Automaton (DFA) A = (D, F) consists of a deterministic transition system D and a set F ⊆ Q of final states. A finite run ρ = q0q1 · · · qn is accepting iff qn ∈ F. A finite string α ∈ Σ∗ is accepted if its run is accepting.

LTLf Synthesis under Assumptions

Over finite traces there is the issue of how a play stops. We redefine agent strategies to be partial functions σag : (2X )+ ↪→ (2Y ) and require environment strategies be total as before σenv : (2Y )∗ → (2X ). Then, we redefine PLAY(σag, σenv) to be the longest (finite or infinite) trace that is consistent with both strategies. Note that a play is finite if it ends in an environment move for which the agent strategy, being a partial function, specifies no next move (which we think of as the agent stopping the play).

Let ϕ, E be LTLf formulas over X ∪ Y . We say that an agent strategy σag enforces ϕ, written σag ▷ ϕ, iff

Asymmetrically, we say that an environment strategy σenv enforces E, written σenv ▷ E, iff

2 In fact all results presented here apply also to the extension LDLf of LTLf , which captures monadic-second-order logic on finite traces [De Giacomo and Vardi, 2013].

The asymmetry stems from the fact that, intuitively, an agent cannot enforce ϕ unless she stops the play.

Remaining definitions. The rest of the LTLf treatment mimics that of LTL simply by replacing LTL by LTLf in Definitions 1, 2, and 3. We also replace DPAs by ordinary finitestate automata. Then, Theorems 1 and 4 hold for LTLf and DFA. In particular, one can obtain a DFA, of 2EXP size, accepting exactly the models of a given LTLf formula [De Giacomo and Vardi, 2013]. Games can be played on DFAs as for DPAs except that the agent is trying to end the play in a final state, i.e., an agent strategy σag is winning if for every environment strategy σenv, the trace PLAY(σag, σenv) is finite and is accepted by the DFA; dually, an environment strategy σenv is winning if for every agent strategy σag, if PLAY(σag, σenv) is finite then it is not accepted by the DFA.

Best-Effort LTLf Synthesis

The algorithm below finds best-effort strategies under environment assumptions in the LTLf case (we contextually discuss each step). The main difference to Algorithm A is that we replace DPAs by DFAs.

Algorithm B. Given LTLf formulas ϕ and E:

1. For every ξ ∈ {¬E, E ⊃ ϕ, E ∧ ϕ} compute the DFAs Aξ = (Dξ, Fξ) [De Giacomo and Vardi, 2013].
2. Form (in linear time) the product D = D¬E ×DE⊃ϕ × DE∧ϕ. Lift the final states of each component to the product, e.g., if AE = (DE, FE) is the DFA for E, then the lifted condition GE consists of all states (q¬E , qE⊃ϕ, qE∧ϕ) ∈ Q such that qE ∈ FE .
3. In the DFA-game (D, FE⊃ϕ), compute (in linear time) a uniform positional winning agent strategy fag. Let W ⊆ Q be the agent's winning region. Finding winning regions and computing uniform positional winning strategies in DFA-games can be done in linear-time by a simple fixed-point algorithm [Apt and Gr¨adel, 2011].
4. In the DFA-game (D, F¬E), compute (in linear time) the environment's winning region V ⊆ Q.
5. Compute (in linear-time) the environment-restrictionD′ of D to the set V .
6. In the DFA-game (D′ , FE∧ϕ), find (in linear time, e.g. using breadth-first search) a co-operatively winning uniform positional strategy gag.
7. Return the agent strategy induced by the positional strategy kag : Q× 2X → 2Y : kag(q,X′ ) = fag(q,X′ ) if q ∈ W, and kag(q, X′ ) = gag(q, X′ ) otherwise.

Algorithm B provides a 2EXPTIME upper-bound; the lowerbound is derived in a similar way to the LTL case by a reduction from LTLf -synthesis which is 2EXPTIMEcomplete [De Giacomo and Vardi, 2015].

Theorem 10. Best-effort synthesis under environment assumptions (for LTLf goals and assumptions) is 2EXPTIMEcomplete.

Thus, Algorithm B is optimal, and although it has the same worst-case complexity as Algorithm A, it makes use of much simpler graph-algorithm building-blocks.

8 RelatedWork

Best-effort strategies are maximal in the dominance order. These notions originate in game-theory, where dominance is also called weak-dominance [Apt and Gr¨adel, 2011], and best-effort is sometimes called admissible.

In formal methods, best-effort synthesis, and synthesis under environment assumptions, were mainly considered in isolation, and almost always in the trace-based setting, e.g., [Pnueli and Rosner, 1989; Faella, 2009; Brenguier et al., 2017]; see [Bloem et al., 2014] for a survey. [Faella, 2009] argues for best-effort strategies as reasonable responses in environments that may not be adversarial, characterizes goals admitting positional best-effort strategies, and shows how to compute such strategies (for LTL goals, this results in a special case of Algorithm A). Few papers, either directly or indirectly, consider best-effort and assumptions at the same time (e.g., [Damm and Finkbeiner, 2014] does so in a trace-based setting). The problems studied there are different: they are mainly concerned with looking for a strategy that dominates all other strategies (i.e., maximum rather than maximal), and in case it exists, they synthesize the weakest-environment assumption under which it achieves the goal.

More closely related are works that consider the multiagent setting where agent i has as an assumption the goal of agent j, and thus naturally take the strategy-based view. Notably, [Berwanger, 2007] pioneers the study of dominance in games played on graphs. [Brenguier et al., 2014] studies the problem of deciding the existence of strategy profiles and corresponding model-checking problems. The problems studied here can be expressed in their setting, however, in our case the existence problem is trivial, and we deal with synthesis not with model-checking. [Brenguier et al., 2017] studies assume-admissible (AA) synthesis which is similar but different to ours; cast in our setting, AA looks for strategies that enforce ϕ against environment strategies that are best-effort (without assumptions) for E, whereas we are looking for besteffort agent strategies for ϕ against environments that enforce E. In particular, if E is environment-enforceable, AA is equivalent to synthesis (without assumptions).

The closest paper to ours is [Aminof et al., 2020] where the problem of best-effort synthesis under environment assumptions is introduced in the context of two environments (expected and exceptional), and shown to be decidable. Strictly speaking, we do not provide an alternative solution to their problem, since we only deal with a single environment specification; and their paper does not include our problem as a special case due to extra requirements that they impose. However, one can extract from their decidability proof a 4EXPTIME upper bound to our problem. Finally, their technique is different from ours: theirs characterizes the set of all best-effort strategies using tree-automata, while ours computes a single best-effort strategy by solving certain games.

Acknowledgments

This work is partially supported by the Austrian Science Fund (FWF): P 32021, the ERC Advanced Grant WhiteMech (No. 834228), and the EU ICT-48 2020 project TAILOR (No. 952215)