Forward LTLf Synthesis: DPLL At Work

Abstract

This paper proposes a new AND-OR graph search approach for synthesis of formulas in Linear Temporal Logic on finite traces ( ltl ) that overcomes some limitations of previous works. We devise a procedure inspired by the Davis-Putnam-Logemann-Loveland (DPLL) algorithm to generate the next available agent-environment moves in a truly depth-first fashion, possibly avoiding exhaustive enumeration or costly compilations. We also propose the use of an equivalence check for search nodes based on the syntactic equivalence of state formulas. Since the resulting procedure is not guaranteed to terminate, we identify a stopping condition to abort execution and restart the search with state-equivalence checking based on Binary Decision Diagrams (BDD), which we show to be correct. The experimental results show that in many cases the proposed technique outperforms other state-of-the-art approaches. Our implementation Nike competed in the ltl Realizability Track in the 2023 edition of SYNTCOMP, and won the competition.

Keywords

• eol>Linear temporal logic on finite traces
• LTLf Synthesis
• AND-OR Graph Search

1. Introduction

Program synthesis is the task of finding a program that provably satisfies a given high-level formal specification [ 2 ]. A commonly used logic for program synthesis is Linear Temporal Logic (ltl) [ 3, 4 ], typically used also in model checking [ 5 ]. ltl on finite traces (ltl ) [ 6 ], a variant of ltl to specify finite -horizon temporal properties, has been recently proposed as specification language for temporal synthesis [ 7 ]. The ltl synthesis setting considers a set of variables controllable by the agent, a (disjoint) set of variables controlled by the environment, and a ltl specification that specifies which finite traces over such variables are desirable. The problem of ltl synthesis consists in finding a finite-state controller that, at every time step, given the values of the environment variables in the history so far, sets the next values for each agent proposition such that the generated traces comply with the ltl specification.

The basic technique for solving ltl synthesis amounts to constructing a deterministic finite automaton (dfa) corresponding to the ltl specification, and then considering it as a game arena where the agent tries to get to an accepting state regardless of the environment’s moves. A winning strategy, i.e. a finite controller returned by the procedure, can be obtained through a backward fixpoint computation for adversarial reachability of the dfa accepting state. Related works. State-of-the-art tools such as Lydia [ 8 ] and Lisa [ 9 ] are based on the classical approach. The main drawback of this technique is that it requires to compute the entire dfa of the ltl specification, which in the worst case can be doubly exponential in the size of the formula. Therefore, the dfa construction step becomes the main bottleneck.

A natural idea is to consider a forward search approach that expands the arena on-the-fly while searching for a solution, possibly avoiding the construction of the entire arena. Forwardbased approaches are at the core of the best solution methods designed for other AI problems: Planning with fully observable non-deterministic domains (FOND) [ 10, 11, 12, 13 ], where the agent has to reach the goal, despite that the environment may choose adversarially the efects of the agent actions, and Planning in partially observable nondeterministic domains (POND), also known as contingent planning, where the search procedure must be performed over the belief-states [ 14, 15, 16 ]. However, techniques developed for such problems cannot be applied to ours: in a FOND planning problem, represented with PDDL [ 17 ], the search space is at most single-exponential [ 18 ], whereas for ltl synthesis the state space can be of double-exponential size wrt the size of the formula; hence, we do not rely on an encoding into PDDL, as [ 19, 20 ], which may result in a PDDL specification with exponential size. In POND planning, despite the double-exponential size of the state space, belief-states have a specific structure [ 16, 21 ], so their solution techniques cannot be directly applied to ltl synthesis.

For these reasons, researchers have been looking into forward search techniques specifically conceived for solving ltl synthesis. Two notable attempts in this direction have been presented in [ 22 ] and [ 23 ]. The former work presents an on-the-fly synthesis approach via conducting a so-called Transition-based Deterministic Finite Automata (TDFA) game, where the acceptance condition is defined on transitions, instead of states. The main issue of that approach is the full enumeration of agent-environment moves, which are exponentially many in the number of variables. Moreover, due to the fact that the acceptance condition is defined on transitions, every generated transition has to be checked for acceptance. The latter work instead proposes a search framework for ltl synthesis, where the dfa arena is seen as an AND-OR graph. The available moves are found according to the formula associated with the current search node by means of a Knowledge Compilation technique: Sentential Decision Diagrams (SDD) [ 24 ]. Notably, they are able to branch on propositional formulas, representing several evaluations, instead of individual ones. This can drastically reduce the branching factor. Nevertheless, for certain types of problem instances, the approach can get stuck with demanding compilations of the state formulas, needed both for state equivalence checking and for search node expansion. Moreover, the requirement of having an irreducible representation of players’ moves can be of little usefulness if the branching factor of the search problem is already high, hence resulting in an even more significant compilation overhead.

We think there is a need for a search approach that scales well with the increase of computational power and that uses such power for actually exploring the search space rather than wasting time either slavishly enumerating the exponentially many variable assignments, or by ifnding the minimal representation of the available search moves.

Contributions. First, we focus our attention on two primitive operations for forward ltl synthesis: state-equivalence checking and search node expansion, and explain at high-level how these are combined in our approach, highlighting limitations of previous related works. Then, we formalize and discuss two well-known instances of equivalence checks; one based on knowledge compilation, and the other on a computationally-cheap syntactical equivalence between state formulas. Furthermore, we propose a novel search graph expansion technique, based on a procedure inspired by the famous Davis-Putnam-Logemann-Loveland (DPLL) algorithm. Finally, we describe the implementation of a new tool, Nike, that integrates the proposed modules in the search procedure, and compare its performance on known benchmarks with other stateof-the-art tools, showing its surprising efectiveness. Nike won the ltl Realizability Track in the 2023 edition of SYNTCOMP 1. The complete technical report, including detailed proofs and comprehensive experimental results, is available on arXiv [ 25 ].

2. Preliminaries

ltl Basics. Linear Temporal Logic over finite traces, called ltl [ 6 ] is a variant of Linear Temporal Logic (ltl) [ 5 ] that is interpreted over finite traces rather than infinite traces (as in ltl). Given a set of propositions , the syntax of ltl is identical to ltl, and defined as (wlog, we require that ltl formulas are in Negation Normal Form (nnf), i.e., negations only occur in front of atomic propositions):

::= tt | ff | | ¬ | 1 ∧ 2 | 1 ∨ 2 | ∘ | ∙ | 1 2 | 1 ℛ 2 tt is always true, ff is always false; ∈ is an atom, and ¬ is a negated atom (a literal is an atom or the negation of an atom); ∧ (And) and ∨ (Or) are the Boolean connectives; and ∘ (Next), ∙ (Weak Next), (Until) and ℛ (Release) are temporal connectives. We use the usual abbreviations true ≡ ∨ ¬, false ≡ ∧ ¬, ♢ ≡ true and □ ≡ false ℛ . Also for convenience we consider traces ∈ (2 )* , i.e., we consider also empty traces as in [ 26 ]. More specifically, a trace = [0], [ 1 ], . . . ∈ (2 )* is a finite sequence, where [] (0 ≤ < | |) denotes the -th interpretation of , which can be considered as the set of propositions that are at instant , and | | represents the length of . We have that |= if is tt , an ℛ-formula or ∙ -formula, hence |= □ . ̸|= if is ff , a literal, -formula or ∘ -formula, hence ̸|= ♢ true.

We consider the semantics of ltl as presented in [ 26 ], that also works for empty traces. Given a finite trace and an ltl formula , we inductively define when is for at point (0 ≤ < | |), written , |= , as follows: - , |= tt and , ̸|= ff ; - , |= if ∈ [], and , |= ¬ if ∈/ []; - , |= 1 ∧ 2 if , |= 1 and , |= 2; - , |= 1 ∨ 2 if , |= 1 or , |= 2; - , |= ∘ if 0 ≤ < | | − 1 and , + 1 |= ; - , |= ∙ if 0 ≤ < | | implies , + 1 |= ; - , |= 1 2 if there exists with ≤ < | | such that , |= 2, and ∀. ≤ < we have , |= 1; 1http://www.syntcomp.org/syntcomp-2023-results/ - , |= 1 ℛ 2 if for all with ≤ < | | either we have , |= 2, or ∃. ≤ < we have , |= 1.

An ltl formula is for , denoted by |= , if and only if , 0 |= . In particular, |= □ and ̸|= ♢ .

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 [ 27 ]. Formally, for an ltl 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 ltl formula , replacing every temporal formula ∈ pa( ) with a propositional variable gives us a propositional formula ; we call this operation propositionalization of . Note that ∈ ℬ+(cl( )), i.e. is a positive Boolean formula over variables cl( ). Let = , we denote with tf = the inverse operation of · . Two formulas 1 and 2 are propositionally equivalent, denoted by 1 ∼ 2, if, |= 1 ↔ |= 2 holds for every propositional assignment ∈ 2pa( 1)∪pa( 2).

An ltl formula is in neXt Normal Form (xnf) if pa( ) only includes literals, ∘ - and ∙ -formulas. For an ltl formula in nnf, we can obtain its xnf by transformation function xnf( ), defined as follows: - xnf( ) = if is a literal, □ , ♢ , ∘ -, ∙ -formula; - xnf( 1 ∧ 2) = xnf( 1) ∧ xnf( 2); - xnf( 1 ∨ 2) = xnf( 1) ∨ xnf( 2); - xnf( 1 2) = (xnf( 2) ∧ ♢ true) ∨ (xnf( 1) ∧ ∘ ( 1 2)); - xnf( 1 ℛ 2) = (xnf( 2) ∨ □ false) ∧ (xnf( 1) ∨ ∙ ( 1 ℛ 2)).

Note that ♢ true (resp. □ false) guarantees that empty trace is not (resp. is) accepted by formulas (resp. ℛ-formulas).

Theorem 1 ([ 27 ]). Every ltl formula in nnf can be converted, with linear time in the formula size, to an equivalent formula in xnf, denoted by xnf( ). ltl Formula Progression [ 23 ]. Consider an ltl formula over and a finite trace = [0], [ 1 ], . . . ∈ (2 )* , in order to have |= , we can start from , progress or push through . The idea behind formula progression is to split an ltl formula into a requirement about now [], which can be checked straightaway, and a requirement about the future that has to hold in the yet unavailable sufix. That is to say, formula progression looks at [] and , and progresses a new formula fp(, []) such that , |= if , + 1 |= fp(, []). 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. [28, 29]. Here we use the formalization provided in [ 23 ].

Note that, since is a finite trace, it is necessary to clarify when the trace ends. To do so, two new formulas are introduced: □ false and ♢ true, which, intuitively, refer to finite trace ends and ifnite 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). For an ltl formula in nnf, the progression function fp(, ), where ∈ 2 , is defined as follows: - fp(tt , ) = tt and fp(ff , ) = ff ; - fp(, ) = tt if ∈ , otherwise ff ; - fp(♢ (), ) = tt and fp(□ ( ), ) = ff ; - fp(¬, ) = tt if ∈/ , otherwise ff ; - fp( 1 ∧ 2, ) = fp( 1, ) ∧ fp( 2, ); - fp( 1 ∨ 2, ) = fp( 1, ) ∨ fp( 2, ); - fp(∘ , ) = ∧ ♢ true, and fp(∙ ,

) = ∨ □ false; - fp( 1 ℛ Note that fp(, - fp( 1 2, ) = fp( 2, ) ∨ (fp( 1, ) ∧ fp(∘ ( 1 2), )); 2, ) = fp( 2, ) ∧ (fp( 1, ) ∨ fp(∙ ( 1 ℛ

2), )).

) is a positive Boolean formula on cl( ), i.e., fp(, following two propositions show that fp(, propositional behavior of ltl formulas.

) strictly follows ltl semantics and retains the ) ∈ ℬ +(cl( )). The fp(, ) be as above. Then , |= if , + 1 |= fp(, []).

Proposition 1 ([ 23 ]). Let be an ltl formula over in nnf, be a finite nonempty trace, Then fp(, ) ∼ fp(,

) holds.

Proposition 2 ([ 23 ]). Let and be two ltl formulas over in nnf s.t. ∼ , and ∈ 2 . |= if |= fp(, ).

We generalize ltl formula progression from single instants to finite traces by defining fp(, ) = , and fp(, ) = fp(fp(,

), ), where ∈ 2 and ∈ (2 )* .

Proposition 3 ([ 23 ]). Let be an ltl formula over in nnf, be a finite trace. We have that We take the definition of the remove-next function RmNext from [ 23 ], defined over propositionalized ltl formulas in xnf, : - RmNext(♢ ) = tt , RmNext(□ ) = ff - RmNext( 1 ∧ 2) = RmNext( 1) ∧ RmNext( 2) - RmNext( 1 ∨ 2) = RmNext( 1) ∨ RmNext( 2) - RmNext(∘ ) = ∧ ♢ true, RmNext(∙ ) = ∨ □ false. have the following proposition: Note that RmNext applies to neither -,ℛ- formulas, since they do not appear in xnf, nor literals (, ¬), as the input of the function is a propositionalized ltl formula in xnf form. We ⊤ if ∈ and ⊥ if ∈ ∖ .

RmNext(xnf( )| ), where xnf( ) | Proposition 4 ([ 23 ]). Given an ltl formula stands for substituting in xnf( ) the variable with in nnf, ∀ ∈ 2 , fp(, ) ≡ state space of the dfa. infinite sequence LTL Synthesis. Let be an ltl formula over = ∪ , and , are two disjoint sets of propositional variables controlled by the environment and the agent, respectively. The synthesis problem (, , ) consists in computing a strategy : (2 )* → 2 , such that for an arbitrary = (0 ∪ ( )), (1 ∪ (0)), . . . , ( ∪ (0, 1, . . . , − 1)). If such a strategy does not exist, then is unrealizable. ltl synthesis can be solved by reducing to an adversarial reachability game on the corresponding Deterministic Finite Automaton (dfa) [ 7 ]. Hence, a strategy can also be represented as a finite-state controller : ↦→ 2 , where denotes the = 0, 1, . . . ∈ (2 ), we can find ≥ 0 such that |= , where Forward ltl Synthesis. Two recent papers Algorithm 1 Forward ltl Synthesis [ 23 ] [ 22, 23 ] proposed a forward approach to solve 21:: funicftiIsoAncScyenptthinegs(is() t)hreenturn strategy the problem of ltl synthesis. Their implementa- 3: AddToStrategy(, true) Ttihonesidaerae icsatlloedb,urieldsptehcetidvfealyo,nLt-tlfhsey-nfly,awndhiCleynptehri-a. 546::: Ini:=trieaGtlueGrtnrGaGrpahept(hSRt)roaotte()gy() forming an adversarial forward search towards 7: found := Search(, ∅) the final states, by considering the dfa as a sort of 89:: irfetfuorunndEmthpetnySrtertuatrnegGy(e)t◁St raitseugyn(r)ealizable AND-OR graph [30]. Therefore, a winning strat- 10: function Search(, path) return True/False egy might be found before constructing the whole 11: if IsSuccessNode() then return True dfa. The state-of-the-art forward technique [ 23 ], 12: if IsFailureNode() then return False implemented in the tool Cynthia, is described by 1134:: if InTPaagtLho(op,(pa)trhe)tuthrnenF◁alsWee found a loop the pseudocode in Algorithm 1. The algorithm is 15: :=FormulaOfNode() basically a top-down, depth-first traversal of the 16: if IsAccepting( ) then AND-OR graph induced by the on-the-fly dfa con- 1187:: TAadgdSTuocSctersasNteogdye((,)true) struction, proceeding forward from the initial state 19: return True and excluding strategies that lead to loops. The 2210:: forf(or(,An,dNd))∈∈GGeettOArnAdrAcrsc(s()AdnodNd) do forward-based generation of the AND-OR graph 22: found :=Search(, [path|]) is based on formula progression and on the ab- 2234:: if foifun¬dfotuhnednthen Break stract functions GetOrArcs and GetAndArcs 25: TagSuccessNode() functions (Line 20 and Line 21, respectively) that, 26: AddToStrategy(, ) taken in input a search node , it produces the 2278:: if IsBTaacgkLPoroopp(())then next available actions and successor states. The 29: return True presence of loops must be carefully handled; when 3301:: rTeatguFranilFuarleseNode() a loop is detected at node , the procedure returns false, temporarily considering as a failure node. Note that node is not tagged as failure, since it is unknown whether all the or-arcs of are explored. If later during the search is discovered as a success node, such information must be propagated from backwards to the ancestor nodes of . 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, implemented in BackProp (Line 28), as illustrated in [31]. The main novelty of Cynthia over Ltlfsyn is that the GetOrArcs and GetAndArcs are based on a compilation of the current state formula in a Sentential Decision Diagram [ 24 ], which was used both for fast state-equivalence checking and for possibly avoiding the exponential enumeration of players’ moves. Indeed, the experimental evaluation of their technique is rather impressive, as its implementation Cynthia, outperformed other state-of-the-art tools on challenging benchmarks, e.g. on the Nim benchmark [32]. For more details on the search algorithm, please refer to the original paper [ 23 ]. 3. DPLL-based Forward ltl Synthesis Our aim is to propose a new approach that tries to overcome the above limitations that we consider crucial for a scalable approach. In the first place, we observe that Algorithm 1 can be seen as an abstract specification that depends on two crucial subprocedures: ( i) stateequivalence checking, denoted with EquivalenceCheck(1, 2), that checks whether the search nodes 1 and 2 can be considered equivalent w.r.t. the current AND-OR search graph; and (ii) search node expansion, denoted with GetAndArcs() (resp. GetOrArcs()), that returns an iterator of AND-arcs (resp. OR-arcs) of the AND-node (resp. OR-node) starting from node . The former is implicitly used, e.g. in the InPath function, while the latter functions are employed at Line 20 and Line 21. Note that this separation was not clearly stated in [ 23 ] and [ 22 ]; in particular, De Giacomo et al. referred to an Expand() function that both computes successors node of and finds a representation for such successors to be used for state equivalence checking. The high-level search algorithm being used is not diferent from the De Giacomo et al.’s one. However, this modular separation allows us to focus on each core component separately, possibly giving a computational advantage in the computation of the solution; later we will show that this is indeed the case. While in this paper we consider the same search algorithm of theirs (i.e. a standard depth-first AND-OR search), these arguments apply also to other AND-OR search algorithms, e.g. AO* [30]. Sometimes we will only refer to GetArcs if the procedure is similar both for GetOrArcs and GetAndArcs (although, in general, they might difer).

The crucial observation is that GetArcs() does not require that the arcs of search node have already been computed or, in other words, that the node has been fully expanded (as done by Expand function). As per specification, GetArcs() is an iterator over the available moves from . The concept of iterator is well-known in the computer science community as a way to decouple algorithms from containers [33]. More interestingly, a special case of iterators, generators [34], would allow to compute the next players’ moves iteratively “on-demand”, therefore allowing a depth-first search algorithm to visit the next arc returned by the generator even if all arcs have not been computed yet. We will use a generator-based implementation of DpllGetArcs in Algorithm 2.

In fact, De Giacomo et al.’s approach can be seen as a special case of the proposed framework, in which both EquivalenceCheck and GetArcs are implemented using SDDs: two search nodes are equivalent if they point to the same SDD node, and GetArcs is an iterator that simply scans the children of the root SDD node of . However, this framework can easily overcome the limiting factors mentioned earlier, namely: (i) computed moves do not have to be disjoint and covering (i.e. diferent moves that lead to the same successor are allowed, although preferably avoided); (ii) if GetArcs is implemented using a generator-like approach, the visit of a child node can happen far before the computation of all the available moves; and (iii) the two main search subtasks, state-equivalence checking and a search node expansion, are implemented by two potentially decoupled functions (EquivalenceCheck and GetArcs, respectively).

We exploit the above observations to design our new ltl synthesis algorithm. At the core of it, there is a novel search node expansion procedure, DpllGetArcs (Algorithm 2), inspired by the DPLL algorithm [35, 36]. Such a procedure is somehow in the middle between full enumeration (as Ltlfsyn) and optimal compilation (as Cynthia) of players’ moves. Unlike Cynthia, it selects an assignment of the relevant variables for the current state formula, hence returning a successor node without requiring the full SDD compilation, which is some cases might be prohibitive. However, unlike Ltlfsyn, the recursive nature of the procedure gives room to propositional formula simplification, which might drastically reduce the size of the action space (i.e. a smaller number of branching variables to be considered). As state equivalence checking procedures, we consider (i) BddEqCheck, which is based on Binary Decision Diagrams (BDD) [37], and (ii) SyntacticEqCheck, based on syntactic equivalence. Intuitively, the BddEqCheck compiles the state formula as Cynthia did using SDDs, but without requiring the variable decomposition for finding the next moves. The SyntacticEqCheck just compares the formulas structurally, which can be implemented very eficiently. A complete formalization of these components, as well as proof of correctness of the constructions, and how these are combined in a unified procedure, will be extensively discussed in the following sections.

4. BDD-based and Syntactic Equivalence Checks

In this section, we describe two equivalence checks that can be used for forward ltl synthesis. The first one is a knoweldge-compilation-based equivalence check, that uses BDDs to compile the state formula and achieve constant (propositional) equivalence checking. The second one is a simple and lightweight equivalence check that has never been used in this context and, as we shall see, turns out to be very useful in the experimental evaluation. However, we discuss implications regarding the completeness of the resulting synthesis procedure. BDD-based EquivalenceCheck. The BDD-based equivalence check is similar to the SDDbased equivalence check performed by Cynthia. That is, for a search node , we take its associated ltl formula with FormulaOfNode (remember that search node is associated with an ltl formula). Then, we compute xnf( ), which is propositionally equivalent to . xnf( ), by construction, is defined over the set of variables ∪ ∪ , where = ⋃︀ ∈cl( ){ | ∈ pa(xnf( )), not literal}. Finally, we get its BDD representation, i.e. := BddRepresentation(xnf( )). We do these operations both for search nodes 1 and 2, whose state formulas are 1 and 2 respectively, yielding xnf( 1) and xnf( 2). The equivalence check whether the two BDDs point to the same BDD node (xnf( 1) = xnf( 2)). If that is the case then it means, thanks to the canonicity property of BDDs, that the associated (propositionalized) formulas are propositionally equivalent.

Lemma 1. Let (, , ) be a ltl synthesis problem instance. The BddEqCheck procedure for such instance induces a search space for Algorithm 1 with no more than 22|(cl( ))| search nodes. Proof. Any ltl formula associated to some search node of Algorithm 1 is such that xnf( ) ∈ ℬ+( ∪ ∪ ). Since there are at most 2|∪ ∪| models, thanks to the canonicity property of BDDs, there can be at most 22|∪∪| propositionally equivalent formulas. Since ∪ ∪ = (cl( )), we get the claim.

We preferred the use of BDDs instead of SDDs since we do not need the decomposing feature of SDDs, and also because robust and optimized implementations for BDDs already exists, e.g. CUDD [38], with useful features such as dynamic variable reordering.

Syntactic EquivalenceCheck. We now consider an equivalence check procedure that is based on structural equivalence: two search nodes 1 and 2 are considered equivalent if their formulas 1 and 2 have the same syntax tree, i.e.: SyntacticEqCheck(1, 2) := FormulaOfNode(1) = FormulaOfNode(2). To make the comparison fast, we can use hash consing [39] which is a technique used to share values that are structurally equal. Using hash consing, two formulas can be stated as structurally equivalent if they point to the same memory address, achieving constant time equality check. Unfortunately, naïvely applying formula progression might give false negatives, as shown by the following result: Theorem 2. Algorithm 1 with SyntacticEqCheck for EquivalenceCheck is sound but not complete for ltl synthesis.

Proof. Soundness follows from the soundness of hash-consing based equivalence check. To disprove completeness, consider the synthesis problem with = □ ♢ , = {} and = {}. Let = {}, 0 = and = fp( − 1, ). It can be shown by induction on the following statement: for all ≥ 1, we have xnf( ) = ((( ∧ ♢ ) ∨ ∘ ♢ ) ∧ ♢ ) ∨ (xnf( − 1) ∧ ((( ∨ □ ) ∧ ∙ □ ) ∨ □ ) ∧ ♢ ). By correctness of fp, the set of formulas 0, 1. . . . are semantically equivalent but structurally diferent, ending up in a infinite loop, which is undetected by the SyntacticEqCheck.

At the core of the issue is that, by how the formula progression works, there are some cases in which a new structurally diferent formula can be always produced by some particular sequence of applications of formula progression rules, although propositionally equivalent formulas have been already produced earlier during the search. Nevertheless, such equivalence check is very computationally cheap and, as we shall see in the experimental section, often it performs better than the BDD-based equivalence check.

To guarantee the termination of this version of the search algorithm, we propose the following procedure: given a synthesis problem, first execute Algorithm 1 with SyntacticEqCheck as equivalence check and some search node expansion procedure. As soon as, during the execution, the size of the formula of any generated search node becomes greater than a given threshold , then abort the execution and resort to the search algorithm by using BddEqCheck as equivalence check. In other words, if the problem does not present the pathological corner case shown in the proof of Theorem 2, then try to solve it, without getting stuck with onerous BDD-based compilations.

Lemma 2. Algorithm 1 with SyntacticEqCheck for EquivalenceCheck with size formula threshold always terminates and is correct.

Proof. Correctness follows from [23, Theorem 5], whereas termination follows from considering that (i) the number of distinct state formulas of size at most is finite, and (ii) in case the threshold is hit, by the correctness of the BDD-based equivalence check (Lemma 1). Lemma 2 says that the threshold guarantees that only a finite number of structurally equivalent formulas can be computed. Empirically, we found that a good threshold that suitably postpones the detection of pathological instances is three times the size of the initial formula: = 3 · | |.

5. DPLL-based Search Node Expansion

In this section, we describe our main novel approach for search node expansion, that we argue is the key ingredient in achieving state-of-the-art performances for forward ltl synthesis, that allows to overcome some limitations of previous works discussed in previous sections. In particular, GetArcs is implemented using a DPLL-based procedure (Algorithm 2). We claim the DPLL-based GetArcs to be efective for solving ltl synthesis in a forward fashion, as also shown by the experimental evidence.

Algorithm 2 DPLL-based GetArcs The DPLL algorithm is a very famous 1: function DpllGetArcs() return [move, node] algorithm for deciding the satisfiability 2: ← xnf(FormulaOfNode()) of proposition logic formulas in conjunc3: ← {} ◁ propositional assignment tive normal form (CNF). Many variants of 45:: if IysOierlNdofdreo(m) DthpelnlGetOrArcs ( , ) it have been proposed that work for gen6: else eral non-clausal formulas [40, 41], moti7: yield from DpllGetAndArcs ( , ) vated by the fact that, quite often, con8: function DpllGetOrArcs(, ) version of a boolean formula to CNF is 9: ′ ← GetAgentVars() both unnecessary and undesirable, e.g. 111210::: if ℓ′ℓ← ̸ =←G∅RettehpBelrnaacnec(hi,nℓ)gLiteral() abnecdaudsueeotfolotshseowfsotrrsutc-ctuarsael einxfpoornmeanttioianl 13: yield from DpllGetOrArcs(ℓ, ∪ {ℓ}) blow-up of the size of the formula. We 14: ¬ℓ ← Replace(, ¬ℓ) agree with this view, and in the following 1165:: elseyield fr◁omNoDbpralnlGcheitnOgroAnracgse(nt¬vℓa,riabl∪es{a¬vaℓi}l)able we assume to deal with propositionalized 17: yield (, tf ) ◁ tf is the next AND node ltl formulas in non-clausal form. 18: function DpllGetAndArcs(, ) We are interested in designing a DPLL19: ′ ← GetEnvVars( ) like procedure to identify the next moves 20: if ′ ̸= ∅ then and successor nodes from a search node 222123::: ℓyiℓ←e← ldGRefrteopBlmraacnDec(ph,lℓilnGg)eLtiAtnerdaAlr(cs)( ℓ, ∪ ℓ) ri.thmO2u),rlikperoapnoysDedPLpLrporcoecdeudruere(,Arlugnos24: ¬ℓ ← Replace(, ¬ℓ) by choosing a literal, assigning a truth 25: yield from DpllGetAndArcs( ¬ℓ, ∪¬ℓ) value to it, simplifying the formula and 26: else ◁ No branching on environmentvariables available then recursively applying the same pro27: ′ ← RmNext( ) 28: yield (, ′) ◁ ′ is the next OR node cedure to the simplified formula, until there are no agent or environment variables to branch on. Both the computed set of assignments resulting from the sequence of recursive calls, (initialized at Line 3), and what remains of the formula = xnf(FormulaOfNode()) after the chosen literals have been replaced with their assigned truth value, are yielded such that they can be consumed by the caller function (see Line 17 and 28; the instruction yield allows a generator to provide a value to the caller).

Given a search node , DpllGetArcs returns a generator over pairs (move, node), where move is a mapping from variables to truth values (the absence of a variable is considered as don’t care), and node is a ltl formula that, as required by ours and De Giacomo et al.’s search framework, represents a search node (either AND or OR). Depending on whether is an OR-node or an AND-node, the DpllGetOrArcs function (Line 5) or the DpllGetAndArcs function (Line 7) is called, respectively. The DpllGetOrArcs function takes in input a propositionalization of , i.e. := , and the current variables’ assignment . If there is still some agent variable in to assign (Line 9), then we decide the next branching literal ℓ (by calling the function GetBranchingLiteral, Line 11), we substitute its truth value to the formula , and simplify it by calling the function Replace (Line 12), obtaining ℓ. Then, we do the recursive call to DpllGetOrArcs with the new propositionalized formula ℓ and updated assignment ∪ {ℓ}, and start generating the next moves with a fixed value for literal ℓ. Intuitively, this step represents a transition to another node of the search tree of a DPLL algorithm. The instruction yield from allows a generator to forward the generation of results to another generating function. When the generation terminates, the negated literal ¬ℓ is replaced to the original formula , yielding another propositionalized ltl formula ¬ℓ, and the available moves starting from this branch are generated. Intuitively, the last step represents the exploration of the opposite branch of the current node of the DPLL search tree, with the branching literal ℓ set at the opposite truth value ¬ℓ. Note that in the base case, we return the pair (, tf ), where contains all the chosen literals in the current final assignment, and tf is the ltl formula that represents the next AND node. The DpllGetAndArcs is analogous to DpllGetOrArcs but for AND nodes; therefore, it aims at finding an assignment of environmentvariables rather than of agent variables . Another diference with DpllGetAndArcs is that in the base case, we use the propositional formula (the result of the substitutions of chosen literals and the subsequent simplifications) to compute the next search node formula ′, using the function RmNext, at Line 27. Note that, at this stage, is a propositional formula over state variables only. By Proposition 4, since = xnf( )| , we have that ′ = RmNext( ) = fp(, ), i.e. the correct next state.

According to the needs of the search algorithm, the procedure can be run exhaustively, i.e. until all available moves from node have been produced. Still, the simplification step can possibly avoid a large part of the naive search space over and ; this is an improvement wrt the Ltlfsyn approach, which blindly enumerates all possible assignments. The simplification step recursively applies the usual propositional simplification rules, e.g. considering the absorbing or neutral boolean values of binary operators. We suggest to simplify the propositional formula to a great extent, but without resorting to any compilations. Instead, we leave the formula in non-clausal form, aiming at eliminating branching variables from the resulting formula. Such variables will be considered as don’t care in the current assignment.

We argue that such kind of procedures, like the one described in Algorithm 2, are suitable for our use-case because of their depth-first nature, which implies a low-space requirement, and because of their “responsive” nature: a candidate move is proposed in linear time in the number of variables (possibly better thanks to simplifications). It is interesting to observe that the full trace of a DPLL execution can be seen as a compilation of the propositional theory [42]. Note that Algorithm 2 is an abstract specification that can be customized by diferent realizations of GetBranchingLiteral and Replace.

Lemma 3. Let (, , ) be a ltl synthesis problem instance. DpllGetArcs correctly expands the search graph.

Proof sketch. By construction, both DpllGetOrArcs and DpllGetAndArcs are complete because they consider all possible agent’s and environment’s variable assignments (possibly avoiding exhaustive enumeration thanks to Replace’s simplifications). Moreover, when DpllGetOrArcs( ) reaches its base case, by definition of AND-OR graph of , (, tf ) is a valid transition from to AND node tf , while DpllGetOrArcs(tf ) returns (, ′), where ′ = RmNext(xnf( ) |) is the correct successor node by Proposition 4.

Theorem 3. Algorithm 1 with BddEqCheck for state-equivalence checking and Algorithm 2 for search node expansion is correct and always terminates.

Proof. Termination follows from Lemma 1 and Thm. 4 of [ 23 ]. Correctness follows from Lemma 1, 3, and Thm. 5 of [ 23 ].

Theorem 4. Algorithm 1 with SyntacticEqCheck and formula size threshold for stateequivalence checking and Algorithm 2 for search node expansion is correct and always terminates. Proof. Termination follows from Lemma 2 and Thm. 4 of [ 23 ]. Correctness follows from Lemma 2, 3, and Thm. 5 of [ 23 ].

6. Implementation and Experiments

We implemented the presented synthesis methods in a tool called Nike, which resulted the winner in the ltl Realizability Track of SYNTCOMP 2023. Nike is an open-source tool implemented in C++11. It uses Syfco to parse the synthesis problems described in TLSF format [43] to obtain the ltl specification and the partition of agent/environment propositions. Nike integrates the preprocessing techniques presented in [ 22 ] to perform one-step realizability/unrealizability checks, which is implemented using the BDD library CUDD [38], at the beginning of the synthesis procedure. If neither one-step check succeeds, the AND-OR search begins. Since the procedure is correct and terminates, either the search procedure does not find a winning strategy, in which case the answer to the ltl synthesis problem is “unrealizable”, or a winning strategy is found, and therefore the outcome is “realizable”. We use n-ary trees with hash-consing for representing the ltl formulas and performing the hash-based state-equivalence checking. The CUDD library is used for the BDD-based state-equivalence checking. Nike, as Cynthia and Ltlfsyn, applies some optimizations to speed up the synthesis procedure. First, when visiting an OR-node for the first time, we perform the pre-processing techniques described in [ 22 ]. More specifically, we check: ( i) there exists a one-step strategy that reaches accepting states from , then 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 , then is tagged as failure. Nike can run in two modes: using BDD-based state-equivalence checking (BDD), and hash-consing-based state-equivalence checking (Hash). In the DPLL-based search node expansion, we considered variables in alphabetical order, and we combined them with three simple branching strategies: True-first (TF) that first sets variables to true, False-first (FF) that first sets variables to false; and Random (Rand) that sets variables at random. This yields six combinations of Nike that we included in these experiments. We also include a parallel version of Nike, Nike-P, that runs in Hash mode all the three branching strategies in parallel.

Experimental Methodology. We evaluated the eficiency of all variants of Nike, by comparing against the following tools: Lisa [ 9 ] and Lydia [ 8 ] are state-of-the-art backward ltl synthesis approaches. Both tools compute the complete dfa first, and then solve an adversarial reachability game following the symbolic backward computation technique described in [44]. We excluded Ltlfsyn from the comparison since it was already superseded by Cynthia.

Experiment Setup. Experiments were run on a VM instance on Google Cloud, type c2-standard-4, endowed with Intel(R) Xeon(R) CPU 3.10GHz, 4 logical CPU threads, 16 GB of memory and 300 seconds of time limit. The correctness of Nike was empirically verified by comparing the results with those from all baseline tools. No inconsistency was found. Nike-Hash-TF Nike-Hash-FF

Nike-Hash-Rand 300 Nike-BDD-TF

Nike-BDD-FF Nike-BDD-Rand Nike-P Lydia

Cynthia Lisa-exp Lisa-sym

Lisa 250 s)d200 econ ts(150 eou iTm100 50 0 0 200 400 600 800 1000 1200 1400

Number of solved instances (c) Random. 102 s) 101 ond 100 ssceco t(10− 1 ieTm1100−− 23 10− 4

Nike-Hash-TF Nike-Hash-FF Nike-Hash-Rand Nike-BDD-TF

Nike-BDD-FF Nike-BDD-Rand Nike-P Cynthia

Lydia Lisa-sym Lisa-exp Lisa

Benchmarks. We collected 1494 ltl synthesis instances from literature: 20 unrealizable pattern and 20 realizable -pattern instances, of the form () = □ (1) ∧ ♢ (2) ∧ · · · ∧ ♢ ) and () = 1 (2 (. . . − 1 )), respectively [45, 46]; 54 Two-player-Games instances [ 47, 9 ]: Single-Counter, where the agent stores an -bit counter (where is the scaling parameter) which it must increment upon a signal by the environment. The agent wins if the counter eventually overflows to 0; Double-Counter is similar to the Single-Counter one, except that in this case there are two -bit counters, one incremented by the environment and another by the agent. The goal of the agent is for its counter to eventually catch up with the environment’s counter; and Nim is a generalized version of the game of Nim with heaps of tokens each [32]. Finally, we considered 1400 Random instances, of which 400 are from [44] and 1000 from [ 8 ], constructed from ltl synthesis datasets Lily and Load Balancer [48].

Analysis. Figure 1a shows the running time of each tool on every instance of the GF-pattern dataset. Across these instances, we can observe that all variants of Nike solve instances very quickly, thanks to the pre-processing techniques. This is done with much less time comparing to backward approaches, represented by Lisa and Lydia, simply because these tools do not have such optimizations. Cynthia solved it in less time, but we attribute this to the set up time of the CUDD BDD manager that worsens the performances. Nevertheless, this amounts to a negligible time cost diference of ≪ 1 second. Results are similar for the U-pattern dataset, shown in the supplementary material. On the Two-player-Games benchmarks, see Figure 1b, we observe that Nike variants dominate all other tools on the Double-Counter instances, while competing with backward approaches on the other instances. On Nim, Cynthia is the best performing tool, but on the other benchmarks Nike shows to be better. The Nike-BDD combinations performs slightly worse on Double Counter than the Nike-Hash combinations. On the Random benchmarks, all variants of Nike, except the ones using Rand, are competitive with state-of-the-art backward approaches, and far better than Cynthia.

It is clear from the plots that Nike, in general, shows an overall better performance than Cynthia, illustrating the eficiency and better scalability of our approach. In particular, there is a notable outperformance of Cynthia on the Double-Counter and in the Random instances. We attribute this to the ability of Nike to not be stuck with compilation processes that can easily become intractable, both on hand-designed datasets like Double-Counter, and in randomly generated intractable cases. On the Nim benchmark, our tool does not perform as good as the others, but its performance are still competitive, especially in the variant Nike-BDD-FF. This is because the Nim formulas were manageable enough for SDD compilation (Cynthia) and for DFA construction (Lydia/Lisa), whereas the blind branching strategies of Nike were not efective in this case, as most of the time is spent on generating successors that have been already visited. The worse performance of the Rand branching strategy on the Random benchmark can be explained by the fact that the TF and the FF strategies might exploit a particular problem structure of these instances, that allow to easily arrive at success nodes or failure nodes, and frees the algorithm to explore more moves thanks to the short-circuit evaluation of the search outcome (see Lines 23 and 24 in Algorithm 1). The best configuration is Nike-BDD-FF, which suggests that for this benchmark the state compilation is not too hard and the canonicity of the representation helps to prevent the revisit of propositionally-equivalent states.

Overall, despite the simplicity of the DPLL-based expansion, performances are very surprising with respect to backward approaches; this suggests that our approach is very promising and worth of future research.

7. Conclusions

We proposed the best forward search ltl synthesis approach so far, and the first that is truly competitive with the considered state-of-the-art tools based on backward computation (as in the Random benchmark). Our implementation ranked first in the ltl Realizability Track of the 2023 edition of SYNTCOMP. We think this work sets the foundations for a new family of ltl synthesis algorithms, and opens several research avenues for investigating efective branching heuristics [49] for the DPLL-based search graph expansion, e.g. non-chronological backtracking, better order in which branching variables are chosen [50], or better termination strategies for searching with syntactic state-equivalence checking.

Acknowledgements

This line of research has started from earlier research work supported by the ERC-ADG WhiteMech (No. 834228). checking, in: AAAI, 2019. [28] E. A. Emerson, Temporal and modal logic, in: Handbook of Theoretical Computer Science, 1990. [29] F. Bacchus, F. Kabanza, Planning for temporally extended goals, Ann. Math. Artif. Intell.

22 (1998). [30] N. J. Nilsson, Problem-solving methods in artificial intelligence, 1971. [31] M. G. Scutellà, A note on dowling and gallier’s top-down algorithm for propositional horn satisfiability, J. Log. Program. 8 (1990) 265–273. [32] C. L. Bouton, Nim, a game with a complete mathematical theory, Annals of Mathematics 3 (1901). [33] E. Gamma, R. Johnson, R. Helm, R. E. Johnson, J. Vlissides, Design patterns: elements of reusable object-oriented software, Pearson Deutschland GmbH, 1995. [34] S. Murer, S. Omohundro, D. Stoutamire, C. Szyperski, Iteration abstraction in sather, ACM

Transactions on Programming Languages and Systems (TOPLAS) 18 (1996) 1–15. [35] M. Davis, H. Putnam, A computing procedure for quantification theory, J. ACM 7 (1960). [36] M. Davis, G. Logemann, D. W. Loveland, A machine program for theorem-proving,

Commun. ACM 5 (1962). [37] R. E. Bryant, Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams,

ACM Comput. Surv. 24 (1992). [38] F. Somenzi, CUDD: CU Decision Diagram Package. Univ. of Colorado at Boulder (2016). [39] L. P. Deutsch, An interactive program verifier (1973). [40] C. Thifault, F. Bacchus, T. Walsh, Solving non-clausal formulas with DPLL search, in:

SAT, 2004. [41] H. Jain, E. M. Clarke, Eficient SAT solving for non-clausal formulas using dpll, graphs, and watched cuts, in: DAC, ACM, 2009, pp. 563–568. [42] J. Huang, A. Darwiche, The language of search, J. Artif. Intell. Res. 29 (2007) 191–219. [43] S. Jacobs, G. A. Perez, P. Schlehuber-Caissier, The temporal logic synthesis format tlsf v1.2, 2023. arXiv:2303.03839. [44] S. Zhu, L. M. Tabajara, J. Li, G. Pu, M. Y. Vardi, A Symbolic Approach to Safety LTL

Synthesis, in: HVC, 2017. [45] K. Y. Rozier, M. Y. Vardi, LTL satisfiability checking, in: SPIN, volume 4595 of Lecture

Notes in Computer Science, Springer, 2007, pp. 149–167. [46] J. Geldenhuys, H. Hansen, Larger automata and less work for LTL model checking, in:

SPIN, volume 3925 of Lecture Notes in Computer Science, Springer, 2006, pp. 53–70. [47] L. M. Tabajara, M. Y. Vardi, Partitioning Techniques in LTL Synthesis, in: IJCAI, 2019. [48] R. Ehlers, Unbeast: Symbolic bounded synthesis, in: TACAS, volume 6605 of Lecture Notes in Computer Science, Springer, 2011, pp. 272–275. [49] J. P. M. Silva, The impact of branching heuristics in propositional satisfiability algorithms, in: EPIA, volume 1695 of Lecture Notes in Computer Science, Springer, 1999, pp. 62–74. [50] P. Liberatore, On the complexity of choosing the branching literal in dpll, Artificial intelligence 116 (2000) 315–326.

References

[1] R. De Benedictis , N. Gatti , M. Maratea , A. Murano , E. Scala , L. Serafini , I. Serina , E. Tosello , A. Umbrico , M. Vallati , Preface to the Italian Workshop on Planning and Scheduling , RCRA Workshop on Experimental evaluation of algorithms for solving problems with combinatorial explosion, and SPIRIT Workshop on Strategies, Prediction, Interaction, and Reasoning in Italy (IPS-RCRA-SPIRIT 2023 ), in: Proceedings of the Italian Workshop on Planning and Scheduling , RCRA Workshop on Experimental evaluation of algorithms for solving problems with combinatorial explosion, and SPIRIT Workshop on Strategies, Prediction, Interaction, and Reasoning in Italy (IPS-RCRA-SPIRIT 2023) co-located with 22th International Conference of the Italian Association for Artificial Intelligence (AI*IA 2023 ), 2023 .

[2] A. Church , Application of recursive arithmetic to the problem of circuit synthesis , Journal of Symbolic Logic 28 ( 1963 ).

[3] A. Pnueli , The temporal logic of programs , in: FOCS, 1977 .

[4] A. Pnueli , R. Rosner , On the Synthesis of a Reactive Module , in: POPL, 1989 .

[5] C. Baier , J. Katoen , Principles of model checking, 2008 .

[6] G. De Giacomo , M. Y. Vardi , Linear Temporal Logic and Linear Dynamic Logic on Finite Traces , in: IJCAI, 2013 .

[7] G. De Giacomo , M. Y. Vardi , Synthesis for LTL and LDL on Finite Traces , in: IJCAI, 2015 .

[8] G. De Giacomo , M. Favorito , Compositional approach to translate LTL /LDL into deterministic finite automata , in: ICAPS , 2021 .

[9] S. Bansal , Y. Li , L. M. Tabajara , M. Y. Vardi , Hybrid compositional reasoning for reactive synthesis from finite-horizon specifications , in: AAAI , 2020 .

[10] M. Ghallab , D. S. Nau , P. Traverso, Automated planning - theory and practice , 2004 .

[11] H. Gefner , B. Bonet , A Concise Introduction to Models and Methods for Automated Planning , 2013 .

[12] A. Cimatti , M. Roveri , P. Traverso , Strong planning in non-deterministic domains via model checking , in: AIPS , 1998 .

[13] A. Cimatti , M. Pistore , M. Roveri , P. Traverso , Weak, strong, and strong cyclic planning via symbolic model checking . 1- 2 ( 2003 ).

[14] J. H. Reif , The complexity of two-player games of incomplete information , JCSS 29 ( 1984 ).

[15] R. P. Goldman , M. S. Boddy , Expressive planning and explicit knowledge , in: AIPS , 1996 .

[16] P. Bertoli , A. Cimatti , M. Roveri , P. Traverso , Strong planning under partial observability , Artif. Intell . 170 ( 2006 ).

[17] P. Haslum , N. Lipovetzky , D. Magazzeni , C. Muise , An Introduction to the Planning Domain Definition Language , 2019 .

[18] J. Rintanen , Complexity of planning with partial observability , in: ICAPS , 2004 .

[19] A. Camacho , J. A. Baier , C. J. Muise , S. A. McIlraith , Finite LTL Synthesis as Planning , in: ICAPS, 2018 .

[20] A. Camacho , S. A. McIlraith , Strong fully observable non-deterministic planning with LTL and LTL goals , in: IJCAI, 2019 .

[21] S. Thanh To , E. Pontelli, T. Cao Son , A conformant planner with explicit disjunctive representation of belief states , in: ICAPS , 2009 .

[22] S. Xiao , J. Li , S. Zhu , Y. Shi , G. Pu , M. Y. Vardi , On-the-fly synthesis for LTL over finite traces , in: AAAI , 2021 .

[23] G. De Giacomo , M. Favorito , J. Li , M. Y. Vardi , S. Xiao , S. Zhu , Ltlf synthesis as AND-OR graph search: Knowledge compilation at work , in: IJCAI , 2022 .

[24] A. Darwiche , SDD: A new canonical representation of propositional knowledge bases , in: IJCAI , 2011 .

[25] M. Favorito , Forward ltlf synthesis: Dpll at work, 2023 . arXiv: 2302 . 13825 .

[26] R. I. Brafman , G. De Giacomo , F. Patrizi , LTL /LDL non-markovian rewards , in: AAAI , 2018 .

[27] J. Li , K. Y. Rozier , G. Pu, Y. Zhang , M. Y. Vardi, Sat-based explicit LTL satisfiability