Synthesis of Maximally Permissive Strategies for LTLf Specifications

1 Introduction

One of the key problems of Artificial Intelligence is to equip intelligent agents with autonomous capability of deliberating the execution of complex courses of action to accomplish desired tasks [Reiter, 2001; Ghallab et al., 2016]. This problem is related to reactive synthesis in Formal Methods: we have an agent acting in an adversarial environment such that the agent controls certain variables (the agent actions) and the environment controls the others (the environment reactions); given a specification of the task, the agent has to find a strategy (plan/policy/controller/program) to choose its actions to fulfill the task in spite of all possible environment reactions [Pnueli and Rosner, 1989]. Specifically, reactive synthesis shares deep similarities with planning in fully observable nondeterministic domains (FOND, strong plans) [Cimatti et al., 2003; Geffner and Bonet, 2013].

In Formal Methods, the most common formalism for specifying tasks is Linear Temporal Logic (LTL) [Pnueli, 1977]. In AI, a finite trace variant of LTL (LTLf ) is popular [Baier and McIlraith, 2006; De Giacomo and Vardi, 2013;

∗Corresponding Author

De Giacomo and Vardi, 2015; Zhu et al., 2017; De Giacomo and Rubin, 2018; Camacho et al., 2019]. The interest on finite traces is due to the observation that typically intelligent agents are not dedicated to a single task all their life, but are supposed to accomplish one task after another.

Deliberating courses of action (i.e., strategies) is also related to controller synthesis in Discrete Event Systems (DES) [Ehlers et al., 2017]. In DES we are primarily interested in a variant of the problem: suitably control an agent's behavior to conform to a set of specifications while preserving its autonomy as much as possible. In other words, we want to synthesize a controller that embeds all possible allowed courses of action so that whatever actual course of action the agent chooses, the specifications are satisfied. Such a controller is said to be maximally permissive [Wonham and Ramadge, 1987; Cassandras and Lafortune, 2008; Wonham and Cai, 2019]. Maximally permissive controllers are indeed also of interest in AI, as discussed, e.g., in [De Giacomo et al., 2012; De Giacomo et al., 2013; Banihashemi et al., 2016; Banihashemi et al., 2018; De Giacomo et al., 2020].

In this paper, following this idea, instead of computing a classical (aka, deterministic) strategy for fulfilling a task, we aim at computing the maximally permissive strategy, i.e., the entire set of strategies that fulfil the task. This allows the agent to be able to choose among them while in execution, without committing to any specific one beforehand.

A classical strategy for a task, while already considers all possible environment reactions, prescribes in any circumstances exactly what action to do until the task is fulfilled. This leaves no freedom to the agent in choosing actions that would not harm fulfilling the original task, but would allow the agent to take additional opportunities, such as additional tasks. The maximally permissive strategy, i.e., the entire set of strategies fulfilling a task, instead, gives the maximal freedom of the agent in taking more opportunities, while guaranteeing that the original task is being accomplished.

To capture the notion of maximally permissive strategy, we rely on nondeterministic strategies. A classical (aka, deterministic) strategy is a function from the history so far to the next action the agent should perform. A nondeterministic strategy is a function from the history to a set of next actions such that by arbitrarily choosing among them, at each step, we get a deterministic strategy that accomplishes the task. In other words, a nondeterministic strategy represents a set of deterministic strategies.

The foundational result of DES is that for the kind of specification of interest in DES, which are safety specifications, there exists a unique nondeterministic strategy that is able to represent the maximally permissive strategy, i.e., the entire set of deterministic strategies. Unfortunately, this powerful result applies only to safety properties [Bernet et al., 2002]. In particular, a nondeterministic strategy that is able to represent the entire set of deterministic strategies does not exist for reachability properties, or for LTLf specifications. Yet, the need for computing the maximally permissive strategies exists, and techniques to approximate it have been studied, e.g., in [Sakakibara and Ushio, 2020].

In this paper, we show that maximally permissive strategies for reachability and general LTLf properties are still representable via nondeterministic strategies. Specifically, the entire set of deterministic strategies to fulfil an LTLf task can be characterized by two (vs. one) nondeterministic strategies and a constraint that requires to eventually switch from the first one to the second one. Interestingly, these two nondeterministic strategies can be computed with minimal overhead wrt the computation of a single deterministic strategy using state-of-the-art tools.

2 Preliminaries

LTLf Basics. Linear-time Temporal Logic on finite traces (LTLf ) is a specification language to express temporal properties on finite traces [De Giacomo and Vardi, 2013]. In particular, LTLf has the same syntax as LTL, which is instead interpreted over infinite traces [Pnueli, 1977]. Given a set of propositions Prop, LTLf formulas are generated as follows:

ϕ ::= a | (ϕ∧ϕ) | (¬ϕ) | (◦ϕ) | (ϕU ϕ) where a ∈ Prop is an atom, ◦ for Next, and U for Until are temporal operators. We make use of standard Boolean abbreviations such as ∨ (or) and → (implies), true and false. In addition, we define the following abbreviations Weak Next ·ϕ ≡ ¬◦¬ϕ, Eventually ♦ϕ ≡ true U ϕ and Always □ϕ ≡ false Rϕ, where R is for Release.

A trace π = π0π1 . . . is a sequence of propositional interpretations (sets), where for every i ≥ 0, πi ∈ 2Prop is the i-th interpretation of π. Intuitively, πi is interpreted as the set of propositions that are true at instant i. We denote the last instant (i.e., index) in a trace π by lst(π). A trace π is an infinite trace if lst(π) = ∞, which is formally denoted as π ∈ (2Prop )ω ; otherwise π is a finite trace, denoted as π ∈ (2Prop )∗ . Moreover, by πk = π0 · · · πk we denote the prefix of π up to the k-th iteration, and πk = ϵ denotes an empty trace if k < 0. LTLf formulas are interpreted over finite, nonempty traces. Given π, we define when an LTLf formula ϕ holds at instant i, 0 ≤ i ≤ lst(π), written as π, i |= ϕ, inductively on the structure of ϕ, as:

• π, i |= a iff a ∈ πi (for a ∈ Prop);
• π, i |= ϕ1 ∧ϕ2 iff π, i |= ϕ1 and π, i |= ϕ2;
• π, i |= ¬ϕ iff π, i ̸|= ϕ;
• π, i |= ◦ϕ iff i < lst(π) and π, i + 1 |= ϕ; · π, i |= ϕ1 U ϕ2 iff ∃j such that i ≤ j ≤ lst(π) and
• π, j |= ϕ2, and ∀k, i ≤ k < j we have that π, k |= ϕ1. We say π satisfies ϕ, written as π |= ϕ, if π, 0 |= ϕ.

Reactive Synthesis. The problem of reactive synthesis can be viewed as a game of the environment and the agent. The goal of reactive synthesis is to synthesize an agent strategy such that no matter how the environment behaves, the combined behavior trace of both players satisfy desired properties [Pnueli and Rosner, 1989]. Formally, a reactive synthesis problem is described as a tuple P = 〈X , Y, ϕ〉, where X and Y are two disjoint sets of variables controlled by the environment and the agent, respectively, and ϕ is a logical specification formula over X ∪Y expressing desired properties. A deterministic agent strategy is a function σag : (2X∪Y )∗ ×2X → 2Y . A play is a sequence π = (X0 ∪ Y0)(X1 ∪ Y1) · · · ∈ (2X∪Y )ω over the alphabet 2X∪Y . A play π is compatible with an agent strategy σag if σag(πi-1 ,Xi) = Yi for every i ≥ 0. Analogously, finite prefix πk is compatible with σag if σag(πi-1 ,Xi) = Yi for every 0 ≤ i ≤ k. Given a synthesis problem P = 〈X , Y, ϕ〉, an agent strategy σag realizes ϕ, with respect to the corresponding X and Y, if every play π that is compatible with σag satisfies ϕ. Sometimes, for simplicity, we do not explicitly mention X and Y if they are clear from the context. In this paper, we focus on LTLf synthesis.

Definition 1 (LTLf synthesis). The problem of LTLf synthesis is described as a tuple P = 〈X, Y, ϕ〉, where ϕ is an LTLf formula over X ∪ Y. Computing an agent strategy that realizes ϕ if one exists, is called the LTLf synthesis problem.

Solving LTLf synthesis is known to be 2EXPTIMEcomplete [De Giacomo and Vardi, 2015].

Two-player Games. Classical solutions to LTLf synthesis relies on a reduction to two-player games. A two-player game is described as a tuple G = (A,W), where A is the game arena and W is the winning objective. For synthesis, we often take the corresponding deterministic automaton of the formula as the game arena, which is a tuple A = (2X∪Y , S, s0, δ), where δ : S × 2X∪Y → S is the transition function. Given a play π = (X0 ∪ Y0)(X1 ∪ Y1) . . . ∈ (2X∪Y )ω , running π on A gives us an infinite sequence ρ = s0s1 . . . ∈ Sω such that s0 is the initial state and si+1 = δ(si,Xi ∪ Yi) for all i ≥ 0. Since the transitions in A are all deterministic, we thus denote by ρ = Run(π, A) the unique sequence of running π on A. Analogously, we denote by ρk = Run(πk ,A) the unique finite sequence of running πk on A, and ρk = s0s1 . . . sk+1. The winning objective W indicates a set of desired plays for the agent. A play π is a winning play with respect to winning objective W if π ∈ W. In this paper, we only consider two-player games with Reachability objectives (Reachability games). More specifically, the winning objective W = Reach(F), and Reach(F) = {π ∈ (2X∪Y )ω | ρ = Run(π,A) and ∃ℓ ≥ 0: ρℓ ∈ F}, where F ⊆ S is a set of goal states. Intuitively, reachability games require that a goal state in F is visited at least once.

An agent strategy σag is winning in G = (A, Reach(F )) if every play π that is compatible with σag is winning, i.e., π ∈ W. In Reachability games, s ∈ S is a winning state for the agent (resp. environment) if the agent (resp. the environment) has a winning strategy in the game G = (A′ ,Reach(F)), where A′ = (2X∪Y , S, s, δ), i.e., the same arena A but with the new initial state s. By Wag(G) (resp. Wenv(G)) we denote the set of all agent (resp. environment) winning states.

Intuitively, Wag represents the "agent winning region", from which the agent is able to win the game, no matter how the environment behaves.

Symbolic LTLf Synthesis. State-of-the-art LTLf synthesis tools [Bansal et al., 2020; De Giacomo and Favorito, 2021] leverage the symbolic synthesis framework presented in [Zhu et al., 2017; Tabajara and Vardi, 2019], which solves the synthesis problem via a symbolic reachability game computation. The game arena A = (2X∪Y , S, s0, δ) is compactly represented symbolically, by encoding the state space using a logarithmic number of propositions. The symbolic representation of A is a tuple As = (X, Y,Z, I, η), where Z is a set of variables such that |Z| = ⌈log |S|⌉, and every state s ∈ S corresponds to an interpretation Z ∈ 2Z over Z. I is a Boolean formula satisfied only by the interpretation of the initial state s0. η : 2X ×2Y ×2Z → 2Z is a Boolean function mapping interpretations X, Y and Z of the propositions of X, Y and Z to a new interpretation Z ′ of the propositions of Z, such that if Z corresponds to a state s ∈ S then Z ′ corresponds to the state δ(s,X ∪ Y ). The set of goal states is represented by a Boolean formula g over Z that is only satisfied by the interpretations of states in F. Accordingly, we denote the symbolic reachability game as Gs = (As, Reach(g)).

The game is solved by performing a least fixpoint computation over two Boolean formulas w over Z and t over Z ∪ X ∪ Y, which represent the agent winning region Wag and tuples of winning states, environment actions with suitable agent actions, respectively. w and t are initialized as w0(Z) = g(Z) and t0(Z,X, Y) = g(Z), since every goal state is an agent winning state. Note that t0 is independent of the propositions from X ∪Y, since once the play reaches goal states, the agent can do whatever it wants. ti+1 and wi+1 are constructed as follows:

The computation reaches a fixpoint when wi+1 ≡ wi. At this point, no more states will be added, and so all agent winning states have been collected. By evaluating wi+1 on I we can know if there exists a winning strategy. If that is the case, ti+1 can be used to compute a winning strategy through the mechanism of Boolean synthesis [Fried et al., 2016].

Nondeterministic Strategies. An agent strategy can also be nondeterministic, which prescribes for each history πk ∈ (2X∪Y )∗ , and an environment action X ∈ 2X , a set of agent actions to choose from nondeterministically. Formally, a nondeterministic agent strategy is denoted as a function Πag : (2X∪Y )∗ × 2X → 22Y . We denote the set of deterministic strategies induced by a nondeterministic strategy Πag as the set [[Πag]]. Every deterministic strategy σag ∈ [[Πag]] is obtained by a corresponding choice function ch: (2X∪Y )∗ × 2X → 2Y such that for every πk ∈ (2X∪Y )∗ that is compatible with ch and X ∈ 2X , ch(πk ,X) ∈ Πag(πk ,X) and σag(πk ,X) = ch(πk ,X). Nondeterministic strategy Πag realizes ϕ if every induced strategy σag ∈ [[Πag]] realizes ϕ. Sometimes, for simplicity, we say σag (resp. Πag) is a winning strategy of ϕ, instead of σag (resp. Πag) realizes ϕ. A

trace π (finite or infinite) is compatible with a nondeterministic strategy Πag if Yi ∈ Πag(πi-1 ,Xi) for every i ≥ 0. Comparing Strategies. Let P = 〈X, Y, ϕ〉 be a synthesis problem, and Πag a winning strategy of ϕ. We consider the permissiveness of Πag with respect to the deterministic strategies that it induces.

Definition 2. Let P = 〈X, Y, ϕ〉 be a synthesis problem, Πag and Π′ag two winning strategies of ϕ. Πag is more permissive than Π′ag if [[Π′ag ]] ⊆ [[Πag]].

3 Maximally Permissive Strategy

We first introduce the notion of maximally permissive strategy for a task, denoted by MaxSet, which consists of the entire set of deterministic winning strategies for the task, from which to choose one during the execution. Then we show that for special cases, we can compute a single nondeterministic strategy to capture MaxSet. However, in general, this does not happen for LTLf specifications.

Definition 3 (Maximally Permissive Strategy). Let P = 〈X, Y, ϕ〉 be a synthesis problem, the maximally permissive strategy of ϕ is MaxSet(ϕ) = {σag | σag is a deterministic winning strategy of ϕ}.

Theorem 1. Let P = 〈X, Y, ϕ〉 be a synthesis problem. If there exists a nondeterministic winning strategy Πag that is more permissive than every other winning strategy, then [[Πag ]] = MaxSet(ϕ). 1

Proof. Suppose there exists a nondeterministic winning strategy Πag that is more permissive than every other winning strategy Π′ag , such that [[Π′ag ]] ⊆ [[Πag]]. Note that every deterministic strategy σag can be considered as a special case of a nondeterministic strategy, in which case, [[σag]] = {σag}. Therefore, it holds that σag ∈ [[Πag]] for every deterministic winning strategy of ϕ, and so [[Πag]] = MaxSet(ϕ).

Although it is practical to utilize a single nondeterministic strategy Πag to express the maximally permissive strategy MaxSet(ϕ), this only applies to the cases where ϕ specifies a safety property, meaning that every violating trace has a finite bad prefix that falsifies the specification ϕ. This is because the problem of synthesizing safety properties can be reduced to a safety game, which always has a nondeterministic winning strategy Πag that is more permissive than every other winning strategy [Bernet et al., 2002]. However, this result does not apply to properties that are not safety [Bernet et al., 2002]. In particular, we give here a direct proof for LTLf specifications.

Theorem 2. In general, LTLf specifications do not admit a nondeterministic winning strategy Πag that is more permissive than every other strategy.

Proof. We prove by showing that such a strategy does not even exist for a simple LTLf specification ϕ = ♦b. In particular, we have b ∈ Y s.t. b is under the control of the agent. It is trivial to see that no matter how the environment behaves on X, the satisfaction of ♦b only relies on the agent. Suppose Πag is a nondeterministic winning strategy of ♦b that is more permissive than every other one. For every deterministic strategy σag ∈ [[Πag]], its corresponding choice function ch: (2{b} )∗ → 2{b} satisfies that ∃k ≥ 0 such that ch emits b at time step k (note that X can be ignored here), and ch keeps emitting ¬b for 0 ≤ i < k. Otherwise, σag is indeed not a winning strategy. Therefore, we can label every choice function with its corresponding k-value. We now take the choice function chm that has the greatest k-value, comparing to other choice functions of Πag. Then we can construct another choice function ch′ that keeps copying chm but postponing the moment of outputting b for one timestep.

1 It should be noted that the definition of maximally permissive strategy and Theorem 1 also applies to LTL synthesis.

Indeed, ch′ leads to a deterministic winning strategy σ′ag , since σ′ag outputs b at timestep m+ 1 and thus the compatible play π (a unique sequence, since X can be ignored in this example) is such that πm+1 |= ♦b holds. Therefore, σ′ag ∈ MaxSet(♦b), but σ′ag /∈ [[Πag]] leading to a contradiction. Thus, in general, LTLf specifications do not admit a nondeterministic winning strategy Πag that is more permissive than every other strategy.

4 MaxSet of LTLf Synthesis

We now explain how to compute MaxSet(ϕ) of LTLf synthesis problem P = 〈X, Y, ϕ〉, by reasoning on its corresponding reachability game. Recall that a winning strategy for safety games can be interpreted as a "staying in the winning region" strategy, since as long as the game stays in the winning region, the agent is able to force the game to move to another state that still belongs to the winning region [Bernet et al., 2002]. Nevertheless, for reachability games, such strategies do not necessarily lead to winning. This is because such a strategy can possibly generate a play that only stays in the winning region but never visits the goal states, which is indeed not a winning play. Therefore, apart from "staying in the winning region" such that the agent has the ability to win, no matter how the strategy keeps "deferring" the winning moment, a winning strategy also needs to start "non-deferring" such that eventually reaching goal states.

Here, we show how to capture the entire set of winning strategies of reachability games with two nondeterministic strategies. Intuitively, the first nondeterministic strategy keeps the agent in the winning region, where the agent is always able to win the game, which is called deferring strategy. The second nondeterministic strategy aims to taking the agent to goal states without any hesitation such that aggressively winning the game, which is called non-deferring strategy. Both strategies are defined with respect to the agent winning region, therefore, we assume that the agent winning region Wag = ⋃0≤i≤n Wi is computed apriori via a least fixpoint computation and s0 ∈ Wag such that there is at least one agent winning strategy of the reachability game [De Giacomo and Vardi, 2015].

4.1 Deferring Strategy

For reachability games G = (A,Reach(F)), a deferring strategy should keep the play in the agent winning region Wag, if the reachability goal F is not visited yet, and so the agent is able to keep deferring the winning moment.

Definition 4 (Deferring strategy of reachability games). Let G = (A,Reach(F)) be a reachability game and Wag the set of agent winning states. σdf ag is a deferring strategy, if for every play that is compatible with σdf ag , ρ = Run(π, A), such that ρ = s0s1 . . . satisfies s0 ∈Wag and ∀ℓ ≥ 0, if sℓ /∈ F then sℓ+1 ∈Wag.

Lemma 1. Let G = (A,Reach(F)) be a reachability game, and Wag be the agent winning region. Then s0 ∈ Wag iff there exists a deferring strategy.

In order to obtain a deferring strategy, we define a strategy generator based on the winning region Wag, represented as a nondeterministic transducer, where nondeterminism is of the kind "don't-care": all nondeterministic choices are equally good. The strategy generator T df = (2X∪Y , S, s0, ϱ, τ) is constructed as follows:

• 2X∪Y , S and s0 are the same as in A;
• ϱdf : S × 2X → 2S is the transition function such that ϱdf (s, X) = {s′ |s′ = δ(s, X ∪ Y ) and Y ∈ τ df (s, X)};

This transducer represents a nondeterministic deferring strategy Πdf ag : (2X∪Y )∗ × 2X → 22Y in the following way: ∀πk ∈ (2X∪Y )∗ that is compatible with Πdf ag , and ∀X ∈ 2X ,

• τ df : S × 2X → 22Y is the output function such that ∀X ∈ 2X , τ df (s,X) = {Y | δ(s,X ∪ Y ) ∈ Wag} if s ∈ Wag\F ; otherwise, τ df (s, X) = 2Y .

where ρk = Run(πk ,A) such that ρk = s0s1 . . . sk+1. Every deterministic deferring strategy σdf ag is generated from Πdf ag by a corresponding choice function chdf : (2X∪Y )∗ × 2X → 2Y such that ∀πk ∈ (2X∪Y )∗ that is compatible with chdf , and ∀X ∈ 2X , chdf (πk ,X) ∈ Πdf ag (πk ,X) and σag(πk , X) = chdf (πk , X).

Theorem3. Let G = (A,Reach(F)) be a reachability game, and Πdf ag be computed as above. Then deterministic strategy σag is a deferring strategy iff σag ∈ [[Πdf ag ]].

4.2 Non-Deferring Strategy

Different from a deferring strategy that keeps deferring the winning moment, a non-deferring strategy brings the play closer to goal states F at every timestep until reaching it. In order to represent the distance towards F, for every state s ∈ Wag, where Wag = ⋃0≤i≤n Wi, computed by a least fixpoint computation, we introduce a distance value d(s) that indicates the shortest distance from s to F. Therefore, ∀s ∈ Wag, if s ∈ F (i,e., s ∈ W0) then d(s) = 0; otherwise, since s ∈ Wi+1\Wi for some 0 ≤ i ≤ n, we have d(s) = i + 1. We now introduce non-deferring strategy.

Definition 5 (Non-Deferring strategy of reachability games). Let G = (A,Reach(F)) be a reachability game and Wag be the agent winning region. σndf ag is a non-deferring strategy, if for every play π that is compatible with σndf ag , ρ = Run(π, A) such that ρ = s0s1 . . . satisfies s0 ∈ Wag and ∃ℓ ≥ 0.d(sℓ) = 0 and ∀0 ≤ j ≤ ℓ.d(sj+1) = d(sj ) - 1.

Lemma 2. Let G = (A,Reach(F)) be a reachability game, and Wag be the agent winning region. Then s0 ∈ Wag iff there exists a non-deferring strategy.

In order to obtain a non-deferring strategy, we also define a strategy generator based on the winning region Wag = ⋃0≤i≤n Wi, represented as a nondeterministic transducer T ndf = (2X∪Y , S, s0, ϱndf , τ ndf ), where

• 2X∪Y , S and s0 are the same as in A;
• ϱndf : S × 2X → 2S is the transition function such that ϱndf (s, X) = {s′ |s′ = δ(s, X ∪ Y ) and Y ∈ τ ndf (s)};

This transducer represents a nondeterministic nondeferring strategy Πndf ag : (2X∪Y )∗ × 2X → 22Y in the following way: ∀πk ∈ (2X∪Y )∗ that is compatible with Πndf ag , and ∀X ∈ 2X

• τ ndf : S × 2X → 22Y is the output function such that ∀X ∈ 2X , τ ndf (s,X) = {Y |δ(s,X ∪ Y ) ∈ Wi} if s ∈ Wi+1\Wi, otherwise τ ndf (s, X) = 2Y .

where ρk = Run(πk ,A) such that ρk = s0s1 . . . sk+1. Every deterministic strategy σndf ag is generated from Πndf ag by a corresponding choice function chndf : (2X∪Y )∗ ×2X → 2Y such that ∀πk ∈ (2X∪Y )∗ that is compatible with chndf , and ∀X ∈ 2X , chndf (πk , X) ∈ Πndf ag (πk ,X) and σndf ag (πk ,X) = chndf (πk , X).

Theorem4. Let G = (A,Reach(F)) be a reachability game, and Πndf ag be computed as above. Then deterministic strategy σag is a non-deferring strategy iff σag ∈ [[Πndf ag ]].

Theorem5. Let G = (A,Reach(F)) be a reachability game, Πdf ag and Πndf ag be computed as above, respectively. Then [[Πndf ag ]] ⊆ [[Πdf ag ]].

4.3 Maximally Permissive Strategy

We now explain how to obtain the maximally permissive strategy MaxSet through nondeterministic strategies Πdf ag and Πndf ag . To do so, we start with showing how to induce deterministic strategies out of Πdf ag and Πndf ag . Every deterministic strategy σag is generated from nondeterministic strategies Πdf ag and Πndf ag by a corresponding choice function ch: (2X∪Y )∗ ×2X → 2Y . Intuitively speaking, apart from restricting σag to be a deferring strategy such that being able to postpone the winning moment, ch also restricts σag to change to a non-deferring strategy such that eventually reaching the goal states. Formally, we require ch satisfying both of the following conditions:

1. for every πk ∈ (2X∪Y )∗ compatible with ch, and ∀X ∈ 2X . ch(πk ,X) ∈ Πdf ag (πk , X);

Every choice function ch: (2X∪Y )∗ × 2X → 2Y that satisfies the above characteristic is able to induce a deterministic strategy out of nondeterministic strategies Πdf ag and Πndf ag . Note that choice functions are a general mathematical means

1. for every π ∈ (2X∪Y )ω compatible with ch, ∃j ≥ 0 such that ∀h ≥ j, ch(πh-1 , Xh) ∈ Πndf ag (πh-1 ,Xh).

to extract deterministic strategies from nondeterministic ones. Their role here is to prove soundness (every choice function with the above characteristic will create a deterministic winning strategy) and completeness (every deterministic winning strategy can be captured by one such choice function). We denote the set of all induced deterministic strategies by [[Πdf ag , Πndf ag ]]. The following theorem shows that [[Πdf ag , Πndf ag ]] can capture the maximally permissive strategy.

Theorem 6. Let P = 〈X, Y, ϕ〉 be an LTLf synthesis problem, and Πdf ag , Πndf ag be computed as above. Then [[Πdf ag , Πndf ag ]] =MaxSet(ϕ).

Proof. We prove [[Πdf ag , Πndf ag ]] = MaxSet(ϕ) by showing that σag ∈ [[Πdf ag , Πndf ag ]] iff σag ∈ MaxSet(ϕ).

(⇒) We need to prove that every deterministic strategy σag ∈ [[Πdf ag , Πndf ag ]] is a winning strategy, such that σag ∈ MaxSet(ϕ). Indeed, σag is generated by a corresponding choice function ch: (2X∪Y )∗ ×2X → 2Y that follows our defined conditions. That is to say, ∀πk ∈ (2X∪Y )∗ that is compatible with σag, and ∀X ∈ 2X , σag(πk , X) ∈ Πdf ag (πk , X). Moreover, ∀π ∈ (2X∪Y )ω that is compatible with σag, ∃j ≥ 0 such that ∀h ≥ j, σag(πh-1 ,Xh) ∈ Πndf ag (πh-1 ,Xh). Thus, for every play π that is compatible with σag, ρ = Run(π,A) such that ρ = s0s1 . . . satisfies that s0 ∈ Wag and ∀ℓ ≥ 0, if sℓ+1 /∈ Wag, then ρℓ = s0s1 . . . sℓ+1 definitely has visited F already such that ϕ is satisfied already. This is because Πdf ag restricts π to stay in Wag before reaching F. Otherwise, from ℓ = j, σag switches to Πndf ag , which restricts ρ to eventually reach F such that ϕ is satisfied. Hence, σag is a winning strategy and so σag ∈ MaxSet(ϕ).

(⇐) We need to prove that every deterministic winning strategy σag ∈ MaxSet(ϕ) is such that σag ∈ [[Πdf ag , Πndf ag ]]. We now show that we can construct a choice function ch: (2X∪Y )∗ × 2X → 2Y that is able to generate the same agent strategy from Πdf ag and Πndf ag . First, we require ch being such that ∀πk ∈ (2X∪Y )∗ that is compatible with σag, ∀X ∈ 2X , ch(πk ,X) = σag(πk ,X). Indeed, every play π that is compatible with ch is also compatible with σag. Therefore, ∀π ∈ (2X∪Y )ω that is compatible with ch, it is trivial to see that ∀k ≥ 0, ch(πk-1 ,Xk) = σag(πk-1 ,Xk) ∈ Πdf ag (πk-1 ,Xk), since π has to stay in Wag before reaching F, otherwise, σag cannot be a winning strategy. Moreover, ∃ℓ ≥ 0, πℓ |= ϕ. Note that we take the smallest ℓ for πℓ |= ϕ. Indeed, ρℓ = Run(πℓ ,A) such that ρℓ = s0s1 . . . sℓ+1 satisfies that sℓ+1 ∈ F. Therefore, we have that ch(πℓ-1 , Xℓ) = σag(πℓ-1 , Xℓ) ∈ Πndf ag (πℓ-1 ,Xℓ), which, by construction, consists of all the Y s that lead sℓ to F in one step with Xℓ. Furthermore, ∀h > ℓ, ch(πh-1 ,Xh) = σag(πh-1 ,Xh) ∈ Πndf ag (πh-1 ,Xh), since ρh visits F already, and so Πndf ag (πh-1 ,Xh) = 2Y . We thus conclude that σag ∈ [[Πdf ag , Πndf ag ]] holds.

5 Implementation and Empirical Evaluation

In this section, we first describe how to leverage synthesis framework being integrated in state-of-the-art LTLf synthesis tools to compute the maximally permissive strategy. Then, by empirical evaluation, we show computing the maximally permissive strategy only brings a minimal overhead with respect to the computation of a single winning strategy.

5.1 Symbolic MaxSet Computation

Recall that the symbolic LTLf synthesis framework presented in [Zhu et al., 2017; Tabajara and Vardi, 2019] consists of computing two Boolean formulas w and t, which represent the agent winning region Wag and tuples of winning states, environment actions with suitable agent actions, respectively. We observe that Boolean formula t over Z ∪ X ∪ Y, in fact, is compatible with the non-deferring strategy generator T ndf = (2X∪Y , S, s0, ϱndf , τ ndf ) introduced in Section 4.2. More specifically, t is satisfied by interpretation (Z ∪ X ∪ Y ) ∈ 2Z × 2X × 2Y iff Y ∈ τ ndf (s,X), where s is the corresponding state of Z. This is because, during the fixpoint computation, an interpretation (Z ∪X ∪Y ) ∈ 2Z ×2X ×2Y satisfies ti+1 if: either (Z∪X∪Y ) satisfies ti; or Z was identified as a new winning state (Z |= wi+1 ∧ ¬wi), and so for every environment action X ∈ 2X we can move from Z to wi by setting agent action to some Y ∈ 2Y as long as following the transition function, expressed by wi(η(Z,X, Y)). Note that the second case restricts the agent to be non-deferring such that the next transition will move closer to goal states. For nondeterministic deferring strategy Πdf ag , we compute a boolean formula tdf over Z ∪ X ∪ Y as follows:

Note that (Z∪X∪Y ) ∈ 2Z∪X∪Y satisfies tdf if: either (Z∪ X ∪ Y ) satisfies t, since every non-deferring strategy is a deferring strategy; or the agent can move back to the winning region wi+1(Z) with another Y ∈ 2Y as long as following the transition function, expressed by wi+1(η(Z,X, Y)). In this case, tdf is satisfied by interpretation (Z∪X∪Y ) ∈ 2Z∪X∪Y iff they are compatible with the deferring strategy generator T df = (2X∪Y , S, s0, ϱdf , τ df ) such that Y ∈ τ df (s,X), where s is the corresponding state of Z.

5.2 Empirical Evaluation

Implementation. We implemented the symbolic maximally permissive strategy computation technique for LTLf synthesis by extending the symbolic synthesis framework [Zhu et al., 2017; Tabajara and Vardi, 2019] integrated in state-of-the-art synthesis tools [Bansal et al., 2020; De Giacomo and Favorito, 2021]. In particular, we based on LTLf synthesis tool LYDIA 2 , the overall best performing tool, and implemented our fixpoint-based computation presented in Section 5.1. More specifically, the computation consists of two steps. In the first step, we based on the code of LYDIA, to perform realizability checking, and the nondeterministic non-deferring strategy is also obtained as a side-effect, represented in Binary Decision Diagrams (BDDs). The second step makes use of Boolean operations provided by BDD library CUDD-3.0.0 [Somenzi, 2016] to compute the nondeterministic deferring strategy. 3

2 https://github.com/whitemech/lydia

3 Source code at https://github.com/Shufang-Zhu/SyftMax

Experiment Setup. All tests were ran on a computer cluster. Each test took exclusive access to a node with Intel(R) Xeon(R) CPU E5-2650 v2 processors running at 2.60GHz. Time out was set to 300 seconds.

Benchmarks. We took the LTLf synthesis benchmarks from literature [Tabajara and Vardi, 2019; Bansal et al., 2020; De Giacomo and Favorito, 2021]. The goal of this experiment is to evaluate the overhead caused by computing the maximally permissive strategy, we thus filtered the benchmarks by taking only the realizable ones that can be solved within the time limit, which are 391 in total.

Evaluation Results. We evaluated the overhead caused by maximally permissive strategy computation by comparing with the time cost of computing a single strategy, which is represented by the time taken from receiving a synthesis instance to finishing realizability checking, by then Boolean formula t, i.e., the nondeterministic non-deferring strategy, is also obtained. The Boolean synthesis time for "choosing" a deterministic strategy out of t is omitted, for a fair comparison, since the same procedure would also be required by "choosing" a deterministic strategy out of the maximally permissive strategy. Figure 1 displays a scatter plot (in log scale) comparing the time cost of two computations for each realizable instance. The gray line represents the points where the xaxis value is equal to the y-axis value. As shown in Figure 1, the points are closely above the gray line, this demonstrates that computing the maximally permissive strategy only brings minor overhead comparing to computing a single strategy.

6 Conclusions

Maximally permissive strategies are of interest when we want to allow for maximal freedom to the agent while still achieving the desired task. We have shown that we can naturally characterize maximally permissive strategies for LTLf specifications with two nondeterministic strategies and a constraint requiring to eventually switch from one to the other. Moreover, such a pair can be computed with minimal overhead. Given this nice computational result, it would be interesting to understand if maximally permissive strategies can be used to benefit LTLf synthesis itself. Indeed, state-of-the-art LTLf synthesis tools integrate techniques to compose specifications. Instead, one could compose the maximally permissive strategy of each specification piece, leading to an even smaller state space, and thus bring promising computational benefits. We leave this for future work.

Acknowledgments

This work is partially supported by the ERC Advanced Grant WhiteMech (No. 834228), the EU ICT-48 2020 project TAILOR (No. 952215), the PRIN project RIPER (No. 20203FFYLK), the JPMorgan AI Faculty Research Award "Resilience-based Generalized Planning and Strategic Reasoning"