1. Introduction
Program synthesis is the task of finding a program that provably satisfies a given high-level
formal specification [
1
]. A commonly used logic for program synthesis is Linear Temporal Logic
(ltl) [
2, 3
], typically used also in model checking [
4
]. ltl on finite traces (ltl ) [
5
], a variant of
ltl to specify finite -horizon temporal properties, has been recently proposed as specification
language for temporal synthesis [
6
]. 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.
Stateof-the-art tools such as Lydia [
7
] and Lisa [
8
] 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) [
9, 10, 11, 12
], 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 [
13, 14, 15
]. However, techniques developed for such problems cannot be applied to
ours directly, which may result in a PDDL specification with exponential size e.g. see [
16, 17
].
For these reasons, researchers have been looking into forward search techniques specifically
conceived for solving ltl synthesis, considering the DFA game as an AND-OR graph search.
Two notable attempts in this direction have been presented in [
18
], proposing the tool Ltlfsyn,
and [
19
] with the tool Cynthia. Our work builds on top of them, by improving certain design
and implementation details, especially regarding the state-equivalence checking and the search
node expansion components, together with a Binary Decision Diagram (BDD)-based check
to achieve completeness when certain conditions are met. Nike uses a computationally-cheap
syntactical equivalence between state formulas, not used in previous works. Furthermore, a
novel search graph expansion technique is proposed, based on a procedure inspired by the
famous Davis-Putnam-Logemann-Loveland (DPLL) algorithm. As in [
18, 19
], the problem is
then reduced to an AND-OR graph search, where the OR nodes represent the agent’s choices,
and the AND nodes represent the environment’s choices. The search algorithm used is a classical
depth-first AND-OR graph search algorithm. The ltl synthesis problem is realizable if there
is a winning strategy for the corresponding AND-OR graph. More details can befound in [
20
].
2. DPLL-based Forward ltl Synthesis
The Search Algorithm. Algorithm 1 describes the AND-OR search procedure that is at
the core of Nike. The algorithm is basically a top-down, depth-first traversal of the AND-OR
graph induced by the on-the-fly dfa construction, proceeding forward from the initial state,
and excluding strategies that lead to loops. The forward-based generation of the AND-OR
graph is based on formula progression and on an abstract GetArcs function that, taken in
input a search node , it produces the next available player moves and successor states. The
presence of loops must be carefully handled; when 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 [
21
]. For more details on the search algorithm, please refer
to the original paper [
19
]. Overall, Algorithm 1 is very similar to the one used by [
19
], except that
instead of relying on the abstract Expand function (see Line 20 of Algorithm 1 of their paper),
our approach relies on two primitive operations: state-equivalence checking and search node
expansion. The state-equivalence check is used to check state equivalence, and it is implicitly
used in functions like InPath to detect loops. The search-node expansion is represented by
the generating function GetArcs and does not have to precompute all successors (Cynthia), or
slavishly enumerating all possible agent’s and env’s variables assignments (Ltlfsyn).
Algorithm 1 Forward ltl Synthesis State-Equivalence Checks. We now describe
1: function Synthesis( ) return strategy two state-equivalence checking approaches:
BDD2: if IsAccepting( ) then based and hash-consing based. The first one
34:: rAedtduTrnoSGtertaSttergayt(,egyt(r)ue) (BddBasedEqCheck) is that, for a search node ,
5: InitialGraph( ) we take its associated ltl formula with
For6: := GetGraphRoot() mulaOfNode (remember that search node is
as87:: iffoufonudn:d=tSheeanrrceht(ur,n∅)GetStrategy() sociated with an ltl formula). Then, we
com9: return EmptyStrategy() ◁ is unrealizable pute xnf( ), which is propositionally equivalent
10: function Search(, path) return True/False to . Finally, we get its BDD representation, i.e.
1112:: iiff IIssSFauiclcuersesNNooddee(()) tthheenn rreettuurrnn TFarulsee :=BddRepresentation(xnf( )). We do these
13: if InPath(, path) then ◁ We found a loop operations both for 1 and 2, yielding xnf( 1)
14: TagLoop() return False and xnf( 2). The equivalence check whether the
1156:: if I:=sAFcocremputilnagO(fN)othdee(n) two BDDs point to the same BDD node (xnf( 1)=
17: TagSuccessNode() xnf( 2)). If true, then it means, by the canonicity
18: AddToStrategy(, true) property of BDDs, that the associated
(proposition1290:: forr(etur,nATnrduNed) ∈GetArcs() do alized) formulas are propositionally equivalent.
21: for (, ) ∈GetArcs(AndNd) do The second check (HashConsingEqCheck) is
2223:: iffou¬nfdou:=ndSetahrecnhB(reak, [path|]) based on structural equivalence: two search nodes 1
24: if found then and 2 are considered equivalent if their formulas
222567::: iTAfadIgdsSTTuaocgScLteorsoasNtp(eogd)yet((h,e)n ) co1mapnadriso2nhfaavste, wtheecsaanmuesesyhnastahxcotnresein.Tgo[2m2a]kwehtihche
28: BackProp() is a technique used to share values that are
struc3209:: TagFairleutruerNnoTdreu(e) turally equal. Using hash consing, two formulas can
31: return False be stated as structurally equivalent if they point to
the same memory address, achieving constant time
equality check. Since this equivalence check is sound but not complete, 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 HashConsingEqCheck as equivalence check
and the search node expansion procedure (DpllGetArcs, see below). 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 Algorithm 1 based on
BddBasedEqCheck and DpllGetArcs. Currently, we use a threshold = 3 · | |.
DPLL-based Search Node Expansion. Given a search node , our expansion node function
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 a don’t care), and node is a
ltl formula that, as required by ours and [
19
] search framework, represents a search node
(either AND or OR). Informally, an agent/environment move is found by picking a variable,
assigning a boolean value, and replacing the value to the state formula. The resulting formula
is processed again until there are no agent/environment variables. The overall assignment is
considered as the next move to explore, and the successor state is computed by applying formula
progression rules (See the function RmNext and Proposition 4 of [
20
]). Note that such kind
of procedure is 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 on the number of variables (possibly better thanks to simplifications). Note that
DpllGetArcs abstract specification that can be customized by the way variables are chosen
and by which value is assigned to them first. In our tool, we consider them in alphabetical
order (as future work we aim to provide less naive and more meaningful orderings), and the
assignments strategies are three: True-First (i.e. the rfist assigment considered is always true),
False-First (i.e. the first assigment considered is always false), and random (i.e. the assignment
considered is random). Due to lack of space, we underspecified some details in the description
of the theory behind the tool, which can be found in [
20
].