Synthesis for LTL and LDL on Finite Traces

1 Introduction

LTLf , Linear Temporal Logic on finite traces, has been extensively used in AI an CS, see [De Giacomo and Vardi, 2013] for a survey. For example, it is at the base of trajectory constraints in PDDL 3.0 [Bacchus and Kabanza, 2000; Gerevini et al., 2009], the de-facto standard formalism for representing planning problems. Also LTLf is used as a declarative formalism to specify (terminating) services and processes by the business process modeling community [Pesic and van der Aalst, 2006; Montali et al., 2010; Sun et al., 2012; De Giacomo et al., 2014].

In this paper we study synthesis from specifications expressed in LTLf and its extension LDLf , Linear Dynamic Logic over finite traces, that allows for regular expressions in the temporal operators [De Giacomo and Vardi, 2013]. We consider propositions partitioned into two sets: the first under the control of our agent and the second not (e.g., variables in the second set are controlled by the environment). The specification consists of an LTLf /LDLf formula (or finite set of formulas), which expresses how both kinds of propositions should evolve over time. The problem of interest is checking whether there are strategies to set the controllable propositions over time so that, in spite of the values assumed by the uncontrollable ones, the specification is fulfilled. If such strategies exist, it is of interest to compute one.

Notice that conditional planning with full observability is indeed a special case of such a problem. Consider a non- Moshe Y. Vardi Rice University, Houston, TX, USA

vardi@cs.rice.edu

deterministic domain with a given initial state and reachability goal. It is easy to encode actions as propositions and then express the nondeterministic domain as a finite set of simple LTLf formulas, the initial state as a propositional formula, and the reachability goal φ as the LTLf formula ♦φ. Here, the controllable propositions are the actions, while the uncontrollable ones are all the others, which we may call fluents. Then, planning amounts to solving a special case of the LTLf synthesis problem. Interestingly, if we add temporal constraints (also specifiable in LTLf ) to be satisfied while reaching the goal [Gerevini et al., 2009], we still get a special case of the LTLf synthesis problem, as we do if we consider temporally extended goals [Bacchus and Kabanza, 1996], instead of reachability goals (as long as we require eventual termination). If we consider procedural execution constrains as in [Fritz and McIlraith, 2007; Baier et al., 2008], which are typically expressible as regular expressions that must be fulfilled by traces, we can resort to LDLf (LTLf is not expressive enough in this case) and planning becomes a special form of the LDLf synthesis problem studied here.

Technically, our synthesis problem relates to the classical Church realizability problem [Church, 1963; Vardi, 1996] and it has been thoroughly investigated in the infinite setting, starting from [Pnueli and Rosner, 1989]. Unfortunately, while theoretically well investigated, algorithmically it still appears to be prohibitive in the infinite setting, not so much due to the high complexity of the problem, which is 2EXPTIMEcomplete, but for the difficulties of finding good algorithms for automata determinization, a crucial step in the solution, see, e.g., [Fogarty et al., 2013].

In the finite setting, the difficulties of determinization disappear and hence a theoretical solution to this problem, as the one provided here, actually promises to be appealing for effective practical implementation.

Specifically, we present a general sound and complete solution technique for the synthesis based on DFA (reachability) games. These are games played over a deterministic automaton whose alphabet is formed by possible propositional interpretations. These games can be solved in linear time in the number of states of the automaton. We show how to transform an LTLf or LDLf specification first into an NFA (on possible propositional interpretations), and then, through determinization, into a DFA on which to play the DFA game.

The presented technique is double exponential in general but optimal, since it can be shown that the problem itself is 2EXPTIME-complete. Notice that in some cases, e.g., in the conditional planning setting, the determinization step is not required and hence our technique becomes single exponential, which is the complexity of conditional planning with full observability [Rintanen, 2004].

2 LTLf and LDLf

In this paper, we adopt standard LTL and its variant LDL interpreted on finite traces. For lack of space, as our main reference we use [De Giacomo and Vardi, 2013], which, apart from introducing LDL on finite traces, surveys the main known results and techniques in the finite traces setting.

Liner Temporal Logic on finite traces (LTLf ). LTL on finite traces, or LTLf , has essentially the same syntax as LTL on infinite traces [Pnueli, 1977], namely, given a set of P of propositional symbols, LTLf formulas are obtained as fol-

where φ is a propositional formula over P, ◦ is the next operator, · is weak next, i.e., ·ϕ is an abbreviation for ¬◦¬ϕ1 , ♦ is eventually, □ is always, and U is until. We make use of the standard boolean abbreviations, including true and false. The semantics of LTLf is given in terms of finite traces, i.e., finite words π, denoting a finite nonempty sequence of consecutive steps, over the alphabet of 2P , consisting of possible interpretations of the propositional symbols in P. We denote by length(π) the length of the trace, and by π(i), with 1 ≤ i ≤ length(π), the propositional interpretation at the i-th position in the trace. Given a finite trace π, we inductively define when an LTLf formula ϕ is true at a step i with 1 ≤ i ≤ length(π), written π, i |= ϕ, as follows:

• π, i |= φ iff π(i) |= φ (φ propositional);
• π, i |= ¬ϕ iff π, i ̸|= ϕ;
• π, i |= ϕ1 ∧ϕ2 iff π, i |= ϕ1 and π, i |= ϕ2;
• π, i |= ϕ1 ∨ϕ2 iff π, i |= ϕ1 or π, i |= ϕ2;
• π, i |= ◦ϕ iff i < length(π) and π, i+1 |= ϕ;
• π, i |= ·ϕ iff i < length(π) implies π, i+1 |= ϕ;
• π, i |= ♦ϕ iff for some j s.t. i ≤ j ≤ length(π), we have π, j |= ϕ;
• π, i |= □ϕ iff for all j s.t. i ≤ j ≤ length(π), we have π, j |= ϕ;
• π, i |= ϕ1 U ϕ2 iff for some j s.t. i ≤ j ≤ length(π), we have π, j |= ϕ2, and for all k s.t. i ≤ k < j, we have π, k |= ϕ1.

Notice that we have the usual boolean equivalences such as ϕ1 ∨ ϕ2 ≡ ¬ϕ1 ∧ ¬ϕ2; furthermore we have that ·ϕ ≡ ¬◦¬ϕ, ♦ϕ ≡ true U ϕ, and □ϕ ≡ ¬♦¬ϕ. It is known that LTLf is as expressive as First Order Logic over finite traces and star-free regular expressions, so strictly less expressive than regular expressions, which in turn are as expressive as Monadic Second Order logic over finite traces. On the other hand, regular expressions are a too low level formalism for expressing temporal specifications, since, for example, they miss a direct construct for negation and for conjunction, see, e.g., [De Giacomo and Vardi, 2013].

1 In LTLf , unlike LTL on infinite traces, ¬◦¬ϕ ̸≡ ◦ϕ.

Linear Dynamic Logic on finite traces (LDLf ). Linear Dynamic Logic on finite traces, or LDLf is as natural as LTLf , but with the full expressive power of Monadic Second Order logic over finite traces [De Giacomo and Vardi, 2013]. LDLf is obtained by merging LTLf with regular expressions through the syntax of the well-known logic of programs PDL, Propositional Dynamic Logic [Fischer and Ladner, 1979; Harel et al., 2000], but adopting a semantics based on finite traces. This logic is an adaptation of LDL interpreted over infinite traces, introduced in [Vardi, 2011].

Formally, LDLf formulas are built as follows:

where φ is a propositional formula over P; ρ denotes path expressions, which are regular expressions over propositional formulas φ with the addition of the test construct ϕ? typical of PDL; and ϕ stands for LDLf formulas built by applying boolean connectives and the modal connectives 〈ρ〉ϕ and [ρ]ϕ. In fact [ρ]ϕ ≡ ¬〈ρ〉¬ϕ.

Intuitively, 〈ρ〉ϕ states that, from the current step in the trace, there exists an execution satisfying the regular expression ρ such that its last step satisfies ϕ, while [ρ]ϕ states that, from the current step, all executions satisfying the regular expression ρ are such that their last step satisfies ϕ. Tests are used to insert into the execution path checks for satisfaction of additional LDLf formulas.

As for LTLf , the semantics of LDLf is given in terms of finite traces, i.e., finite words, denoting a finite, nonempty, sequence of consecutive steps π over the alphabet of 2P . As above, we use the notation length(π) and π(i), and in addition we denote by π(i, j) the segment of the trace π starting at the i-th step end ending at the j-th step. If j > length(π), we get the segment from i-th step to the end.

The semantics of LDLf is defined by simultaneous induction on formulas and path expressions as follows: given a finite trace π, an LDLf formula ϕ is true at a step i, with 1 ≤ i ≤ length(π), in symbols π, i |= ϕ, if:

• π, i |= φ iff π(i) |= φ (φ propositional);
• π, i |= ¬ϕ iff π, i ̸|= ϕ;
• π, i |= ϕ1 ∧ϕ2 iff π, i |= ϕ1 and π, i |= ϕ2;
• π, i |= ϕ1 ∨ϕ2 iff π, i |= ϕ1 or π, i |= ϕ2;
• π, i |= 〈ρ〉ϕ iff there exists j ≥ i such that π(i, j) ∈ L(ρ) and π, j |= ϕ;
• π, i |= [ρ]ϕ iff for all j ≥ i such that π(i, j) ∈ L(ρ), we have π, j |= ϕ;

where the relation π(i, j) ∈ L(ρ) is as follows:

• π(i, j) ∈ L(φ) if j = i + 1, j ≤ length(π), and π, i |= φ (φ propositional);
• π(i, j) ∈ L(ϕ?) if j = i and π, i |= ϕ;
• π(i, j) ∈ L(ρ1 + ρ2) if π(i, j) ∈ L(ρ1) or π(i, j) ∈ L(ρ2);
• π(i, j) ∈ L(ρ1; ρ2) if there exists k, with i ≤ k ≤ j, such that π(i, k) ∈ L(ρ1) and π(k, j) ∈ L(ρ2);
• π(i, j) ∈ L(ρ∗ ) if j = i or there exists k, with i ≤ k ≤ j, such that π(i, k) ∈ L(ρ) and π(k, j) ∈ L(ρ∗ ).

Notice that we have the usual boolean equivalences, and in addition [ρ]ϕ ≡ ¬〈ρ〉¬ϕ. We use the abbreviation last, standing for [true]false, to denote the last step of the trace.

It is easy to encode LTLf into LDLf : it suffices to observe that we can express the various LTLf operators by recursively applying the following translations:

• ◦ϕ translates to 〈true〉ϕ;
• ·ϕ translates to ¬〈true〉¬ϕ = [true]ϕ;
• ♦ϕ translates to 〈true ∗ 〉ϕ;
• □ϕ translates to [true ∗ ]ϕ;
• ϕ1 U ϕ2 translates to 〈(ϕ1?; true)∗ 〉ϕ2.

It is also easy to encode into LDLf regular expressions, used as a specification formalism for traces. Assuming all traces end with a special making symbol end (i.e., the last element of the trace is not part of regular expressions), a regular expression specification ρ translates to 〈ρ〉(last ∧ end).

We say that a trace satisfies an LTLf /LDLf formula ϕ, written π |= ϕ, if π, 1 |= ϕ. Also sometimes we denote by L(ϕ) the set of traces that satisfy ϕ: L(ϕ) = {π | π |= ϕ}.

3 LDLf Automata

We can associate with each LDLf formula ϕ an (exponential) NFA Aϕ that accepts exactly the traces that make ϕ true. Here, we provide a simple direct algorithm for computing the NFA corresponding to an LDLf formula. The correctness of the algorithm is based on the fact that (i) we can associate each LDLf formula ϕ with a polynomial alternating automaton on words (AFW) Aϕ that accepts exactly the traces that make ϕ true, and (ii) every AFW can be transformed into an NFA, see, e.g., [De Giacomo and Vardi, 2013]. However, to formulate the algorithm, we do not need these notions, but we can work directly on the LDLf formula. In order to proceed, we put LDLf formulas ϕ in negation normal form nnf (ϕ) by exploiting equivalences and pushing negation inside as much as possible, until negation signs are eliminated except in front of propositional formulas. Note that computing nnf (ϕ) can be done in linear time. Then, we define an auxiliary function δ (which corresponds directly to the transition function of the AFW Aϕ) that takes an LDLf formula ψ in negation normal form and a propositional interpretation Π for P, including explicitly a special proposition last to denote the last element of the trace, and returns a positive boolean formula whose atoms are subformulas of ψ:

Using the auxiliary function δ, we can build the NFA Aϕ of an LDLf formula ϕ in a forward fashion according to the following algorithm:

In the algorithm LDLf2NFA, states S of Aϕ are sets of atoms, where each atom consists of quoted subformulas of ϕ. Such sets of atoms are interpreted as conjunctions and in particular ∅, i.e., the empty conjunction, stands for true. Formula ∧("ψ"∈q) δ("ψ",Π) is a positive boolean formula whose atoms are again quoted subformulas of ϕ. Finally, q′ is a set of atoms, consisting again of quoted subformulas of ϕ, such that, when seen as a propositional interpretation, makes ∧("ψ"∈q) δ("ψ",Π) true. (In fact, we do not need to get all q′ such that q′ |= ∧("ψ"∈q) δ("ψ",Π), but only the minimal ones.) Notice that trivially we have (∅, a, ∅) ∈ ϱ for every a ∈ Σ. The algorithm LDLf2NFA terminates in at most an exponential number of steps, and generates a set of states S whose size is at most exponential in the size of ϕ.

Theorem 1. Let ϕ be an LDLf formula and Aϕ the NFA constructed by algorithm LDLf2NFA. Then π |= ϕ iff π ∈ L(Aϕ) for every finite trace π.

To see why the above theorem holds consider that given a LDLf formula ϕ, δ grounded on the subformulas of ϕ becomes the transition function of the AFW, with initial state

"ϕ" and no final states, corresponding to ϕ. LDLf2NFA essentially amounts to the procedure that transforms an AFW into an NFA, cf. [De Giacomo and Vardi, 2013]. Notice that we never need to construct the AFW using the above algorithm. We directly build the NFA using the rules δ. Finally, If we want to remove the special proposition last from P, we can easily transform the obtained automaton Aϕ = (2P , S, {"ϕ"}, ϱ, {∅}) into the new automaton A′ϕ by adding a special state ended:

where (q, Π′ , q′ ) ∈ ϱ′ if and only if (q, Π′ , q′ ) ∈ ϱ or (q, Π′ ∪ {last}, true) ∈ ϱ and q′ = ended.

It is easy to see that the NFA obtained can be built on-thefly while checking for nonemptiness, hence we have:

Theorem2. Satisfiability of an LDLf formula can be checked in PSPACE by nonemptiness of Aϕ (or A′ϕ).

Considering that it is known that satisfiability in LDLf is a PSPACE-complete problem, we can conclude that the proposed construction is optimal wrt computational complexity for satisfiability, as well as for validity and logical implication, which are linearly reducible to satisfiability in LDLf , cf. [De Giacomo and Vardi, 2013].

4 LTLf and LDLf Synthesis

In this section, we study the general form of synthesis for LTLf and LDLf , sometimes called realizability, or Church problem, or simply reactive synthesis [Vardi, 1996; Pnueli and Rosner, 1989]. We partition the set P of propositions into two disjoint sets X and Y. We assume to have no control on the truth value of the propositions in X, while we can control those in Y. The problem then becomes: can we control the values of Y in such a way that for all possible values of X a certain LTLf /LDLf formula remains true? More precisely, traces now assume the form π = (X0, Y0)(X1, Y1)(X2, Y2) · · · (Xn , Yn), where (Xi, Yi) is the propositional interpretation at the i-th position in π, now partitioned in the propositional interpretation Xi for X and Yi for Y. Let us denote by πX |i the interpretation π projected only on X and truncated at the i-th element (included), i.e., πX |i = X0X1 · · ·Xi. The realizability problem checks the existence of a function f : (2X )∗ → 2Y such that for all π with Yi = f(πX |i), we have that π satisfies the formula φ. The synthesis problem consists of actually computing such a function. Observe that in realizability/synthesis we have no way of constraining the value assumed by the propositions in X: the function we are looking for only acts on propositions in Y. Realizability and synthesis for LTL on infinite traces has been introduced in [Pnueli and Rosner, 1989] and shown to be 2EXPTIME-complete for arbitrary LTL formulas.

We are going to devise a technique in this section to do the same kind of synthesis in the case of finite traces for LTLf and LDLf . To do so, we will rely on DFA games, introduced below (see [Mazala, 2002] for a survey on game based approaches in the infinite trace setting).

DFA Games. DFA games are games between two players, here called respectively the environment and the controller, that are specified by a DFA. We have a set of X of uncontrollable propositions, which are under the control of the environment, and a set Y of controllable propositions, which are under the control of the controller. A round of the game consists of both the controller and the environment setting the values of the propositions they control. A (complete) play is a word in (2X×Y )∗ describing how the controller and environment set their propositions at each round till the game stops. The specification of the game is given by a DFA G of the form G = (2X×Y , S, s0, δ, F ), where:

• 2X×Y is the alphabet of the game;
• S are the states of the game;
• s0 is the initial state of the game;
• δ : S × 2X×Y → S is the transition function of the game: given the current state s and a choice of propositions X and Y , respectively for the enviroment and the controller, δ(s, (X, Y )) = s′ is the resulting state of the game;
• F are the final states of the game, where the game can be considered terminated.

A play is winning for the controller if such a play leads from the initial to a final state. A strategy for the controller is a function f : (2X )∗ → 2Y that, given a history of choices from the environment, decides which propositions Y to set to true/false next. A winning strategy is a strategy f : (2X )∗ → 2Y such that for all π with Yi = f(πX |i) we have that π leads to a final state of G. The realizability problem consists of checking whether there exists a winning strategy. The synthesis problem amounts to actually computing such a strategy.

We now give a sound and complete technique to solve realizability for DFA games. We start by defining the controllable preimage PreC(E) of a set E of states E of G as the set of states s such that there exists a choice of values for propositions Y such that for all choices of values for propositions X, game G progresses to states in E. Formally:

Using such a notion, we define the set Win(G) of winning states of a DFA game G, i.e., the set formed by the states from which the controller can win the DFA game G. Specifically, we define Win(G) as a least-fixpoint, making use of approximates Wini(G) denoting all states where the controller wins in at most i steps:

• Win0(G) = F (the final states of G);
• Wini+1(G) = Wini(G) ∪ PreC (Wini(G)).

Then, Win(G) = ⋃i Wini(G). Notice that computing Win(G) requires linear time in the number of states in G. Indeed, after at most a linear number of steps Wini+1(G) = Wini(G) = Win(G).

Theorem 3. A DFA game G admits a winning strategy iff s0 ∈ Win(G).

Next, we turn to actually computing the strategy. To do so, we define a strategy generator based on the winning sets Wini(G). This is a nondeterministic transducer, where nondeterminism is of the kind "don't-care": all nondeterministic choices are equally good. The strategy generator TG = (2X×Y , S, s0, ϱ, ω) is as follows:

• 2X×Y is the alphabet of the trasducer;
• S are the states of the trasducer;
• s0 is the initial state;
• ϱ : S × 2X → 2S is the transition function such that ϱ(s,X) = {s′ | s′ = δ(s, (X, Y )) and Y ∈ ω(s)};
• ω : S → 2Y is the output function such that

The transducer TG generates strategies in the following sense: for every way of further restricting ω(s) to return only one of its values (chosen arbitrarily), we get a strategy.

Synthesis in LTLf and LDLf . To do synthesis in LTLf or LDLf , we translate an LDLf /LTLf specification ϕ into an NFA Aϕ, e.g., using the algorithm LDLf2NFA presented above. This is an exponential step. Then, we transform the resulting NFA into a DFA Adϕ, e.g., using the standard determinization algorithm based on the subset construction [Rabin and Scott, 1959]. This will cost us another exponential. At this point we view the resulting DFA Adϕ as a DFA game, considering exactly the separation between controllable and uncontrollable propositions in the original LDLf /LTLf specification, and we solve it by computing Win(Adϕ) and the corresponding strategy generator TAdϕ . This is a linear step. The following theorem assesses the correctness of this technique:

Theorem 4. Realizability of an LDLf /LTLf specification ϕ can be solved by checking whether s0 ∈ Win(Adϕ). Synthesis can be solved by returning any strategy generated by TAdϕ .

Moreover, considering the cost of each of the steps above, we get the following worst-case computational complexity upper bound.

Theorem 5. Realizability in LDLf /LTLf can be solved in 2EXPTIME, and synthesis (i.e., returning a winning strategy) can be done in time double exponential.

A matching lower-bound can be shown by reduction from EXPSPACE alternating Turing machines.

Theorem 6. Realizability (and synthesis) in LDLf /LTLf is 2EXPTIME-hard.

5 Relationship with planning

In this section, we discuss the relationship between LTLf /LDLf synthesis and conditional planning with full observability. We can characterize an action domain by the set of allowed evolutions, each represented as a sequence of states of affair of the domain, which with a little abuse of terminology, we may call situations [Reiter, 2001]. To do so, we typically introduce a set of atomic facts, called fluents, whose truth value changes as the system evolves from one situation to the next one because of actions. Since LTL/LTLf do not provide a direct notion of action, we use propositions to denote them, as in [Calvanese et al., 2002]. Hence, we partition P into fluents F and actions A, adding structural constraints such as □(∨a∈A a) ∧□(∧a∈A(a→ ∧b∈A,b̸=a ¬b)), to specify that one action must be performed to get to a new situation, and that a single action at a time can be performed. Then, the initial situation is described by a propositional formula ϕinit involving only fluents, while effects can be modelled as:

where a ∈ A, while ϕ and ψ are arbitrary propositional formulas involving only fluents. Such a formula states that performing action a under the conditions denoted by ϕ brings about the conditions denoted by ψ. A formula like □(ϕ →·(a → ϕ)) corresponds to a frame axiom expressing that ϕ does not change when performing a. Alternatively, we can formalize effects through Reiter's successor state axioms [Reiter, 2001] (which implicitly provide a solution to the frame problem), as in [Calvanese et al., 2002; De Giacomo and Vardi, 2013], by translating the (instantiated) successor state axiom F (do(a, s)) ≡ ϕ+(s) ∨ (F (s) ∧ ¬ϕ-(s)), where ϕ+(s) (resp. ϕ-(s)) is the condition that makes the fluent F true (resp. false) after action a, into the LTLf formula:

In general, to specify effects we need LTLf formulas that talk only about the current and the next state, to capture how the domain transitions from the current to the next state, as above.

Turning to goals, usual reachability goals can be expressed as ϕgoal = ♦φ. where φ is a propositional formula on fluents.

PDDL trajectory constraints [McDermott and others, 1998; Gerevini et al., 2009] are also representable in LTLf /LDLf . As an example:

where φ is a propositional formula on fluents, and ϕ1 W ϕ2 .= (ϕ1 U ϕ2 ∨□ϕ1) is the so-called weak until, which states that ϕ1 holds until ϕ2 or forever.

Finally, we turn to procedural constraints. Typically, these cannot be expressed in LTLf but they can be expressed in LDLf . For example, let us consider them expressed in a propositional variant of GOLOG [Levesque et al., 1997; Fritz and McIlraith, 2007; Baier et al., 2008]:

a atomic action φ? test for a condition δ1; δ2 sequence if φ then δ1 else δ2 conditional while φ do δ while loop δ1|δ2 nondeterministic branch πx.δ nondeterministic choice of argument 2 δ∗ nondeterministic iteration

One can translate such programs into regular expressions:

Note that the atomic action a is translated into a test of an action proposition a (meaning action a has just been performed) in the next state. Then one can express GOLOG procedural constraints such as: δ must be executed at least once during the plan, as 〈tr(δ)〉true; plans for goal φ must be an executions of δ, as 〈tr(δ)〉φ; along the plan every time δ is executed ψ must hold, as [tr(δ)]ψ.

Given a LTLf /LDLf formulas Ψdomain describing the action domain (a transition formula), φinit describing the initial state (a propositional formula), Φconstraints describing trace constraints, and ϕgoal describing the goal, conditional planning amonts to solving the synthesis problem for the following specification:

where action propositions A are controllable and fluent propositions F are uncontrollable. The same holds if we consider arbitrary temporally extended goals expressed in LTLf /LDLf . In other words, by using the synthesis technique presented here we can generate plans in a very general setting: nondeterministic domains, arbitrary LTLf /LDLf goals, arbitrary LTLf /LDLf trajectory constraints.

Notice that in case we drop (declarative and procedural) trajectory constraints and we concentrate our attention to reachability goals of the form ♦φ, we get the classical conditional planning setting, which is known to be EXPTIMEcomplete [Rintanen, 2004]. Interestingly, our technique in this case matches the EXPTIME complexity, and hence is an optimal technique (wrt worst case computational complexity) for solving conditional planning problems. To see this, consider that the goal ♦φ gives rise to a linear size DFA over the alphabet of propositional interpretations. The domain itself, once represented in LTLf /LDLf , also gives rise to a deterministic automaton over the alphabet of propositional interpretations: given the current state, which is a propositional interpretation, and the next propositional interpretation, the domain can only accept it if it conforms to its transition rules or discard it if it does not. Indeed, the "nondeterminism" of the planning domain corresponds to the uncontrollability of the fluents and not to the nondeterminism of the automata on traces of propositional interpretations. As a result, the automaton that we get by translating the LTLf /LDLf formula corresponding to the domain, initial state, and reachability goal (corresponding to the conditional planning problem) is indeed deterministic. So determinization, which in general costs an exponential, is skipped, and we can directly solve the DFA game, getting overall a single exponential procedure as in [Rintanen, 2004].

2 Notice that the GOLOG nondeterministic pick construct πx.δ(x) makes sense only if the propositions in the domain are generated by finitely instantiating parametrized propositions as, for instance, in PDDL.

However, determinization may be required for more complex LTLf /LDLf goals or trajectory constraints, since the goals or constrains themselves may give rise to NFAs over traces of propositional interpretations.

6 Conclusion

We have studied LTLf /LDLf synthesis, assessing its complexity and devising an effective procedure to check the existence of a winning strategy and to actually compute it if it exists.

The complexity characterization of the problem in the case of LTLf /LDLf on finite traces is the same as the one for infinite trace, namely, 2EXPTIME-complete. Also the procedure for computing it is analogus [Mazala, 2002]. Starting from the logical specification, we get a nondeterministic automaton (NFA in the finite case, B¨uchi in the infinite case), we determinize it (in the infinite case, we change the automaton, e.g., to a parity one, since B¨uchi automata are not closed under determinization, indeed deterministic B¨uchi automata are strictly less espressive that nondeterministic ones), and then we solve the corresponding game (DFA games for finite traces, parity games for the infinite ones) considering which propositions are controllable and which are not. However, in the case of infinite traces, the determinization remains a very difficult step, and there are no good algorithms yet to perform it [Fogarty et al., 2013]. As a consequence, virtually no tools are available (an exception is Lily [Jobstmann and Bloem, 2006]). In the finite case, determinization is much easier: it requires the usual subset constructions and good algorithms are available. So effective tools can indeed be developed.

With respect to the latter, it would be particularly interesting to study how techniques developed for planning could be used to actually translate an LTLf /LDLf specification and determinize the automaton on-the-fly while playing the DFA game [Baier and McIlraith, 2006; Geffner and Bonet, 2013].

Our work is also related to other forms of synthesis that are well established in AI, such as ATL model checking [Alur et al., 2002] or 2-player game structure model checking, see e.g., [De Giacomo et al., 2010]. The latter was used to solve our kind of syntesis for GR(1) LTL formulas in the infinite trace setting [Bloem et al., 2012]. The key difference between that kind of synthesis and the general one considered here is that there the game arena is given while the goal to play for is determined by the ATL or mu-calculus formula. In our case, instead, the game arena, i.e., the DFA game, is computed from the formula, while the goal to play for is fixed to be reachability of the final state of the automaton.

Acknowledgements. The authors would like to thank anonymous reviewers for their comments and Diego Calvanese for insightful discussions on the topic of the paper.