Sergej Scheck
email: sergej.scheck@unicaen.fr

Alexandre Niveau
email: alexandre.niveau@unicaen.fr

Bruno Zanuttini
email: bruno.zanuttini@unicaen.fr

Knowledge Compilation for Nondeterministic Action Languages

We study different languages for representing nondeterministic actions in planning from the point of view of knowledge compilation. Precisely, we consider succintness issues (how succinct is the description of an action in each language?) and complexity issues (tractability or hardness of several queries which arise naturally in planning and belief tracking). We study an abstract, nondeterministic version of PDDL, nondeterministic conditional STRIPS, the language NNFAT of NNF action theories, and the language NPDDL seq obtained by adding a sequence operator to nondeterministic PDDL. We show that these languages have different succinctness and different complexity even for the most natural queries.

Introduction

In automated planning, a central aspect of the description of problems is the formal representation of actions. Such representations are indeed needed for specifying the actions available to the agent (PDDL [START_REF] Mcdermott | PDDL-the planning domain definition language[END_REF]) is a standard language for this), and also for the planners to operate on them while searching for a plan.

We consider different representation languages in the formal framework of the knowledge compilation map [START_REF] Darwiche | A knowledge compilation map[END_REF]. This framework deals with the study of formal languages under the point of view of queries (how efficient is it to answer various queries depending on the language?), transformations (how efficient is it to transform or combine different representations in a given language?), and succinctness (how concise is it to represent knowledge in each language?).

The knowledge compilation map has been introduced for representations of Boolean functions, such as Boolean formulas in negation normal form, ordered binary decision diagrams, etc. [START_REF] Darwiche | A knowledge compilation map[END_REF]. As far as we know there has been no systematic study of languages for representing actions per themselves. This is however an important problem, as planners need to query action representations again and again while searching for a plan (e.g., to find out which actions are applicable at the current node of the search tree). Hence having a clear picture of the properties of languages is of interest for developing such planners.

Copyright c 2021, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.

For instance, if a planner uses an efficient representation of actions (like binary decision diagrams) but this representation is exponentially larger than the specification of the action (for instance, in PDDL), then it may not be worth overall to convert the specification into the efficient representation, and this might suggest to make the planner work directly with the specification. The complexity of querying the various representations (like checking whether the action is applicable in some state, or whether it can lead from some state to another one) is also of importance for the development of algorithms: depending on the type of queries used by the algorithm, one language may be preferred to another one because it allows to answer them more efficiently. Of course, there is typically a tradeoff between succinctness of languages and tractability of queries.

However, there have been few papers studying these aspects for planning. [START_REF] Nebel | On the compilability and expressive power of propositional planning formalisms[END_REF] has considered questions very similar to ours; his study uses a rather powerful notion of compilation, where translations from one formal language to another are allowed to change the set of variables and the set of actions. This captures compilation schemes where one is interested in preserving the existence of plans and their size. Contrastingly, we are interested in a strict notion of compilation, where the set of variables and the specification of initial states and goals are unchanged by the translation, while each action is translated into one with the same semantics. This is more restricted , but makes translations applicable in broader settings (for instance, to problems where we want to count or enumerate plans). [START_REF] Bäckström | Algorithms and Limits for Compact Plan Representations[END_REF] have studied representations of plans with respect to their size and to the complexity of retrieving the individual actions which they prescribe at each step . This is also related to our work, but with a focus on languages for representing plans, while we study languages for representing actions. Also related is the translation of HTN specifications into PDDL proposed by [START_REF] Alford | Translating HTNs to PDDL: A small amount of domain knowledge can go a long way[END_REF]. The objects of interest there (HTN specifications) are different from ours (plain action specifications), though our study of action specifications using a construct for sequences is reminiscent of HTN decompositions.

We are interested in (purely) nondeterministic actions, as in fully observable nondeterministic planning and conformant planning [START_REF] Rintanen | Complexity of Planning with Partial Observability[END_REF][START_REF] Albore | Compiling Uncertainty Away in Non-Deterministic Conformant Planning[END_REF][START_REF] Geffner | A Concise Introduction to Models and Methods for Automated Planning[END_REF][START_REF] Muise | Non-Deterministic Planning With Conditional Effects[END_REF][START_REF] To | A generic approach to planning in the presence of incomplete information: Theory and implementation[END_REF][START_REF] Geffner | Compact Policies for Fully Observable Non-Deterministic Planning as SAT[END_REF]. We also focus on propositional domains, in which states are assignments to a given set of propositions.

We consider four representation languages: NPDDL, which is a grounded, nondeterministic version of PDDL, a language typically used for specifying actions (by a domain expert); NSTRIPS, a nondeterministic version of conditional STRIPS; NNF action theories, which are typically used as an internal representation by solvers [START_REF] Cimatti | Automatic OBDD-based generation of universal plans in nondeterministic domains[END_REF][START_REF] To | A generic approach to planning in the presence of incomplete information: Theory and implementation[END_REF]; and NPDDL seq , obtained by enriching NPDDL by a sequence operator, like in DL-PA [START_REF] Balbiani | Dynamic logic of propositional assignments: a well-behaved variant of PDL[END_REF]. Despite different typical uses, these are all languages for representing actions (as nondeterministic mappings from states to states). We choose these because they use different constructs, different structural restrictions on expressions, and different representations of persisting values. Our midterm goal is to give a systematic picture of languages arising from combinations of such constructs and restrictions.

Orthogonally, we also study two concrete representations of expressions, as syntactic trees or as more compact circuits, where identical subexpressions are not repeated. The former representation gives a natural measure of the size of action specifications, while the latter is more compact and is the one typically used for algorithmic efficiency (in particular for binary decision diagrams [START_REF] Bryant | Symbolic boolean manipulation with ordered binary-decision diagrams[END_REF]).

We first give background about actions and logic, then we define the action languages which we consider. We then give our results: polynomial-time translations between the languages, then results about the complexity of queries, and finally separation results, which allow us to determine the relative succinctness of the languages. Finally, we conclude.

Preliminaries

We consider a countable set of propositional state variables P = {p i | i ∈ N}. Let P ⊂ P be a finite set of state variables; a subset of P is called a P-state, or simply a state. The intended interpretation of a state s ∈ 2 P is the assignment to P in which all variables in s are true, and all variables in P \ s are false. For instance, for P = {p 1 , p 2 , p 3 }, s = {p 1 , p 3 } denotes the state in which p 1 , p 3 are true and p 2 is false. We write V(ϕ) for the set of variables occuring in an expression ϕ; note that expressions may involve both variables in P and variables not in P, so in general we do not have V(ϕ) ⊆ P.

Actions We consider (purely) nondeterministic actions, which map states to sets of states. Hence a single state may have several successors through the same action.

Definition 1 (action). Let P ⊂ P be a finite set of variables. A P-action is a mapping a from 2 P to 2 (2 P ) . The states in a(s) are called a-successors of s.

Note that a(s) is defined for all states s. We will consider a to be applicable in s if and only if a(s) = / 0.

Example 2. Consider a hunting example, described by whether the rabbit is in sight and/or alive, and whether the rifle is loaded. Let P = {in sight, alive, loaded}.

The action shoot rabbit can be described as "if alive then: if loaded and in sight, then not loaded, and either alive and not in sight, or not alive and in sight; otherwise state unchanged". The action is applicable only if the rabbit is alive (otherwise it is not sensible to shoot at him). Then, if the hunter is ready to shoot (the rifle is loaded and he sees the rabbit), he shoots the rabbit (he might miss the rabbit who hears the shot and runs away, so the action is nondeterministic), and if he is not ready to shoot, then nothing happens.

Let s = {in sight, alive, loaded} be the state where all variables are true. Then shoot rabbit(s) is the set of states ("successors") {s , s } with s = s \ {loaded, in sight} = {alive} and s = s \ {loaded, alive} = {in sight}.

We now introduce a formal setting for studying different representations of actions. Definition 3 (action language). An action language is an ordered pair L, I , where L is a set of expressions and I is a partial function on L × 2 P such that, when defined on α ∈ L and P ⊂ P, I(α, P) is a P-action.

We call the expressions in L action descriptions, and call I the interpretation function of the language. Observe that those sets P's such that I(α, P) is defined are a priori not related to V(α); α may involve auxiliary variables (not in P) which are not part of the state descriptions, and dually, a state may assign variables of P which do not occur in α. If L, I, P are fixed or clear from the context, then we write α(s) instead of I(α, P)(s) for the set of all α-successors of s. Definition 4 (translation). A translation from an action language L 1 , I 1 to another language L 2 , I 2 is a function f : L 1 × 2 P → L 2 such that I 1 (α, P) = I 2 ( f (α, P), P) holds for all α ∈ L 1 and P ⊂ P such that I 1 (α, P) is defined.

In words, this means that the L 1 -expression α and the L 2expression f (α, P) describe the same P-action. Again, when P is clear from the context, we write f (α) for f (α, P).

The translation f is said to be polynomial-time if it can be computed in time polynomial in the size of α and P, and polynomial-size if the size of f (α, P) is bounded by a fixed polynomial in the size of α and P. Clearly, a polynomialtime translation is necessarily also a polynomial-size one, but the converse is not true in general.

Negation Normal Form A Boolean formula ϕ over a set Q of variables is in negation normal form (NNF) if it is built up from literals using conjunctions and disjunctions, i.e., if it is generated by the grammar ϕ ::

= q | ¬q | ϕ ∧ ϕ | ϕ ∨ ϕ,
where q ranges over Q. Like other expressions, Q may involve state variables (in P) and other variables (not in P).

The set of NNF formulas is complete, i.e., any Boolean function can be described by an NNF formula. It is important to note that a formula ϕ with V(ϕ) ⊆ Q for some set of variables Q can be viewed as a formula over Q (and the truth value of the corresponding Boolean function does not depend on the variables in Q \ V(ϕ)). For a Boolean formula ϕ over Q and an assignment t to Q, we write t |= ϕ ("t satisfies ϕ") if ϕ evaluates to true under the assignment t. We always use notation s,t, . . . for states, a, b, . . . for actions, α, β , . . . for action descriptions, and ϕ, ψ, . . . for logical formulas.

Action Languages

The first language which we consider is the well-known planning domain description language (PDDL). This language is a standardized one used for specifying actions at the relational level, widely used as an input for planners, especially in the international planning competitions (Mc-Dermott 1998;Fox andLong 2002, 2003). Since we are interested in nondeterministic actions, we consider a nondeterministic variant of PDDL inspired by NPDDL [START_REF] Bertoli | Extending PDDL to nondeterminism, limited sensing and iterative conditional plans[END_REF], and so as to abstract away from the precise syntax of the specification language, we consider an idealized version. Finally, we consider a grounded (propositional) version. Definition 5 (NPDDL). An NPDDL action description is an expression α generated by the grammar

α ::= ε | +p | -p | ϕ α | (α ∪ α) | α α
where p ranges over P and ϕ over formulas in NNF over P.

Intuitively, • ε describes the action with no effect (∀s : ε(s) = {s}),

• +p (resp. -p) is the action which sets p true (resp. false),

• denotes conditional execution, • ∪ denotes (exclusive) nondeterministic choice, • denotes simultaneous execution, and, importantly, variables not explicitly set by the action are assumed to keep their value. Also observe that auxiliary variables are not allowed -only variables in P can occur.

We insist that this syntax is an idealization of nondeterministic (grounded) PDDL; for instance, the action which we write x +y ∪ (-y +z) would be written when x (oneof y (and (not y) z)) with the syntax of NPDDL [START_REF] Bertoli | Extending PDDL to nondeterminism, limited sensing and iterative conditional plans[END_REF].

In order to define the interpretation function I of NPDDL, we first introduce a function J which for given α, P, s with V(α) ⊆ P and s ⊆ P, gives a set of ordered pairs Q + , Q -, where Q + (resp. Q -) is a set of variables of P which are explicitly set to true (resp. to false) by α when executed in s (the other variables being left unchanged from s): • J(ε, P, s) := { / 0, / 0 }, • J(+p, P, s) := { {p}, / 0 }, and J(-p, P, s) := { / 0, {p} }, • J(ϕ α, P, s) := J(α, P, s) if s |= ϕ, and J(ϕ α, P, s)

:= { / 0, / 0 } if s |= ϕ, • J(α ∪ β , P, s) := J(α, P, s) ∪ J(β , P, s), • J(α β , P, s) := { Q + α ∪ Q + β , Q - α ∪ Q - β | Q + α , Q - α ∈ J(α, P, s), Q + β , Q - β ∈ J(β , P, s), Q + α ∩ Q - β = Q - α ∩ Q + β = / 0}
where the last line can be read "when executed in s, α β has all those effects which are the consistent union of an effect of α in s and one of β in s".

As an example, for α = (+p 1 ∪ (-p 2 +p 3 )) (-p 2 ∪ +p 2 ), P = {p 1 , p 2 , p 3 }, and any s, we have J(α, P, s) = { {p 1 }, {p 2 } , {p 1 , p 2 }, / 0 , {p 3 }, {p 2 } }, since in the last combination, -p 2 +p 3 and +p 2 are not consistent. 1Then the interpretation function just formalizes the fact that the other variables retain their value; for all NPDDL expressions α and sets of variables P with V(α) ⊆ P ⊂ P, ∀s ⊆ P : I(α, P)(s)

:= {(s∪Q + )\Q -| Q + , Q -∈ J(α, P, s)} and I(α, Q) is undefined for Q ⊇ V(α) .
Note that the expression +p -p (for an arbitrary p ∈ P) defines an action with no successor (which can be interpreted as an execution failing). We use ⊥ as a shorthand for it (hence I(⊥, P)(s) = / 0 for all P ⊆ P, s ⊆ P). Example 6 (continued). The following is an NPDDL action description for the action shoot rabbit of Example 2.

(¬alive ⊥) (alive ∧ in sight ∧ loaded) (-loaded (-in sight ∪ -alive))
We also study a natural extension of conditional STRIPS to nondeterministic actions. Definition 7 (NSTRIPS). An NSTRIPS action description is an NPDDL expression of the form

i∈I ϕ i ( 1,1 i . . . 1, j 1 i ) ∪ . . . ∪ ( k i ,1 i . . . k i , j k i i
)

where each k, j i is either ⊥, or +p or -p for some p ∈ P. In words, an NSTRIPS action description specifies a set of conditions so that, when the action is applied in a state s, for each condition satisfied by s exactly one of the corresponding effects occurs. Example 8 (continued). The following is an NSTRIPS action description for the action shoot rabbit of Example 2:

(¬alive ⊥) (alive ∧ in sight ∧ loaded) ((-loaded -in sight) ∪ (-loaded -alive))
The language NSTRIPS is complete, since any action a can at least be represented by one condition for each state s (satisfied by exactly s), associated to either (1) a choice (∪) between some "conjunctions" of atoms, one conjunction per a-successor s of s (setting all variables as in s ), or (2) to the degenerate choice of conjunctions ⊥, when a(s) is empty.

We are also interested in the language NPDDL as extended by the sequential execution operator ";". Definition 9 (NPDDL seq ). An NPDDL seq action description is an expression α generated by the grammar

α ::= ε | +p | -p | ϕ α | (α ∪ α) | α α | α ; α
where p ranges over P and ϕ over formulas in NNF over P.

Let us emphasize that ";" is not bound to occur only at the root of the expression. The interpretation function is the same as for NPDDL expressions, augmented with ∀s ⊆ P : I(α; β , P)(s) := {s ⊆ P | ∃t ∈ α(s) : s ∈ β (t)} Example 10. The NPDDL seq description + p even ;

+ p 1 (p even -p even ) (¬p even +p even ) ∪ -p 1 ;

. . . + p n (p even -p even ) (¬p even +p even ) ∪ -p n ;

¬p even ⊥ describes an action which maps any state to the set of all states with an even number of p i 's, and p even , set to true.

Since NSTRIPS is a sublanguage of NPDDL and NPDDL seq , NPDDL and NPDDL seq are also complete.

We finally define the language of (NNF) action theories. Such representations are typically used by planners which reason explicitly on sets of states (aka belief states), since they allow for symbolic operations on belief states [START_REF] Cimatti | Conformant Planning via Symbolic Model Checking[END_REF][START_REF] Bryce | Planning Graph Heuristics for Belief Space Search[END_REF][START_REF] To | A generic approach to planning in the presence of incomplete information: Theory and implementation[END_REF]. Note that such planners in fact use more efficient representations, like OBDDs or DNFs, which are defined by further restrictions on NNF. However, as our results show, NNF action theories are already more efficient (for queries) but larger (less succinct) than the other languages which we study, so this holds for all sublanguages of NNF, too. Then a sublanguage of NNF to work with can be chosen using the knowledge compilation map for Boolean functions [START_REF] Darwiche | A knowledge compilation map[END_REF].

To prepare the definition we associate an auxiliary variable p / ∈ P to each variable p ∈ P; p denotes the value of p after the action took place, while p denotes the value before. Definition 11 (NNFAT). An NNFAT action description is a Boolean formula α in NNF over P α ∪ {p | p ∈ P α } for some set of state propositions P α ⊂ P.

The interpretation of an NNFAT action description α is defined for all P ⊆ P such that P ⊇ V(α) ∩ P (that is, when all state propositions have a value) by ∀s ⊆ P :

I(α, P)(s) = {s | s ∪ {p | p ∈ s } |= α} where s ∪ {p | p ∈ s } is the assignment to P ∪ {p | p ∈ P α }
induced by s, s . For P ⊇ V(α) ∩ P, I(α, P) is not defined. In words, an NNFAT expression represents the set of all ordered pairs s, s such that s is a successor of s, as a Boolean formula over variables in P ∪ {p | p ∈ P}.

Importantly, NNFAT does not assume persistency of values, so that if, for example, a variable does not appear at all in an NNFAT expression, then this means that its value after the execution of the action can be arbitrary. For instance,

I(p 1 ∨ ¬p 2 , {p 1 , p 2 , p 3 })({p 2 }) = {{p 1 }, {p 1 , p 2 }, {p 1 , p 3 }, {p 1 , p 2 , p 3 }}
Obviously, every action can be represented in NNFAT, since NNF is a complete language for Boolean functions. Example 12 (continued). The action shoot rabbit of Example 2 can be written as follows (using → and ↔ for readability, but keeping in mind that they are shorthand notation for longer NNF formulations): alive

∧   (loaded ∧ in sight) → ¬loaded ∧ (in sight ∧ ¬alive ) ∨ (¬in sight ∧ alive )   ∧     (alive ↔ alive ) ∨ (in sight ↔ in sight ) ∨ (loaded ↔ loaded )   → loaded ∧ in sight  
As can be seen, encoding the fact that the values of variables persist unless stated otherwise requires subexpressions (here the last conjunct) playing the same role as successor-state (or frame) axioms in the situation calculus [START_REF] Reiter | The frame problem in the situation calculus: A simple solution (sometimes) and a completeness result for goal regression[END_REF]. This typically requires much space, for what we give a formal meaning later in the paper (Proposition 32).

Representations Since we study the succinctness of languages, it is crucial to define the size of action descriptions. For this we consider two variants of each language.

The first variant corresponds to a representation of the expressions α in the language by their syntactic tree (including the Boolean formulas occuring in the expression, if any). The second variant corresponds to the representation of these expressions α by the directed acyclic graph, or circuit, obtained from the syntactic tree of α by iteratively identifying the roots of two isomorphic subexpressions to each other, until no more reduction is possible (like for binary decision diagrams [START_REF] Bryant | Symbolic boolean manipulation with ordered binary-decision diagrams[END_REF]). Clearly, for all expressions α, the circuit associated to α in this manner is unique, and it can be computed in polynomial time from the tree or from a nonreduced circuit.

As an illustration, Figure 1 gives the tree (left) and the associated circuit (right) for the same NPDDL seq expression.

Depending on the representation, we obtain two languages based on NNFAT, two based on NPDDL, and two based on NPDDL seq . We write T-NNFAT, T-NPDDL, and T-NPDDL seq for those languages with expressions represented as trees, and C-NNFAT, C-NPDDL, and C-NPDDL seq for those languages with expressions represented as reduced circuits. Since NSTRIPS is flat (the depth of the underlying graph is bounded), there is no difference between the circuit and the tree versions up to polynomialtime transformations, except for the representation of conditions ϕ; since, as it turns out, the representation of conditions does not affect the results in this paper, we only write NSTRIPS without specifying the representation, and we say that NSTRIPS is a sublanguage of T-NPDDL or C-NPDDL, meaning each time the corresponding version of NSTRIPS.

Finally, for all languages and representations, we write |α| for the size of an expression α in the representation, namely the number of nodes and edges in the tree or DAG.

Polynomial-Time Translations

In this section we give some (easy) results about polynomial-time translations between languages. We now proceed to show that there is a polynomial-time translation from NNFAT to NPDDL, for both representations. The translation looks like a simple rewriting of α, but we have to take care about the fact that in NNFAT, a variable not explicitly set to a value can take any value in the next state s , contrary to persistency by default in NPDDL. PROOF. Let f be defined inductively as follows, for all NNFAT expressions α and sets of variables P ⊇ V(α) ∩ P: 2. for p ∈ P, f (¬p) = (p ⊥) ¬p q∈P (+q ∪ -q) ; 3. for p ∈ P, f (p ) = +p q∈P,q =p (+q ∪ -q) ; 4. for p ∈ P, f (¬p ) = -p q∈P,q =p (+q ∪ -q) ; 5.

1. for p ∈ P, f (p) = (¬p ⊥) p q∈P (+q ∪ -q) ; ; ∪ +p 2 -p 2 -p 1 +p 1 -p 1 ; ; ∪ ∪ +p 4 -p 4 -p 3 +p 3 -p 3 +p 4 -p 4 -p 3 +p 3 -p 3 ¬ϕ T -p sat ¬ϕ T -p sat ¬ϕ T -p sat ¬ϕ T -p sat ; ∪ +p 2 -p 2 -p 1 +p 1 -p 1 ; ∪ +p 4 -p 4 -p 3 +p 3 -p 3 ¬ϕ C -p sat
f (β ∧ γ) = f (β ) f (γ); 6. f (β ∨ γ) = f (β ) ∪ f (γ).
Items 1-4 take care of the fact that there is no implicit persistency of values in NNFAT. Then it is easy to show by induction that f is indeed a translation from NNFAT to NPDDL. In particular, Case 5 works despite the different semantics of ∧ and because (by induction) all effects are explicit in both f (β ) and f (γ), so that acts as ∧ in this precise translation. Case 6 works despite the fact that ∨ is inclusive but ∪ is not because the effects brought about by β and γ are by definition brought about by, say, β alone and hence, by induction, by f (β ) alone, so that ∪ acts as ∨ in this translation.

Since f rewrites each node of α independently of the others, it is polynomial-time both when applied to an expression in T-NNFAT (with a result in T-NPDDL) and to an expression in C-NNFAT (with a result in C-NPDDL).

Complexity of Queries

We now turn to studying the complexity of queries to expressions. We concentrate on three natural queries for planning, corresponding to checking the existence of a transition, deciding applicability of an action, and deciding whether a (sequential) plan reaches a goal. Let L, I be a fixed action language, and let α, α 1 , . . . , α k denote expressions in L, P ⊆ P denote a set of variables such that I(α, P) and I(α 1 , P), . . . , I(α k , P) are defined, and s, s denote P-states. Definition 15 (IS-SUCC). The decision problem IS-SUCC takes as input α, P, s, s , and asks whether s ∈ α(s). Definition 16 (IS-APPLIC). The decision problem IS-APPLIC takes as input α, P, s, and asks whether α(s) = / 0. Definition 17 (ENTAILS). The decision problem ENTAILS takes as input α 1 , . . . , α k , P, s, and an NNF formula ϕ over P, and asks whether s satisfies ϕ for all s ∈ (α 1 ; . . . ; α k )(s).

It is important to note that if s has no successor through α 1 ; . . . ; α k , then it entails any formula ϕ.

It turns out that the query IS-SUCC is central, hence we start with it. Proposition 18. IS-SUCC can be solved in linear time for T-NNFAT and C-NNFAT.

PROOF. By definition of NNFAT, s ∈ α(s) holds if and only if the assignment to P ∪ {p | p ∈ P} induced by s, s satisfies α, which can be decided by replacing each leaf in the representation of α by its value in s or s , then evaluating α in a bottom-up fashion. Clearly, this can be done in linear time for both tree and circuit representations.

Proposition 19. IS-SUCC is in NP for T-NPDDL seq .
PROOF. We define a witness for a positive instance to be composed of either β or γ for each subexpression β ∪ γ of α. Such a witness is clearly of polynomial size, and verifying it amounts to deciding successorship for a deterministic NPDDL seq description, which is clearly doable in polynomial time by simulating the (only) execution.

For hardness, we first define an encoding of a 3-CNF formula ϕ over n variables as an assignment to polynomially many state variables. Notation 20. Let n ∈ N, and let X n = {x 1 , . . . , x n } be a set of variables. Observe that there are a cubic number N n of clauses of length 3 over X n . We fix an arbitrary enumeration γ 1 , γ 2 , . . . , γ N n of all these clauses, and we define P n ⊂ P to be the set of state variables {p 1 , p 2 , . . . , p N n }. Write ∈ γ i if the literal occurs in the clause γ i . Then to any 3-CNF formula ϕ we associate the P n -state s(ϕ) = {p i | i ∈ {1, . . . , N n }, γ i ∈ ϕ}, and dually, to any P n -state s, we associate the 3-CNF formula over X n , written ϕ(s), which contains exactly those clauses γ i for which p i ∈ s holds. Example 21. Consider an enumeration of all clauses over

X 2 = {x 1 , x 2 } which starts with γ 1 = (x 1 ∨ x 1 ∨ x 2 ), γ 2 = (x 1 ∨ x 1 ∨ ¬x 2 ), γ 3 = (x 1 ∨ ¬x 1 ∨ x 2 ), . . . Then the 3-CNF ϕ = (x 1 ∨ x 1 ∨ x 2 ) ∧ (x 1 ∨ ¬x 1 ∨ x 2 ) is encoded by s(ϕ) = {p 1 , p 3 }. Proposition 22. IS-SUCC is NP-hard for NSTRIPS.
PROOF. We give a reduction from 3-SAT. Let ϕ be a 3-CNF formula over variables x 1 , . . . , x n and containing (w.l.o.g.) the clauses γ 1 , . . . , γ k (encoded by p 1 , . . . , p k ). We define

α := x i   γ j ∈ϕ : x i ∈γ j +p j ∪ γ j ∈ϕ : ¬x i ∈γ j +p j  
Clearly, α is a polynomial-time constructible NSTRIPS expression. We claim that the state {p 1 , . . . , p k } is an αsuccessor of / 0 if and only if ϕ is satisfiable. Indeed, α can be seen as deciding nondeterministically, for every variable x i , whether to set it true or false, and then setting p j true for all γ j which are satisfied by the chosen value. Thus, if all p j 's have been set to true, all clauses are satisfied by the chosen assignment to the x i 's, and hence ϕ is satisfiable. Conversely, if ϕ is satisfiable, then there exists a consistent choice of literals 1 , . . . , n which satisfies all γ j 's. Then the execution of α which, for each x i , chooses the left or the right side of the ∪ choice according to the polarity of i , indeed witnesses that {p 1 , . . . , p k } is an α-successor of / 0.

As NSTRIPS is a sublanguage of NPDDL and NPDDL seq , using Propositions 19 and 22 we get:

Corollary 23. IS-SUCC is NP-complete for NSTRIPS, T-NPDDL, and T-NPDDL seq .

IS-SUCC is NP-complete for C-NPDDL as well:

Proposition 24. IS-SUCC is NP-complete for C-NPDDL.

PROOF. Hardness follows from Corollary 23, since NSTRIPS is a sublanguage of C-NPDDL. For membership, the intuition is to guess a branch to be chosen for each ∪node in the circuit as in the proof of Proposition 19. However, in circuits, a ∪-node might have exponentially many paths from the root to it, inducing parallel executions, and in each of these a new child may be chosen. 2For that reason, we define a witness of s ∈ α(s) to be the number of times each node in the circuit is executed along an execution of α leading from s to s . Hence a witness is a labelling of each node and edge in the circuit by a number in [0..2 |α| ] (using O(|α|) bits per node). We then claim that such a labelling is indeed a witness that s ∈ α(s) holds, if and only if the following six conditions hold:

1. the root is labelled with 1, 2. each edge out of a -node has the same label as its source, 3. the labels of the edges out of a ∪-node sum up to the label of their source, 4. the edge from a -node α of the form (ϕ β ) to node β has the same label as α if s satisfies ϕ, and 0 otherwise, 5. the label of each node is the sum of the labels of the edges pointing to it, 6. the action 1 • • • k , where 1 , . . . , k are those leaves of the circuit (that is, elementary assignments ±p) whose label is nonzero, maps s to s (in particular, these assignments are consistent together).

Clearly, this can be verified in polynomial time. Now it can be checked by induction that a labelling of the circuit of α is correct, as defined by Items 1-5 above, if and only if the action 1 • • • k of Item 6 is a valid execution of α, which concludes the proof.

The proof of Proposition 24 relies on the fact that there is no sequence operator in C-NPDDL, and hence that when a node is executed several times, the order does not matter. For this reason, it cannot be generalized to C-NPDDL seq . Proposition 25. IS-SUCC is PSPACE-complete for C-NPDDL seq .

PROOF. For membership, observe that we can simulate all possible executions (induced by nondeterministic choices) of the circuit in polynomial space, and simply decide whether one witnesses that s is a successor of s.

Now for hardness, we give a reduction from the problem of deciding the validity of a QBF of the form Φ = ∃p 1 ∀p 2 ∃p 3 ∀p 4 . . . ∃p 2n-1 ∀p 2n : ϕ, where ϕ is a 3-CNF formula. Given such a QBF, let p sat ∈ P be a fresh variable, define α n to be the NPDDL seq expression ¬ϕ -p sat , and for i = n -1, . . . , 0, define α i to be (+p 2i+1 ∪ -p 2i+1 ) ; +p 2i+2 ; α i+1 ; -p 2i+2 ; α i+1 ; -p 2i+1 Clearly, α 0 has a circuit of size polynomial in ϕ (e.g., Fig. 1 (right) depicts α 0 for n = 2).

Intuitively, the action guesses a value for p 2i+1 , then verifies that together with p 2i+2 set to true, the nested formula α i+1 is valid, then that together with p 2i+2 set to false instead, α i+1 is again valid, and finally resets p 2i+1 to false. Then it can be shown that the reduction is correct, using induction on i = n, n -1, . . . , 0 with the following hypothesis: for all literals 1 , . . . , 2i over p 1 , . . . , p 2i , respectively, the state s = {p sat } ∪ {p j | j = p j } is an α i -successor of itself if and only if Φ i := ∃p 2i+1 ∀p 2i+2 . . . ∃p 2n-1 ∀p 2n ϕ | 1 ,..., 2i is valid, where ϕ | 1 ,..., 2i denotes propositional conditioning, that is, ϕ with the occurrences of p 1 , . . . , p 2i replaced by their value and simplified. In the end, we obtain that s = {p sat } is an α 0successor of itself if and only if Φ 0 is valid, which concludes the proof since by construction we have Φ 0 = Φ.

We now turn to the query IS-APPLIC. Proposition 26. IS-APPLIC is NP-complete for T-NNFAT and C-NNFAT.

PROOF. Membership is clear, because applicability of α in s can be justified by giving a successor, which can be verified in linear time for both T-NNFAT and C-NNFAT by Proposition 18. For hardness, let ϕ be a propositional formula over variables p 1 , . . . , p n , and let α be the T-NNFAT expression obtained from ϕ by replacing each p i with p i . Then clearly, α is applicable in any state (say in s = / 0) if and only if ϕ is satisfiable. Hence IS-APPLIC is NP-hard for T-NNFAT, and clearly this entails NP-hardness for C-NNFAT also.

For the other languages, we will use the following lemma. Lemma 27. IS-SUCC is polynomial-time reducible to IS-APPLIC for NSTRIPS, T-NPDDL, C-NPDDL, T-NPDDL seq and C-NPDDL seq .

Conclusion

We studied several languages for describing nondeterministic actions along two criteria: succinctness and complexity of different decision problems natural to automated planning. We also considered two representations, by trees and by circuits. Our results are summarized in Table 1, where we have ordered languages with respect to their relative succinctness (we emphasize that we did not study the relative succinctness of two representations of the same language).

One conclusion is that converting an NPDDL specification into an NNFAT representation necessarily yields an explosion in some cases. Hence it can be worth developing planners which tackle directly the PDDL specification [START_REF] Lesner | Efficient Policy Construction for MDPs Represented in Probabilistic PDDL[END_REF] proposes one for the stochastic case), or, dually, to ask the experts to specify actions directly in NNFAT, so as to avoid the conversion. The latter may indeed make sense in some settings, since NNFAT can be seen as a declarative language (it is easy to specify that the action sets p 1 to the same value as p 2 , for instance), quite complementary to PDDL, which is more "imperative".

Also interesting is the different complexity of queries for NPDDL seq with trees or circuits. While it is intuitively clear that there must be some languages which are strictly less compact with trees than with circuits, and languages with less tractable queries with circuits than with trees, this gives a concrete example of this phenomenon. Finally, it is interesting that the complexity of the three queries is the same for tree-represented NPDDL with or without sequence. This means that as far as these queries are concerned, one can let an expert use the richer language for specifying actions, and a solver can just compile away sequence operators efficiently and work with plain NPDDL, as if the specification was constrained to be in this language.

Our picture is almost complete for the languages which we studied: we only leave open the relative succinctness of NSTRIPS and NNFAT on the one hand, and NSTRIPS and NPDDL on the other hand. Our main perspective is a more systematic study, for languages constructed using combinations of features like the sequence operator, modalities, Kleene star, etc. A very expressive language to consider is DL-PPA [START_REF] Herzig | Dynamic logic of parallel propositional assignments and its applications to planning[END_REF]. Another perspective is to consider languages for stochastic actions, and for actions with observations (and hence queries on belief states rather than states). We are also interested in studying the complexity of other queries, e.g. counting and enumerating successors or randomly generating a successor state. The ultimate goal is to draw clear pictures of what language to choose depending on the queries which are used by, e.g., a planning algorithm or a simulator.

Proposition 13 .

 13 The identity function is a polynomial-time translation from NSTRIPS to T-NPDDL, from NSTRIPS to C-NPDDL, from T-NPDDL to T-NPDDL seq , and from C-NPDDL to C-NPDDL seq .

Proposition 14 .

 14 There is a polynomial-time translation from T-NNFAT to T-NPDDL, and from C-NNFAT to C-NPDDL.

Figure 1 :

 1 Figure 1: Tree (left) and circuit (right) representations of the same NPDDL seq action. Children are ordered from left to right; ϕ T (resp. ϕ C ) denotes a tree (resp. circuit) for ϕ. On the right diagram, nodes -p 1 and -p 3 are duplicated for readability.

Note that this is in contrast to the usual semantics of STRIPS, where addition would override deletion, thus "forgetting" -p

.

For instance, the bottom left ∪ node in the expression of Figure 1 (right) is executed twice along any execution of the action.

Acknowledgements

This work has been supported by the French National Research Agency (ANR) through project PING/ACK (ANR-18-CE40-0011).

PROOF. For L any of these languages, let α be an L expression and s, s be two states. Then s ∈ α(s) if and only if

is applicable in s. Indeed, β is just the action α executed simultaneously with the deterministic action which necessarily leads from s to s . Thus β is applicable in s if and only if α allows the transition from s to s . Now it is easy to see that β is indeed an L expression and can be built in polynomial time, which concludes the proof. PROOF. For membership, recall that deciding successorship is in NP for all the languages. Fix a language L. Suppose we are given a state s, a formula ϕ, and L-actions α 1 , . . . , α k .

To show that the given sequence of actions does not entail ϕ it is enough to guess a sequence of states s 1 , s 2 , . . . s k with s 1 ∈ α 1 (s), s 2 ∈ α 2 (s 1 ), . . . , s k ∈ α k (s k-1 ), and s k |= ϕ, and guess the corresponding certificates for s i ∈ α i (s i-1 ). Then the non-entailment can be verified in polynomial time.

For hardness, fix P = {p 1 , . . . , p n }. Observe that all languages can encode the "omnipotent" action a (∀s, a(s) := 2 P ) efficiently, either by α = p 1 ∨ ¬p 1 (for NNFAT) or by α = p∈P (+p ∪ -p). Now let ϕ be a 3-CNF formula over P. Then ϕ is not satisfiable if and only if all assignments to P satisfy ¬ϕ, which amounts to all α-successors of an arbitrary state (say s = / 0) satisfying ¬ϕ, which is indeed an entailment problem with a single action. Proposition 30. ENTAILS is PSPACE-complete for C-NPDDL seq . PROOF. Suppose we are given a state s ⊆ P, a formula ϕ over P = {p 1 , . . . , p n }, and α 1 ; . . . ; α k with α i in C-NPDDL seq . PSPACE-membership is obvious for the same reason as for IS-SUCC: we simulate every execution of α 1 ; . . . ; α k (each time using a polynomial amount of space) and check whether the resulting state satisfies ϕ. Now we recall that if a state has no successors through α then it entails any formula ϕ. Hardness follows from a reduction of the complement of IS-APPLIC to ENTAILS: α is not applicable in s if and only if α ; -p 1 entails ϕ in s, with ϕ := p 1 . Indeed, if α is applicable in s, then α ; -p 1 leads to at least one state s with p 1 / ∈ s , while if it not applicable in s, then all its successors (vacuously) satisfy ϕ.

Succinctness

We now give negative results about the existence of polynomial-size translations, hence about the relative succinctness of languages [START_REF] Darwiche | A knowledge compilation map[END_REF]. Recall that all the languages which we study are complete.

Our separation results use the nonuniform complexity class P/poly of all decision problems such that for all n ∈ N, there is a polynomial-time algorithm which decides the problem for all inputs of size n [START_REF] Arora | Computational complexity: a modern approach[END_REF]. The assumption NP ⊆ P/poly which we use is a standard one; in particular, NP ⊆ P/poly would imply a collapse of the polynomial hierarchy at the second level (Karp-Lipton theorem).

We start with NPDDL and NNFAT. Using Notation 20, for all n ∈ N we define the NPDDL (but not NSTRIPS) expression α sat n by

Intuitively, α sat n chooses an assignment (true or false) to each variable in X n (outermost ∪). Whenever it chooses an assignment for x, for each possible clause which is satisfied by this assignment (innermost ), it chooses whether to include this clause into the result, or not(innermost ∪). Hence it builds a formula which is satisfied at least by its choices, and clearly, any satisfiable 3-CNF formula can be built in this manner. Lemma 31. Let n ∈ N, and let ϕ be a 3-CNF formula over X n . Then ϕ is satisfiable if and only if s(ϕ) is an α sat nsuccessor of the state / 0. Proposition 32. There is no polynomial-size translation from T-NPDDL to T-NNFAT, nor from C-NPDDL to C-NNFAT, unless NP ⊆ P/poly holds. PROOF. The size of α sat n is clearly polynomial in n in both the tree and circuit representations. Assume that there is a polynomial-size translation f from T-NPDDL to T-NNFAT, and for all n ∈ N let β sat n = f (α sat n ). Then the following is a nonuniform polynomial time algorithm for the 3-SAT problem; given a 3-CNF ϕ : 1. encode ϕ into a state s(ϕ) as in Notation 20; 2. decide whether s(ϕ) is a β sat n -successor of the state / 0; 3. if yes, claim that ϕ is satisfiable, otherwise unsatisfiable. All steps are polynomial-time (Proposition 18), the algorithm is correct (Lemma 31), and it depends only on the number of variables in ϕ (which is polynomially related to its size), hence this is indeed a nonuniform polynomial time algorithm for 3-SAT. Hence NP ⊆ P/poly holds.

The proof is exactly the same for circuits. Before proceeding to show that NPDDL seq is strictly more succinct than NPDDL, we need the following technical result about restricting an action to pairs of states s, s which satisfy a given assignment to a subset of the variables. Lemma 33. Let P and Q be disjoint sets of variables, and α be a T-NPDDL (resp. C-NPDDL) expression for a (P ∪ Q)-action. Let t ⊆ Q be an assignment to the variables in Q. Then we can compute a T-NPDDL (resp. C-NPDDL) expression α |t for a P-action which satisfies Table 1: Summary of the complexity results for the queries. The languages (except NSTRIPS) are ordered according to their succinctness, i.e. the tree (circuit) representation of a language on the left is strictly less succinct than the tree (circuit) representation of a language on the right. We do not compare succincntess of tree and circuit representations.

PROOF. Simply replace all leaves of the form +q with q ∈ Q ∩ t by ε, all leaves of the form +q with q ∈ Q \ t by ⊥ (failure), and dually for -q, and for all subexpressions ϕ β , simplify ϕ by the assignment t to Q. (+p

where ψ n is the NNF N n i=1 (¬p i ∨ ∈γ i ), which is satisfied if and only if each clause γ i which is in ϕ (as witnessed by p i being true) is also satisfied. In words, γ sat n guesses an assignment to V(ϕ), then sets p sat according to whether ϕ is satisfied by this assignment, and finally resets all guessed variables to false. Note that γ sat n depends on n but not on ϕ, and that γ sat n is polynomial in n. Clearly, s(ϕ) ∪ {p sat } is a γ sat n -successor of s(ϕ) if and only if ϕ is satisfiable. Hence the following decision problem is NP-hard:

• Input: a 3-CNF formula ϕ • Question: is s(ϕ) ∪ {p sat } a γ sat n -successor of s(ϕ)? Now assume that there is a polynomial-size translation f from T-NPDDL seq to T-NPDDL. Fix n ∈ N, and let δ sat n = f (γ sat n ). Let ϕ be a 3-CNF formula. Since δ sat n is in NPDDL, we can apply Lemma 33 with Q = P n ∪ {p ϕ 1 , . . . , p ϕ n } and t = s(ϕ), to get an expression in which the only occuring variable is p sat , and {p sat } is a successor of / 0 if and only if s(ϕ) ∪ {p sat } is a δ sat n -sucessor of s(ϕ), that is, if and only if ϕ is satisfiable. Now since this expression has only one variable, it is easy to see that successorship can be decided in polynomial time, implying NP ⊆ P/poly.

The proof is exactly the same for circuits.