Introduction

Program synthesis is one of the most ambitious and challenging problem of CS and AI. Reactive synthesis is a class of program synthesis problems which aims at synthesizing a program for interactive/reactive ongoing computations [1,2]. We have two sets of Boolean variables 𝒳 and 𝒴, controlled by the environment and the agent, respectively, and a specification 𝜙 over 𝒳 ∪ 𝒴 in terms of Linear Temporal Logic (ltl) [3]. The synthesis has to generate a program, aka a strategy, for the agent such that for every environment strategy the simultaneous execution of the two strategies generate a trace that satisfies 𝜙 [2,4,5].

Recently, the problem of reactive synthesis has been studied in the case the specification is expressed in ltl over finite traces (ltl 𝑓 ) and its variants [6]. This logic is particularly fitting for expressing temporally-extended goals in Planning since it retains the fact that ultimately the goal must be achieved and the plan terminated [7].

In the classical formulation of the problem of reactive synthesis the environment is free to choose an arbitrary move at each step, but in AI typically we have a model of world, i.e., of the environment behavior, e.g., encoded in a planning domain [8,9,10], or more generally directly in temporal logic [11,12,13,14]. In other words, we are interested in synthesis under environment specifications [15,16,17,18,19,20,21], which can be reduced to standard synthesis of the implication: 𝐸𝑛𝑣 → 𝐺𝑜𝑎𝑙 where 𝐸𝑛𝑣 is the specification of the environment (the environment specification) and 𝐺𝑜𝑎𝑙 is the specification of the task of the agent [13,16]. The agent has to realize its task 𝐺𝑜𝑎𝑙 only on those traces that satisfy the environment specification 𝐸𝑛𝑣. Specifically, we focus on synthesis under environment specifications for ltl 𝑓 goals. However, while it is natural to consider the task specification 𝐺𝑜𝑎𝑙 as an ltl 𝑓 formula, requiring that also 𝐸𝑛𝑣 is an ltl 𝑓 formula is often too strong, since accomplishing the agent task may require an unbounded number of environment moves and such number is decided by the agent that determines when its task is finished. As a result 𝐸𝑛𝑣 typically needs to be expressed over ltl not ltl 𝑓 [17,21]. So, even when focusing on ltl 𝑓 , what we need to study is the case where we have the task 𝐺𝑜𝑎𝑙 expressed in ltl 𝑓 and the environment specification 𝐸𝑛𝑣 expressed in ltl.

One way to handle this case is to translate 𝐺𝑜𝑎𝑙 into ltl [22] and then do ltl synthesis for 𝐸𝑛𝑣 → 𝐺𝑜𝑎𝑙, see e.g. [17]. But, while synthesis in ltl 𝑓 and in ltl have the same worst-case complexity, being both 2exptime-complete [2,6], the algorithms available for ltl synthesis are much harder in practice than those for ltl 𝑓 synthesis as experimentally shown [23,24,25].

For these reasons, several specific forms of ltl environment specifications have been considered. In this communication we reports recent results showing how to avoid the detour to LTL synthesis in cases where the environment specifications are in the form of fairness or stability [21], or gr(1) formulas [20], or specified in both ltl 𝑓 (e.g., for representing nodeterministic planning domains or other safety properties) and ltl (e.g., for liveness/fairness), but separating the contributions of the two by limiting the second one as much as possible [18].

ltl and ltl 𝑓

ltl is one of the most popular logics for temporal properties [3]. Given a set of propositions 𝒫, the formulas of ltl are generated by the following grammar:

𝜙 ::= 𝑝 | (𝜙 1 ∧ 𝜙 2 ) | (¬𝜙) | ( ○ 𝜙) | (𝜙 1 𝒰 𝜙 2 )

where 𝑝 ∈ 𝒫. We use common abbreviations for eventually ♢𝜙 ≡ true 𝒰 𝜙 and always as □𝜙 ≡ ¬♢¬𝜙.

ltl formulas are interpreted over infinite traces 𝜋 ∈ (2 𝒫 ) 𝜔 . A trace 𝜋 = 𝜋 0 𝜋 1 . . . is a sequence of propositional interpretations (sets), where for every 𝑖 ≥ 0, 𝜋 𝑖 ∈ 2 𝒫 is the 𝑖-th interpretation of 𝜋. Intuitively, 𝜋 𝑖 is interpreted as the set of propositions that are 𝑡𝑟𝑢𝑒 at instant 𝑖. Given 𝜋, we define when an ltl formula 𝜙 holds at position 𝑖, written as 𝜋, 𝑖 |= 𝜙, inductively on the structure of 𝜙, as follows:

• 𝜋, 𝑖 |= 𝑝 iff 𝑝 ∈ 𝜋 𝑖 (for 𝑝 ∈ 𝒫); • 𝜋, 𝑖 |= 𝜙 1 ∧ 𝜙 2 iff 𝜋, 𝑖 |= 𝜙 1 and 𝜋, 𝑖 |= 𝜙 2 ; • 𝜋, 𝑖 |= ¬𝜙 iff 𝜋, 𝑖 ̸ |= 𝜙; • 𝜋, 𝑖 |= ○ 𝜙 iff 𝜋, 𝑖 + 1 |= 𝜙;

• 𝜋, 𝑖 |= 𝜙 1 𝒰 𝜙 2 iff there exists 𝑖 ≤ 𝑗 such that 𝜋, 𝑗 |= 𝜙 2 , and for all 𝑘, 𝑖 ≤ 𝑘 < 𝑗 we have that 𝜋, 𝑘 |= 𝜙 1 .

We say 𝜋 satisfies 𝜙, written as 𝜋 |= 𝜙, if 𝜋, 0 |= 𝜙. ltl 𝑓 is a variant of ltl interpreted over finite traces instead of infinite traces [22]. The syntax of ltl 𝑓 is the same as the syntax of ltl. We define 𝜋, 𝑖 |= 𝜙, stating that 𝜙 holds at position 𝑖, as for ltl, except that for the temporal operators we have:

• 𝜋, 𝑖 |= ○ 𝜙 iff 𝑖 < last(𝜋) and 𝜋, 𝑖 + 1 |= 𝜙;

• 𝜋, 𝑖 |= 𝜙 1 𝒰 𝜙 2 iff there exists 𝑗 such that 𝑖 ≤ 𝑗 ≤ last(𝜋) and 𝜋, 𝑗 |= 𝜙 2 , and for all 𝑘, 𝑖 ≤ 𝑘 < 𝑗 we have that 𝜋, 𝑘 |= 𝜙 1 .

where last(𝜋) denotes the last position (i.e., index) in the finite trace 𝜋. In addition, we define the weak next operator • as abbreviation of • 𝜙 ≡ ¬ ○ ¬𝜙. Note that, over finite traces, it does not holds that ¬ ○ 𝜙 ̸ ≡ ○ ¬𝜙, but instead ¬ ○ 𝜙 ≡ • ¬𝜙. We say that a trace satisfies an ltl 𝑓 formula 𝜙, written as 𝜋 |= 𝜙, if 𝜋, 0 |= 𝜙.

ltl 𝑓 Synthesis Under Environment Specifications

Let 𝒳 and 𝒴 Boolean variables, controlled by the environment and the agent, respectively. An agent strategy is a function 𝜎 𝑎𝑔 : (2 𝒳 ) * → 2 𝒴 , and an environment strategy is a function

𝜎 𝑒𝑛𝑣 : (2 𝒴 ) + → 2 𝒳 . A trace is a sequence (𝑋 0 ∪ 𝑌 0 )(𝑋 1 ∪ 𝑌 1 ) • • • ∈ (2 𝒳 ∪𝒴 ) 𝜔 . A trace (𝑋 𝑖 ∪ 𝑌 𝑖 ) 𝑖 is consistent with an agent strategy 𝜎 𝑎𝑔 if 𝜎 𝑎𝑔 (𝜖) = 𝑌 0 and 𝜎 𝑎𝑔 (𝑋 0 𝑋 1 • • • 𝑋 𝑗 ) = 𝑌 𝑗+1 for every 𝑗 ≥ 0. A trace (𝑋 𝑖 ∪ 𝑌 𝑖 ) 𝑖 is consistent with and environment strategy if 𝜎 𝑒𝑛𝑣 (𝑌 0 𝑌 1 • • • 𝑌 𝑗 ) = 𝑋 𝑗 for every 𝑗 ≥ 0.

For an agent strategy 𝜎 𝑎𝑔 and an environment strategy 𝜎 𝑒𝑛𝑣 let play(𝜎 𝑎𝑔 , 𝜎 𝑒𝑛𝑣 ) denote the unique trace induced by both 𝜎 𝑎𝑔 and 𝜎 𝑒𝑛𝑣 , and play 𝑘 (𝜎 𝑎𝑔 , 𝜎 𝑒𝑛𝑣 ) = (𝑋 0 ∪ 𝑌 0 ), . . . , (𝑋 𝑘 ∪ 𝑌 𝑘 ) be the finite trace up to 𝑘.

Let 𝐺𝑜𝑎𝑙 be an ltl 𝑓 formula over 𝒳 ∪ 𝒴. An agent strategy 𝜎 𝑎𝑔 realizes 𝐺𝑜𝑎𝑙 if for every environment strategy 𝜎 𝑒𝑛𝑣 there exists 𝑘 ≥ 0, chosen by the agent, such that the finite trace play 𝑘 (𝜎 𝑎𝑔 , 𝜎 𝑒𝑛𝑣 ) |= 𝐺𝑜𝑎𝑙, i.e., 𝐺𝑜𝑎𝑙 is agent realizable.

In standard synthesis the environment is free to choose an arbitrary move at each step, but in AI typically the agent has some knowledge of how the environment works, which it can exploit in order to enforce the goal, specified as an ltl 𝑓 formula 𝐺𝑜𝑎𝑙. Here, we specify the environment behaviour by an ltl formula Env and call it environment specification. In particular, Env specifies the set of environment strategies that enforce Env [16]. Moreover, we require that Env must be environment realizable, i.e., the set of environment strategies that enforce Env is not empty. Formally, given an ltl formula 𝜙, we say that an environment strategy enforces 𝜙, written 𝜎 𝑒𝑛𝑣 ▷ 𝜙, if for every agent strategy 𝜎 𝑎𝑔 we have play(𝜎 𝑎𝑔 , 𝜎 𝑒𝑛𝑣 ) |= 𝜙.

The problem of ltl 𝑓 synthesis under environment specifications is to find an agent strategy 𝜎 𝑎𝑔 such that ∀𝜎 𝑒𝑛𝑣 ▷ Env : ∃𝑘.play 𝑘 (𝜎 𝑎𝑔 , 𝜎 𝑒𝑛𝑣 ) |= 𝐺𝑜𝑎𝑙.

As shown in [16], this can be reduced to solving the synthesis problem for the implication Env → 𝐿𝑇 𝐿(𝐺𝑜𝑎𝑙) where 𝐿𝑇 𝐿(𝐺𝑜𝑎𝑙) being a suitable ltl 𝑓 -to-ltl transformation [22], which is 2exptime-complete [2].

GR(1) Environment Specifications

There have been two success stories with ltl synthesis, both having to do with the form of the specification. The first is the GR(1) approach: use safety conditions to determine the possible transitions in a game between the environment and the agent, plus one powerful notion of fairness, Generalized Reactivity(1), or GR (1). The second, inspired by AI planning, is focusing on finite-trace temporal synthesis, with ltl 𝑓 as the specification language. In [20] we take these two lines of work and bring them together, devising an approach to solve ltl 𝑓 synthesis under gr(1) environment specification. In more details, to solve the problem we observe that the agent's goal is to satisfy ¬Env 𝐺𝑅(1) ∨ 𝐺𝑜𝑎𝑙, while the environment's goal is to satisfy Env 𝐺𝑅(1) ∧ ¬𝐺𝑜𝑎𝑙. Moreover, 𝐺𝑜𝑎𝑙 can be represented by a deterministic finite automata (dfa) [6]. Then, focusing on the environment point of view, we show that the problem can be reduced a gr (1) game in which the game arena is the complement of the dfa for 𝐺𝑜𝑎𝑙 and Env 𝐺𝑅(1) is the gr(1) winning condition. Since we want a winning strategy for the agent, we need to deal with the complement of the gr(1) game to obtain a winning strategy for the antagonist.

This framework can be enriched by adding safety conditions for both the environment and the agent, obtaining a highly expressive yet still scalable form of ltl synthesis. These two kinds of safety conditions differ, since the environment needs to maintain its safety indefinitely (as usual for safety), while the agent has to maintain its safety conditions only until s/he fulfills its ltl 𝑓 goal, i.e., within a finite horizon. Again, the problem can be reduced to a gr(1) game in which the game arena is the product of the dfa for the environment safety condition and the complement of the dfa obtained by the product of deterministic automaton of the agent safety condition and the one for the agent task. Tool. The two approaches were implemented in a so-called tool GFSynth which is based on two tools: Syft [25] for the the construction of the corresponding dfas and Slugs [26] to solve and compute a strategy in a gr(1) game.

Fairness and Stability Environment Specifications

We now consider two different basic forms of environment specifications: a basic form of fairness □♢𝛼 (always eventually 𝛼), and a basic form of stability ♢□𝛼 where in both cases the truth value of 𝛼 is under the control of the environment, and hence the environment specifications are trivially realizable by the environment. Note that due to the existence of ltl 𝑓 goals, synthesis under both kinds of environment specifications does not fall under known easy forms of synthesis, such as gr(1) formulas [27]. For these kinds of environment specifications, [18] develops a specific algorithm based on using the dfa for the ltl 𝑓 goal as the arena and then computing 2-nested fixpoint properties over such arena.

The algorithm proceeds as follows. First, translate the ltl 𝑓 𝐺𝑜𝑎𝑙 into a dfa 𝒢. Then, in case of fairness environment specifications, solve the fair dfa game 𝒢, i.e., a game over the dfa 𝒢, in which the environment (resp. the agent) winning condition is to remain in a region (resp., to avoid the region) where 𝛼 holds infinitely often, meanwhile the accepting states are forever avoidable, by applying a nested fixed-point computation on 𝒢.

Likewise, for stability environment specifications, solve the stable dfa game 𝒢, in which the environment (resp. the agent) winning condition is to reach a region (resp., to avoid the region) where 𝛼 holds forever, meanwhile the accepting states are forever avoidable, by applying a nested fixed-point computation on 𝒢. Tool. The fixpoint-based techniques for solving ltl 𝑓 synthesis under fainerss and stability environment specifications are implemented in two tools called FSyft and StSyft, both based on Syft, a tool for solving symbolic ltl 𝑓 synthesis.

General ltl Environment Specifications

We now consider the general case where the environment specifications are expressed in both ltl 𝑓 and ltl. For this case, in [18] we develop two-stage technique to effectively handle general ltl environment specifications. This technique takes advantage of the simpler way to handle ltl 𝑓 goals in the first stage and confines the difficulty of handling ltl environment specification to the bare minimum in stage 2. In particular, given an ltl environment specification and an ltl 𝑓 formula 𝐺𝑜𝑎𝑙 that specifies the agent goal, the problem is to find a strategy for the agent 𝜎 𝑎𝑔 that realizes 𝐺𝑜𝑎𝑙 under ltl environment specification Env 𝐿𝑇 𝐿 . The algorithm proceeds by taking the following stages.

• Stage 1: Build the corresponding deterministic finite automaton 𝒜 𝐺𝑜𝑎𝑙 of 𝐺𝑜𝑎𝑙 and solve the reachability game for the agent over 𝒜 𝐺𝑜𝑎𝑙 . If the agent has a winning strategy in 𝒜 𝐺𝑜𝑎𝑙 , then return it.

• Stage 2: If not, computes the following steps:

1. remove from 𝒜 𝐺𝑜𝑎𝑙 the agent winning region, obtaining 𝒜 ′ 𝐺𝑜𝑎𝑙 ; 2. do the product of 𝒜 ′ 𝐺𝑜𝑎𝑙 with the corresponding deterministic parity automaton (dpa) of 𝐸𝑛𝑣 𝐿𝑇 𝐿 𝒟, obtaining ℬ = 𝒜 ′ × 𝒟, and solve the parity game for the environment over it [28,29,30]; 3. if the agent has a winning strategy in ℬ then the synthesis problem is realizable and hence return the agent winning strategy as a combination of the agent winning strategies in the two stages.

An interesting observation in [18] is that when the part of the environment specifications are expressed in ltl 𝑓 , i.e., the environment specifications have the form 𝐸𝑛𝑣 = 𝐸𝑛𝑣 ∞ ∧ 𝐸𝑛𝑣 𝑓 , where 𝐸𝑛𝑣 ∞ can be expressed as ltl formula and 𝐸𝑛𝑣 𝑓 as an ltl 𝑓 formula. In this case the synthesis problem 𝐸𝑛𝑣 → 𝐺𝑜𝑎𝑙 becomes (𝐸𝑛𝑣 ∞ ∧ 𝐸𝑛𝑣 𝑓 ) → 𝐺𝑜𝑎𝑙 which is equivalent to 𝐸𝑛𝑣 ∞ → (𝐸𝑛𝑣 𝑓 → 𝐺𝑜𝑎𝑙) where (𝐸𝑛𝑣 𝑓 → 𝐺𝑜𝑎𝑙) is expressible in ltl 𝑓 . In this way 𝐸𝑛𝑣 𝑓 does not contribute the resulting dpa and can be handled during stage 1 instead of 2 of our technique. Specifically, it builds a dfa as the union of the dfa 𝒜 𝐸𝑛𝑣 𝑓 , i.e., the complement of the dfa for 𝐸𝑛𝑣 𝑓 , and the dfa 𝒜 Goal for the goal. Tool. The two-stage technique was implemented in the tool 2SLS which is based on two tools: Syft [25] for building the corresponding dfas and OWL [31] a tool for translating LTL into different types of automata, and thus dpas.