A Herzig
email: herzig@irit.fr

J Lang
email: lang@irit.fr

D Longin
email: longin@irit.fr

T Polacsek
email: polacsek@irit.fr

A logic for planning under partial observability

We propose an epistemic dynamic logic EDL able to represent the interactions between action and knowledge that are fundamental to planning under partial observability. EDL enables us to represent incomplete knowledge, nondeterministic actions, observations, sensing actions and conditional plans; it also enables a logical expression of several frequently made assumptions about the nature of the domain, such as determinism, full observability, unobservability, or pure sensing. Plan verification corresponds to checking the validity of a given EDL formula. The allowed plans are conditional, and a key point of our framework is that a plan is meaningful if and only if the branching conditions bear on the knowledge of the agent only, and not on the real world (to which that agent may not have access); this leads us to consider "plans that reason" which may contain branching conditions referring to implicit knowledge to be evaluated at execution time.

Introduction

A large amount of work has been done recently about planning under incomplete information. By incomplete information, we mean (as usual) that the initial state of the world is not fully known and/or the actions are not deterministic. The gap between planning under complete and incomplete information relies on the role of knowledge in the latter and especially the interactions between knowledge and action. These interactions work in both ways:

• the choice of an action to perform is guided by the knowledge the agent has on the actual state of the world, and especially by the observations made after performing previous actions. As soon as performance of an action allows gathering knowledge by a susbsequent observation, the choice of the following action will be generally conditioned by this observation.

• performing an action may bring some more knowledge (and help the agent acting in a better way, as explained just above) by means of consecutive observations; this has led many researchers to focus and formalize sensing actions, which do not change the state of the world but only the agent's beliefs.

On the other hand, the planning community has recently paid a lot of attention to the role of logic in representing and solving planning problems. This includes both (1) the SAT-PLAN framework [START_REF] Kautz | Planning as satisfiability[END_REF] and its very recent extensions to planning under incomplete knowledge (Rintanen 1999) and (2) the action description languages and their recent application to planning under incomplete knowledge [START_REF] Lobo | Adding knowledge to the action description language a[END_REF] [START_REF] Baral | Computational complexity of planning and approximate planning in the presence of incompleteness[END_REF]. The former (1) led to powerful resolution algorithms which benefit from the theoretical and experimental results on satisfiability. The latter (2) gave birth to very expressive languages that enable reasoning with nondeterminism, minimal change, ramifications, concurrent actions, and more recently interactions between action and knowledge. But so far these approaches did not lead yet to the practical development of planning algorithms based on automated proof procedures.

The question now consists of identifying the "simplest" logic containing the notions of incomplete knowledge, nondeterministic actions, observations, conditional plan and sensing actions. Two of these words evoque two well-known families of logics:

• dynamic logic aims at reasoning with complex combinations of actions (including sequential and conditional actions). Decidability and complexity results, as well as automated proof procedures for the standard propositional dynamic logic and its variants are a familiar part of the logical landscape. Still, surprisingly, dynamic logic has not been much considered for planning.

• epistemic logics aim at reasoning with explicit knowledge of an agent. Some simple epistemic logics are computationally not harder than classical logic.

What is missing to propositional dynamic logic (PDL) so as to render it suitable for planning under incomplete information is (1) the possibility for actions to have epistemic effects and (2) the possibility to branch on epistemic conditions. This second point needs some comments: indeed, PDL enables expressing some kinds of conditional actions, but these conditional actions are not suitable for expressing conditional plans, because while a program can be supposed to know at any instant the value of any variable, this is generally not the case for an agent acting in an incomplete environment, for whom some parts of the world are hidden (see e.g. [START_REF] Levesque | What is planning in the presence of sensing?[END_REF]).

Example 1 There are d doors. Behind exactly t of the doors, there is a tiger (t < d). Behind one (and only one) of the doors, there is a princess and no tiger. The agent has no prior knowledge about what is behind each of the doors (he only knows the values of d and t). The available actions are listening to what happens behind a given door, which results in hearing the tiger roaring if and only if there is one behind the door, and opening a given door, which may result in marrying the princess or being eaten by the tiger or nothing, depending on what is behind the door. The goal of the agent is to stay alive and marry the princess.

The propositional variables p(i) and t(i) mean respectively that there is a princess (a tiger) behind door i. Consider the following plan

π1: if p(1) then open(1) else if p(2) then open(2) (...)
Clearly, π 1 is not executable by the agent, because in general he does not know whether p(i) holds or not, and therefore he is unable to branch on such a condition. The solution is to allow for epistemic conditions only. Suppose therefore that our language contains a modal operator K. A plan such as

π2: if Kp(1) then open(1) else if Kp(2) then open(2) else (...)
can then be formulated. However, except when d = 1, it misses the goals, because the agent ignores whether p(i) is true or not, therefore he will not open any door. Thus, agents branch on epistemic conditions only, because they are able to decide whether they know a given formula or not, whereas they are not always able to decide whether this formula is true in the actual world.

This brings us to the following specificity of our logic: it enables the expression of plans that explicitely involve a reasoning task. For Example 1, the shortest succeeding plan (in terms of the average number of actions, given uniform probabilities for princess and tigers locations) can be expressed informally by: repeat (listen to a door and open if there is no tiger) until either the princess is delivered or the two tigers have been found; in this second case, open all remaining doors until the princess is discovered. Such a plan succeeds, but it explicits all branches and it is thus space-consuming: when d and t vary, the size of a valid plan increases exponentially1 . Now, the branching condi-tions of such plans are only conjunctions of elementary observations (those elementary observations are t(i) or ¬t(i)one of these is observed after listen(i) is performed), which means that, at any step of the execution, (i) the agent decides in unit time what is the next action to follow and (ii) he is not asked to reason (only to obey, to follow a fully explicited plan).

Let us now consider a plan π 4 where epistemic branching conditions are allowed.

We use the following abbreviations: It can be checked that π 4 reaches the goals. Interestingly, if d and t vary, there is a plan in the style of π 4 (using epistemic branching conditions) whose size is linear in d while any valid plan in the style of π 3 (with no epistemic branching conditions) has an exponential size. It is important to notice that this gain in size is counterbalanced by a loss of execution time: indeed, although π 1 -like plans have a size in O(2 d ), their execution time (assuming that actions are performed in unit time) takes only O(d). Contrastedly, for π 4 -like plans whose size is in O(d), their execution requires a linear number of calls to a NP-complete oracle (to compute "KnowWherePrincess" and "KnowWhereTiger"). Therefore, a plan with epistemic branching conditions is all the more interesting as the ratio between cost of space and cost of expensive on-line execution time is high.

KnowW hereP rincess = Kp(1) ∨ Kp(2) ∨ . . . ∨

An epistemic dynamic logic

Language of EDL

The language of epistemic dynamic logic EDL is constructed from a set of atomic formulas VAR, a set of atomic actions ACT 0 , the classical logic operators →, ∧, ∨, ¬, the epistemic operator K, the dynamic operator [.], and the action operators λ and ;. The formula [α]q is read "after the execution of the action α, q is true". Note that we allow for nested epistemic and dynamic operators. λ is the action "do nothing". The complex action α; β is read "execute α and then β". α A is an abbreviation of ¬([α]¬A), and

[if A then α else β]C is an abbreviation of (A → [α]C) ∧ (¬A → [β]C).
An EDL formula is • objective iff it does not contain any modality;

• static iff it does not contain any dynamic modality;

• an epistemic atom iff it is of the form KA, where A is any EDL formula;

• an epistemic formula iff it is formed from epistemic atoms and the connectives of classical logic.

For instance, a

∨ (b ∧ c) is objective; K(a ∨ ¬K(a → [α]b)) is an epistemic atom; K(a ∨ ¬K(a → [α]b)) ∨ ¬K[β]c is an epistemic formula; a∨¬K(b∧Kc) is static but not epistemic; Ka ∨ ¬K(b ∧ Kc) is both static and epistemic.

Semantics of EDL

The semantics of EDL is in terms of possible worlds (states).

We interpret the knowledge of the agent at a possible world w by a set of worlds associated to w. Actions are interpreted as transition relations on worlds. We define a model for EDL as a quadruple M = W, R K , {R α : α ∈ ACT 0 }, V where W is a set of possible worlds, R K ⊆ W × W and every R α ⊆ W × W is an accessibility relation 2 , and V associates to each world an interpretation. We require

• R K to be an equivalence relation on W , • R λ {w} = {w}, • R α;β = R α • R β , • R α • R K ⊆ R K • R α .
The truth conditions are defined as usual, in particular:

• |= M,w KA if |= M,v A for every state v ∈ R K (w) • |= M,w [α]A if |= M,w A for every state w ∈ R α (w)
Logical consequence (with global axioms) is noted |=.

Axiomatization of EDL

Our axiomatisation of EDL contains that of classical logic together with modal logics S5 for knowledge and K for actions.

N(K)

A KA

N([α]) A [α]A K(K) (KA ∧ K(A → C)) → KC T(K) KA → A 5(K) ¬KA → K¬KA Def(λ) [λ]A ↔ A Def(α; β) [α; β]A ↔ [α][β]A K([α]) ([α]A ∧ [α](A → C)) → [α]C Acq([α], K) K[α]C → K[α]KC
All the axioms are standard, except Acq([α], K) which means that if the agent knows what will be true after an action then he does not loose this knowledge after the action. Note that Acq([α], K) could be replaced by

K[α]C → [α]
KC to which it is equivalent given the other axioms.

2 We shall sometimes identify R K and Rα with mappings R K :

W -→ 2 W and Rα : W -→ 2 W .

Action and information

Our language is sufficiently expressive to distinguish explicitly between the ontic and the epistemic effects of actions, where ontic (respectively epistemic) effects are meant to be effects on the physical world only (resp. on the epistemic state of the agent only). Two particular classes of actions are uninformative actions whose effects are purely ontic and purely informative actions whose effects are purely epistemic. Intuitively, uninformative actions cannot bring any new knowledge, which means that everything that is known after the action is performed could be predicted before it was performed. The other way round, purely informative actions do not change the world. In our example, the actions listen(i) are purely informative, while the actions open(i) are not.

A key hypothesis of our logic is that any action α can be decomposed into two actions, namely α = α e • α o , where α e is purely informative and α o uninformative. open(i) can be written as open(i) e • open(i) o , where its uninformative component open(i) o has the effect of making the agent married, eaten, or none of both, without him being aware, and its informative component open(i) e has the effect to make the agent learn whether he gets married, eaten or none of both.

Given that α = α e • α o , what is the relation between α o and α e ? Ideally, all changes brought about by α o are perceived through α e . We call actions of this kind (i.e., actions informing the agent about all changes they cause) fully informant. Formally, α is fully informant iff for any objective formula A, we have that A → [α](¬A → K¬A) holds. Purely informative actions α are fully informant because the ontic part is empty, i.e. α o = λ. In our example open(i) is fully informant because it makes the agent aware of the change of truth value of eaten or married when it occurs.

Noticeably, these properties (purely informative, uninformative, fully informant) are about individual actions. Nevertheless, global properties of environments (domain descriptions) can be captured from local properties of actions. An environment Σ consists of a nonlogical theory T describing the general laws of the world and what is known about the effects of actions, together with the description of what is known about the initial state Σ Init . An environment Σ is fully observable iff (i) each α ∈ ACT 0 is fully informant, and (ii)

Σ Init is epistemically complete 3 . Σ is unobservable iff each α ∈ ACT 0 is uninformative. Σ is purely informative iff each α ∈ ACT 0 is purely informative. Σ is deterministic iff each α ∈ ACT 0 is deterministic.

Uninformative actions

We characterize uninformative actions by two axioms.

DetEpi([α], K) α KA → [α]KA Con([α], K) [α]KC → ([α]⊥ ∨ K[α]C)
The first expresses that uninformative actions are epistemically deterministic, in the sense that if there is a way of executing α such that A is known afterwards, then A should be known after every possible execution of α. This is natural, given that α does not bring any new knowledge (in particular about the way it has been executed). The second says that the epistemic effects of α are known before hand. Semantically, the axioms correspond to the conditions

• If w , w ∈ R α (w) then R K (w ) = R K (w ) • If R α (w) = ∅ and w 1 R K • R α w 2 then w 1 R α • R K w 2
It can be proved that these two axioms together are equivalent to the more compact criterion of uninformativeness ¬K[α]A → [α]¬KA. It says that the agent cannot observe anything after α is performed: indeed, for any formula A, if he cannot predict before α is performed that A will hold after α, then he will not know A after α is performed. Acq([α], K) together with Con([α], K) gives us the equivalence

[α]KC ≡ ([α]⊥ ∨ K[α]C).

Purely informative actions

Purely informative actions do not change the world but only the knowledge; they are characterized by the axiom

Pres([α])

A → [α]A if A is an objective formula.

Semantically, this corresponds to the condition

• if w 1 R α w 2 then V w1 = V w2
It follows from Acq([α], K) and standard modal principles that purely informative actions do not diminish the knowledge of an agent. Proposition 1 Let A be an objective formula and α a purely informative action. Then

Pres([α], KA → [α]KA is provable from EDL.
If A is subjective then this does not necessarily hold, in particular if A expresses ignorance. For example K¬KA → [α]K¬KA cannot be accepted, given that K¬KA ↔ ¬KA is valid in our logic of knowledge S5.

A solution to the Frame Problem

We must solve the Frame Problem in order to put to work our logic. Basically, we could integrate any solution into our framework, given that we have analysed the epistemic effects of an action in terms of its ontic effects on possible worlds. Scherl and Levesque e.g. used Reiter's solution to the Frame Problem, and applied regression as a reasoning method [START_REF] Scherl | The frame problem and knowledge-producing actions[END_REF]. We adopt the solution in [START_REF] Castilho | Formalizing action and change in modal logic I: the frame problem[END_REF]) based on dependence relations, which can be taken over without modifications and which we briefly recall here.

We associate to every atomic action α the set of atomic formulas it influences. listen(1)]t(1) andp(2) → [listen(1)]p(2). Combining all these atomic frame axioms by principles of classical logic, we obtain the following.

Proposition 2 Let A be objective, and let atm(A) be the set of atoms of A. If atm(A) ∩ DEP (α) = ∅ then:

• |= DEP A → [α]A; • |= DEP KA → [α]KA.

Plan verification in EDL

The set of meaningful plans is the smallest set such that • α is a meaningful plan for every α ∈ ACT 0 ∪ {λ};

• if π and π are meaningful plans and A is an epistemic formula then π; π and if A then π else π are meaningful plans.

Intuitively, a meaningful plan is a plan whose branching conditions are "epistemically interpretable", which means that the agent can decide whether the branching condition holds or not (which would not necessarily be the case if the formula were not epistemic, cf. example).

A plan verification problem V is defined by a 5-tuple T, Σ Init , DEP, G, π where

• T = S, E, X is an EDL theory composed of a set of state axioms S expressing static laws of the domain, laws about the effects of actions E, and executability laws X.

Static laws are static formulas; effect laws are formulas of the form A → [α]C with A objective and C an epistemic formula; executability laws are formulas of the form A ↔ α with A objective.

• Σ Init is an epistemic atom;

• DEP is a dependency function;

• G is a static formula (the goal);

• π is an meaningful plan.

Given a plan verification problem V, π is said to be

• executable for V iff T |= DEP Σ Init → π holds. • valid for V iff T |= DEP Σ Init → [π]G holds.
The validity problem in EDL is PSPACE-hard, and the consequence problem is EXPTIME-hard. The reason is that EDL extends modal logic K, where these problems are PSPACEand EXPTIME-complete, respectively. Nevertheless, the complexity of the much more specific plan verification problem in EDL is much lower:

Proposition 3 (complexity of plan verification) PLAN VERIFICATION in EDL is Π p 2 -complete.
Note that if branching conditions were restricted to elementary conjunctions of observations instead of any epistemic conditions then the problem would be "only" coNPcomplete.

It is worth investigating what plan validation becomes when some specific assumptions are made about observability.

Unobservable environments When the environment is unobservable, we can show by induction that uninformativeness extends to any meaningful plan: for any meaningful plan π and any objective formula A, ¬K[π]A → [π]¬KA holds, which leads to the following intuitive result: if there is a meaningful valid plan π for V = T, Σ Init , DEP, G then there is a nonbranching (i.e., without tests) meaningful valid plan for V.

Fully observable environments When the environment is fully observable, we can show by induction that for any meaningful plan π and any objective formula A, we have [π](KA ∨ K¬A) holds, and that the epistemic operator is needless, which is expressed intuitively by the following result: if there is a meaningful valid plan π for V then there is an epistemic-free (e.g., without any occurrence of K) meaningful valid plan for V. Thus, a fragment of PDL is sufficient for capturing plan verification in fully observable environments.

Purely epistemic environments When the environment is fully epistemic, all actions are commutative and knowledge preserving. This leads to the following result: if there is a meaningful valid plan π for P then α 1 ; α 2 ; ...; α n is a valid plan for P, where ACT 0 = {α 1 , ..., α n }.

We end up the section with some considerations on plan existence. Informally, the plan existence problem reads: given P = T, Σ Init , DEP, G , is there a plan π for P? Similar to verification problems, we check whether there is a proof of T, ¬G |= DEP ¬Σ Init . If this is the case, then we can associate a meaningful executable plan π to P. π can then be checked for validity (which will not always be the case, in particular when actions are nondeterministic). π is certainly only a first step towards a plan. We leave this issue to further research.

Example

How we can handle our running example in our logic? For the sake of readability, suppose d = 2 and t = 1. A meaningful valid plan is Proving the validity of π 2,1 amounts to proving that the formula T |= DEP Σ Init → [π 2,1 ](married ∧ alive) is a theorem, where the initial situation Σ Init is

ΣInit = alive ∧ ((t(1) ∧ ¬t(2) ∧ p(2))∨ (t(2) ∧ ¬t(1) ∧ p(1)))
and T is the nonlogical theory of the domain, consisting of the following set T of effect axioms:

T = { t(i) → [listen(i)]Kt(i), ¬t(i) → [listen(i)]K¬t(i), p(i) → [open(i)]married, t(i) → [open(i)]¬alive, (¬p(i) ∧ ¬married) → [open(i)]¬married, (¬t(i) ∧ alive) → [open(i)]alive, listen(i) , open(i) }.
(where we suppose i ∈ {1, 2}).

Related work and conclusion

There is a significant amount of related work about the interactions between action and knowledge, both in the KR and the planning communities. Combining knowledge and action in a logical framework comes back to the work of [START_REF] Moore | A formal theory of knowledge and action[END_REF] who provided a theory of action including knowledge-producing actions. Building on this theory, [START_REF] Scherl | The frame problem and knowledge-producing actions[END_REF]) represent knowledge-producing actions in the situation calculus by means of an explicit accessibility relation between situations, treated as an ordinary fluent, that corresponds to our epistemic accessibility relation. [START_REF] Levesque | What is planning in the presence of sensing?[END_REF] then uses this knowledge fluents to represent complex plans involving, like ours, nondeterminism, observations and branching (and also loops, that we did not consider). He points out that the executability of a plan requires that the agent needs to know how to execute it, which implies that branching conditions must involve knowledge and not objective facts whose truth may not be accessible to the agent. On the one hand, in our logic, consisting of a fragment of propositional PDL extended with epistemic modalities to represent the effects of actions, the interactions between dynamic and epistemic modalities enable a simple representation of various observability assumptions; on the other hand, by using the situation calculus, Levesque handles more easily than us value tests returning the value of a variable (for instance, he is able to represent in a simple way a plan such as search Mary's phone number in the phonebook and then dial it whereas we cannot do it unless we write down a finite but unreasonable amount of propositional formulas). This approach was extended in [START_REF] Lakemeyer | AOL: a logic of acting, sensing, knowing, and only knowing[END_REF]) so as to introduce the only knowing modality. [START_REF] Bacchus | Modeling an agent's incomplete knowledge during planning and execution[END_REF] point out the practical impossibility to generate explicit conditional plans, because they get too large, and thus advocate for the need of reasoning about knowledge during plan execution, which is one of the key points of our logic. Their representation model makes use of an epistemic modality. Our approach could be thought of as being complementary to theirs, because we provide a simple way to represent various kinds of interactions between knowledge and action while they focus on the practical computation of the effects of a plan contain-ing sensing actions and knowledge preconditions. [START_REF] Geffner | Modeling action, knowledge and control[END_REF] provide a general language enabling representing nondeterministic actions, sensing actions, observations and conditional plans. Their notion of executable policy is very similar to our notion of meaningful plan, though it is not expressed the same way technically speaking: to avoid generating unreasonably large policies (which happens whenever all accessible belief states are explicitely considered), they express policies on states rather than on belief states; a policy is then said to be executable in a belief state Bel if, roughly speaking, it assigns equivalent actions to all states considered possible in Bel. We choose another way to escape representing explicitly conditional plans, namely by calling for reasoning tasks during execution. [START_REF] Lobo | Adding knowledge to the action description language a[END_REF] extend Gelfond and Lifschitz' language A for reasoning about action so as to represent knowledge effects. An interesting notion in their approach is knowledge removing actions that may affect the knowledge the agent has on a fluent. These knowledge removing actions (such as toss) can be easily handled in EDL.

These approaches focus on representing actions and conditional plans involving knowledge preconditions and effects, and checking whether a given plan reaches the goal. Up to know, little has been done in order to generate plans having knowledge preconditions. [START_REF] Rintanen | Constructing plans by a theorem prover[END_REF] extends the planning as satisfiability framework to planning under incomplete knowledge by means of Quantified Boolean Formulae. [START_REF] Boutilier | Computing optimal policies for partially observable decision processes using compact representations[END_REF] provide a propositionallike representation and resolution framework for POMDPs. None of these works makes use of epistemic nor dynamic modalities.

Lastly, a few authors developed logical systems integrating dynamic and epistemic modalities, but not from a planning perspective. [START_REF] Del Val | Qualitative reasoning about perception and belief[END_REF] study from a logical perspective the relations between what the agent perceive and what they believe; this is much related to our logical expressions of observability assumptions in EDL. [START_REF] Fagin | Reasoning about knowledge[END_REF]) have a language with temporal 'next' and 'always' operators instead of action operators. They have axioms of perfect recall similar to our Acq([α], K) (axioms KT1, KT2). They do not integrate a solution to the Frame Problem into their approach. Also slightly related to our work is [START_REF] Meyer | Test as epistemic updates[END_REF] who consider tests as epistemic updates.

Apart from the handling of plan existence, further work includes the study of the complexity of validity for the full logic EDL (so far we only have a complexity result for plan verification in EDL) and next, the complexity of plan existence with epistemic preconditions, which would complete the panorama of complexity results for planning under incomplete knowledge [START_REF] Littman | Probabilistic planning: representation and complexity[END_REF][START_REF] Baral | Computational complexity of planning and approximate planning in the presence of incompleteness[END_REF].

  Formally, we suppose given a dependency function DEP : ACT 0 -→ VAR. p ∈ DEP (α) means that α may change the truth value of the atom p. The other way round, if p ∈ DEP (α) then α does not change the truth value of p. In other words, DEP represents frame axioms in an economic way. This is expressed by the generic frame axiom Pres DEP ([α]) if p ∈DEP (α) then p →[α]p and ¬p →[α]¬p Semantically, the axiom corresponds to the condition • For all w, w ∈ W and p ∈ VAR, if w ∈ R α (w) and p ∈ DEP (α) then |= M,w p iff |= M,w p. Given a dependence relation DEP , |= DEP is the corresponding extension of theEDL consequence relation. As a particular case, purely informative actions verify DEP (α) = ∅. Thus, we have for instance the frame axioms t(1) → [

π2, 1

 1 = listen(1); if Kt(1) then open(2) else open(1)

  Moreover, let DEP (listen(i)) = ∅ and DEP (open(i)) = {married, alive}. (The dependence-based solution to the Frame Problem requires the last two conditional frame axioms of T .) We establish that T |=DEP ΣInit → [π2,1](married ∧ alive) by proving T |=DEP (t(1) ∧ ¬t(2) ∧ p(2) ∧ alive) → [π2,1](married ∧ alive) and T |=DEP (t(2) ∧ ¬t(1) ∧ p(1) ∧ alive) → [π2,1](married ∧ alive). Then the disjunction of the respective antecedens is nothing but Σ Init , and since (Kt(1) ∧[open(2)](alive ∧ married))∨ (K¬t(1) ∧ [open(1)](alive ∧ married)) is equivalent to [listen(1); if Kt(1) then open(2) else open(1)](alive ∧ married), putting things together we obtain what we wanted.

  Kp(d) and KnowW hereT igers =

	(Kt(1) ∨ K¬t(1)) ∧ . . . ∧ (Kt(d) ∨ K¬t(d)) and we define the
	procedures:
	OpenIf KnowW hereP rincess:
	if Kp(1) then open(1) else if Kp(2) then
	open(2)...
	OpenIf KnowW hereT igers:

if K¬t(1) then open(1); if ¬Kmarried ∧ K¬t(2) then open(2); ... π4:listen(1); listen(2); if ¬KnowW hereP rincess ∧ ¬KnowW hereT igers then listen(3); if KnowW hereP rincess then OpenIf KnowW hereP rincess else OpenIf KnowW hereT igers

This is because the evaluation of the condition "the d tigers have been found" after having listened to k doors needs counting the tigers heard so far, which needs explicitly listing the ( k t ) corresponding cases.

i.e. if ΣInit |= KA ∨ K¬A for all objective A


Gabriela Demarchi

Julie Subervie

Thibault Catry

Isabelle Tritsch

Using publicly available remote sensing products to evaluate REDD+ projects in Brazil

Keywords: REDD+, remote sensing products, additionality, deforestation, Brazilian Amazon

come

Forest cover change is a leading cause of Brazil's greenhouse gas emissions. 1 As a result, there has been a proliferation of sub-national initiatives financed by the United Nation's REDD+ (Reducing Emissions from Deforestation and forest Degradation) mechanism in the Brazilian Amazon for some years [START_REF] Sills | REDD+ on the ground: A case book of subnational initiatives across the globe[END_REF]. Brazil currently hosts about 50 REDD+ projects targeting small farmers and financed by REDD+ funds or carbon markets [START_REF] Simonet | REDD+ projects in 2014: an overview based on a new database and typology[END_REF]. The perpetuity and improvement of REDD+ projects require rigorous impact evaluations of their effectiveness. Yet, robust evidence about their effectiveness on reducing deforestation remains scarce [START_REF] Jayachandran | Reduce Deforestation[END_REF]Simonet et al., 2018b;[START_REF] Roopsind | Evidence that a national REDD+ program reduces tree cover loss and carbon emissions in a high forest cover, low deforestation country[END_REF]. One of the reasons for this lack of evidence is related to the high cost to access the data needed for impact analysis [START_REF] Blackman | Evaluating forest conservation policies in developing countries using remote sensing data: An introduction and practical guide[END_REF][START_REF] Pagiola | Evaluation of the permanence of land use change induced by payments for environmental services in Quindío, Colombia[END_REF].

Over the past 20 years, however, remotely-sensed data for detecting changes in land cover worldwide has evolved dramatically, which offered new opportunities for the evaluation of forest conservation programs. In particular, a number of derived and modelled remote sensing (RS) products that extract information from raw earth observation (EO) data became publicly available [START_REF] Kugler | People and Pixels 20 years later: the current data landscape and research trends blending population and environmental data[END_REF]. Though these RS products represent a great opportunity to measure changes in forest cover at a large scale, the suitability of these readily available data-sets to perform proper impact evaluations of sub-national REDD+ initiatives has rarely been questioned so far [START_REF] Bos | Global data and tools for local forest cover loss and REDD+ performance assessment: Accuracy, uncertainty, complementarity and impact[END_REF].

For the present study, we focus on two well-known data-sets: the Global Forest Change (GFC) dataset provided by the University of Maryland and the PRODES data-set provided by the National Institute for Space Research (INPE) of Brazil. GFC provides free of charge global historical record of annual tree-cover loss and has already been used to assess the effectiveness of forest conservation policies in Ecuador [START_REF] Jones | Estimating the counterfactual impact of conservation programs on land cover outcomes: The role of matching and panel regression techniques[END_REF][START_REF] Jones | Forest conservation incentives and deforestation in the Ecuadorian Amazon[END_REF] and French Guyana [START_REF] Roopsind | Evidence that a national REDD+ program reduces tree cover loss and carbon emissions in a high forest cover, low deforestation country[END_REF]. In the Brazilian context however, the most often used deforestation data-set has been PRODES, an accessible and transparent RS product, provided free of charge as well. In particular, it has been employed in particular to study the effectiveness of protected areas on avoiding deforestation in the Amazon [START_REF] Nolte | Governance regime and location influence avoided deforestation success of protected areas in the Brazilian Amazon[END_REF][START_REF] Herrera | Impacts of protected areas vary with the level of government: Comparing avoided deforestation across agencies in the Brazilian Amazon[END_REF].

In this study, we assessed the applicability of these two RS datasets to evaluate the impact of REDD+ local projects targeting smallholders in the Brazilian Amazon. To do so, we concentrated on a Brazilian REDD+ flagship project for curbing deforestation, the Sustainable Settlements in the Amazon (SSA) project, which offered technical assistance and conditional payments to 350 households for maintaining forest cover on at least half of their land between 2012 and 2016 (see SI Appendix for details). We focused on a local REDD+ program implemented in a country characterized by the highest annual loss of forest in the world. This project has already been evaluated by Simonet et al. (2018a) using survey data collected at the early stage of the program. The authors found that an average of 4 ha of forest were saved on each participating farm in 2014. 2 A potentially important caveat in this study, however, is the extent to which participants might have under-declared their actual deforestation (compared to non-participants). RS data does not suffer from such problem. 3 RS data also have at least three additional advantages over survey data. First, using RS data generally makes it possible to run analysis from larger samples than those available from surveys, thus affording increased statistical power, for a much lower access cost. In the case of the SSA project, this means that we can estimate the forest loss on the individual plots of the entire population of participants, rather than a sample of them.

Second, using RS data allows us to estimate what would have been the forest loss on these farms in the absence of any program (the so-called counter-factual situation) with more precision. To make valid inferences about participants, there must be a sufficient number of non-participants with a high potential to be selected as matched counterparts. Using RS data allows access to a larger pool of candidates for the matching procedure, which increases the probability of finding good matches. 4 Third, the use of RS data allows us to study the effects of the program several years after its end. It is very expensive to collect information in the field repeatedly, over a long period. For this reason, the analysis based on survey data generally do not provide evidence of the permanence of the effects of conservation programs. On the contrary, RS data make it possible to study the long-term effects of conservation programs, from their early stage of implementation to the most recent period, by highlighting, if they exist, the effects of attenuation, rebounds, or compensation, which may arise after the program ends.

So far, a number of programs for forest conservation or reforestation have been evaluated applying microeconometric methods to RS data (see [START_REF] Pattanayak | Show me the money: do payments supply environmental services in developing countries?[END_REF]; [START_REF] Samii | Effects of payment for environmental services and decentralized forest management on deforestation and poverty in low and middle income countries: a systematic review[END_REF]; Alix-Garcia and [START_REF] Wolff | Payment for ecosystem services from forests[END_REF]; [START_REF] Börner | The Effectiveness of Payments for Environmental Services[END_REF] for reviews of the literature). Most studies have been conducted in Costa Rica [START_REF] Sanchez-Azofeifa | Costa Rica's payment for environmental services program: intention, implementation, and impact[END_REF][START_REF] Arriagada | Do payments for environmental services affect forest cover? A farm-level evaluation from Costa Rica[END_REF][START_REF] Garbach | Payment for ecosystem services: the roles of positive incentives and information sharing in stimulating adoption of silvopastoral conservation practices[END_REF][START_REF] Robalino | Ecopayments and Deforestation in Costa Rica: A Nationwide Analysis of PSA's Initial Years[END_REF] and Mexico (Honey-Rosés, Baylis, and Ramirez, 2011;[START_REF] Scullion | Evaluating the environmental impact of payments for ecosystem services in Coatepec (Mexico) using remote sensing and on-site interviews[END_REF][START_REF] Shapiro | Forest conservation and slippage: Evidence from Mexicoâs national payments for ecosystem services program[END_REF][START_REF] Sims | Improving environmental and social targeting through adaptive management in Mexico's payments for hydrological services program[END_REF][START_REF] Sims | Only one tree from each seed? Environmental effectiveness and poverty alleviation in Mexico's Payments for Ecosystem Services Program[END_REF][START_REF] Costedoat | How effective are biodiversity conservation payments in Mexico?[END_REF]. 5 2 Simonet et al. (2018a) moreover showed that this conservation came at the expense of pastures rather than croplands. This amounts to a decrease in the deforestation rate of about 50 percent. They find no evidence of within-community spillovers.

3 RS deforestation data can suffer from measurement and classification errors, but there is no reason a priori for these errors to be more frequent on the plots enrolled in conservation programs. 4 This is referred to as the common support assumption. Those non-participants who displayed a pattern identical to that of the participants during the period preceding the program typically have high potential to be selected as counter-factual in the matching procedure. The larger the pool of non-participants, the more likely the common support hypothesis is to hold. 5 Those programs typically offer conditional payments to participants. Overall, the results of these studies

As for REDD+ programs, recent impact evaluations include a study by [START_REF] Jayachandran | Reduce Deforestation[END_REF] in Uganda using remote-sensed data developed from QuickBird satellite images, [START_REF] Mohebalian | Beneath the Canopy: Tropical Forests Enrolled in Conservation Payments Reveal Evidence of Less Degradation[END_REF] in Ecuador using remote-sensed data developed from Landsat TM images, and [START_REF] Roopsind | Evidence that a national REDD+ program reduces tree cover loss and carbon emissions in a high forest cover, low deforestation country[END_REF] in Guyana using the GFC data-set. Overall, the results of these studies suggest that the impact of REDD+ programs on forest loss may be large. [START_REF] Jayachandran | Reduce Deforestation[END_REF] indeed find that tree cover in Uganda declined by 4.2 percent during the two-year period under study in treatment villages, compared to 9.1 percent in control villages, thus reporting a 54 percent decrease in deforestation rates. [START_REF] Roopsind | Evidence that a national REDD+ program reduces tree cover loss and carbon emissions in a high forest cover, low deforestation country[END_REF] estimate that the annual tree cover loss was 0.056 percent in Guyana against 0.087 percent in the synthetic counter-factual, thus reporting a 35 percent decrease in annual deforestation rates thanks to the program.

Our with the main objective to quantify and geolocalize deforestation in the Brazilian Legal Amazon 6 and help the Brazilian government to make informed decisions and establish environmental and development public policies for the region 7 [START_REF] Câmara | Metodologia para o cálculo da taxa anual de desmatamento na Amazônia Legal[END_REF]. Annual rates are estimated from the deforestation increments identified in Landsat images 8 . PRODES uses the seasonal year, starting on August 1st, to calculate annual deforestation, so images are selected as near to this date as possible. Next, the images are masked to exclude non-forest, previous deforestation, and water using the previous year's analysis.

suggest that the impact of the programs on the average annual forest cover varies substantially across regions (Simonet et al., 2018a). 6 The Brazilian Legal Amazon occupies an area that corresponds to 59 percent of the Brazilian territory. 7 PRODES' data are employed in: (1) certification of agribusiness supply chains such as the Soy Moratorium; (2) national inventory reports on GHG Emissions; and (3) monetary donations from the Amazon Fund uses PRODES's data as a reference for deforestation activity in the Legal Amazon.

8 PRODES uses mainly Landsat series images, but when there's too much cloud coverage, analysts employ SENTINEL-2 and CBERS-4 images.

Finally, the identification of deforestation is done by photo-interpretation, where analysts delineate deforested polygons in the intact forest of the previous year -the patterns of clear cutting are based on three main observable elements present in the images: tone, texture and context (see INPE (2019b) for a detailed description of PRODES' methodology).

Like any RS product, PRODES has some technical limitations because its methodology (entirely done by visual photo-interpretation) can only detect contiguous areas of cleared forest that are greater than 6.25 hectares. Therefore, smaller deforestation patches and forest degradation due to logging are not recorded in the dataset unless accumulated over several years. Also, deforestation estimates only consider primary forests and do not account for secondary or regenerating forests, and, since it relies on optical imagery, constant cloud coverage prevents Landsat sensors from capturing land cover imagery.

The Global Forest Change dataset (GFC)

The most known global deforestation dataset currently available is the University of Maryland's Global Forest Change data-set (GFC) -also popularly called Hansen data. This dataset has the objective to produce annual globally consistent characterizations of tree cover loss [START_REF] Hansen | High-resolution global maps of 21stcentury forest cover change[END_REF]. GFC maps annual forest loss starting in 2001. The maps produced by the GFC initiative are also based on the Landsat satellite images, but the classification process is 100% automated. The classification process of cloud-free Landsat image mosaics is carried out using decision tree algorithms. As the classification is carried out pixel by pixel, the minimum area mapped by this product is 900 square meters (30 x 30 meters).

For this dataset tree-cover is defined as all vegetation taller than 5 meters in height across a range of canopy densities (from 0 percent to 100 percent) for an area of approximately 0.1 hectare (equivalent to a Landsat pixel). Therefore, this layer can represent primary and secondary natural forests as well as tree plantations. Also, this data-set require users to choose a percentage threshold value to determine whether a pixel is considered forest or not. Forest loss is defined as the complete removal of tree cover canopy at the Landsat pixel scale (see [START_REF] Hansen | High-resolution global maps of 21stcentury forest cover change[END_REF] for complete methodological explanation).

While GFC is a major progress in the understanding and quantification of global forest change research and conservation planning there exist limits of this dataset. First, tree cover loss can be the result of human activities (e. g., plantation harvesting, selective logging and clear-cut) as well as natural causes (such as disease, storm and fire damage). Second, plantations such as, cocoa, palm oil or eucalypt are included as forests [START_REF] Tropek | Comment on âHigh-resolution global maps of 21st-century forest cover changeâ[END_REF], though they are not considered forest according to the Brazilian Forest Code.

The purposes and methodologies of PRODES and GFC are quite diverging (Table 1).

Firstly, GFC includes forest changes in every type of vegetation greater than 5 m in height while PRODES only focuses on primary forest loss. Secondly, GFC is a global dataset while PRODES only focuses on the Brazilian Amazon. Finally, PRODES's methodology is based on contextual classification (i. e., image segmentation and analyst interpretation) and GFC's methodology is grounded on pixel-based classifications (i. e., automated decision tree).

There is therefore no reason a priori for the information relating to the loss of forest provided by the two products to coincide.

Results

Comparing deforestation estimates from both data-sets

A paired t-test of annual differences in deforestation revealed significant difference between the PRODES and GFC data for the years 2008 to 2018, the only exception is the year of 2015 (SI Appendix, Table 1). Furthermore, GFC detects higher rates of deforestation than PRODES for all years except 2010 and 2011. Also, several spatial differences emerged when comparing the GFC and PRODES data. To highlight these differences, we aggregated deforestation pixels for the 2008-2017 period from PRODES and GFC data into binary raster layers. To measure the spatial consistency between the two RS products, we overlapped both layers and performed validation samples of the areas of agreement and conflict between the two input map products. Overall, the extent of the match between the two products appears rather small. We found that datasets have a 39 percent agreement at the municipality scale, a 36 percent agreement at the settlement scale and a 27 percent agreement at SSA plot's scale. This low spatial agreement between the two products suggests that one or both products may not be suitable for monitoring deforestation under REDD+ programs. This, however, does not necessarily call into question the interest of these products for evaluating the effectiveness of REDD+ programs in curbing deforestation. Indeed, it is possible that the level of precision of the forest loss measurement is nevertheless sufficient for a significant difference to be detected between the participating plots and the control ones (if this difference exists).

Additionality of the REDD+ initiative

We identified the causal effect of the SSA program using a matching approach that uses pretreatment outcomes to correct for selection bias. The results of the estimates of the ATT are displayed in Table 2 in Appendix. According to GFC data, the ATT ranges between -0.38 and -0.57 hectares for the year 2013, between -0.76 and -0.91 ha for the year 2014 and between -0.42 and -0.77 ha for the year 2015, suggesting that the SSA project prevented about 1.86 hectares of forest, on average, from being cleared on each participating farm during the first three years of the SSA program. Similarly, we find significant negative point estimates using PRODES data. The ATT ranges between -0.48 and -0.57 ha for the year 2014, between -0.87 and -1.19 ha for the year 2015 and between -0.59 and -0.93 ha for the year 2016, implying that the program prevented around 2.24 of forest from being cleared during these years on each enrolled plot.

The results for the estimations are shown graphically on Figure 1. According to GFC dataset, the participant group deviates significantly from the trajectory of the control group from 2012, until 2015. The same phenomenon is demonstrated with PRODES data (with one-year lag). Under the hypotheses that we made when constructing the control groups, this clear break in the deforestation trend among participants can be attributed to the SSA program.

Permanence of the effects of the REDD+ initiative

We failed to detect a significant impact of the program for the years 2016, 2017 and 2018 using GFC data and for the years of 2017 and 2018 using PRODES data. The fact that the ATT becomes insignificant as the program comes to an end, indicates that the treated group, whose trajectory had diverged from that of the control group, go back to the same behaviour after three years. This is clearly illustrated in Figure 1, which shows that the trajectory of the treated group joined that of the control group -the two curves overlap again -from 2016 (or 2017, depending on the dataset used).

These results suggest that the gains achieved by the program until 2018 represent a 3-year delay in the deforestation that otherwise would have occurred in the absence of the program.

This mean that we are in the scenario where the program participants consented to modify their behaviour during the duration of the program, only to return to the business-as-usual pattern after the end of the program. This suggests that the intervention was not sufficient to trigger long-lasting change in farmers' behaviour. It is however important to mention that we do not detect a higher rate of deforestation in the participating group than the control group after the end of the program, meaning that participants did not catch up on their postponed deforestation (at least not until 2018). Thus, the environmental gain generated during the three first years of the program was not subsequently destroyed. It lasts at least until 2018, when our analysis ends.

Spillover effects of the REDD+ initiative

In any conservation program targeting individuals, the possible presence of spillover effects, i.e. an impact of the program on individuals who were not initially targeted by the program but were exposed to, must be considered. In the case of the SSA program, these individuals are farmers who have not signed any PES contracts, but who have been able to benefit from some non-financial components of the program, such as information campaigns or free registration in the rural registry (see SI Appendix for details about the SSA program). Moreover, the development of low deforestation activities among participants in the PES program may have benefited surrounding families on the adoption of new practices, access to inputs, and increasing labour demand.

To test for the presence of such spillovers, we focused on the deforestation that may have occurred in the plots surrounding participating farms. Therefore, we assessed the impact of the program on those 3,793 farm-holds that were less than three kilometres distant from a treated one. We applied the same identification strategy to these potential beneficiaries of the program as that applied to the treated plots. The results are displayed in Table 3 in the SI Appendix. We found that that tree cover loss on plots surrounding participating farms between 2013 and 2015 was lower than forest loss on control plots, suggesting that the program indeed had a positive spillover effect of avoiding about one hectare of deforestation on average on each surrounding plot.

Cost effectiveness of the REDD+ initiative

Following to [START_REF] Jayachandran | Reduce Deforestation[END_REF] and Simonet et al. (2018a), we calculated the value of the carbon benefit over the 2013 to 2018 period using the Social Cost of Carbon (SSC) and compared this value to the program's costs. The benefits of the SSA project were computed by using our estimates of the additionality in terms of hectares of forest saved thanks to the program. We computed the average stock of carbon in our study area, using the estimates of biomass provided by the World Resources Institute, i.e. 116 tons of CO2 aboveground per hectare of forest with at least 50 percent tree cover. We found that the program had avoided the emission of 309,746 tons of CO2.

The costs of the PES component of the SSA project were computed using the amount disbursed to participants from 2014 to 2017 (626 USD per participant), which lead to 838,849 USD of discounted costs (using a 3 percent discount rate). By relating this expenditure to the emissions avoided, we found that the cost of the project was thus 2.8 USD per ton of CO2 emissions avoided. By then computing the value of the carbon benefit using the SSC, we finally found that the discounted benefit of the avoided emissions was about 1,255,976 USD, which gives us a benefit/cost ratio of about 1.5, meaning that one dollar invested in the program would have translated into a dollar and a half of environmental gain. Such estimate, however, does not take into account the start-up and operational costs of the program, nor the gains generated by the spillover effects. When all the costs are included, 9 the total (discounted) project costs over the 2012-2017 period reaches 8,607,246 USD. On the other side, the total of avoided emissions including the positive spillover gain, reaches 1,924,490 tons of CO2. This brings us to a new estimate of the cost of the program, which this time would amount to 4.47 USD per ton. Using again the SSC, we find that the discounted benefit of the avoided emission would be about 9,086,840 USD, that is to say a benefit/cost ratio of about 1.1. Again, this suggests that the program may well have been cost-effective.

Discussion

Remote-Sensing products

The divergence that we found between the two RS products can be partially explained by methodological differences in the construction of the products. First, small deforestation is not incorporated within PRODES estimates (because deforestation activities are only reported if they accumulate beyond the 6.25-hectare threshold), while it can be detected more easily in GFC. Second, GFC estimates detects secondary forest clearings, while PRODES does not. Third, some of the cover loss reported in GFC dataset may be due to forest degradation (e.g. such as forest fires and selective logging), something that is less likely to occur with PRODES estimates. All this may explain why GFC often detects higher rates of deforestation than PRODES. This result calls for at least two comments. The first one is that neither of the two products seems to completely outperform the other. PRODES estimates are validated in the field but are not able to account for small deforestation operations. GFC, on the other hand, can detect small patches, but sometimes wrongly, when it is not strictly deforestation. This should encourage REDD+ project evaluators to cross-validate their results using multiple datasets when available.

The second comment relates to the suitability of PRODES and GFC products for the evaluation of REDD+ programs. Incontestably, any deforestation RS product may contain classification errors and deforestation area estimates that diverge from reality. Does this mean that these products are of no use in properly estimating the impact of PES programs targeting smallholders who own a hundred hectares or less? Although these products do not seem suitable for the fine monitoring of this type of program, our analysis nevertheless suggests that they make it possible to assess the effectiveness of a PES program. This can be done provided that (i) the impact of the program is large enough to be detected despite the lack of precision of the RS products and (ii) the noise caused by the imprecision of the RS product estimates is distributed normally between the treated and control plots, so that it is net out through the comparison between the two groups.

Local REDD+ effectiveness

We assessed the impact of SSA project over 2013-2018 and estimated that an average of about 2 hectares of forest were saved during the early years of SSA project on each participating farm, regardless the source of deforestation data used. Even though the size of the estimated effect is smaller than the one estimated using survey data by Simonet et al. (2018a), it is quite similar in magnitude to those found for other PES-based forest conservation programs run in Latin America [START_REF] Robalino | Ecopayments and Deforestation in Costa Rica: A Nationwide Analysis of PSA's Initial Years[END_REF][START_REF] Shapiro | Forest conservation and slippage: Evidence from Mexicoâs national payments for ecosystem services program[END_REF].

We failed to detect a positive impact of the program during its last year (the difference between participants and the counterfactual group vanishes even before the end of the program), suggesting that the program's effects were primarily realized in its first years. Evidence thus suggests that the SSA project may have failed on prompting a transition to more sustainable agricultural practices on the following years. Similarly, [START_REF] Giudice | Selection biases and spillovers from collective conservation incentives in the Peruvian Amazon[END_REF] and [START_REF] Fiorini | Forest cover effects of payments for ecosystem services: Evidence from an impact evaluation in Brazil[END_REF] found that Peru's Natural Forest Conservation Program and Water and Forest Producers Program succeeded in increasing forest cover only in the program's first years. One possible explanation for that is that the opportunity costs of complying with the program requirements increased during the period when the program was in place, leading farmers to return to their business-as-usual practices even before the end of the program.

As we can see in SI Appendix, Figure 2, the price of cattle sharply increased from 97 BRL per arroba in January 2013 to 144 BRL in January 2015. This hasty increase in cattle prices may have played a determining role on the decision of deforestation, by increasing the relative profitability of expanding pastures compared to complying with the program requirements.

Finally, it should be stressed that the SSA program had several components, other than the PES, which may have played a role in the effects we estimated. Actually, we are unable to disentangle the effects of each of these components on the detected impact on forest cover among participant plots. However, our results, which show that deforestation decreased on farm-holds surrounding treated plots between 2013 and 2015, suggest that non-monetary components of the program may have been at play too.

Conclusion

In sum, the four key messages one can take away from this analysis relate to (i) the suitability of RS products for evaluating conservation program effectiveness, (ii) the likely short-term and long run effectiveness of PES programs, (iii) the likely spillover effects of such programs and ultimately (iv) their cost-effectiveness.

Overall, our findings suggest that despite the disagreement between GFC and PRODES on forest cover loss estimates at the individual plot-level, such datasets represent a valuable source of data to evaluate forest conservation projects.

We found evidence that the local REDD+ initiative was effective in reducing deforestation during its early years of implementation in the Transamazon region, an area with historically high deforestation rates. This suggests that PES program targeting smallholders in the Brazilian Amazon may well be effective at least in the short-run. We moreover found evidence that farm-holds located close to enrolees were somehow impacted by the program, as they decrease deforestation also during the early years of program implementation as a consequence of the program. This suggests that PES program may change the behaviour of farmers who are not the primary beneficiaries of the program -although we are not able to show by which channel such phenomenon occurs.

In addition, we found that the participants resumed their normal rate of deforestation even before the end of the program. Our findings suggest that the SSA project have failed in generating permanent effects on farmers' decision about deforestation and inducing more sustainable agricultural practices on the following years. Despite this, we valued the threeyear delayed CO2 emissions highlighted by the impact assessment and found that the SSA program benefit were larger than its costs.

Materials and Methods

Reconstructing forest loss on individual plots

We used property boundaries from the Environmental Rural Registry (CAR in the original Portuguese acronym)10 of 21,492 titled households in our study area (SI Appendix, Figure 1).

We delimited a 50-kilometer buffer around the Transamazonian highway for the municipalities of Altamira, Senador Jose Porfirio, Anapu and Pacaja in order to delimit the rural properties that would be included in our initial sample. Georeferenced data on deforestation and registered private rural properties were overlapped to enable identification of patches cleared inside properties boundaries. We used information from GFC and PRODES to determine the location of forest clearings at an annual basis. All geographical datasets were re-projected to a common spatial reference (SIRGAS 2000/UTM 22S). Our sample covers the 2008-2018 period. Since we did not have information about changes in properties' borders during our sample period, we assumed that they were constant throughout this period. For this study we used a threshold of 75 percent of vegetation cover for GFC tree cover layer as a definition of the forest -average threshold used in studies in Amazonian context [START_REF] Baker | Climate benefits of intact Amazon forests and the biophysical consequences of disturbance[END_REF][START_REF] Gasparini | Determining a Threshold to Delimit the Amazonian Forests from the Tree Canopy Cover 2000 GFC Data[END_REF].

Identification strategy for the impact assessment

In this section, we describe our empirical approach and its key assumptions to estimate the mean difference between the deforestation extent observed on participating farms and the deforestation extent that would have been observed in those farms if they were not enrolled in the program, the so-called average treatment effect on the treated (ATT). Estimating treatment effects using observational data brings the problematic of selection bias, because participants self-select into the program, so that the treated and untreated units might be differ-ent for many reasons other than the treatment itself. This bias occurs because some of the factors that influence the selection of participants also determine the outcomes of interest.

Observations of pre-treatment outcomes might help to correct for selection bias because they contain information on these confounding factors. Thus, matching treated and untreated groups on pre-treatment deforestation outcomes allows to correct for selection bias [START_REF] Abadie | Synthetic control methods for comparative case studies: Estimating the effect of Californiaâs tobacco control program[END_REF].

In addition to pre-treatment outcomes, we also selected a number of covariates that were likely to drive both the participation in the SSA project as well as decisions regarding deforestation, in order to improve the matching procedure. These covariates include: the forest cover as observed in 2000, the farm size, the distance to the main road (Transamazon highway), the distance from the main navigable river (Xingu river), the distance from the main market (Altamira city), and the distance from the nearest small village (local market).

We performed an estimation for the ATT using the Nearest Neighbour Matching (NNM) and the Propensity Score Matching (PSM) estimators. We apply both matching estimators to our data to estimate the average effect of the SSA project on the deforestation rate of participants, using the comparison group to estimate the counter-factual level of deforestation (SI Appendix, Table 4).

To deal with the Stable Unit Treatment Value Assumption (SUTVA), we excluded from the untreated group those plots that were less than 3 km distant from a treated plot, thus creating a kind of buffer zone between treated plots and potential control ones. By doing so, we ended up with 11,466 observations. We performed the same procedure when estimating the impact of the program on those farms that did not receive any PES but were located close enough to enrolled plots to indirectly benefit from the program. In practice, we again created a buffer zone between beneficiaries (whether direct or indirect) and potential controls, by excluding from the sample of untreated plots those farm-holds located between 3 and 6 kilometres from an enrolled plot.

Description of the REDD+ Case Study

The SSA project is a sub-national REDD+ initiative implemented by the Amazon Environmental Research Institute (or IPAM), a Brazilian non-governmental organization involved in the design and implementation of several forest conservation programs in Brazil [START_REF] Cromberg | Sustainable Settlements in the Amazon, Brazil[END_REF]. The SSA project started in 2012 and was financed by the Amazon Fund Our analysis focuses on the 350 farm-holders2 that benefited from all the above-mentioned components. These small landowners live in land reform settlements located in the municipalities of Anapu, Pacaja, and Senador Jose Porfirio (Simonet et al., 2018). These three farm-holds (n=21,492). A paired t-test of annual differences in deforestation revealed significant difference between the PRODES and GFC estimates for the period 2008-2018, the only exception is the year of 2015. Furthermore, GFC detects systematically higher rates of deforestation than PRODES (except for 2010 and 2011). 0.01 0.18 -0.24 0.28 Note: ***, **, and * denote rejection of the null hypothesis of no impact at the 1%, 5% and 10% level. ATT is the Average Treatment effect on the Treated. NNM(4X) (resp. 2X and 1X) refers to the nearest neighbor estimator using 4 (resp. 2 and 1) matched observations as controls. PSM(4N) (resp. 2N and 1N) refers to the propensity score matching estimator using 4 (resp. 2 and 1) matched observations as controls. NNM (4X) -0,023 0,098 NNM (2X) -0,029 0,114 PSM (4N) -0,010 0,082 PSM (2N) 0,016 0,087 Note: ***, **, and * denote rejection of the null hypothesis of no impact at the 1%, 5% and 10% level. ATT is the Average Treatment effect on the Treated. NNM(4X) (resp. 2X and 1X) refers to the nearest neighbor estimator using 4 (resp. 2 and 1) matched observations as controls. PSM(4N) (resp. 2N and 1N) refers to the propensity score matching estimator using 4 (resp. 2 and 1) matched observations as controls. The goal of matching is to make the covariate distributions of participants and nonparticipants similar. After we compare the extent of balancing between the participant and comparison groups before and after the matching procedure. We calculate the normalized difference between these two groups for the pre-treatment covariates. The normalized difference is the most commonly accepted diagnostic used to assess covariate balance (Rosenbaum and Rubin 1985).

The normalized difference is considered negligible when it is below of 0.25 standard deviations (Imbens and Wooldridge 2009). Column 6 of Table 4 shows that, before matching, the participant group (column 3) differs significantly from the comparison group (column 2) in terms of distance from nearest village, distance from Altamira, distance from Belo Monte dam, distance from Transamazon highway and distance from Xingu river Column 7 of Table 4 reports the normalized mean differences between participants and the constructed matched group. All normalized differences are below 0.25 standard deviations, which indicates that the matching procedure was successful in constructing a valid control group.

  r i e l a D e m a r c h i J u l i e S u b e r v i e T h i b a u l t C a t r y & & I s a b e l l e T r i t s c h 1 Introduction

Figure 1 :

 1 Figure 1: Effect of the SSA program on avoided deforestation on enrolled farms

Figure 2 :

 2 Figure 2: Localization of treated and matched plots used for estimating counterfactual levels of forest loss

  scheme to 350 smallholders.

  municipalities, located close to the Transamazon highway, still figure in the ranking of the 10 ten critical municipalities for their deforestation rates until today 3 . The value accessed by the 350 households in the PES scheme was of who participated in the project received 1680 Brazilian reais (BRL) per month (about 526 USD 4 ) from January 2014 to February 2017 (Pinto de Paulo Pedro, 2016). The payments offered to project participants were conditional on forest conservation and agricultural transition toward a fire-free production system 5 . The payments were made every three months, according to the compliance to the established guidelines. The monitoring of the compliance was made annually by IPAM , based on analysis of PRODES data for the forest cover and on the performance of the low-deforestation activities certified by the project technical assistance team (Pinto de Paulo Pedro, 2016).

FiguresFigure 1 :

 1 Figures

2 Remote-Sensing products The Amazon Deforestation Monitoring Project (PRODES) PRODES was created in 1988 by the Brazilian National Institute for Space Research (INPE),

	study adds to the existing literature by providing new evidence on the effectiveness
	of REDD+ programs, focusing on a region characterized by the highest annual loss of for-
	est in the world, while previous studies were on areas where deforestation may appear less
	pressing. To the best of our knowledge, despite the abundance of REDD+ initiatives in Brazil,
	there are no studies assessing the long term impacts of such projects, combining ready-to-
	use RS products and property-level data. Our study aims at filling this gap. Furthermore, this
	is the first study assessing the effectiveness of a Brazilian REDD+ local project conservation
	program using two different sources of remotely-sensed deforestation data to cross validate
	impact assessment results.

Table 1 :

 1 Comparison between GFC and PRODES

		PRODES	GFC
	Data source	Mainly Landsat	Landsat
	Resolution	30 meters	30 meters
	Minimum patch size	6.25 hectares	0.09 hectares
	Coverage	Brazilian Amazon	Global
	Tree cover definition	Primary forest	Vegetation taller than 5 meters
	Method	Image segmentation and analyst interpretation	Automated decision tree
	Observation Period	August 1 to July 31	January 1 to December 31

Table 1 :

 1 Paired t-tests on the equality of deforestation means (ha)

	Tables
	Year GFC Std. Dev. PRODES Std. Dev.	ND	t	p-value
	2008 3.27	7.52	1.98	6.76	0.126 23.07	0
	2009 2.35	5.68	1.01	4.49	0.184 28.21	0
	2010 1.44	3.99	1.98	5.93	0.074 -12.23	0
	2011 1.45	3.65	2.86	7.07	0.178 -26.67	0
	2012 2.42	5.58	0.46	2.22	0.325 45.86	0
	2013 1.86	4.36	0.53	2.68	0.259 42.63	0
	2014 3.10	7.09	0.78	3.73	0.289 49.73	0
	2015 1.63	5.76	1.56	5.68	0.007	1.49	0.13
	2016 2.94	6.94	1.29	5.52	0.185 39.61	0
	2017 4.01	7.54	1.30	5.13	0.296 57.61	0
	2018 2.66	6.49	1.17	4.59	0.187 41.27	0
	Note: Mean forest loss (in hectares) of GFC and PRODES yearly estimates
	for individual

Table 2 :

 2 Additional effects of the REDD+ initiative

	Y ear Estimator ATT PRODES SE	ATT GFC	SE
		NNM (4X) -0.19	**	0.10 -0.57 ***	0.15
		NNM (2X) -0.21		0.11 -0.47 ***	0.19
	2013	NNM (1X) -0.11 PSM (4N) -0.06		0.13 -0.41 ** 0.08 -0.38 ***	0.21 0.15
		PSM (2N) -0.02		0.08 -0.42 ***	0.18
		PSM (1N) -0.09		0.11 -0.71 ***	0.29
		NNM (4X) -0.54	***	0.15 -0.79 ***	0.25
		NNM (2X) -0.57	***	0.21 -0.91 ***	0.29
	2014	NNM (1X) -0.90 PSM (4N) -0.48	*** ***	0.30 -0.70 ** 0.12 -0.82 ***	0.33 0.24
		PSM (2N) -0.50	***	0.15 -0.76 ***	0.26
		PSM (1N) -0.58	***	0.19 -0.55	0.30
		NNM (4X) -0.95	***	0.28 -0.64 ***	0.22
		NNM (2X) -1.19	***	0.33 -0.77 ***	0.31
	2015	NNM (1X) -1.38 PSM (4N) -0.87	*** ***	0.39 -0.95 ** 0.24 -0.50 ***	0.45 0.13
		PSM (2N) -0.90	***	0.28 -0.42 ***	0.16
		PSM (1N) -0.98	***	0.35 -0.59 ***	0.22
		NNM (4X) -0.59	***	0.18 -0.28	0.28
		NNM (2X) -0.64	***	0.20 -0.38	0.32
	2016	NNM (1X) -0.78 PSM (4N) -0.93	*** ***	0.26 -0.27 0.19 -0.36	0.33 0.27
		PSM (2N) -0.83	***	0.24 -0.23	0.29
		PSM (1N) -1.00	***	0.32 -0.32	0.34
		NNM (4X) -0.20		0.25 -0.61	0.33
		NNM (2X) -0.36		0.30 -0.88 ***	0.41
	2017	NNM (1X) -0.25 PSM (4N) -0.06		0.34 -0.74 0.23 -0.87 ***	0.46 0.33
		PSM (2N) -0.06		0.24 -0.69	0.37
		PSM (1N) -0.14		0.28 -0.25	0.39
		NNM (4X) -0.15		0.16 -0.15	0.19
		NNM (2X) -0.24		0.18 -0.21	0.22
	2018	NNM (1X) -0.27 PSM (4N) -0.06		0.23 -0.43 0.13 0.02	0.26 0.20
		PSM (2N) -0.06		0.16 -0.19	0.22
		PSM (1N)

Table 3 :

 3 Spillover effects of the REDD+ initiative

	Outcome	Estimator	ATT	S.E.

Table 4 :

 4 Balancing tests

	Means	Variances	Standardized differences	Variance ratio

Although the annual deforestation rate in Brazil fell by 70 percent between

[START_REF] Blackman | Evaluating forest conservation policies in developing countries using remote sensing data: An introduction and practical guide[END_REF]and (Nepstad et al. 2014), more than 9,700 square kilometers of the Brazilian Amazon were cleared between 2018 and 2019, representing an increase of 30 percent in the annual deforestation rate and the highest rate since 2008(INPE, 2019a).

Source: Amazon Fund (http://www.fundoamazonia.gov.br/pt/projeto/Assentamentos-Sustentaveis-na-Amazonia/).

The CAR is a mandatory and self-declaratory registry for all Brazilian rural properties. To obtain CAR, landholders must document georeferenced property's boundaries, as well as within-property areas of native vegetation. CAR has a public consultation module where data from properties, detaining either temporary or permanent registrations, are available for download in vector format at http://www.car.gov.br/publico/municipios/downloads.

The Amazon Fund is a REDD+ instrument designed to raise donations for non-reimbursable investments in efforts to curb deforestation as well as to promote sustainable use of resources in the Brazilian Amazon.

The map with the localization of the farm-holds enrolled in SSA program is publicly available at IPAM's website (http://www.pas-simpas.org.br/). Therefore, we used this available data to geolocalize

plots from the 350 that received payments conditional on forest conservation.3 The first settlers arrived in the area during the Plan for National Integration (PIN) for the colonization of the Brazilian Amazon. At that time, poverty in north-eastern Brazil was the immediate issue, especially following the extreme drought of 1970[START_REF] Fearnside | Brazil's Amazon settlement schemes. Conflicting objectives and human carrying capacity[END_REF]. The transfer of poor north-easterners to colonization areas along the Transamazon highway was raised as the solution by the Brazilian Government at that time. Encouraging quick installation of settlers and the construction of the Transamazonian highway has intensified deforestation in the area without achieving many of its development goals. Colonizers were explicitly encouraged by the government to deforest at least 50 percent of their plots to pledge ownership[START_REF] Souza | O desenvolvimento socioambiental na Transamazônica: a trajetória de um discurso a muitas vozes[END_REF]. The livelihoods of small landowners in this area still depend on slash-and-burn agriculture and extensive cattle ranching, which are the two primary drivers of deforestation in the Brazilian Amazon[START_REF] Smith | Agroforestry trajectories among smallholders in the Brazilian Amazon: innovation and resiliency in pioneer and older settled areas[END_REF][START_REF] Soares-Filho | Modelling conservation in the Amazon basin[END_REF].

1,680 Reais converted to USD by applying the average conversion rate of Brazilian Real to American dollars in 2017

Thirty percent of the payment was conditional on conserving forest on at least 50 percent of the farm, another thirty percent of the payment was conditional on the maintenance of 15-meter-wide forest riparian zones and the remaining 40 percent of the payment relied on the adoption of fire-free practices. A minimum of 30 percent of forest cover was required to be eligible for payments, but only participants with at least 50 percent of forest cover received the full payments (seeSimonet et al. (2018) for a detailed description of the SSA program).

CEE-M Working Papers / Contact : laurent.garnier@inra.fr  RePEc https://ideas.repec.org/s/hal/wpceem.html  HAL https://halshs.archives-ouvertes.fr/CEE-M-WP/

Supplementary Information

CEE-M Working Papers