LTLf Synthesis as AND-OR Graph Search: Knowledge Compilation at Work

1 Introduction

Program synthesis aims at automatically generating a program from declarative specifications expressed in temporal logic [Pnueli and Rosner, 1989; Ehlers et al., 2017]. A commonly used logic for program synthesis is Linear Temporal Logic (LTL), typically used also in model checking [Baier and Katoen, 2008]. Recently, synthesis has been investigated for specifications expressed in LTLf , a finite-trace variant of LTL [De Giacomo and Vardi, 2013]. Roughly speaking, we consider an alphabet of propositions partitioned into those controlled by the agent (one may think of these as a binary encoding of agent actions) and those controlled by the environment (one may think of these as fluents), and then we use LTLf to specify which finite traces are desirable. The outcome of the synthesis procedure is a program (a finite-state controller) that at every time step, given the values of the environment propositions in the history so far, sets the next value of the agent propositions so that the traces generated satisfy the LTLf specification [De Giacomo and Vardi, 2015].

∗The views and opinions expressed in this paper are those of the authors and do not necessarily reflect the official policy or position of Banca d'Italia.

†Corresponding Author

LTLf synthesis has been proven to be one of the most successful synthesis settings so far. Several tools have been developed recently, among which Lisa [Bansal et al., 2020] and Lydia [De Giacomo and Favorito, 2021] are possibly the best performing ones to date. Both these tools are based on first constructing a DFA corresponding to the LTLf specification, and then considering it as a game arena where the agent tries to get to an accepting state in spite that the environment tries to avoid it. A winning strategy, which is a finite controller returned by the synthesis procedure, can be obtained through a backward fixpoint computation for adversarial reachability of the DFA accepting states [De Giacomo and Vardi, 2015]. The main difficulty of this approach is that it requires computing the entire DFA of the LTLf specification, which can be, in the worst case, doubly exponential in the size of the specification [De Giacomo and Vardi, 2015]. Hence, even though the backward fixpoint computation can be performed symbolically, enabling scalable performance [Zhu et al., 2017], the DFA construction step can become a significant bottleneck [Zhu et al., 2019].

An alternative approach is to expand the arena while searching for the accepting states via forward search [Xiao et al., 2021], which is analogous to the approach taken by most work in adversarial Planning with fully observable nondeterministic domains (FOND), where the agent controls the actions and the environment controls the fluents [Ghallab et al., 2004; Geffner and Bonet, 2013]. The agent has to reach the goal, despite that the environment may choose adversarially the effects of the agent actions (strong plans in FOND) [Cimatti et al., 1998; Cimatti et al., 2003; Geffner and Bonet, 2013]. The typical way to deal with this kind of planning is through forward search on an AND-OR graph [Nilsson, 1971], where the OR-nodes correspond to the choices (quantified existentially) of the agent and the ANDnodes correspond to the choices (quantified universally) of the environment [Mattm¨uller et al., 2010; Mattm¨uller, 2013;

Geffner and Bonet, 2013]. Note that the search space generated for FOND planning with a compactly represented domain, say, in PDDL [Haslum et al., 2019], is at most singleexponential [Rintanen, 2004].

Instead, to handle LTLf synthesis, we need to deal with a state space that can be of double-exponential size. Searching over a double-exponential state space has been studied in Planning in partially observable nondeterministic domains (POND), aka contingent planning, where the search procedure must be performed over the belief-states [Reif, 1984; Goldman and Boddy, 1996; Bertoli et al., 2006; Geffner and Bonet, 2013]. However, belief-states have a specific structure [Bertoli et al., 2006; Thanh To et al., 2009], the techniques utilized in contingent planning cannot be directly applied to LTLf synthesis.

In this work, we investigate LTLf forward synthesis adopting an AND-OR graph search as in FOND Planning [Mattm¨uller et al., 2010; Mattm¨uller, 2013], but over a doubly exponential search space, as for contingent planning [Bertoli et al., 2006]. We do not rely on an encoding into PDDL, as [Camacho et al., 2018; Camacho and A. McIlraith, 2019], which may result into a PDDL specification with exponential size. Instead, we develop specific techniques to create the search space on-the-fly while exploring it, such that we can possibly decide realizability/unrealizability before reaching the worst-case double-exponential blowup.

In details, we propose a technique to create on-the-fly the DFA corresponding to the LTLf specification. This technique avoids a detour to automata theory and instead builds directly deterministic transitions from a current state. In particular, this technique exploits LTL formula progression [Emerson, 1990; Bacchus and Kabanza, 1998] to separate what happens now (label) and what should happen next accordingly (successor state). Crucially, we exploit the structure that formula progression provides to branch on propositional formulas (representing several evaluations), instead of individual evaluations. This drastically reduces the branching factor of the AND-OR graph to be searched (recall that in LTLf synthesis, both the agent choices and the environment choices can be exponentially many). More specifically, we label transitions/edges with propositional formulas on propositions controlled by the agent (for OR-nodes) and by the environment (for AND-nodes). Every such propositional formula captures a set of evaluations leading to the same successor node. We leverage Knowledge Compilation (KC) techniques, and in particular Sentential Decision Diagrams (SDDs) [Darwiche, 2011], to effectively generate such propositional formulas for OR-nodes and AND-nodes, and thus reduce the branching factor of the search space. We implemented our approach in a tool called Cynthia and conducted comprehensive experiments by comparing to existing LTLf synthesis tools, including Lisa, Lydia and Ltlfsyn from [Xiao et al., 2021] and demonstrate the merits of our approach.

2 Preliminaries

LTLf Basics. Linear Temporal Logic over finite traces, called LTLf [De Giacomo and Vardi, 2013] is a variant of Linear Temporal Logic (LTL) [Baier and Katoen, 2008] that is interpreted over finite traces rather than infinite traces (as in LTL). Given a set of propositions P, the syntax of LTLf is identical to LTL, and defined as (wlog, we require LTLf formulas are in Negation Normal Form (NNF), i.e., negations only occur in front of atomic propositions): ϕ ::= tt | ff | p | ¬p | ϕ1 ∧ ϕ2 | ϕ1 ∨ ϕ2 | ◦ϕ | ·ϕ | ϕ1 U ϕ2 | ϕ1Rϕ2. tt is always true, ff is always false; p ∈ P is an atom, and ¬p is a negated atom (a literal l is an atom or the negation of an atom); ∧ (And) and ∨ (Or) are the Boolean connectives; and ◦ (Next), · (Weak Next), U (Until) and R (Release) are temporal connectives. We use the usual abbreviations true ≡ p∨¬p, false ≡ p∧¬p, ♦ϕ ≡ true U ϕ and □ϕ ≡ false Rϕ. Also for convenience we consider traces ρ ∈ (2P )∗ , i.e., we consider also empty traces ϵ as in [Brafman et al., 2018]. More specifically, a trace ρ = ρ[0], ρ[1], . . . ∈ (2P )∗ is a finite sequence, where ρ[i] (0 ≤ i < |ρ|) denotes the i-th interpretation of ρ, which can be considered as the set of propositions that are true at instant i, and |ρ| represents the length of ρ. We have that ϵ |= ϕ if ϕ is tt, an R-formula or ·- formula, hence ϵ |= □false. ϵ ̸|= ϕ if ϕ is ff , a literal, U-formula or ◦-formula, hence ϵ ̸|= ♦true. Detailed semantics of LTLf can be found in [De Giacomo and Vardi, 2013; Brafman et al., 2018].

We denote by cl(ϕ) the set of subformulas of ϕ, including tt and ff . We denote by pa(ϕ) ⊆ cl(ϕ) the set of literals and temporal subformulas of ϕ whose primary connective is temporal [Li et al., 2019]. Formally, for an LTLf formula ϕ in NNF, we have pa(ϕ) = {ϕ} if ϕ is a literal or temporal formula; and pa(ϕ) = pa(ϕ1) ∪ pa(ϕ2) if ϕ = (ϕ1 ∧ ϕ2) or ϕ = (ϕ1 ∨ ϕ2).

Having LTLf formula ϕ, replacing every temporal formula ψ ∈ pa(ϕ) with a propositional variable aψ gives us a propositional formula ϕp . As a consequence, two formulas ϕ1 and ϕ2 are propositionally equivalent, denoted by ϕ1 ∼p ϕ2, if, C |= ϕp1 ↔ C |= ϕp2 holds for every propositional assignment C ∈ 2pa(ϕ1)∪pa(ϕ2) . The equivalence class of a formula ψ ∈ cl(ϕ) is denoted by [ψ]∼p and defined as [ψ]∼p = {y ∈ cl(ϕ) | ψ∼py}. The quotient set of a subset C ⊆ cl(ϕ) is denoted by C/∼p and defined as C/∼p = {[ψ]∼p | ψ ∈ C}.

Definition 1. An LTLf formula ϕ is in neXt Normal Form (XNF) if pa(ϕ) only includes literals, ◦- and ·- formulas.

For an LTLf formula ϕ in NNF, we can obtain its XNF by transformation function xnf(ϕ), defined as follows:

• xnf(ϕ) = ϕ if ϕ is a literal, □false, ♦true, ◦-, ·-formula;
• xnf(ϕ1 ∨ ϕ2) = xnf(ϕ1) ∨ xnf(ϕ2);
• xnf(ϕ1 ∧ ϕ2) = xnf(ϕ1) ∧ xnf(ϕ2);
• xnf(ϕ1Uϕ2)=(xnf(ϕ2)∧♦true)∨(xnf(ϕ1)∧◦(ϕ1Uϕ2));

Theorem 1 ([Li et al., 2019]). Every LTLf formula ϕ in NNF can be converted, with linear time in the formula size, to an equivalent formula in XNF, denoted by xnf(ϕ).

- xnf(ϕ1Rϕ2)=(xnf(ϕ2)∨□false)∧(xnf(ϕ1)∨·(ϕ1Rϕ2)). Note that ♦true (resp. □false) guarantees that empty trace is not (resp. is) accepted by U-formulas (resp. R-formulas).

LTLf Synthesis. The problem of LTLf synthesis is described as a tuple (ϕ, X , Y), where ϕ is an LTLf formula over X ∪ Y, and X , Y are two disjoint sets of variables controlled by the environment and the agent, respectively. Sometimes, for simplicity, we do not mention X and Y explicitly, if they are clear from the context.

Definition 2. The synthesis problem (ϕ,X, Y) aims to computing a strategy g : (2X )∗ → 2Y , such that for an arbitrary infinite sequence λ = X0, X1, . . . ∈ (2X )ω , we can find k ≥ 0 such that ρk |= ϕ, where ρk = (X0 ∪ g(ϵ)), (X1 ∪ g(X0)), . . . , (Xk ∪g(X0,X1, . . . ,Xk-1)). If such a strategy does not exist, then ϕ is unrealizable.

LTLf synthesis can be solved by reducing to an adversarial reachability game on the corresponding Deterministic Finite Automaton (DFA) [De Giacomo and Vardi, 2015]. Hence, a strategy can also be represented as a finite-state controller g : S ↦→ 2Y , where S denotes the state space of the DFA.

Sentential Decision Diagrams (SDDs). SDDs [Darwiche, 2011] is a Knowledge Compilation (KC) technique designed for an efficient representation and manipulation of Boolean functions. In order to represent a Boolean function, the classical method is applying Shannon decomposition, as done in Ordered Binary Decision Diagrams (BDDs) [Bryant, 1992]. Intuitively, BDD decomposes Boolean functions with one variable at a time. Therefore, the canonicity of BDD is determined wrt a specific ordering of variables. SDD, instead, utilizes a more general decomposition technique that decomposes Boolean functions with a set of variables at each round. Let f(Y ∪ X) be a Boolean function over variables Y ∪ X, where Y, X are disjoint. Given an (Y, X )-partition, where Y variables are considered primary and X variables are considered subsequent, the SDD of f, with respect to the (Y,X)- partition, can be written as ∨ni=1 [primei(Y) ∧ subi(X)]. Intuitively, SDD decomposes f into n children, each of which consists of Boolean functions primei(Y) (what are satisfied in primary) and subi(X) (what should be satisfied in subsequent, according to primei(Y)). In particular, besides that all the primes are disjoint and covering, i.e., primei ∧ primej = false for i ̸= j, and ∨ni=1 primei = true, SDD also guarantees that all the subs are compressed, i.e., subi(X) ̸= subj(X) for i ̸= j. Hence, the canonicity of SDDs is determined wrt a specific partition of variables.

3 DFAConstruction from LTLf

The classical approach to LTLf synthesis first constructs the complete DFA, and then solves an adversarial reachability game through a backward fixpoint computation on this DFA [De Giacomo and Vardi, 2015]. An alternative approach presented in [Xiao et al., 2021] is an on-the-fly synthesis technique that is able to construct the automaton while solving the game in a forward way. Yet, the game arena generated there is explicit, s.t. during search, there can be an exponential number of options to explore at every state, leading to a major drawback for scalability. We now present a new DFA construction based on an incremental technique called formula progression that is suitable for exploiting SDDs.

LTLf Formula Progression. Consider an LTLf formula ϕ over P and a finite trace ρ = ρ[0], ρ[1], . . . ∈ (2P )∗ , in order to have ρ |= ϕ, we can start from ϕ, progress or push ϕ through ρ. The idea behind formula progression is to consider LTLf formula ϕ into a requirement about now ρ[i], which can be checked straightaway, and a requirement about the future that has to hold on the yet unavailable suffix. That is to say, formula progression looks at ρ[i] and ϕ, and progresses a new formula fp(ϕ, ρ[i]) such that ρ, i |= ϕ iff ρ, i + 1 |= fp(ϕ, ρ[i]). This procedure is analogous to DFA reading trace ρ, where reaching accepting states is essentially achieved by taking one transition after another. Formula progression has been studied in prior work, cf. [Emerson, 1990; Bacchus and Kabanza, 1998]. Here we use it for constructing DFA from LTLf formulas.

Note that, since ρ is a finite trace, it is necessary to clarify when the trace ends. To do so, we introduce two new formulas □false and ♦true, which, intuitively, refer to finite trace ends and finite trace not ends, respectively. For simplicity, we enrich cl(ϕ), the set of proper subformulas of ϕ, to include them such that cl(ϕ) is reloaded as cl(ϕ) ∪ cl(♦true) ∪ cl(□false ).

Definition 3 (LTLf Formula Progression). For an LTLf formula ϕ in NNF, the progression function fp(ϕ, σ), where σ ∈ 2P , is defined as follows:

• fp(tt , σ) = tt and fp(ff , σ) = ff ;
• fp(p, σ) = tt if p ∈ σ, otherwise ff ;
• fp(ϕ1 ∧ ϕ2, σ) = fp(ϕ1, σ) ∧ fp(ϕ2, σ);
• fp(¬p, σ) = tt if p /∈ σ, otherwise ff ;
• fp(ϕ1 ∨ ϕ2, σ) = fp(ϕ1, σ) ∨ fp(ϕ2, σ);
• fp(·ϕ, σ) = ϕ ∨ □false; - fp(ϕ1Uϕ2, σ)=fp(ϕ2, σ)∨(fp(ϕ1, σ)∧fp(◦(ϕ1Uϕ2), σ));
• fp(◦ϕ, σ) = ϕ ∧ ♦true;
• fp(ϕ1Rϕ2, σ)=fp(ϕ2, σ)∧(fp(ϕ1, σ)∨fp(·(ϕ1Rϕ2), σ)).

The following two lemmas show that fp(ϕ, σ) strictly follows LTLf semantics and retains the propositional behavior of LTLf formulas.

Note that fp(ϕ, σ) is a positive Boolean formula on cl(ϕ), i.e., fp(ϕ, σ)∈B+(cl(ϕ)).

Lemma 1. Let ϕ be an LTLf formula over P in NNF, ρ be a finite nonempty trace, fp(ϕ, σ) be as above. We have that ρ, i |= ϕ iff ρ, i + 1 |= fp(ϕ, ρ[i]).

Lemma 2. Let ϕ and ψ be two LTLf formulas over P in NNF s.t. ϕ ∼p ψ, and σ ∈ 2P . Then fp(ϕ, σ) ∼p fp(ψ, σ) holds.

We generalize LTLf formula progression from single instants to finite traces by defining fp(ϕ, ϵ) = ϕ, and fp(ϕ, σu) = fp(fp(ϕ, σ), u), where σ ∈ 2P and u ∈ (2P )∗ .

Lemma 3. Let ϕ be an LTLf formula over P in NNF, ρ be a finite trace. We have that ρ |= ϕ iff ϵ |= fp(ϕ, ρ).

Given an LTLf formula ϕ, we can consider it as the initial state, and recursively apply formula progression to obtain all reachable states (through deterministic transitions), denoted by Reach(ϕ) = {fp(ϕ, ρ) | ρ ∈ (2P )∗ }. Note that once applying propositional equivalence, there can only be 22|cl(ϕ)| elements in Reach(ϕ)/∼p . Lemma 3 shows that a state ψ ∈ Reach(ϕ)/∼p can be recognized as accepting iff ϵ |= ψ, indicating that there exists a trace ρ such that ψ = fp(ϕ, ρ) and ρ is completely "consumed" by formula progression, returning a formula, corresponding to an accepting state, that holds on the empty trace ϵ. In particular, given that every state ψ is actually a positive Boolean formula on cl(ϕ), checking ϵ |= ψ only requires dealing with Boolean operators of disjunction and conjunction, which can be done in linear time. The correctness and complexity of our DFA construction are stated below.

Theorem 2. Given LTLf formula ϕ, the following DFA recognizes L(ϕ): A = (2P , S, s0, δ,Acc), where the states S = Reach(ϕ)/∼p , the initial state s0 = ϕ∼p , the transition function δ([ψ]∼p , σ) = fp([ψ]∼p , σ), ∀σ ∈ 2P and the accepting states Acc = {ψ | ϵ |= ψ}.

Theorem 3. Let ϕ be an LTLf formula, the constructed DFA A can have, in the worst case, 22|cl(ϕ)| states.

4 LTLf Synthesis as AND-ORGraph Search

Recall that LTLf synthesis can be viewed as an adversarial reachability game on the DFA of the given formula. Interestingly, this game can actually be considered as an AND-OR graph, where the OR-nodes indicate the agent actions (quantified existentially), and the AND-nodes indicate the environment responses (quantified universally). In this case, the DFA construction approach described in the previous section allows us to solve LTLf synthesis via on-the-fly ANDOR graph search. Now, we present our approach of solving LTLf synthesis via on-the-fly AND-OR graph search, and explain how to leverage KC techniques, Sentential Decision Diagrams (SDDs) [Darwiche, 2011] to significantly reduce the branching factor of the constructed graph.

4.1 Synthesis Algorithm

Given problem (ϕ,X, Y), our synthesis algorithm searches for a strategy by exploring the constructed AND-OR graph on the fly. This algorithm is basically a top-down traversal of the search space, proceeding forward from the initial, and excluding strategies that lead to loops. Since we apply the crucial step of propositional equivalence check whenever computing a new state, for simplicity, we omit the propositional equivalence symbol ∼p and denote every newly constructed DFA state by ψ, instead of [ψ]∼p , e.g., the initial state is denoted by ϕ, instead of [ϕ]∼p . Every DFA state is stored as an OR-node, each outgoing transition (or-arc) leads to an AND-node. Every or-arc is stored as an action-AndNode pair (act, AndNd). Every outgoing transition (and-arc) of an AND-node is stored as a response-OrNode pair (resp, n). A strategy is stored as a set of state-action pairs. If ϕ is unrealizable, we obtain strategy as an empty set. In order to avoid exploring the same state over and over, we assign a tag to its associated OR-node n after exploring it. More specifically, n is tagged as success if the corresponding DFA state ψ is accepting or there exists an act such that, regardless of what the environment resp is, all corresponding followup OR-nodes are already tagged as success. In this case, we also add state-action pair (ψ, act) to strategy. If such act does not exist, n is tagged as failure. Moreover, we also put a loop tag on an OR-node n if a loop is detected on n, which is considered as temporary failure.

As shown in Algorithm 1, the SYNTHESIS procedure takes a given LTLf formula ϕ as input (X, Y are omitted for simplicity), and first checks whether the initial state ϕ is accepting. If this is the case, state-action pair (ϕ, true) is added to

Algorithm 1 SDD-based Forward Synthesis

1: function SYNTHESIS(ϕ) return strategy 2: if ISACCEPTING(ϕ) then 3: ADDTOSTRATEGY(ϕ, true) 4: return GETSTRATEGY() 5: INITIALGRAPH(ϕ) 6: n := GETGRAPHROOT() 7: found := SEARCH(n, ∅) 8: if found then return GETSTRATEGY() 9: return EMPTYSTRATEGY() ▷ ϕ is unrealizable 10: function SEARCH(n, path) return True/False 11: if ISSUCCESSNODE(n) then return True 12: if ISFAILURENODE(n) then return False 13: if INPATH(n, path) then ▷ We found a loop 14: TAGLOOP(n) return False 15: ψ :=FORMULAOFNODE(n) 16: if ISACCEPTING(ψ) then 17: TAGSUCCESSNODE(n) 18: ADDTOSTRATEGY(ψ, true) 19: return True 20: EXPAND (n) ▷ Uses SDD to partition ψ wrt Y and X 21: for (act, AndNd) ∈GETORARCS(n) do 22: for (resp, succ) ∈GETANDARCS(AndNd) do 23: found :=SEARCH(succ, [path|n]) 24: if ¬found then Break 25: if found then 26: TAGSUCCESSNODE(n) 27: ADDTOSTRATEGY(ψ, act) 28: if ISTAGLOOP(n) then 29: BACKPROP(n) 30: return True 31: TAGFAILURENODE(n) 32: return False

strategy and returned (Line 4). This is because the agent can do whatever it wants (i.e., assign any value to its variables Y) after reaching an accepting state. Otherwise, we initialize the graph by creating an OR-node n out of ϕ, and start the main procedure SEARCH. The SEARCH procedure is a recursive routine, taking an OR-node n and the path leading to n as inputs, returning True (resp. False) indicating that a strategy is (resp. isn't) found by the current recursion. Hence, if the outmost SEARCH returns True, a strategy consisting of all state-action pairs added until then is returned (Line 8). Otherwise, an empty strategy is returned.

SEARCH processes an OR-node n by first checking whether n is tagged already, if so, it returns True for success tag, and False for failure tag. Then, if n exists on path thus leading to a loop, we put a loop tag on node n, and return False. Intuitively, when a loop is detected at node n, the procedure returns False, temporally considering n as a failure node. Note that we do not tag n as failure, since it is unknown here whether all the or-arcs of n are explored. Indeed, the returned False will be taken into account when tagging the ancestor nodes of n. Therefore, when later n is tagged as success, this information needs to be propagated back to the

Algorithm 2 Propagate Success Backwards

ancestor nodes of n.

Later on, the procedure continues by checking whether the associated DFA state ψ of n is accepting, if so, n is tagged as success, and (ψ, true) is added to the strategy. If none of these checks succeeds, n is expanded by EXPAND, which constructs all its or-arcs (act, AndNd), and and-arcs (resp, succ) of every AndNd. The crucial constraint is that all the agent actions acts of OR-node n should be disjoint and covering, the same with environment responses resp of every AndNd. Indeed, EXPAND is based on SDDs, see Section 4.2. As a side-effect, the EXPAND function stores the newly constructed nodes and arcs from n. We explore OR-node n, by iteratively processing the list of AND-nodes AndNd connected to n, until a strategy is found (Lines 21-32). In Line 23, we recursively call SEARCH with the by n extended path. For every AndNd, once False is detected for searching some succ, we give up on the current AndNd and proceed with the next one (Line 24). If searching every succ of AndNd returns True (Line 25), n is tagged as success, and the corresponding state-action pair (ψ, act) is stored. Moreover, if n carries a loop tag, it is easy to see that n has been temporally considered as a failure node, and this information has been taken into account when tagging the ancestor nodes of n. Therefore, it is necessary to propagate this success information from n backwards to the ancestor nodes of n (Lines 28-29). If no strategy is found after exploring n, we tag it as failure, and SEARCH returns False. It should be noted that, in a forward search on an AND-OR graph, it is critical to handle loops with the assistance of this backward propagation, by BACKPROP, as illustrated in [Scutell`a, 1990].

As shown in Algorithm 2, BACKPROP is basically a bottom-up traversal of the subgraph rooted at n, that starts from the leaves, and propagates success backwards. In particular, only the nodes that are tagged as failure must be considered. This is because once a node n is tagged as success, it indicates that n is not affected by any temporary failure of its children. We start from the direct parents of n, and put them in a queue N. For every direct failure parent node np of n, np can be tagged as success only if there exists an or-arc (act, AndNd), such that all the followup OR-nodes are already tagged as success. In this case, the corresponding state-action pair (ψ, act) is stored. Moreover, the success information of np should also be propagated, since np was tagged as failure, which could have affected the tag information of the direct parent nodes of np. Therefore, we add the failure nodes of

Algorithm 3 SDD-based ExpandGraph from An OrNode

them to N. The propagation continues until N gets empty. It is easy to see that the backward propagation does not change the forward nature of the SEARCH procedure, since the backward propagation has to be considered only as an instrument to correctly propagate the success whenever needed, i.e., in the presence of loops.

A major challenge arises, however, when looking into the branching factor of this AND-OR graph. Note that, in EXPAND, if we simply use Y ∈ 2Y as act for every OR-node n, and X ∈ 2X as resp for every AndNd connected to n, there can be far too many directions to explore, which leads to crucial performance limitation. Another challenge comes from the propositional equivalence check, which needs to be performed whenever computing a new state. We now explain how to use Sentential Decision Diagrams (SDDs) [Darwiche, 2011] to tackle both these challenges.

4.2 SDD-based EXPAND

The crucial reason of adopting SDDs in the implementation of EXPAND (Algorithm 3), rather than other KC techniques, e.g., BDDs, is that, while maintaining canonicity to check propositional equivalence in constant time, SDDs can provide a disjoint, covering and compressed partition of a Boolean function, wrt a hierarchy of (Y,X)-partition. This allows us to easily partition the transition labels into disjoint agent moves and disjoint environment moves, compressed as much as possible, and so labeling transitions symbolically by propositional formulas. Let ψ be the associated DFA state of n, the input of EXPAND(n). The algorithm starts from computing xnf(ψ), which is equivalent to ψ, and intuitively, encodes all the possibilities of what happens now, expressed by Y ∪ X variables, and what happens next accordingly, expressed by variables Z = ⋃θ∈cl(ϕ) {zα|α ∈ pa(xnf(θ)), α not literal}. Note that it is crucial to consider the closure of the original LTLf formula ϕ, instead of the current state ψ, as the propositional equivalence check between two states requires their SDDs to be defined over the same set of variables.

In Line 3, we represent xnf(ψ), considering it as a propositional formula over pa(xnf(ψ)), into an SDD T := ∨ni=1 [primei(Y) ∧ subi(X ∪ Z)] such that all Y s leading to the same set of possible successors subi(X ∪ Z) (X is not decided yet) are clustered into a propositional formula primei(Y). primei(Y) and subi(X ∪Z) are extracted as act and corresponding AndNd, respectively (Lines 5&6). Moreover, subi(X ∪ Z) = ∨mj=1 [primei,j(X) ∧ subi,j(Z)] is such that all Xs leading to the same successor are clustered into formula primej(X), and subi,j(Z) refers to the successor state of agent-env choices (primei(Y), primei,j(X)). They are extracted as resp and corresponding succ, respectively (Lines 9-11). Note that SDDs guarantee that all disjuncts generated are disjoint, covering and compressed, hence we can use SDDs to reduce the branching factor as much as possible. In particular, every successor state succ is obtained by stripping ◦ and ·, introduced by XNF, through the remove-next function RMNEXT, defined below:

• RMNEXT(♦true) = tt , RMNEXT(□false) = ff
• RMNEXT(ϕ1 ∧ ϕ2) = RMNEXT(ϕ1) ∧ RMNEXT(ϕ2)
• RMNEXT(◦ϕ) = ϕ∧♦true, RMNEXT(·ϕ) = ϕ∨□false Note that RMNEXT applies to neither U-,R- formulas, since they do not appear in XNF, nor literals (p, ¬p), since its input is a propositional formula over variables Z that does not contain literals.
• RMNEXT(ϕ1 ∨ ϕ2) = RMNEXT(ϕ1) ∨ RMNEXT(ϕ2)

Lemma 4. Algorithm 3 is correct, i.e., given an OR node n, EXPAND correctly expands the search graph.

Proof. (Sketch) We prove the lemma by first showing that the XNF of the LTLf formula ψ, associated to n, essentially captures all the transitions that can be obtained by applying formula progression on ψ. The SDD representation of xnf(ψ) correctly provides a disjoint and covering partitions of all the transitions. Hence, the SDD-based EXPAND is correct.

Theorem 4. Algorithm 1 terminates in at most doubleexponential time, in the size of ϕ of problem (ϕ, X, Y).

Proof. (Sketch) This is guaranteed by the fact that the number of recursive calls in SEARCH is bounded by the worstcase doubly-exponential number of states in the constructed DFA via the SDD-based technique. Note that every recursive call first checks for success, failure, and loop (Lines 11-19). Then if the recursive call gets to Line 20, it will eventually tag the current node as success or failure. Therefore, every node is explored only once in a forward manner. Note that if a success node n was also tagged loop, BACKPROP is called before completing the current recursive call. BACKPROP is essentially a Breadth First Search (BFS) on the subgraph rooted at n. Since there can be at most linear number of (n1, (act, resp), n2) edges in this subgraph, and every (n1, (act, resp), n2) edge is visited only once during the BFS, BACKPROP terminates in linear time in the size of the subgraph rooted at n. Hence, we conclude that Algorithm 1 terminates in at most double-exponential time, in the size of ϕ of problem (ϕ, X , Y).

Theorem 5. Algorithm 1 is correct, i.e., it returns a nonempty strategy iff the given synthesis problem is realizable.

Proof. (Sketch)We prove by showing themain recursive procedure SEARCH is correct. If SEARCH does not detect any loops on the graph, we can see that once an OR-node n is tagged, the tag is stored until the algorithm terminates. n is tagged as success if either n is detected as accepting, or there exists an agent act, following which, all the successors are also tagged as success, regardless of what the environment resp is, and the current recursion returns True. Note that, only in this case, the corresponding state-action pair is added to strategy. If neither condition happens, n is tagged as failure, and the current recursion returns False.

If SEARCH detects a loop on n in the graph, the presence of the loop leads to temporary failure. It could happen that a parent node np (also further ancestor nodes) of n is tagged as failure due to this temporary failure of n. Therefore, once n is tagged as success, the success tag should be propagated in the loops through BACKPROP. BACKPROP is correct, since the tag of a parent node np (also further ancestor nodes) changes from failure to success iff there exists an agent act, following which, all the successors are also tagged as success, regardless of what the environment resp is. Therefore, BACKPROP is able to eliminate the temporary failure caused by loops. Hence, if a failure tag stays until the algorithm terminates, this is a confirmed failure that is not affected by any temporary failure. As a result, Algorithm 1 terminates with the initial node tagged as success and returns a non-empty strategy iff the given synthesis problem is realizable.

5 Implementation and Empirical Evaluations

We implemented the forward synthesis problem presented in Section 4 in a tool called Cynthia in C++ 1 . Cynthia is able to take an LTLf synthesis problem (ϕ, X , Y) and constructs a strategy that realizes ϕ if one exists. We make use of library SDD-2.0 (http://reasoning.cs.ucla.edu/sdd) to handle all SDD related operations.

Cynthia also applies some optimizations to speed up the synthesis procedure. First, right before EXPAND an ORnode n, we perform the pre-processing techniques described in [Xiao et al., 2021]. More specifically, we check: (i) there exists a one-step strategy that reaches accepting states from n, then n is tagged as success; or (ii) there does not exist an agent move that can avoid sink state (a non-accepting state only going back to itself) from n, then n is tagged as failure. Moreover, despite being a depth-first search, the SDD-based EXPAND(n), in fact, constructs all the connected AndNd of n, and followup OR-nodes succ at once, which allows us to conduct a "look-ahead" check. More specifically, this "look-ahead" check tries to tag constructed succ by the preprocessing techniques to speed up further search.

Experimental Methodology. We evaluated the efficiency of Cynthia, by comparing against the following tools: Lisa [Bansal et al., 2020] and Lydia [De Giacomo and Favorito, 2021] are state-of-the-art backward LTLf synthesis approaches. Both tools compute the complete DFA first, and then solve an adversarial reachability game following the symbolic backward computation technique described in [Zhu et al., 2017]. Ltlfsyn [Xiao et al., 2021] implements a SATbased on-the-fly forward synthesis approach.

Experiment Setup. Experiments were run on a computer cluster, where each instance took exclusive access to a computing node with Intel-Xeon processor running at 2.6 GHz, with 8GB of memory and 300 seconds of time limit. The correctness of Cynthia was empirically verified by comparing the results with those from all baseline tools. No inconsistencies were encountered for all solved instances.

1 Tool available at https://whitemech.github.io/cynthia.

Benchmarks. We collected, in total, 1494 LTLf synthesis instances from literature: 40 Patterns instances [Xiao et al., 2021]; 54 Two-player-Games instances [Tabajara and Vardi, 2019; Bansal et al., 2020]; 1400 Random instances [Zhu et al., 2017; De Giacomo and Favorito, 2021].

Results and Analysis. Figure 1a and Figure 1b show the running time of each tool on every instance of the GF-, and U-pattern, respectively. Across these instances, we observe that Cynthia is able to solve all instances with much less time comparing to backward approaches, represented by Lisa and Lydia. Comparing to Ltlfsyn, Cynthia is able to achieve comparative performance on the GF-pattern instances, with time cost difference of <1 second (y-axis is in log scale), see Figure 1a. On the U-pattern instances, Cynthia shows significantly better performance, see Figure 1b. On the Two-playerGames benchmarks, see Figure 1c, we observe that Cynthia is able to dominate all other tools on the Nim instances. Yet, on both Counter(s) instances, backward approaches show better performance over all forward approaches, and Cynthia is almost on par with Ltlfsyn. On the Random benchmarks, Cynthia, in general, performs better than Ltlfsyn, by solving more instances with less time, see Figure 1d. Nevertheless, Cynthia cannot beat backward approaches.

It is clear from the plots that Cynthia, in general, shows an overall better performance than Ltlfsyn, illustrating the efficiency and better scalability of our approach. In particular, there is a notable outperformance of Cynthia on the U-pattern instances, see Figure 1b. The challenge in the U-pattern instances lies mostly in proving realizable, and can be achieved by just satisfying variables under control. Since every variable appears only once on the right side of the U operator, our approach is able to compress the branching labels as propositional formulas, such that highly reducing the branching factor and thus speeding up the search procedure.

When comparing Cynthia with backward approaches integrated tools, it should be noted that, in general, forward approaches perform well on the instances where the result can be obtained far before exploring the whole search space. In our benchmarks, this is exactly what happens for Nim and Pattern instances, where Cynthia shows dominating performance over all tools, which demonstrates the promising efficiency of forward synthesis.

On the other hand, backward approaches perform better when it is necessary to explore the entire search space. In the case of the Counter(s) instances, due to their specific structure, in order to obtain a strategy, the searching space to explore grows exponentially fast. In particular, the branching factor of AND-nodes, even after clustering, can remain exponential in the number of environment variables, and so leaving no space to further reduce. Nevertheless, backward approaches can leverage powerful minimization to highly reduce the searching space such that achieving better performance, as also observed in [Tabajara and Vardi, 2019]. For the Random instances, which are randomly conjuncted LTLf formulas, the advantage of possibly being lucky and finding a solution quickly without exploring the entire search space is overwhelmed by the fact that backward approaches integrated with composition techniques [Bansal et al., 2020; De Giacomo and Favorito, 2021] are able to first decompose the conjuncted formula into smaller pieces, obtain the minimized DFA of each conjunct and then compose them for final game solving. It might be possible that similar composition ideas could be leveraged to forward synthesis approaches as well, although further research is necessary in this direction.

6 Conclusions

We investigated the effectiveness of forward search in LTLf synthesis. We observed that even an uninformed search is able to drastically improve the synthesis capability in several cases (as in the Nim benchmarks above). This shows that our approach is quite promising, especially considering that we could move from the uninformed search presented here to informed search exploiting heuristics [Mattm¨uller, 2013; Jim´enez and Torras, 2000].

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", NSFC No. 62002118, No. U21B2015 and Shanghai Pujiang Talent Plan No. 20PJ1403500, NSF grants IIS1527668, CCF-1704883, IIS-1830549, CNS-2016656, DoD

• MURI grant N00014-20-1-2787, and an award from the Maryland Procurement Office.