Synthesizing strategies under expected and exceptional environment behaviors

1 Introduction

Synthesis, originally developed in the context of reactive systems, is concerned with the automatic generation of behaviors, or strategies, from requirements. In its usual form, the requirements are given as temporal specifications, and the resulting behaviors are returned in the form of automata [Pnueli and Rosner, 1989; Finkbeiner, 2016]. Applying and developing concepts related to synthesis in an AI context poses considerable challenges compared with the traditional setting, including the presence of multiple agents, noise, normative requirements, and fairness constraints [Daniele et al., 1999; De Giacomo et al., 2013; D'Ippolito et al., 2018; Belardinelli et al., 2017; Bonet et al., 2017; Maubert and Murano, 2018; Belle, 2018; Aminof et al., 2020].

A crucial aspect that all the work on synthesis in AI has in common is the need for a model of the environment in which the agent acts. In planning, for example, such a model is given in terms of a "domain" which specifies, in each state, how the environment enacts the (possibly nondeterministic) effects of the action performed by agent [Geffner and Bonet, 2013; Reiter, 2001]. This should be contrasted with traditional synthesis where one does not make an actual distinction between the agent specification, i.e., the goal, and the environment specification [Pnueli and Rosner, 1989]. Synthesizing with a model of the environment is related to synthesis under assumptions as studied in the Verification literature [Chatterjee and Henzinger, 2007; Bloem et al., 2015; Brenguier et al., 2017] and, building on that literature, it has been satisfactorily addressed in [Camacho et al., 2018; Aminof et al., 2018] and especially in [Aminof et al., 2019a].

Following [Aminof et al., 2019a], the environment is specified in terms of possible strategies that it could enact, and is formalized through a linear temporal logic specification E. In this way we are able to extend planning domains in many ways, e.g., by allowing for the possibility of having deferred effects, or introducing fairness or stability conditions on effects. The agent goal is also expressed as a linear temporal logic specification ϕ, much as is done in planning for temporally extended goals [Bacchus and Kabanza, 1996; Bacchus and Kabanza, 2000; De Giacomo and Vardi, 1999; De Giacomo and Rubin, 2018; Camacho et al., 2018]. Then, synthesis under environment specifications is the problem of finding a winning strategy for the agent, which enforces the goal ϕ no matter what strategy, among those specified by E, the environment happens to follow.

While this strategy-based approach to modeling environments is well suited for capturing synthesis in AI, it suffers from one severe limitation: the environment model is assumed to be given in a "monolithic way", i.e., with a single specification, and without distinguishing expected behaviors (i.e., strategies) and exceptional or uncommon variations, such as rare faults or failures. As a consequence, the agent is meant to synthesise a winning strategy against all possible environment behaviors, independently of them being expected or exceptional. In real situations however, coming up with a suitable monolithic model of the environment may be unfeasible. If the model only captures the expected behaviors of the environment, then a winning strategy for the agent may be ineffective, since it may be losing against exceptional behaviors not captured by the model. On the other hand, if the model also includes possible exceptions, such as faults, failures, or non-compliance with the expected behaviors, there may simply not exist a winning strategy for the agent since handling all possible exceptions may be impossible.

In this paper we abandon a single monolithic model of the environment in favor of two distinct models, i.e., two environment specifications: one capturing the expected behaviors, and one that also includes the exceptional behaviors. Using these two models we formally show how to appropriately and simultaneously handle expected and exceptional behaviors.

The central tenet of our contribution is that, in such situations, an agent should use a winning strategy against the expected environment behaviors, that, in addition, also provides a satisfactory response, as far as possible, to the exceptional behaviors of the environment. Such a "best-effort" strategy may not be sufficient to realize the agent specification against all possible exceptions, but it does constitute rational agent behavior: on the one hand, it is guaranteed to be winning against the expected behaviors; and on the other hand, it also does not miss any opportunity to be winning against exceptional environment behaviors. We make these intuitions precise by formulating "as far as possible" as requiring the agent strategy to be also winning against a maximal set of exceptional environment behaviors, where "maximal" is induced by the game-theoretic notion of (weak)-dominance order on agent strategies. Notably, we show that if there is a winning strategy against the expected-environment specification then there is one that, in addition, is making a best effort against the exceptional-environment specification. Moreover, we show that one can compute such a strategy.

2 Preliminaries

We fix the notation for concepts that will be used in the rest of the paper. We follow the notation in [Aminof et al., 2019a].

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): ϕ ::= p | ϕ ∨ ϕ | ¬ϕ|Xϕ|ϕUϕ. 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 a non-negative integer n, write τn for the valuation at position n (we index starting with n = 0). A history h is a finite prefix of a trace; its length is denoted by |h|. 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 it is not the case that (τ, n) |= ϕ; (τ, 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) |= ϕ to represent that τ satisfies ϕ and that τ is a model of ϕ. We use the usual abbreviations, ϕ ⊃ ϕ′ .= ¬ϕ ∨ ϕ′ , true .= p ∨ ¬p, false .= ¬true, Fϕ .= trueUϕ, Gϕ .= ¬F¬ϕ. We write |= ψ when ψ is logically valid, i.e., τ |= ψ for all traces τ .

Reactive synthesis. (Reactive) synthesis concerns constructing the behaviours of an agent that achieves a given goal while interacting with its environment. We specify goals as well as environment specifications 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 (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 sequence of valuations of the environment variables to the next valuation of the agent variables. Similarly, an environment strategy is a function σenv :

(2Y )∗ → 2X . Note that an environment strategy can accept the empty sequence λ since the environment makes the first move. We denote by Σall ag (resp. Σall env ) the set of all agent (resp. environment) strategies. 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. Let PLAY(σag, σenv) denote the unique trace consistent with both strategies. Let ϕ be an LTL formula over X ∪ Y . An agent strategy σag enforces ϕ, written σag ▷ ϕ, if for every environment strategy σenv, the sequence PLAY(σag, σenv) satisfies ϕ, i.e., ∀σenv ∈ Σall env . PLAY(σag, σenv) |= ϕ. Such strategies are called winning strategies. A specification ϕ is agent enforceable if some agent strategy enforces it. The set of all such agent strategies is denoted by Σϕag . The notion of environment enforceability, σenv ▷ ϕ, and the set Σϕenv of all environment strategies enforcing ϕ, are defined similarly, e.g., σenv ▷ ϕ if ∀σag ∈ Σall ag . PLAY(σag, σenv) |= ϕ. Given an LTL formula ϕ (the goal), the synthesis problem for the agent is to devise a strategy σag for the agent that enforces ϕ, i.e., such that σag ▷ ϕ. The synthesis problem for the environment is defined similarly. Note that if a strategy exists, also a finitestate one exists, i.e., one that is computed by a finite-state transducer [Pnueli and Rosner, 1989].

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

Environment specifications. In most AI scenarios the agent has some knowledge of how the environment works, which the agent can exploit in order to enforce its goals. To capture this, besides the specification of the goal, we introduce a specification of the environment. In particular, an environment specification is also given by an LTL formula E and, following [Aminof et al., 2019a], it determines the set ΣEenv of strategies that the environment can adopt, i.e., those that enforce E. Formally, let ΣEenv .= {σenv ∈ Σall env | σenv ▷ E}. For the environment specification to be useful, one requires that ΣEenv to be nonempty, i.e., that E is environment-enforceable. Given an LTL formula ϕ and LTL specification E (typically assumed to be environmentenforceable), the synthesis under environment specifications problem concerns determining an agent strategy σag such that: ∀σenv ∈ ΣEenv . PLAY(σag, σenv) |= ϕ. It can be shown that most forms of planning with LTL goals, including on nondeterministic domains, are special cases of this synthesis problem, see [Aminof et al., 2019a]. Moreover:

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

We observe that the verification literature on synthesis under assumptions, e.g., [Chatterjee and Henzinger, 2007], gives one an alternative (weaker) way to interpret LTL environment specifications E, i.e., E directly restricts the traces of interest to the ones that satisfy E (in contrast, we restrict the strategies to the ones that enforce E). In that case, synthesis amounts to devising a strategy of the agent that enforces the implication E ⊃ ϕ. It turns out, that while these two ways of interpreting environment specifications are distinct, their synthesis problems are inter-reducible [Aminof et al., 2019a]. We will return to this point at the end of Section 3.

3 Synthesis Under Expected and Exceptional Environment Specifications

Consider a setting with two environment specifications - E captures the "expected" behaviors of the environment, while E ′ captures, in addition, "exceptional" behaviors of the environment, i.e., satisfying the following constraints (†):

1. the goal ϕ, and environment specifications E and E ′ are LTL formulas;
2. ΣEenv ⊆ ΣE ′ env ;

Furthermore, we will be mostly interested in the case where ϕ is agent-enforceable under E but not under E ′ , i.e., no agent strategy works (to satisfy the goal) against all environment strategies in ΣE ′ env , but there may be agent strategies that work against some of them. Although it may not be clear what a good agent-strategy should do, there is a basic principle about what it should not do: it should not do anything for which it can do better. Said positively, it should do a "best effort". Intuitively, the agent should use a strategy that enforces the goal under E, and also achieve the goal, as much as possible, under E ′ . Before we formalize this, consider the following:

Example 1. Take a robot whose goal is to go from the lobby to the roof using either the main elevator (ME) or the service elevator (SE). The robot starts by ME, and has 20 time-steps worth of battery life. There is a charging port inside each elevator (thus, once inside an elevator, it is certain to achieve the goal). The trip between the elevators takes 11 time-steps. Furthermore, the robot makes no partial trips (unless it runs out of battery), and once an elevator arrives the robot immediately takes it. The two environment specifications are:

• Expected (E): ME arrives within 5 time-steps of being called; the timing of SE is unpredictable.
• Exceptional (E ′ ): as above, but one of the elevators may be broken. Thus, in particular, if ME does not come within 5 time-steps then it is broken.

Consider the following two types of strategies (1) wait for ME until it comes or the battery runs out; (2) wait for ME for 0 ≤ w < 9 time-steps and then go to SE and wait there until it comes, or the battery runs out. Below we give an intuitive analysis of these strategies (the analysis will be formalised after we define the concept of best-effort in the next section).

Under the expected specification, the robot can enforce the goal using any strategy that waits at least 5 time-steps for ME (and does whatever if it doesn't arrive). In particular, it can do so using the strategy of type (1). However, the strategy of type (1) performs very poorly under the exceptional specification: if ME is broken, the goal is guaranteed to never be achieved.

Nonetheless, strategies that (i) enforce the goal under the expected specification, and (ii) do a best-effort under the exceptional specification - instead of hopelessly waiting forever for an obviously broken ME - do exist (such strategies will be captured by Definition 2 in Section 3). E.g., the strategy of type (2) with w = 5. It is important to note that this is not the only such strategy (i.e., it is not the "best" strategy) and that any strategy of type (2) with 5 ≤ w < 9 is just as good. While it seems that taking w = 5 gives the most opportunities to catch SE ("why wait by an obviously broken elevator?"), this is not true, as it implicitly assumes that the timing of SE is independent of the robot's actions - an assumption that is not part of the specification. Indeed, when facing the environment strategy that breaks ME and then sends SE to the lobby at time max(w + 1, 27 - w), the robot would achieve the goal if it chooses w = 8, but not if it takes w = 5.

Best-Effort Strategies. To formalize the notion of besteffort strategy, we first define what it means for an agent strategy to be better than another. The notion is sometimes called weak-dominance [Apt and Gr¨adel, 2011]. Here we call it simply dominance. Let E be an environment specification, and let ϕ be an agent goal. Define a binary relation ≥ϕ|E on agent strategies:

Definition 1 (Dominance). σ1 ≥ϕ|E σ2 iff for every σenv ∈ ΣEenv , PLAY(σ2, σenv) |= ϕ implies PLAY(σ1, σenv) |= ϕ. As usual, write σ1 >ϕ|E σ2 iff σ1 ≥ϕ|E σ2 and σ2 ≱ϕ|E σ1. If σ1 >ϕ|E σ2 we say that σ1 dominates σ2 (for goal ϕ under environment specification E).

Note that ≥ϕ|E is a preorder, and >ϕ|E is a strict partial order. For a set Σag of agent strategies, we say that σ2 ∈ Σag is maximal (with respect to >ϕ|E) if there is no σ1 ∈ Σag such that σ1 >ϕ|E σ2. The set of such maximal strategies is denoted MAXϕ|E (Σag).

Intuitively, σ1 >ϕ|E σ2 means that σ1 does as least as well as σ2 against every environment strategy enforcing E, and strictly better against at least one such environment strategy. In particular, if σ2 is not maximal, say σ1 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. Thus, within our framework, we consider maximal strategies as doing a "besteffort" to achieve the goal. See the related-work discussion for more on interpreting maximal strategies as "best-effort".

Obviously, enforcing strategies dominate all others. Thus:

Proposition 3. If ϕ is agent-enforceable under E, then MAXϕ|E (Σall ag ) is the set of strategies enforcing ϕ under E.

Going back to Example 1, we remark that we have seen that if an agent only focuses on strategies that enforce the goal ϕ under the expected specification E, it may result in strategies that fall short of the ideal. We now argue that only focusing on strategies that are best-effort under the exceptional specification E ′ may also fall short of the ideal. Indeed, since under this specification it is not clear which elevator works, and what the timing of the service elevator is, no strategy of type (2) is better than another, i.e., they are all making a besteffort for the goal under E ′ . This includes the strategy that immediately goes to SE and waits there, which clearly does not enforce the goal under E.

The Synthesis Problem. We now formally define the synthesis problem under expected and exceptional environments.

Definition 2. Given ϕ, E, E ′ satisfying (†), find an agent strategy in MAXϕ|E ′ (Σϕag ).

In words: amongst the agent strategies enforcing ϕ under the expected environment specification E (if any), find one that does the best-effort for ϕ under the exceptional environment specification E ′ . Note that the case E = E ′ is synthesis under environment specifications (cf. Theorem 2), and the cast E = E ′ = true is classical synthesis (cf. Theorem 1).

Our synthesis problem has two important properties, captured by Theorems 4 and 7 below. The first is that if a goal ϕ is agent-enforceable under the expected specification E, then there always exists a strategy that enforces ϕ under the expected specification E and that is best-effort under the exceptional specification E ′ :

Theorem 4. Given ϕ, E, E ′ satisfying (†), if ϕ is agentenforceable under E, then MAXϕ|E ′(MAXϕ|E(Σall ag )) ̸= ∅.

The proof of this theorem requires a sophisticated argument, which we now sketch. We start by giving alternative characterizations of dominance and maximality, which are of interest in their own right. These characterizations are adaptations of ones in [Berwanger, 2007] to our setting. Intuitively, one assigns to a strategy σag, and an environmenthistory h ∈ (2X )+, the value +1 (winning) if σag, starting from h, enforces ϕ under E; the value -1 (losing) if σag, starting from h, enforces ¬ϕ under E; and 0 (pending) otherwise. The characterization says that σ1 ≥ϕ|E σ2 iff the value of σ1 is as least as big as that of σ2 on all environment histories at which σ1, σ2 agree except for the last point. Formally, an environment-history h ∈ (2X )+ is the projection of a (joint) history h′ ∈ (2X∪Y )+ if hn = h′n ∩ X for all n < |h|. Say that h is compatible with σag, σenv iff h is the projection of a prefix of PLAY(σag, σenv). Given a set Σenv of environment strategies, let H(σag,Σenv) be the set of environment histories compatible with σag, σenv for some σenv ∈ Σenv. Given a goal ϕ and an environment specification E, for every h ∈ H(σag,ΣEenv ), let:

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

Agent-strategies σ1, σ2 split at an environment-history h if σ1(h′ ) = σ2(h′ ) for every proper prefix h′ of h, but σ1(h) ̸= σ2(h). Since σ1, σ2 agree on proper prefixes of h, then, for every environment strategy σenv, the history h is compatible with σ1, σenv iff it is compatible with σ2, σenv. If σ1, σ2 split at h, denote by σ1[h ← σ2] the strategy that agrees with σ1 everywhere, except on h and all its extensions where it agrees with σ2. A set Σag is closed under shifting if for all σ1, σ2 ∈ Σag and every h at which they split, σ1[h ← σ2] ∈ Σag.

Lemma 5 (Characterization of Dominance). Given a goal ϕ, an environment specification E, and agent strategies σ1, σ2, then A) σ1 ≥ϕ|E σ2 iff for every h ∈ H(σ1,ΣEenv ), if σ1, σ2 split at h then: (i) valϕ|E(σ1, h) ≥ valϕ|E(σ2, h), and (ii) it is not the case that valϕ|E(σ1, h) = valϕ|E(σ2, h) = 0. Furthermore, B) σ1 >ϕ|E σ2 iff also (iii) σ1, σ2 split at some h ∈ H(σ1, ΣEenv ) such that valϕ|E (σ1, h) > valϕ|E (σ2, h).

Proof sketch. We will show case A. For i ∈ {1, 2}, let ‡i denote that PLAY(σi, σenv) |= ϕ. Suppose (i) and (ii) hold for σ1, σ2. To see that σ1 ≥ϕ|E σ2 we show that for every σenv ∈ ΣEenv for which ‡2 holds, also ‡1 holds. Indeed, if PLAY(σ1, σenv) ̸= PLAY(σ2, σenv), let h be the longest common environment-history compatible with σ1, σenv and σ2, σenv, and note that σ1, σ2 split at h. If ‡2 holds then valϕ|E(σ2, h) ≥ 0 which implies, by (i) and (ii), that valϕ|E(σ1, h) = 1, and in particular ‡1 holds.

For the converse, suppose that for some h at which σ1, σ2 split, either (i) or (ii) is violated. We will show that σ1 ̸≥ϕ|E σ2, i.e., that there is σenv ∈ ΣEenv such that ‡2 holds but ‡1 does not. If (i) fails then at h either σ1 is losing and σ2 is pending/winning, or σ1 is pending and σ2 is winning. In either case, for some σenv, ‡2 holds but not ‡1. If (ii) fails, there are strategies δ1, δ2 ∈ ΣEenv , such that h is compatible with both σ1, δ1 and σ2, δ2, and PLAY(σ1, δ1) |= ¬ϕ and PLAY(σ2, δ2) |= ϕ. Let w ∈ (2Y )+ be the agent-history describing the outputs of σ1 (as well as σ2, since they agree on these prefixes) on the proper prefixes of h. Consider the environment-strategy σenv that agrees with δ1 everywhere, except on w·σ2(h) and all its extensions where it agrees with δ2, and observe that ‡2 holds but not ‡1. Note that σenv ∈ ΣEenv since both δ1 and δ2 enforce E.

Lemma 6 (Characterization of Maximality). For Σag closed under shifting, σ ∈ MAXϕ|E(Σag) iff for every σ′ ∈ Σag, and every h ∈ H(σ,ΣEenv ) at which σ, σ′ split, valϕ|E(σ, h) ≥ valϕ|E (σ′ , h).

Proof sketch. If valϕ|E(σ, h) < valϕ|E(σ′ , h) then σ ̸∈ MAXϕ|E(Σag) since, by Lemma 5, it is dominated by σ[h ← σ′ ]. For the other direction, if σ′ dominates σ then by Lemma 5, valϕ|E(σ′ , h) > valϕ|E(σ, h) for some h.

Proof Sketch of Theorem 4. Since ϕ is enforceable under E then, by Proposition 3, Σag .= MAXϕ|E (Σall ag ) is not empty. It remains to construct a strategy σag ∈ MAXϕ|E ′(Σag), which we do by constructing a chain of strategies, σ1, σ2, · · · that eventually stabilises on each history, and then let σag be the point-wise limit of this sequence, i.e., σag(h) := limi σi(h). We start with an arbitrary strategy σ0 ∈ Σag, and process the environment histories in increasing length-lexicographic order. At step i ≥ 1, consider the smallest history h not yet marked as stabilized, and mark it. Let Σh ⊆ Σag be the set of strategies that agree with σi on all proper prefixes of h, and let σ ∈ Σh be a strategy for which valϕ|E ′(σ, h) is the highest. If valϕ|E ′(σi, h) < valϕ|E ′(σ, h), then let σi+1 .= σi[h ← σ], and otherwise let σi+1 .= σi. Moreover, if valϕ|E ′(σi+1, h) ̸= 0, then also mark all the extensions of h as stabilized. The full proof shows that valϕ|E ′(σi, h) cannot deteriorate after h is marked and thus, by Lemma 5, σag is not dominated. Finally, using a careful argument involving Lemma 6 and the fact that ΣEenv ⊆ ΣE ′ env , one shows that σag ∈ Σag, and conclude that σag ∈ MAXϕ|E ′ (Σag).

The second important property of our synthesis problem is that instead of taking the best-effort strategies for ϕ assuming E, and amongst those choosing one that is best-effort for ϕ assuming E ′ , one can simply pick a strategy that is both besteffort for ϕ assuming E and best-effort for ϕ assuming E ′ .

Theorem 7. If ϕ, E, E ′ satisfy the constraint (†) then MAXϕ|E ′ (MAXϕ|E (Σall ag )) = MAXϕ|E(Σall ag )∩MAXϕ|E ′(Σall ag ).

Proof Sketch. Let Σag .= MAXϕ|E(Σall ag ) and observe that MAXϕ|E ′ (Σall ag )∩Σag ⊆ MAXϕ|E ′ (Σag) since a strategy σag ∈ Σag that is not dominated by any strategy is also not dominated by any strategy in Σag. For the reverse inclusion, observe that we only need to show that if σag ∈ MAXϕ|E ′(Σag) then σag ∈ MAXϕ|E ′(Σall ag ), i.e., no strategy whatsoever is >ϕ|E ′ σag. Suppose σ >ϕ|E ′ σag. Then σ ≥ϕ|E σag by item (2) in the constraint (†). But σag is ≥ϕ|E-maximal, hence so is σ, i.e., σ ∈ Σag. Since σag ∈ MAXϕ|E ′ (Σag), no strategy in Σag is >ϕ|E ′ σag, which is a contradiction.

We now discuss this theorem for the case that ϕ is agentenforceable under the expected specification E. In this case, by Proposition 3, the agent-strategies that are best-effort for ϕ under E are simply those that enforce ϕ under E. Then, Theorem 7 implies that solving the synthesis problem amounts to finding an agent strategy that enforces the goal under the expected environment on the one hand, and does a best-effort under the exceptional environment on the other hand. Thus, there is no trade-off between enforcing the goal under the expected environment specification, and making a best-effort for it under the exceptional one. This is quite surprising since it is analogous to saying that to get the tallest professors one can get the tallest people and intersect them with the professors. Indeed, there is no reason to think that there are any professors among the tallest people.

Interestingly, an analogue of Theorem 7 fails under the alternative view that environment specifications restrict traces of interest as in [Chatterjee and Henzinger, 2007], instead of environment strategies as in [Aminof et al., 2019a] and this paper (cf. Section 2).

Proposition 8. There exist LTL formulas ϕ, E, and E ′ with |= E ⊃ E ′ , the formula E ⊃ ϕ agentenforceable, the formula E ′ ⊃ ϕ not agent-enforceable, such that MAXE⊃ϕ|true(Σall ag ) ∩ MAXE ′⊃ϕ|true(Σall ag ) = ∅ and MAXE ′⊃ϕ|true(MAXE⊃ϕ|true(Σall ag )) ̸= ∅.

Proof. Let X .= {x}, Y .= {y}, E .= x ⊃ Gy, E ′ := true and ϕ .= x ⊃ (GFx ∧ Gy). Then, strategies in the set M of maximal agent-strategies for E ⊃ ϕ do the following: if the environment starts with ¬x then they can do anything (since, in this case, both E and ϕ are true); if the environment starts with x then at some point they do ¬y (since, doing this, the agent ensures that the assumption E fails, and thus E ⊃ ϕ is satisfied). On the other hand, strategies in the set M ′ of maximal agent-strategies for E ′ ⊃ ϕ, i.e., for ϕ, do the following: if the environment does ¬x they can do anything, and otherwise they always do y (which ensures, in this case, that ϕ is satisfied if the environment does x infinitely often). Note, however, that M ∩ M ′ = ∅. On the other hand MAXE ′⊃ϕ|true(MAXE⊃ϕ|true(Σall ag )) is non-empty (indeed, it contains all strategies inM.)

Hence, even if the two views of environment specifications share most properties when synthesizing under single environment specifications [Aminof et al., 2019a], they do not under expected and exceptional environment specifications.

4 Decidability of Synthesis

Next we show that the synthesis problem is decidable. We do so using an automata-theoretic approach. We represent strategies as trees, build tree-automata that recognize the sets MAXϕ|E ′ (Σall ag ) and Σϕag , then pick a strategy (if one exists) in their intersection. This outline is correct by Theorem 7 and Proposition 3.

Theorem 9. There is an algorithm that solves the problem of synthesis under expected and exceptional environments, i.e., that given ϕ, E, E ′ satisfying (†) returns a finite-state strategy in MAXϕ|E ′ (Σϕag ).

We give a succinct review of the relevant notation and results about tree automata, see [Gr¨adel et al., 2002].

Encoding. Functions of the form f : B∗ → A can be thought of as B-branching A-labeled trees, i.e., the nodes are the elements of B∗ and the label of w is f(w). Similarly, a pair (f1, f2) of functions fi : B∗ → A can be encoded as the tree in which node w ∈ A∗ is labeled by the pair (f1(w), f2(w)). We encode agent-strategies, and pairs of agent-strategies in this way, i.e., B .= 2X ,A .= 2Y (the label of the root is assumed to be fixed since it does not encode anything).

Tree Automata. An alternating parity tree automata (APT) T is a tuple (B,A,Q, q0, δ, c) a finite branching alphabet B, a finite input alphabet A, a finite set of states Q, an initial state q0 ∈ Q, a transition function δ : Q×A → PosBool(B ×Q), and a priority function c : Q → N. Here PosBool(X) is the set of positive Boolean formulas over the atoms X. An APT in which every formula is of the form ∧b∈B (b, qb) is called deterministic. Tree automata take trees t : B∗ → A as input, and process them, starting at the root in the initial state. Intuitively, if the APT is at node w ∈ A∗ of the input tree t, and the current state is q ∈ Q, then the APT picks a satisfying assignment C ⊆ B × Q of the formula δ(q, t(w)) and, for each (b, q) ∈ C sends a copy of itself in state q in the direction b. Intuitively, a tree t is accepted by an APT T if the evolution of every sequence of copies has the property that the smallest priority seen infinitely often is even. The set of all trees accepted by T is called the language of T. APTs are effectively closed under Boolean operations and projection. Moreover, one can decide, given an APT T, if its language is non-empty, and in this case also extract a finite-state representation of some t accepted by T. We also use automata on words. We can think of words as trees with |B| = 1, i.e., no branching. In this case we will ignore B and write δ : Q × A → PosBool(Q). Given an LTL formula ϕ, one can construct a deterministic parity word automaton (DPW) Dϕ accepting exactly the models of ϕ. We write Dϕ = (2AP , Qϕ, qϕ, δϕ, cϕ).

Proof Sketch of Theorem 9. The interesting step is to show how to build an APT D′ that accepts exactly the pairs (σ1, σ2) of agent strategies such that σ1 ̸≥ϕ|E ′ σ2. Given this, one can build an APT Mϕ|E ′ that accepts exactly the agent strategies σ in MAXϕ|E ′(Σall ag ) by using the fact that maximality is definable in terms of D′ , Boolean operations, and projection, i.e., following Definition 1, σ is maximal iff ¬∃σ′ . (σ′ ≥ϕ|E ′ σ)∧(σ ̸≥ϕ|E ′ σ′ ). Finally, one can extract a finite-state strategy from Mϕ|E ′ .

To illustrate some of the core ideas, we first sketch how to build an APT T ′ that accepts σag iff σag does not enforce ϕ under E ′ , i.e., iff there exists σenv such that σenv ▷ E ′ and PLAY(σag, σenv) |= ¬ϕ. Let DE ′ and D¬ϕ be DPWs for E ′ and ¬ϕ respectively. Intuitively, T ′ will use its nondeterminism to guess σenv (step by step), and simulate DE ′ to verify σenv ▷ E ′ , and simulate D¬ϕ to verify that PLAY(σag, σenv) |= ¬ϕ.

The states of T ′ are of the form (s, q) and s where s ∈ QE ′ and q ∈ Q¬ϕ. For the transitions, we describe what the automaton does when it is at node w ∈ (2X )∗ in a given state. When w is the empty string, the APT T ′ nondeterministically chooses X′ ⊆ X and sends a copy in state (sE ′ , q¬ϕ) in direction X′ (this corresponds to guessing σenv(λ), the first action of the environment). When w is not the empty-string, the APT T ′ reads the agent action σag(w) ⊆ Y , and works differently depending if it is in a state of the form (s, q) or s.

If the APT T ′ is in a state of the form (s, q) it does two things: 1) for every Y ′′ ⊆ Y such that Y ′′ ̸= σag(w), it nondeterministically chooses an environment action X′′ ⊆ X and sends in direction X′′ a copy of DE ′ in state s′ := δE ′(s,X′′ ∪ Y ′′ ); and 2) for Y ′′ = σag(w), it also guesses an environment action X′′ ⊆ X and sends (s′ , q′ ) in direction X′′ where s′ is as before and q′ := δ¬ϕ(q,X′′ ∪ Y ′′ ). Intuitively, 1) means that T ′ is implicitly guessing an environment strategy σenv and checks that it enforces E ′ ; and 2) means that it checks that PLAY(σag, σenv) satisfies ¬ϕ.

If the APT T ′ is in a state of the form s it does the following: for every Y ′′ ⊆ Y (including the current label) it nondeterministically chooses an environment action X′′ ⊆ X and sends in direction X′′ a copy of DE ′ in state s′ := δE ′(s,X′′ ∪ Y ′′ ). Intuitively, this is like 1) in the previous case, except that since it is at a node that is not on PLAY(σag, σenv) it no longer simulates D¬ϕ.

We now describe how to adapt this construction to build the APT D′ . Recall that we require that D′ accepts (σ1, σ2) iff there exists σenv ▷ E ′ such that PLAY(σ1, σenv) |= ¬ϕ and PLAY(σ2, σenv) |= ϕ. The states of D′ are of the form (s, q, r), (s, q), (s, r), and s, where s ∈ QE ′ , q ∈ Q¬ϕ, and r ∈ Qϕ. Intuitively, transitions from states of the form s and (s, q) are as before, transitions from states (s, r) are like those of (s, q) but they use the automaton Dϕ instead of D¬ϕ, and transitions of the form (s, q, r) from node w ∈ (2X )+ send copies of the form (s′ , q′ , r′ ) if σ1(w) = σ2(w), and copies of the form (s′ , q′ ) and (s′ , r′ ) otherwise. In any case, they also send copies of the form s′ , as before. Thus, the copies of s verify that σenv ▷ E ′ , the copies of q that PLAY(σ1, σenv) |= ¬ϕ, and the copies of r that PLAY(σ2, σenv) |= ϕ.

5 RelatedWork and Conclusions

Agents in our framework have two models of environment behaviour, expected and exceptional. The importance of multiple environment models is recognized in other work on agents operating in complex AI scenarios. E.g., in [Chakraborti et al., 2019] agents use one model of the world to plan, and a different model is used for explanations for the human operator, and in [De Giacomo et al., 2019; Camacho et al., 2019] reinforcement learning agents complement their features extracted from the world with a second model which specifies rewards based on knowledge representation.

An alternative approach to capturing expected behaviour is to use a stochastic setting. In the usual approach to synthesis for probabilistic systems the environment is not given as a set of strategies, as we do, but rather as a single stochastic system (e.g., as an MDP). This setting has been extended to include a second environment in the so-called "beyond worstcase synthesis problem", which concerns finding a strategy that guarantees worst-case performance against an adversarial environment, while maximising the expected performance against a fixed stochastic environment [Bruy`ere et al., 2017].

The synthesis problem can be expressed in a number of logics tailored for strategic reasoning. In particular, Strategy Logic and its variants [Mogavero et al., 2014; Berthon et al., 2017; Aminof et al., 2019b] - which can quantify over variables for (possibly randomized) strategies - can naturally express complex strategic properties, including dominance and maximality.

"Best-effort" strategies, sometimes called "admissible", were studied in the verification literature, however, without distinguishing expected from exceptional environments. For instance, [Berwanger, 2007] studies the process of iteratively avoiding dominated strategies, [Faella, 2009] justifies admissibility amongst other solution-concepts in environments that may not be adversarial, and [Brenguier et al., 2017] assumes the environment has its own objective and both the agent and the environment use non-dominated strategies.

Exceptional environments are related to safety analysis via fault-injection [Bozzano and Villafiorita, 2007; Ezekiel et al., 2011; Ezekiel and Lomuscio, 2017]. Specifically, exceptional environments may be seen as the result of mutations from expected environments via fault-injection. While safety-analysis is concerned with generating these mutated models algorithmically using fault-profiles and then verifying them, we assume that they are given and use them to synthesize agent strategies against them.

The exact complexity of the synthesis problem under expected and exceptional environments is left open. Other future work includes finding better algorithms for special cases, including nondeterministic planning domains and LTL formulas on finite traces for specifying non-Markovian domains.

Acknowledgements

Benjamin Aminof is supported by the Austrian Science Fund (FWF): P 32021. Giuseppe De Giacomo is supported in part by the ERC under the European Union's Horizon 2020 Programme through the ERC Advanced Grant WhiteMech (No. 834228). Alessio Lomuscio is supported by a Royal Academy of Engineering Chair in Emerging Technologies.