# ltlƒ_synthesis_with_fairness_and_stability_assumptions__0c0f979a.pdf

The Thirty-Fourth AAAI Conference on Artiﬁcial Intelligence (AAAI-20)

LTLf Synthesis with Fairness and Stability Assumptions

Shufang Zhu,1 Giuseppe De Giacomo,2 Geguang Pu,1 Moshe Y. Vardi3

1Each China Normal University, 2Sapienza Universit a di Roma, 3Rice University shufangzhu.szhu@gmail.com, degiacomo@diag.uniroma1.it, ggpu@sei.ecnu.edu.cn, vardi@cs.rice.edu

In synthesis, assumptions are constraints on the environment that rule out certain environment behaviors. A key observation here is that even if we consider systems with LTLf goals on ﬁnite traces, environment assumptions need to be expressed over inﬁnite traces, since accomplishing the agent goals may require an unbounded number of environment action. To solve synthesis with respect to ﬁnite-trace LTLf goals under inﬁnite-trace assumptions, we could reduce the problem to LTL synthesis. Unfortunately, while synthesis in LTLf and in LTL have the same worst-case complexity (both 2EXPTIME-complete), the algorithms available for LTL synthesis are much more difﬁcult in practice than those for LTLf synthesis. In this work we show that in interesting cases we can avoid such a detour to LTL synthesis and keep the simplicity of LTLf synthesis. Speciﬁcally, we develop a BDD-based ﬁxpoint-based technique for handling basic forms of fairness and of stability assumptions. We show, empirically, that this technique performs much better than standard LTL synthesis.

Introduction

In many situations we are interested in expressing properties over an unbounded but ﬁnite sequence of successive states. Linear-time Temporal Logic over ﬁnite traces (LTLf) and its variants have been thoroughly investigated for doing so. There has been broad research for logical reasoning (De Giacomo and Vardi 2013; Li et al. 2019), synthesis (De Giacomo and Vardi 2015; Camacho et al. 2018), and planning (Camacho et al. 2017; De Giacomo and Rubin 2018). Recently synthesis under assumptions in LTLf has attracted speciﬁc interest (De Giacomo and Rubin 2018; Camacho, Bienvenu, and Mc Ilraith 2018). First, planning for LTLf goals can be considered as a form of LTLf synthesis under assumptions, where the assumptions are the dynamics of the environment encoded in the planning domain (Green 1969; Camacho, Bienvenu, and Mc Ilraith 2018; Aminof et al. 2018; 2019). However, more generally, assumptions can be arbitrary constraints on the environment that can be exploited by the agent in devising a strategy to fulﬁll its goal.

Copyright c 2020, Association for the Advancement of Artiﬁcial Intelligence (www.aaai.org). All rights reserved.

Synthesis under assumptions has been extensively studied in LTL, where environment assumptions are expressed as LTL formulas (Chatterjee and Henzinger 2007; Chatterjee, Henzinger, and Jobstmann 2008; D Ippolito et al. 2013; Bloem, Ehlers, and K onighofer 2015; Brenguier, Raskin, and Sankur 2017). In fact, LTL formulas can be used as assumptions as long as it is guaranteed that the environment is able to behave so as to keep the assumptions true, i.e., assumptions are environment realizable. Under these circumstances, it is possible to reduce synthesis for LTL goal ψG under assumptions ψA to standard synthesis for ψA ψG. Note that because of the guarantee of ψA being environment realizable, no agent strategy can win ψA ψG by falsifying ψA. See (Aminof et al. 2019) for a discussion.

When we turn to LTLf, a key observation is that even if we consider (ﬁnite-trace) LTLf goals for the agent, assumptions need to be expressed considering inﬁnite traces, since accomplishing the agent goals may require an unbounded number of environment action. So we have an assumption ψA expressed in LTL and a goal φG expressed in LTLf. To solve synthesis under assumptions in LTLf, we could translate φG into LTL getting ψG, by applying the translation of LTLf into LTL in (De Giacomo and Vardi 2013), and then do LTL synthesis for ψA ψG, see e.g. (Camacho, Bienvenu, and Mc Ilraith 2018).

Unfortunately, while synthesis in LTLf and in LTL have the same worst-case complexity, being both 2EXPTIMEcomplete (Pnueli and Rosner 1989; De Giacomo and Vardi 2015), the algorithms available for LTL synthesis are much harder in practice than those for LTLf synthesis. In particular, the lack of efﬁcient algorithms for the crucial step of automata determinization is prohibitive for ﬁnding scalable implementations (Fogarty et al. 2013; Finkbeiner 2016). In spite of recent advancement in synthesis such as reducing to parity games (Meyer, Sickert, and Luttenberger 2018), bounded synthesis based on solving iterated safety games (Kupferman and Vardi 2005; Finkbeiner and Schewe 2013; Gerstacker, Klein, and Finkbeiner 2018), or recent techniques based on iterated FOND planning (Camacho et al. 2018), LTL synthesis remains very challenging. In contrast, LTLf synthesis is based on a translation to Deterministic Finite Automaton (DFA) (Rabin and Scott 1959), which

can be seen as a game arena where environment and agent make their own moves. On this arena, the agent wins if a simple ﬁxpoint condition (reachability of the DFA accepting states) is satisﬁed. Hence, when we introduce assumptions, an important question arises: can we retain the simplicity of LTLf synthesis? In particular, we are thinking about algorithms based on devising some sort of arena and then extracting winning strategies by relying on computing a small number of nested ﬁxpoints (note that the reduction of LTL synthesis to parity games may generate exponentially many nested ﬁxpoints (Gr adel, Thomas, and Wilke 2002)). We consider here two different basic, but quite signiﬁcant, forms of assumptions: a basic form of fairness GFα (always eventually α), and a basic form of stability FGα (eventually always α), where in both cases the truth value of α is under the control of the environment, and hence the assumptions are trivially realizable by the environment. Note that due to the existence of LTLf goals, synthesis under both kinds of assumptions does not fall under known easy forms of synthesis, such as GR(1) formulas (Bloem et al. 2012). For these kinds of assumptions, we devise a speciﬁc algorithm based on using the DFA for the LTLf goal as the arena and then computing 2-nested ﬁxpoint properties over such arena. It should be noted that the kind of nested ﬁxpoint that we compute for fairness GFα is similar to the one in (De Giacomo and Rubin 2018), but it is clear that the fairness stated there is different from what we claim in this paper. The fairness in (De Giacomo and Rubin 2018) is interpreted as all effects happening fairly, therefore the assumption is hardcoded in the arena itself. Here, instead, we only require that a selected condition α happens fairly, and our technique extends to deal with stability assumptions as well. We compare the new algorithm with standard LTL synthesis (Meyer, Sickert, and Luttenberger 2018) and show empirically that this algorithm performs signiﬁcantly better, in the sense that solving more cases with less time cost. Some proofs have been removed due to the lack of space.1

Preliminaries Linear-time Temporal Logic over ﬁnite traces (LTLf) has the same syntax as LTL over inﬁnite traces introduced in (Pnueli 1977). Given a set of propositions P, the syntax of LTLf formulas is deﬁned as φ ::= a | φ | φ1 φ2 | Xφ | φ1Uφ2. Every a P is an atom. A literal l is an atom or the negation of an atom. X for Next , and U for Until , are temporal operators. We make use of the standard Boolean abbreviations, such as (or) and (implies), true and false. Additionally, we deﬁne the following abbreviations Weak Next Xwφ X φ, Eventually Fφ true Uφ and Always Gφ false Rφ, where R is for Release . A trace ρ = ρ[0], ρ[1], . . . is a sequence of propositional interpretations (sets), where ρ[m] 2P (m 0) is the m-th interpretation of ρ, and |ρ| represents the length of ρ. Intuitively, ρ[m] is interpreted as the set of propositions which are true at instant m. Trace ρ is an inﬁnite trace if |ρ| = ,

1A full version is available on ar Xiv. Geguang Pu is the corresponding author.

which is formally denoted as ρ (2P)ω; otherwise ρ is a ﬁnite trace, denoted as ρ (2P) . LTLf formulas are interpreted over ﬁnite, nonempty traces. Given a ﬁnite trace ρ and an LTLf formula φ, we inductively deﬁne when φ is true on ρ at step i (0 i < |ρ|), written ρ, i |= φ, as follows: ρ, i |= a iff a ρ[i]; ρ, i |= φ iff ρ, i |= φ; ρ, i |= φ1 φ2 iff ρ, i |= φ1 and ρ, i |= φ2; ρ, i |= Xφ iff i + 1 < |ρ| and ρ, i + 1 |= φ; ρ, i |= φ1Uφ2 iff there exists j such that i j < |ρ| and ρ, j |= φ2, and for all k, i k < j, we have ρ, k |= φ1. An LTLf formula φ is true on ρ, denoted by ρ |= φ, if and only if ρ, 0 |= φ. LTLf synthesis can be viewed as a game of two players, the environment and the agent, contrasting each other. The aim is to synthesize a strategy for the agent such that no matter how the environment behaves, the combined behavior trace of both players satisfy the logical speciﬁcation expressed in LTLf (De Giacomo and Vardi 2015).

Fair and Stable LTLf Synthesis

In this paper, we focus on LTLf synthesis under assumptions in two different basic forms: fairness and stability, which we call in the following fair LTLf synthesis and stable LTLf synthesis, respectively. In such synthesis problems, both players (environment and agent) have Boolean variables under their respective control. Here, we use X to denote the set of environment variables that are uncontrollable for the agent, and Y the set of agent variables that are controllable for the agent. Therefore, X and Y are disjoint. In general, assumptions are speciﬁc forms of constraints.

Deﬁnition 1 (Environment Constraint). An environment constraint α is a Boolean formula over X.

In particular, we deﬁne here two different basic, but common forms of assumptions.

Deﬁnition 2 (Fairness and Stability Assumptions). An LTL formula ψ is considered as a fairness assumption if it is of the form GFα, and a stability assumption if of the form FGα, where in both cases α is an environment constraint.

A fair or stable trace can then be deﬁned in terms of the corresponding assumption (fairness or stability).

Deﬁnition 3 (Fair and Stable Traces). A trace ρ (2X Y)ω is α-fair if ρ |= GFα and it is α-stable if ρ |= FGα.

Intuitively, α holds inﬁnitely often on an α-fair trace, while eventually holds forever on an α-stable trace. Note that, if trace ρ is not α-fair, i.e., ρ GFα, then ρ |= FG( α) such that ρ is α-stable. Similarly, if trace ρ is not α-stable, i.e., ρ FGα, then ρ |= GF( α) such that ρ is α-fair. Although there is a duality between fairness and stability, such duality breaks when applying these environment assumptions to the problem of LTLf synthesis. This is because in addition to the assumptions, the synthesis problems also require the LTLf speciﬁcation to be satisﬁed. We now deﬁne fair and stable LTLf synthesis by making use of fair and stable traces.

Deﬁnition 4 (Fair (Stable) LTLf Synthesis). LTLf formula φ, deﬁned over X Y, is α-fair (resp., α-stable) realizable if there exists a strategy g : (2X )+ 2Y, such that for an arbitrary environment trace λ = X0, X1, . . . (2X )ω, if λ is α-fair (resp., α-stable), then we can ﬁnd k 0 such that φ is true in the ﬁnite trace ρk = (X0 g(X0)), (X1 g(X0, X1)), . . . , (Xk g(X0, X1, . . . , Xk)). A fair (resp., stable) LTLf synthesis problem, described as a tuple X, Y, α, φ , consist in checking whether φ, deﬁned over X Y, is α-fair (resp., α-stable) realizable. The synthesis procedure aims to computing a strategy if realizable. Intuitively speaking, φ describes the desired goal when the environment behaviors satisfy the assumption. An agent strategy g : (2X )+ 2Y for fair (resp., stable) synthesis problem X, Y, α, φ is winning if it guarantees the satisfaction of the objective φ under the condition that the environment behaves in a way that α holds inﬁnitely often (resp., α eventually holds forever). The realizability procedure of X, Y, α, φ aims to answer the existence of a winning strategy g and the synthesis procedure amounts for computing g if it exists. In fact one can consider two variants of the synthesis problem, depending on the player who moves ﬁrst, in the sense of assigning values to variables under its control ﬁrst. Here we consider the environment as the ﬁrst-player (as in planning), but a version where the agent moves ﬁrst can be obtained by a small modiﬁcation. Since every LTLf formula φ can be translated to a Deterministic Finite Automaton (DFA) Gφ that accepts exactly the same language as φ (De Giacomo and Vardi 2013), we are able to reduce the problems of fair LTLf synthesis and stable LTLf synthesis to speciﬁc two-player DFA games, in particular, fair DFA game and stable DFA game, respectively. We start with introducing DFA games.

Games over DFA Two-player games on DFA are games consisting of two players, the environment and the agent. X and Y are disjoint sets of environment Boolean variables and agent Boolean variables, respectively. The speciﬁcation of the game arena is given by a DFA G = (2X Y, S, s0, δ, Acc), where 2X Y is the alphabet, S is a set of states, s0 S is an initial state, δ : S 2X Y S is a transition function and Acc S is a set of accepting states. A round of the game consists of both players setting the values of variables under their respective control. A play ρ over G records how two players set the values at each round and how the DFA proceed according to the values. Formally, a play ρ from state si0 is an inﬁnite trace (si0, X0 Y0), (si1, X1 Y1) . . . (S 2X Y)ω such that sij+1 = δ(sij, Xj Yj). Moreover, we also assign the environment as the ﬁrst-player, which sets values ﬁrst. A play ρ is considered as a winning play if it follows a certain winning condition. Different winning conditions lead to different games. In this paper, we consider two speciﬁc two-player games, fair DFA game and stable DFA game, both of which are described as G, α , where G is the game arena and α is the environment constraint. Fair DFA Game. Although the ultimate goal for solving a fair DFA game is to perform winning plays for the agent,

since it is more straightforward to formulate the game considering the environment as the protagonist, we ﬁrst deﬁne the winning condition of the environment over a play. A play ρ = (si0, X0 Y0), (si1, X1 Y1) . . . over G is winning for the environment with respect to a fair DFA game G, α if the following two conditions hold: Recurrence: ρ is α-fair (that is, ρ |= GFα), Safety: sij Acc for all j 0 (Acc is avoided). Consequently, a play ρ is winning for the agent if one of the following conditions holds: Stability: ρ is not α-fair (that is, ρ |= FG( α)), Reachability: sij Acc for some j 0 (Acc is reached). Stable DFA Game. As for a stable DFA game G, α , a play ρ = (si0, X0 Y0), (si1, X1 Y1) . . . over G is winning for the environment if the following two conditions hold: Stability: ρ is α-stable (that is, ρ |= FGα), Safety: sij Acc for all j 0 (Acc is avoided). Consequently, a play ρ is winning for the agent if one of the following conditions holds: Recurrence: ρ is not α-stable (that is, ρ |= GF( α)), Reachability: sij Acc for some j 0 (Acc is reached). Since we consider here the environment as the ﬁrst-player, a strategy for the agent is a function g : (2X )+ 2Y, deciding the values of the controllable variables for every possible history of the uncontrollable variables. Respectively, an environment strategy is a function h : (2Y) 2X . A play ρ = (si0, X0 Y0), (si1, X1 Y1) . . . (S 2X Y)ω follows a strategy g (resp., a strategy h), if Yj = g(X0, . . . , Xj) for all j 0 (resp., Xj = h(Y0, . . . , Yj 1) for all j > 0). We can now deﬁne winning states and winning strategies.

Deﬁnition 5 (Winning State and Winning Strategy). In the game G, α described above, s S is a winning state for the agent (resp., environment) if there exists strategy g (resp., h) s.t. every play ρ from s that follows g (resp., h) is an agent (resp., environment) winning play. Then g (resp., h) is a winning strategy for the agent (resp., environment) from s.

As shown in (Martin 1975), both of the fair DFA game and stable DFA game described above are determined, that is, a state s S is a winning state for the agent if and only if s is not a winning state for the environment. The realizability procedure of the game consists of checking whether there exists a winning strategy for the agent from initial state s0. The synthesis procedure aims to computing such a strategy. We then show how to reduce the problems of fair LTLf synthesis and stable LTLf synthesis to fair DFA game and stable DFA game, respectively. Hence we can solve the DFA game, thus settling the corresponding synthesis problem.

Solution to Fair LTLf Synthesis In order to perform fair synthesis on LTLf, given problem X, Y, α, φ , we ﬁrst translate the LTLf speciﬁcation φ into a DFA Gφ. We then view Gφ, α as a fair DFA game, and consider exactly the separation between environment and agent variables as in the original synthesis problem. Speciﬁcally, we assign X as the environment variables and Y as the agent variables. Finally, we solve the fair DFA game, thus settling the fair LTLf synthesis problem. The following theorem assesses the correctness of this technique.

Theorem 1. Fair LTLf synthesis problem X, Y, α, φ is realizable iff fair DFA game Gφ, α is realizable.

Proof. We prove the theorem in both directions. : Since Gφ, α is realizable for the agent, the initial state s0 is an agent winning state with winning strategy g : (2X )+ 2Y. Therefore, a play ρ = (s0, X0 g(X0)), (s1, X1 g(X0, X1)), . . . over Gφ from s0 following g is a winning play for the agent. Moreover, for every such play ρ from s0, either of the following conditions holds: ρ GFα such that ρ is not α-fair. ρ |= GFα such that ρ is α-fair. Since ρ is winning for the agent, there exists j 0 such that sj Acc. This implies that ρj |= φ holds, where ρj = (s0, X0 g(X0)), (s1, X1 g(X0, X1)), . . . , (sj, Xj g(X0, X1, . . . , Xj)). Consequently, the strategy g assures that for an arbitrary environment trace λ = X0, X1, . . . (2X )ω, if λ is α-fair, then there is j 0 such that φ is true in the ﬁnite trace ρj. We conclude that X, Y, α, φ is realizable. : For this direction, we assume that X, Y, α, φ is realizable, then there exists a strategy g : (2X )+ 2Y that realizes φ. Thus consider an arbitrary environment trace λ (2X )ω, either of the following conditions holds: λ is not α-fair, then the induced play ρ = (s0, X0 g(X0)), (s1, X1 g(X0, X1)), . . . over Gφ from s0 that follows g is winning for the agent by default. λ is α-fair, then on the induced play ρ = (s0, X0 g(X0)), (s1, X1 g(X0, X1)), . . . over Gφ from s0, there exists j 0 such that φ is true in the ﬁnite trace ρj = (s0, X0 g(X0)), (s1, X1 g(X0, X1)), . . . , (sj, Xj g(X0, X1, . . . , Xj)), in which case sj Acc. Therefore, ρ is winning for the agent. Consequently, we conclude that fair DFA game Gφ, α is realizable for the agent.

Fair DFA Game Solving Winning fair DFA games means that the agent can eventually reach an agent wins region from which if the constraint α holds, then it is possible to reach an accepting state. Given a fair DFA game G, α , we proceed as follows: (1) Compute agent wins region in fair DFA game G, α ; (2) Check realizability; (3) Return an agent winning strategy if realizable. Since the environment winning condition is more intuitive, in order to show the solution to fair DFA game, we start by solving the Recurrence-Safety game, which considers the environment as the protagonist. The idea for winning such game is that the environment should remain in an environment wins region from which the constraint α holds inﬁnitely often referring to Recurrence game, meanwhile the accepting states are forever avoidable referring to Safety game. Therefore, in order to have both of Recurrence such that having GFα holds and Safety such that avoiding accepting states s Acc, the environment wins region computation is deﬁned as: Envf = νZ.μ ˆZ.( X. Y.((X |= α δ(s, X Y ) Z\Acc) δ(s, X Y ) ˆZ\Acc)), where X ranges over 2X and Y over 2Y. The ﬁxpoint stages for Z (note Zi+1 Zi, for i 0, by monotonicity) are:

Z0 = S, Zi+1 = μ ˆZ.( X. Y.((X |= α δ(s, X Y ) Zi\Acc) δ(s, X Y ) ˆZ\Acc)). Eventually, Envf = Zk for some k such that Zk+1 = Zk. The ﬁxpoint stages for ˆZ with respect to Zi (note ˆZj ˆZj+1, for j 0, by monotonicity) are: ˆZi,0 = , ˆZi,j+1 = X. Y.((X |= α δ(s, X Y ) Zi\Acc) δ(s, X Y ) ˆZi,j\Acc). Finally, ˆZi = ˆZi,k for some k such that ˆZi,k+1 = ˆZi,k. The following theorem assures that the nested ﬁxpoint computation of Envf collects exactly all environment winning states in fair DFA game.

Theorem 2. For a fair DFA game G, α and a state s S, we have s Envf iff s is an environment winning state.

Proof. We prove the two directions separately. : We prove by showing the contrapositive. If a state s / Envf, then s must be removed from Envf at stage i + 1, therefore, s Zi\Zi+1. Then s / μ ˆZ.( X. Y.((X |= α δ(s, X Y ) Z\Acc) δ(s, X Y ) ˆZ\Acc)). That is, no matter what the (environment) strategy h is, traces from s satisfy neither of the following conditions: α holds and the trace gets trapped in Z without visiting accepting states such that X |= α δ(s, X Y ) Z\Acc holds, in which case s is a new environment winning state; α eventually gets hold and from there we can have α as true inﬁnitely often without visiting accepting states such that δ(s, X Y ) ˆZ\Acc holds, in which case s is a new environment winning state. Therefore, s is not an environment winning state. So if s is an environment winning state then s Envf holds. : If a state s Envf, then s μ ˆZ.( X. Y.((X |= α δ(s, X Y ) Z\Acc) δ(s, X Y ) ˆZ\Acc)). That is, no matter what the (agent) strategy g is, traces from s satisfy either of the following conditions: α holds and the trace gets trapped in Z without visiting accepting states such that X |= α δ(s, X Y ) Z\Acc holds, in which case s is a new environment winning state; α eventually gets hold and from there we can have α as true inﬁnitely often without visiting accepting states such that δ(s, X Y ) ˆZ\Acc holds, in which case s is a new environment winning state. Thus s is a winning state for the environment.

Due to the determinacy of fair DFA game, the set of agent winning states Sysf can be computed by negating Envf: Sysf = μZ.ν ˆZ.( X. Y.((X |= α δ(s, X Y ) Z Acc) δ(s, X Y ) ˆZ Acc)).

Theorem 3. A fair DFA game G, α has an agent winning strategy if and only if s0 Sysf.

Strategy Extraction Having completed the realizability checking procedure, this section deals with the agent winning strategy generation if G, α is realizable. It is known that if some strategy that

realizes φ exists, then there also exists a ﬁnite-state strategy generated by a ﬁnite-state transducer that realizes φ (Buchi and Landweber 1990). Formally, the agent winning strategy g : (2X )+ 2Y can be represented as a deterministic ﬁnite transducer based on the set Sysf, described as below. Deﬁnition 6 (Deterministic Finite Transducer). Given a fair DFA game G, α , where G = (2X Y, S, s0, δ, Acc), a deterministic ﬁnite transducer T = (2X , 2Y, Q, s0, ϱ, ωf) of such game is deﬁned as follows: Q S is the set of agent winning states s.t. Q = Sysf; ϱ : Q 2X Q is the transition function such that ϱ(q, X) = δ(q, X Y ) and Y = ωf(q, X); ωf : Q 2X 2Y is the output function such that at an agent winning state q with assignment X, ωf(q, X) returns an assignment Y leading to an agent winning play. The transducer T generates g in the sense that for every λ (2X )ω, we have g(λ) = ωf(ϱ(λ)), with the usual extension of δ to words over 2X from s0. Note that there are many possible choices for the output function ωf. The transducer T deﬁnes a winning strategy by restricting ωf to return only one possible setting of Y. We extract the output function ωf : Q 2X 2Y for the game from the approximates for Z assuming ˆZ to be Sysf, from where no matter what the environment strategy is, traces have to always get α hold. Thus, we consider: μZ.( X. Y.((X |= α δ(s, X Y ) Z Acc) δ(s, X Y ) Sysf Acc)) with approximates deﬁned as: Z0 = , Zi+1 = X. Y.((X |= α δ(s, X Y ) Zi Acc) δ(s, X Y ) Sysf Acc). Deﬁne an output function ωf : Sysf 2X 2Y as follows: for s Zi+1\Zi, for all possible values X 2X , set Y to be such that (X |= α δ(s, X Y ) Zi Acc) δ(s, X Y ) Sysf Acc holds for s / Acc. Consider a deterministic ﬁnite transducer T deﬁned in the sense that constructing ωf as described above, the following theorem guarantees that T generates an agent winning strategy g. Theorem 4. Strategy g with g(λ) = ωf(ϱ(λ)) is a winning strategy for the agent.

Solution to Stable LTLf Synthesis Solving stable LTLf synthesis problem X, Y, α, φ relies on solving the stable DFA game Gφ, α , where Gφ is the corresponding DFA of φ. The following theorem guarantees the correctness of such reduction. Theorem 5. Stable LTLf synthesis problem X, Y, α, φ is realizable iff stable DFA game Gφ, α is realizable.

Proof. We prove the theorem in both directions. : Since Gφ, α is realizable for the agent, the initial state s0 is an agent winning state with winning strategy g : (2X )+ 2Y. Therefore, a play ρ = (s0, X0 g(X0)), (s1, X1 g(X0, X1)), . . . over Gφ from s0 following g is a winning play for the agent. Moreover, for every such play ρ from s, either of the following conditions holds: ρ FGα such that ρ is not α-stable. ρ |= FGα such that ρ is α-stable. Since ρ is winning for

the agent, there exists j 0 such that sj Acc. Therefore, ρj |= φ holds, where ρj = (s0, X0 g(X0)), (s1, X1 g(X0, X1)), . . . , (sj, Xj g(X0, X1, . . . , Xj)). Consequently, the strategy g assures that for an arbitrary environment trace λ = X0, X1, . . . (2X )ω, if λ is αstable, then there exists j 0 such that φ is true in ﬁnite trace ρj. Thus X, Y, α, φ is realizable. : For this direction, we assume that X, Y, α, φ is realizable, then there exists a strategy g : (2X )+ 2Y that realizes φ. Thus consider an arbitrary environment trace λ (2X )ω, either of the following conditions holds: λ is not α-stable, then the induced play ρ = (s0, X0 g(X0)), (s1, X1 g(X0, X1)), . . . over Gφ from s0 that follows g is winning for the agent by default. λ is α-stable, then on the induced play ρ = (s0, X0 g(X0)), (s1, X1 g(X0, X1)), . . . over Gφ from s0, there exists j 0 such that φ is true in the ﬁnite trace ρj = (s0, X0 g(X0)), (s1, X1 g(X0, X1)), . . . , (sj, Xj g(X0, X1, . . . , Xj)), in which case sj Acc. Therefore, ρ is winning for the agent. Consequently, we conclude that stable DFA game Gφ, α is realizable for the agent.

Stable DFA Game Solving Despite the duality between fairness and stability, solving the stable DFA game here cannot directly dualize the solution to fair DFA game. This is because the computation here involves a Stability-Safety game, which is not dual to the Recurrence-Safety game in fair DFA game solving. In order to deal with stable DFA game, we again ﬁrst consider the environment as the protagonist. We compute the set of environment winning states as follows: Envst = μZ.ν ˆZ.( X. Y.((X |= α δ(s, X Y ) ˆZ\Acc) δ(s, X Y ) Z\Acc)), where X ranges over 2X and Y over 2Y. The following theorem assures that the nested ﬁxpoint computation of Envst collects exactly all environment winning states in stable DFA game.

Theorem 6. For a stable DFA game G, α and a state s S, we have s Envst iff s is an environment winning state.

Correspondingly, since stable DFA game is determined, the set of agent winning states can be computed as follows: Sysst = νZ.μ ˆZ.( X. Y.((X |= α δ(s, X Y ) ˆZ Acc) δ(s, X Y ) Z Acc)).

Theorem 7. A stable DFA game G, α has an agent winning strategy if and only if s0 Sysst.

Strategy Extraction Here, the agent winning strategy g : (2X )+ 2Y can also be represented as a deterministic ﬁnite transducer T = (2X , 2Y, Q, s0, ϱ, ωst) in terms of the set of agent winning states such that Q = Sysst. We extract the output function ωst : Q 2X 2Y for the game from the approximates for Z assuming ˆZ to be Sysst, from where no matter what the environment strategy is, traces cannot always get α hold. Thus, we consider the ﬁxpoint computation as follows:

νZ.( X. Y.((X |= α δ(s, X Y ) Sysst Acc) δ(s, X Y ) Z Acc)). Deﬁne an output function ωst : Sysst 2X 2Y s.t. for s Zi+1 Zi, for all possible values X 2X , set Y to be s.t. (X |= α δ(s, X Y ) Sysst Acc) δ(s, X Y ) Zi Acc holds for s / Acc. The following theorem guarantees that T generates an agent winning strategy g.

Theorem 8. Strategy g with g(λ) = ωst(ϱ(λ)) is a winning strategy for the agent.

We observe that a straightforward approach to LTLf synthesis under assumptions can be obtained by a reduction to standard LTL synthesis, which allows us to utilize tools for LTL synthesis to solve the fair (or stable) LTLf synthesis problem. In this section, we ﬁrst revisit the reduction to standard LTL synthesis, and then show an experimental comparison with the approach proposed earlier in this paper. Reduction to LTL Synthesis. The insight of reducing LTLf synthesis under assumptions to LTL synthesis comes from the reduction in (Zhu et al. 2017b) for general LTLf synthesis, and in (Camacho, Bienvenu, and Mc Ilraith 2018) for constraint LTLf synthesis, where the constraint describes the desired environment behaviors, under which the goal is to satisfy the given LTLf speciﬁcation. Both reductions adopt the translation rules in (De Giacomo and Vardi 2013) to polynomially transform an LTLf formula φ over X Y into an LTL formula ψ over X Y {alive}, retaining the satisﬁability equivalence, where proposition alive indicates the last instance of the ﬁnite trace. Such translation bridges the gap between LTLf over ﬁnite traces and LTL over inﬁnite traces. Based on the translation from LTLf to LTL, we then reduce fair (resp., stable) LTLf synthesis problem X, Y, α, φ to LTL synthesis problem X, Y {alive}, GFα ψ (resp., X, Y {alive}, FGα ψ ). Implementation. Based on the LTLf synthesis tool Syft 2, we implemented our ﬁxpoint-based techniques for solving fair LTLf synthesis and stable LTLf synthesis in two tools called FSyft and St Syft, respectively (name after Syft). Both frameworks consist of two steps: the symbolic DFA construction and the respective DFA game solving. In the ﬁrst step, we based on the code of Syft, to construct the symbolic DFA represented in Binary Decision Diagrams (BDDs). The implementation of the nested ﬁxpoint computation for solving DFA games over such symbolic DFA, borrows techniques from (Zhu et al. 2017a) for greatest ﬁxpoint computation and from Syft for least ﬁxpoint computation. The construction of the transducer for generating the winning strategy utilizes the boolean-synthesis procedure introduced in (Fried, Tabajara, and Vardi 2016) for realizable formulas. The implementation makes use of the BDD library CUDD3.0.0 (Somenzi 2016). In order to evaluate the performance of FSyft and St Syft, we compared it against the solution of reducing to standard LTL synthesis shown above. For such comparison, we employed the LTLf-to-LTL translator implemented in SPOT (Duret-Lutz et al. 2016) and chose

2https://github.com/safﬁepig/Syft

Strix (Meyer, Sickert, and Luttenberger 2018), the winner of the synthesis competition SYNTCOMP 2019 3 over LTL synthesis track, as the baseline.

Experimental Methodology

Benchmarks. We collected 1200 formulas consisting of two classes of benchmarks: 1000 randomly conjuncted LTLf formulas over 100 basic cases, generated in the style described in (Zhu et al. 2017b), the length of which, indicating the number of conjuncts, ranges form 1 to 5. The assumption (either fairness or stability) is assigned by randomly selecting one variable from all environment variables; 200 LTLf synthesis benchmarks with assumptions generated from a scalable counter game, described as follows: There is an n-bit binary counter. At each round, the environment chooses whether to increment the counter or not. The agent can choose to grant the request or ignore it. The goal is to get the counter having all bits set to 1, so the counter reaches the maximal value. The fairness assumption is to have the environment inﬁnitely request the counter to be incremented. The stability assumption is to have the environment eventually keep requesting the counter to be incremented. We reduce solving the counter game above to solving LTLf synthesis with assumptions. First, we have n agent variables {bn 1, bn 2, . . . , b0} denoting the value of n counter bits. We also introduce another n + 1 agent variables {cn, cn 1, . . . , c0} representing the carry bits. In addition, we have an environment variable add representing the environment making an increment request or not, and c0 as true is considered as the agent granting the request. We then formulate the counter game into LTLf formula as follows: Init = (( c0) . . . ( cn 1) ( b0) . . . ( bn 1))), Goal = F(b0 . . . bn 1), B = G(( add) Xw( c0)),

((( ci) ( bi)) Xw(( bi) ( ci+1))) ((( ci) bi) Xw(bi ( ci+1))) (((ci bi) Xw(bi ( ci+1))) (((ci bi) Xw(( bi) ci+1))).

The LTLf formula φ is then (Init B

0 i n G(Bi)) Goal, and the constraint α is add. Obviously, such counter game only returns realizable cases, since a winning strategy for the agent is to grant all increment requests. In order to get unrealizable cases, we can make some modiﬁcations on the counter game above. One possibility is to have the counter increment by 2 if the agent chooses to grant the request sent by the environment. Such modiﬁcation leads to no winning strategy for the agent, since the maximal counter value of having each bit as 1 is odd. However, incrementing by 2 at each time will never reach an odd value. Therefore, for bit Bi such that i > 0, we keep the same formulation. While for bit B0, we change as follows:

3http://www.syntcomp.org/syntcomp-2019-results/

0.01 0.1 1.0 10.0 100.0 1000.0

Number of solved cases

FSyft Strix

Figure 1: Fair LTLf synthesis. Comparison of the number of solved cases with limited time between FSyft and Strix over random conjunction benchmarks.

0.01 0.1 1.0 10.0 100.0 1000.0

Number of solved cases

St Syft Strix

Figure 2: Stable LTLf synthesis. Comparison of the number of solved cases with limited time between St Syft and Strix over random conjunction benchmarks.

((( c0) ( b0)) Xw(( b0) ( c1))) ((( c0) b0) Xw(b0 ( c1))) (((c0 b0) Xw( b0 (c1))) (((c0 b0) Xw((b0) c1))). Therefore, we have 200 counter game benchmarks in total, with the number of counter bits n ranging from 1 to 100, and both realizable and unrealizable cases for each n. Experiment Setup. All tests were ran on a computer cluster. Each test took an exclusive access to a node with Intel(R) Xeon(R) CPU E5-2650 v2 processors running at 2.60GHz. Time out was set to 1000 seconds. Correctness. Our implementation was veriﬁed by comparing the results returned by FSyft and St Syft with those from Strix. No inconsistency encountered for the solved cases.

Experimental Results. We evaluated the efﬁciency of FSyft and St Syft in terms of the number of solved cases and total time cost. We compared these two tools against Strix by performing an endto-end comparison experiment. Therefore, both of the DFA construction time and the ﬁxpoint computation time were counted for FSyft and St Syft. For Strix, we counted the running time from feeding the corresponding LTL formula to Strix to receiving the result. Both comparison on two classes of benchmarks show the advantage of the ﬁxpoint-based

FSyft Strix

Figure 3: Fair LTLf synthesis. Comparison of running time between FSyft and Strix, in log scale. Bars of the maximum height indicate cases timed out.

technique proposed in this paper as an effective method for both of fair LTLf synthesis and stable LTLf synthesis 4. Randomly Conjuncted Benchmarks. Figure 1 and Figure 2 show the number of solved cases as the given time increases on fair LTLf synthesis and stable LTLf synthesis, respectively. As shown in the ﬁgures, both of FSyft and St Syft are able to handle almost all cases (1000 in total for each), while Strix only solves a small fraction of the cases that FSyft and St Syft can solve. Moreover, as presented there, half of the cases that can be solved by FSyft and St Syft, around 400, are ﬁnished in less than 0.1 second, while Strix is unable to solve any cases given such time limit. Counter Game. Figure 3 and Figure 4 show the running time of all tools on the counter game benchmarks. Since all of them got failed on cases with counter bits n > 10, here we only show realizable/unrealizale cases with counter bits n 10, so we have 20 cases for each synthesis problem. The x-labels c-rea/unrea-n indicate the realizability and the number of counter bits of each case. Both of FSyft and St Syft are able to deal with cases with n 10, while Strix only solves cases with n up to 7, either stable LTLf synthesis or fair LTLf synthesis. For those common solved cases, both of FSyft and St Syft take much less time than Strix.

Conclusions In this paper we presented a ﬁxpoint-based technique for LTLf synthesis with assumptions for basic forms of fairness and stability, which is quite effective, as our experiment shows. Our technique can be summarized as follows: use the DFA for the LTLf formula as the arena to play a game for the environment whose winning condition is to avoid reaching the accepting states while making the assumption true. Note that for a general LTL assumption (see (Aminof et al. 2019)), we can transform such an assumption into a parity automaton, take the Cartesian product with the DFA and play the parity/reachability game over the resulting arena. Comparing this possible approach to the reduction to LTL synthesis is a subject for future work. Acknowledgments. Work supported in part by European

4We recommend viewing the ﬁgures online for a better vision.

St Syft Strix

Figure 4: Stable LTLf synthesis. Comparison of running time between St Syft and Strix, in log scale. Bars of the maximum height indicate cases timed out.

Research Council under the European Union s Horizon 2020 Programme through the ERC Advanced Grant White Mec (No. 834228), NSF grants IIS-1527668, CCF-1704883, and IIS-1830549, NSFC Projects No. 61572197, No. 61632005 and No. 61532019.

References Aminof, B.; De Giacomo, G.; Murano, A.; and Rubin, S. 2018. Synthesis under Assumptions. In KR, 615 616. Aminof, B.; De Giacomo, G.; Murano, A.; and Rubin, S. 2019. Planning under LTL Environment Speciﬁcations. In ICAPS. Bloem, R.; Jobstmann, B.; Piterman, N.; Pnueli, A.; and Sa ar, Y. 2012. Synthesis of Reactive(1) Designs. J. Comput. Syst. Sci. 78(3):911 938. Bloem, R.; Ehlers, R.; and K onighofer, R. 2015. Cooperative Reactive Synthesis. In ATVA, volume 9364 of Lecture Notes in Computer Science, 394 410. Springer. Brenguier, R.; Raskin, J.; and Sankur, O. 2017. Assumeadmissible synthesis. Acta Inf. 54(1):41 83. Buchi, J. R., and Landweber, L. H. 1990. Solving Sequential Conditions by Finite-State Strategies. Camacho, A.; Triantaﬁllou, E.; Muise, C.; Baier, J. A.; and Mc Ilraith, S. 2017. Non-Deterministic Planning with Temporally Extended Goals: LTL over Finite and Inﬁnite Traces. In AAAI. Camacho, A.; Baier, J. A.; Muise, C. J.; and Mc Ilraith, S. A. 2018. Finite LTL Synthesis as Planning. In ICAPS, 29 38. Camacho, A.; Bienvenu, M.; and Mc Ilraith, S. A. 2018. Finite LTL Synthesis with Environment Assumptions and Quality Measures. In KR, 454 463. Chatterjee, K., and Henzinger, T. A. 2007. Assumeguarantee synthesis. In TACAS, 261 275. Chatterjee, K.; Henzinger, T. A.; and Jobstmann, B. 2008. Environment Assumptions for Synthesis. In CONCUR, 147 161. De Giacomo, G., and Rubin, S. 2018. Automata-Theoretic Foundations of FOND Planning for LTLf/LDLf Goals. In IJCAI, 4729 4735.

De Giacomo, G., and Vardi, M. 2013. Linear Temporal Logic and Linear Dynamic Logic on Finite Traces. In IJCAI, 854 860. De Giacomo, G., and Vardi, M. Y. 2015. Synthesis for LTL and LDL on Finite Traces. In IJCAI, 1558 1564. D Ippolito, N.; Braberman, V. A.; Piterman, N.; and Uchitel, S. 2013. Synthesizing nonanomalous event-based controllers for liveness goals. ACM Trans. Softw. Eng. Methodol. 22(1):9:1 9:36. Duret-Lutz, A.; Lewkowicz, A.; Fauchille, A.; Michaud, T.; Renault, E.; and Xu, L. 2016. Spot 2.0 a framework for LTL and ω-automata manipulation. In ATVA, 122 129. Finkbeiner, B., and Schewe, S. 2013. Bounded Synthesis. STTT 15(5-6):519 539. Finkbeiner, B. 2016. Synthesis of Reactive Systems. Dependable Software Systems Eng. 45:72 98. Fogarty, S.; Kupferman, O.; Vardi, M. Y.; and Wilke, T. 2013. Proﬁle Trees for B uchi Word Automata, with Application to Determinization. In Gand ALF. Fried, D.; Tabajara, L. M.; and Vardi, M. Y. 2016. BDDBased Boolean Functional Synthesis. In CAV. Gerstacker, C.; Klein, F.; and Finkbeiner, B. 2018. Bounded Synthesis of Reactive Programs. In ATVA, 441 457. Gr adel, E.; Thomas, W.; and Wilke, T., eds. 2002. Automata, Logics, and Inﬁnite Games: A Guide to Current Research [outcome of a Dagstuhl seminar, February 2001], volume 2500 of Lecture Notes in Computer Science. Springer. Green, C. 1969. Theorem Proving by Resolution as Basis for Question-Answering Systems. In Machine Intelligence, volume 4. American Elsevier. 183 205. Kupferman, O., and Vardi, M. Y. 2005. Safraless Decision Procedures. In FOCS, 531 542. IEEE Computer Society. Li, J.; Rozier, K. Y.; Pu, G.; Zhang, Y.; and Vardi, M. Y. 2019. Sat-based explicit ltlf satisﬁability checking. In AAAI, 2946 2953. Martin, D. 1975. Borel Determinacy. Annals of Mathematics 65:363 371. Meyer, P. J.; Sickert, S.; and Luttenberger, M. 2018. Strix: Explicit Reactive Synthesis Strikes Back! In CAV, 578 586. Pnueli, A., and Rosner, R. 1989. On the Synthesis of a Reactive Module. In POPL. Pnueli, A. 1977. The Temporal Logic of Programs. In FOCS, 46 57. Rabin, M. O., and Scott, D. 1959. Finite Automata and Their Decision Problems. IBM J. Res. Dev. 3:114 125. Somenzi, F. 2016. CUDD: CU Decision Diagram Package 3.0.0. Universiy of Colorado at Boulder. Zhu, S.; Tabajara, L. M.; Li, J.; Pu, G.; and Vardi, M. Y. 2017a. A Symbolic Approach to Safety LTL Synthesis. In HVC, 147 162. Zhu, S.; Tabajara, L. M.; Li, J.; Pu, G.; and Vardi, M. Y. 2017b. Symbolic LTLf Synthesis. In IJCAI, 1362 1369.