Planning as Model Checking for Extended Goals in Non-deterministic Domains

1 Introduction

Most real world planning domains are intrinsically "nondeterministic". This is the case, for instance, of several robotics, control, and space application domains. Most often, applications in non-deterministic domains require planners to deal with goals that are more general than sets of final desired states. The planner needs to generate plans that satisfy conditions on their whole execution paths, i.e., on the sequences of states resulting from execution. E.g., in a robotic application, we may need to specify that a mobile robot should "move to a given room while avoiding certain areas all along the path".

When dealing with non-deterministic domains, the task of extending the notion of goal leads to a main key issue, related to the fact that the execution of a given plan may nondeterministically result in more than one sequence of states. Consider the previous example in the robotics context. On the one hand, we would like to require a plan that guarantees to reach the room and also guarantees that dangerous areas are avoided. On the other hand, in several realistic domains, no plan might satisfy this strong requirement. We might therefore accept plans that satisfy weaker requirements, e.g., we might accept that the robot has a possibility of reaching the room without being guaranteed to do so, but it is however guaranteed to avoid dangerous areas. Alternatively, we may require a plan that guarantees that the robot reaches the desired location, just trying, if possible, to avoid certain areas, e.g., areas that are too crowded.

In this paper, we define and implement a planning algorithm that generates automatically plans for extended goals in non-deterministic domains. Extended goals are CTL formulas [Emerson, 1990]. They can express temporal conditions that take into account the fact that an action may non-deterministically result in different outcomes. Hence extended goals allow us to distinguish between temporal requirements on "all the possible executions" and on "some executions" of a plan.

The plans built by the algorithm are strictly more expressive than plans that simply map states to actions to be executed, like universal plans [Schoppers, 1987], memory-less policies [Bonet and Geffner, 2000], and state-action tables [Cimatti et al., 1998; Daniele et al., 1999]. Beyond expressing conditional and iterative behaviors, the generated plans can execute different actions is a state, depending on the previous execution history. This expressiveness is required to deal with extended goals.

We have implemented the planning algorithm inside MBP [Cimatti et al., 1998]. MBP uses symbolic techniques based on BDDs [Burch et al., 1992] that provide the ability to represent compactly and explore efficiently large state spaces. In the paper we present preliminary experimental results that show that the proposed algorithmworks in practice.

This paper is structured as follows. We first define nondeterministic planning domains and extended goals. We then define the structure of plans that can achieve extended goals. Finally, we describe the planning algorithm, describe its implementation, and show some experimental results.

2 Planning Domains

A (non-deterministic) planning domain can be described in terms of (basic) propositions, which may assume different values in different states, of actions and of a transition relation describing how an action leads from one state to possibly many different states.

Definition 1 A planning domain BW is a tuple B4BUBN BNBTBNAXB5, where BU is the finite set of (basic) propositions, AI BE BU is the set of states, BT is the finite set of actions, andAXAI A2BTA2 is the transition relation. We write D5 CP AX D5 BC for B4D5BN CPBN D5 BC B5 BEAX.

We require that the transition relationAX is total, i.e., for every D5 BE there is some CP BE BT and D5 BC BE such that D5 CP AX D5 BC . We denote with BTCRD8B4D5B5 the set of the actions that can be performed in state D5: BTCRD8B4D5B5 BP CUCP BM BLD5 BC BM D5 CP AX D5 BC CV. We denote with BXDCCTCRB4D5BN CPB5 the set of the states that can be reached from D5 performing action CP BE BTCRD8B4D5B5: BXDCCTCRB4D5BN CPB5 BP CUD5 BC BM D5 CP AX D5 BC CV.

In Figure 1 we depict a simple planning domain, where an item can be loaded/unloaded to/from a container which can be locked/unlocked. Actions load and adjust are nondeterministic. load can either succeed, and lead to state 3 where the item is loaded correctly and the container can be locked, or it may fail, and lead to state 5, where the item needs to be adjusted to a correct position in order to lock the container. Action adjust may in its turn fail, and leave the item positioned incorrectly. For all states in the domain, we assume to have an action wait (not represented in the figure) that leaves the state unchanged. The basic propositions are loaded, locked and misplaced. loaded holds in states 3 and 4, locked in states 1 and 4, misplaced in state 5.

All the work presented in this paper is independent of the language for describing planning domains. However many of these languages (e.g., ADL-like languages as PDDL) are not able to represent non-deterministic domains and should be extended allowing for disjunctive effects of the actions. For instance, the action load might be described with an extension of PDDL as follows.

:action load :precondition (and (not loaded) (not locked) (not misplaced)) :effect (OR (loaded) (misplaced))

3 Extended Goals

Extended goals are expressed with CTL formulas.

Definition 2 Let BU be the set of basic propositions of a domain BW and let CQ BE BU. The syntax of an (extended) goal CV for BW is the following:

"X", "U", and "W" are the "next time", "(strong) until", and "weak until" temporal operators, respectively. "A" and "E" are the universal and existential path quantifiers, where a path is an infinite sequence of states. They allow us to specify requirements that take into account non-determinism. Intuitively, the formula BTCGCV (BXCGCV) means that CV holds in every (in some) immediate successor of the current state. BTB4CV BD UCV BE B5 (BXB4CV BD UCV BE B5) means that for every path (for some path) there exists an initial prefix of the path such that CV BE holds at the last state of the prefix and CV BD holds at all the other states along the prefix. The formula BTB4CV BD WCV BE B5 (BXB4CV BD WCV BE B5) is similar to BTB4CV BD UCV BE B5 (BXB4CV BD UCV BE B5) but allows for paths where CV BD holds in all the states and CV BE never holds. Formulas BTBYCV and BXBYCV (where the temporal operator "F" stands for "future" or "eventually") are abbreviations of BTB4BQUCVB5 and BXB4BQUCVB5, respectively. BTBZCV and BXBZCV (where "G" stands for "globally" or "always") are abbreviations of BTB4CVWBRB5 and BXB4CVWBRB5, respectively. A remark is in order: even if BM is allowed only in front of basic propositions, it is easy to define BMCV for a generic CTL formula CV, by "pushing down" the negations: for instance BMBTCG CV AH BXCGBMCV and BMBTB4CV BD WCV BE B5 AH BXB4BMCV BE UB4BMCV BD CM BMCV BE B5B5.

Goals as CTL formulas allow us to specify different interesting requirements on plans. Let us consider first some examples of reachability goals. BTBYCV ("reach CV") states that a condition should be guaranteed to be reached by the plan, in spite of non-determinism. BXBYCV ("try to reach CV") states that a condition might possibly be reached, i.e., there exists at least one execution that achieves the goal. As an example, in Figure 1, the strong requirement B4locked CM BMloadedB5 AX BTBY B4locked CM loadedB5 cannot be satisfied, while the weaker requirement B4locked CM BMloadedB5 AX BXBY B4locked CM loadedB5 can be satisfied by unlocking the container, loading the item and then (if possible) locking the container. A reasonable reachability requirement that is stronger than BXBYCV is BTB4BXBYCVWCVB5: it allows for those execution loops that have always a possibility of terminating, and when they do, the goal CV is guaranteed to be achieved. In Figure 1, the goal B4lockedCM BMloadedB5 AX BTB4BXBY B4lockedCMloadedB5 WB4lockedCMloadedB5B5 can be satisfied by a plan that unlocks, loads, and, if the outcome is state 3, locks again, while if the item is misplaced (state 5) repeatedly tries to adjust the position of the item until (hopefully) state 3 is reached, and finally locks the container.

We can distinguish among different kinds of maintainability goals, e.g., BTBZ CV ("maintain CV"), BTBZ BMCV ("avoid CV"), BXBZ CV ("try to maintain CV"), and BXBZBMCV ("try to avoid CV"). For instance, a robot should never harm people and should always avoid dangerous areas. Weaker requirements might be needed for less critical properties, like the fact that the robot should try to avoid to run out of battery.

We can compose reachability and maintainability goals. BTBYBTBZCV states that a plan should guarantee that all executions reach eventually a set of states where CV can be maintained. For instance, an air-conditioner controller is required to reach eventually a state such that the temperature can then be maintained in a given range. Alternatively, if you consider the case in which a pump might fail to turn on when it is selected, you might require that "there exists a possibility" to reach the condition to maintain the temperature in a desired range (BXBYBTBZCV). As a further example, the goal BTBZBXBYCV intuitively means "maintain the possibility of reaching CV".

Reachability - preserving goals make use of the "until operators" (BTB4CV BD UCV BE B5 and BXB4CV BD UCV BE B5) to express reachability goals while some property must be preserved. For instance, an air-conditioner might be required to reach a desired temperature while leaving at least D2 of its D1 pumps off.

As a last example in the domain of Figure 1, consider the goal "from state 2, where the container is unlocked and empty, lock the container first, and then maintain the possibility of reaching a state where the item is loaded and the container is locked (state 4)". It can be formalized as B4BMlocked CM BMloaded CM BMmisplacedB5 AX B4BTBY B4locked CM BTBZBXBYB4locked CM loadedB5B5B5. In the rest of the paper, we call this example of goal "lock-then-load goal".

Notice that in all examples above, the ability of composing formulas with universal and existential path quantifiers is essential. Logics that do not provide this ability, like LTL [Emerson, 1990], cannot express these kinds of goals 1 .

4 Plans for Extended Goals

A plan describes the actions that have to be performed in a given state of the world. In order to satisfy extended goals, actions that have to be executed may also depend on the "internal state" of the executor, which can take into account, e.g., previous execution steps. Consider again the "lock-then-load goal" for domain in Figure 1. The plan, starting from state 2, has first to lead to state 1, and then to state 4. In state 2, the first time we have to execute action lock, while we have to load the item the second time. In general, a plan can be defined in terms of an action function that, given a state and an execution context encoding the internal state of the executor, specifies the action to be executed, and in terms of a context function that, depending on the action outcome, specifies the next execution context.

Definition 3 A plan for a domain BW is a tuple CWBVBN CR BC BN actBN ctxtCX, where:

• AF BV is a set of (execution) contexts,
• AF CR BC BE BV is the initial context,
• AF act BM A2BV B6BT is the action function,
• AF ctxt BM A2BV A2 B6BV is the context function.

If we are in state D5 and in execution context CR, then actB4D5BN CRB5 returns the action to be executed by the plan, while ctxtB4D5BN CRBN D5 BC B5 associates to each reached state D5 BC the new execution context. Functions act and ctxt may be partial, since some state-context pairs are never reached in the execution of the plan. An example of a plan that satisfies the lockthen-load goal is shown in Figure 2. Notice that the context changes from CR BC to CR BD when the execution reaches state 1. This allows the plan to execute different actions in state 2.

In the rest of the paper we consider only plans that are executable and complete. We say that plan AP is executable if, whenever actB4D5BN CRB5 BP CP and ctxtB4D5BN CRBN D5 BC B5 BP CR BC , then D5 CP AX D5 BC . We say that AP is complete if, whenever actB4D5BN CRB5 BP CP and D5 CP AX D5 BC , then there is some context CR BC such that ctxtB4D5BN CRBN D5 BC B5 BP CR BC and actB4D5 BC BN CR BC B5 is defined. Intuitively, a complete plan always specifies how to proceed for all the possible outcomes of any action in the plan.

1 In general, CTL and LTL have incomparable expressive power (see [Emerson, 1990] for a comparison). We focus on CTL since it provides the ability of expressing goals that take into account nondeterminism.

Figure 3: An example of execution structure

The execution of a plan results in a change in the current state and in the current context. It can therefore be described in terms of transitions between pairs state-context. Formally, given a domain BW and a plan AP, a transition of plan AP in BW is a tuple B4D5BN CRB5 CP AX B4D5 BC BN CR BC B5 such that D5 CP AX D5 BC , CP BP actB4D5BN CRB5, and CR BC BP ctxtB4D5BN CRBN D5 BC B5. A run of plan AP from state D5 BC is an infinite sequence B4D5 BC BN CR BC B5 CP BC AX B4D5 BD BN CR BD B5 CP BD AX B4D5 BE BN CR BE B5 CP BE AX B4D5 BF BN CR BF B5 A1 A1 A1 where B4D5 CX BN CR CX B5 CP CX AX B4D5 CXB7BD BN CR CXB7BD B5 are transitions. Given a plan, we may have an infinite number of runs due to the nondeterminism of the domain. This is the case of the plan in Figure 2, since the execution can loop non-deterministically over the pair state-context B45BN CR BD B5. We provide a finite presentation of the set of all possible runs of a plan with an execution structure, i.e, a Kripke Structure [Emerson, 1990] whose set of states is the set of state-context pairs, and whose transition relation corresponds to the transitions of the runs.

Definition 4 The execution structure of plan AP in a domain D from state D5 BC is the structure  BP CWCBBN CABN CX, where:

• AF CB BP CUB4D5BN CRB5 BM actB4D5BN CRB5 is definedCV,
• AF B4B4D5BN CRB5BN B4D5 BC BN CR BC B5B5 BE CA if B4D5BN CRB5 CP AX B4D5 BC BN CR BC B5 for some CP,
• AF B4D5BN CRB5 BP CUCQ BM CQ BE D5CV

As an example, the execution structure of the plan in Figure 2 is depicted in Figure 3.

We define when a goal CV is true in B4D5BN CRB5, written BN B4D5BN CRB5 CYBP CV by using the standard semantics for CTL formulas over the Kripke Structure . The complete formal definition can be found in, e.g., [Emerson, 1990]. In order to make the paper self contained, we present here some cases. Propositional formulas are treated in the usual way. BN B4D5BN CRB5 CYBP BTCGCV iff for every path B4D5BN CRB5 BC B4D5BN CRB5 BD B4D5BN CRB5 BE A1 A1 A1 , with B4D5BN CRB5 BP B4D5BN CRB5 BC , we have BN B4D5BN CRB5 BD CYBP CV. BN B4D5BN CRB5 CYBP BTB4CV BD UCV BE B5 iff for every path B4D5BN CRB5 BC B4D5BN CRB5 BD B4D5BN CRB5 BE A1 A1 A1 , with B4D5BN CRB5 BP B4D5BN CRB5 BC , there exists CX AL BC such that BN B4D5BN CRB5 CX CYBP CV BE and, for all BC AK CY BO CX, BN B4D5BN CRB5 CY CYBP CV BD . The definition is similar in the case of existential path quantifiers. We can now define the notion of plan that satisfies a given goal.

Definition 5 Let BW be a planning domain and CV be a goal for BW. Let AP be a plan for BW and  be the corresponding execution structure. Plan AP satisfies goal CV from initial state D5 BC , written APBN D5 BC CYBP CV, if BN B4D5 BC BN CR BC B5 CYBP CV. Plan AP satisfies goal CV from the set of initial states BC if APBN D5 BC CYBP CV for each D5 BC BE BC .

For instance, the plan in Figure 2 satisfies the lock-then-load goal from state 2.

5 Planning Algorithm

The planning algorithm searches through the domain by trying to satisfy a goal CV in a state D5. Goal CV defines conditions on the current state and on the next states to be reached. Intuitively, if CV must hold in D5, then some conditions must be projected to the next states. The algorithm extracts the information on the conditions on the next states by "progressing" the goal CV. For instance, if CV is BXBYCV BC , then either CV BC holds in D5 or BXBYCV BC must still hold in some next state, i.e., BXCGBXBYCV BC must hold in D5. One of the basic building blocks of the algorithm is the function progr that rewrites a goal by progressing it to next states. progr is defined by induction on the structure of goals.

• AF progrB4D5BN BQB5 BP BQ and progrB4D5BN BRB5 BP BR;
• AF progrB4D5BN CQB5 BP if CQ BE D5 then BQ else BR;
• AF progrB4D5BN BMCQB5 BP if CQ BE D5 then BR else BQ;
• AF progrB4D5BN CV BD CM CV BE B5 BP progrB4D5BN CV BD B5 CM progrB4D5BN CV BE B5;
• AF progrB4D5BN CV BD CN CV BE B5 BP progrB4D5BN CV BD B5 CN progrB4D5BN CV BE B5;
• AF progrB4D5BN BTCG CVB5 BP BTCG CV and progrB4D5BN BXCG CVB5 BP BXCG CV;
• AF progrB4D5BNBTB4CVUCV BC B5B5 BP B4progrB4D5BN CVB5 CM BTCGBTB4CVUCV BC B5B5 CN progrB4D5BN CV BC B5 and progrB4D5BN BXB4CVUCV BC B5B5 BP B4progrB4D5BN CVB5 CM BXCG BXB4CV U CV BC B5B5 CN progrB4D5BN CV BC B5;
• AF progrB4D5BN BTB4CV WCV BC B5B5 BP B4progrB4D5BN CVB5 CM BTCGBTB4CV WCV BC B5B5 CN progrB4D5BN CV BC B5 and progrB4D5BN BXB4CVWCV BC B5B5 BP B4progrB4D5BN CVB5 CM BXCG BXB4CV W CV BC B5B5 CN progrB4D5BN CV BC B5.

The formula progrB4D5BN CVB5 can be written in a normal form. We write it as a disjunction of two kinds of conjuncts, those of the form BTCGCU and those of the form BXCGCW, since we need to distinguish between formulas that must hold in all the next states and those that must hold in some of the next states:

where CU BE BT CX (CW BE BX CX ) if BTCGCU (BXCGCW) belongs to the CX-th disjunct of progrB4D5BN CVB5. We have CY
CY different disjuncts that correspond to alternative evolutions of the domain, i.e., to alternative plans we can search for. In the following, we represent progrB4D5BN CVB5 as a set of pairs, each pair containing the BT CX and the BX CX parts of a disjunct:

with progrB4D5BN BQB5 BP CUB4BNBN BNB5CV and progrB4D5BN BRB5 BP BN.

Given a disjunct B4BTBNBXB5 of progrB4D5BN CVB5, we can define a function that assigns goals to be satisfied to the next states. We denote with assign-progrB4B4BTBNBXB5BN B5 the set of all the possible assignments CX BM AX BE BTCJBX such that each universally quantified goal is assigned to all the next states (i.e., if CU BE BT then CU BE CXB4D5B5 for all D5 BE ) and each existentially quantified goal is assigned to one of the next states

(i.e., if CW BE BX and CW BIBE BT then CU BE CXB4D5B5 for one particular D5 BE ). Consider the following example in the domain of Figure 1. Let CV be BTBY lockedCMBXCGmisplacedCMBXCG loaded and let the current state D5 be 2. We have that BTCGBTBY lockedCM BXCGmisplaced CM BXCGloaded BE progrB42BN CVB5. If we consider action load, the next states are 3 and 5. Then BTBY locked must hold in 3 and in 5, while misplaced and loaded must hold in 3 or in 5. We have therefore four possible state-formulas assignments CX BD BN BM BM BM BN CX BG to be explored (in the following we write CU BD for BTBY locked, CW BD for misplaced, and CW BE for loaded):

In this simple example, it is easy to see that the only assignment that may lead to a successful plan is CX BF .

Given the two basic building blocks progr and assign-progr, we can now describe the planning algorithm build-plan that, given a goal CV BC and an initial state D5 BC , returns either a plan or a failure. 2 The algorithm is reported in Figure 4. It performs a depth-first forward search: starting from the initial state, it picks up an action, progresses the goal to successor states, and iterates until either the goal is satisfied or the search path leads to a failure. The algorithm uses as the "contexts" of the plan the list of the active goals that are considered at the different stages of the exploration. More precisely, a context is a list CR BP CJCV BD BN BM BM BM BN CV D2 CL, where the CV CX are the active goals, as computed by functions progr and assig-progr, and the order of the list represents the age of these goals: the goals that are active since more steps come first in the list.

The main function of the algorithm is function build-plan-auxB4D5BN CRBN pl BN openB5, that builds the plan for context CR from state D5. If a plan is found, then it is returned by the function. Otherwise, BR is returned. Argument pl is the plan built so far by the algorithm. Initially, the argument passed to build-plan-aux is pl BP CWBVBN CR BC BN actBN ctxtCX BP CWBNBN CV BC BN BNBN BNCX. Argument open is the list of the pairs state-context of the currently open problems: if B4D5BN CRB5 BE open then we are currently trying to build a plan for context CR in state D5. Whenever function build-plan-aux is called with a pair state-context already in open, then we have a loop of states in which the same sub-goal has to be enforced. In this case, function is-good-loopB4B4D5BN CRB5BN openB5 is called that checks whether the loop is valid or not. If the loop is good, plan pl is returned, otherwise function build-plan-aux fails.

Function is-good-loop computes the set loop-goals of the goals that are active during the whole loop: iteratively, it considers all the pairs B4D5 BC BN CR BC B5 that appear in open up to the next occurrence of the current pair B4D5BN CRB5, and it intersects loop-goals with the set setofB4CR BC B5 of the goals in list CR BC . Then, function is-good-loop checks whether there is some strong until goal among the loop-goals. If this is a case, then the loop is bad: the semantics of CTL requires that all the strong until goals are eventually fulfilled, so these goals should not

2 It is easy to extend the algorithm to the case of more than one initial state.

function build-planB4D5 BC BN CV BC B5 BM Plan return build-plan-auxB4D5 BC BN CJCV BC CLBN CWBNBN CV BC BN BNBN BNCXBN BNB5 function build-plan-auxB4D5BN CRBN pl BN openB5 BM Plan if B4D5BN CRB5 BE open then if is-good-loopB4B4D5BN CRB5BN openB5 then return pl else return BR if defined pl BMact CJD5BN CRCL then return pl foreach CP BE BTCRD8B4D4B5 do foreach B4BTBN BXB5 BE progrB4D5BN CRB5 do foreach CX BE assign-progrB4B4BTBN BXB5BN BXDCCTCRB4D5BN CPB5B5 do pl BC BMBP pl pl BC BMBV BMBP pl BC BMBV CJ CUCRCV pl BC BMactCJD5BN CRCL BMBP CP open BC BMBP concB4B4D5BN CR BC B5BN openB5 foreach D5 BC BE BXDCCTCRB4D5BN CPB5 do CR BC BMBP order-goalsB4CXCJD5 BC CLBN CRB5 pl BC BMctxtCJD5BN CRBN D5 BC CL BMBP CR BC pl BC BMBP build-plan-auxB4D5 BC BN CR BC BN pl BC BN open BC B5 if pl BC BP BR then next CX return pl BC return BR function is-good-loopB4B4D5BN CRB5BN openB5 BM boolean loop-goals BMBP setofB4CRB5 while B4D5BN CRB5 BIBP headB4openB5 do B4D5 BC BN CR BC B5 BMBP headB4openB5 loop-goals BMBP loop-goals CK setofB4CR BC B5 open BMBP tailB4openB5 if BLCV BE loop-goals BM CV BP BTB4 U B5 or CV BP BXB4 U B5 then return false else return true

stay active during a whole loop. In fact, this is the difference between strong and weak until goals: executions where some weak until goal is continuously active and never fulfilled are acceptable, while the strong untils should be eventually fulfilled if they become active.

If the pair B4D5BN CRB5 is not in open but it is in the plan pl (i.e., B4D5BN CRB5 is in the range of function act and hence condition "defined pl BMact CJD5BN CRCL" is true), then a plan for the pair has already been found in another branch of the search, and we return immediately with a success. If the pair state-context is neither in open nor in the plan, then the algorithm considers in turn all the executable actions CP from state D5, all the different possible progresses B4BTBN BXB5 returned by function progr, and all the possible assignments CX of B4BTBNBXB5 to BXDCCTCRB4D5BN CPB5. Function build-plan-aux is called recursively for each destination state in D5 BC BE BXDCCTCRB4D5BN CPB5. The new context is computed by function order-goalsB4CXCJD5 BC CLBN CRB5: this function returns a list of the goals in CXCJD5 BC CL that are ordered by their "age": namely those goals that are old (they appear in CXCJD5 BC CL and also in CR) appear first, in the same order as in CR, and those that are new (they appear in CXCJD5 BC CL but not in CR) appear at the end of the list, in any order. Also, in the recursive call, argument pl is updated to take into account the fact that action CP has been selected from state D5 in context CV. Moreover, the new list of open problems is updated to concB4B4D5BN CRB5BN openB5, namely the pair B4D5BN CRB5 is added in front of argument open.

Any recursive call of build-plan-aux updates the current plan pl BC . If all these recursive calls are successful, then the final value of plan pl BC is returned. If any of the recursive calls returns BR, then the next combination of assign decomposition, progress component and action is tried. If all these combinations fail, then no plan is found and BR is returned.

As an example, call build-planB42BN lock-then-loadB5 is successful and returns the plan in Figure 2 where CR BC and CR BD are goals BTBYB4locked CM BTBZBXBYB4locked CM loadedB5B5 and BTBZBXBYB4locked CM loadedB5, respectively.

The algorithm always terminates, and it is correct and complete: given a state D5 of a domain BW and a goal CV for BW, if build-planB4D5BN CVB5 BP AP then APBN D5 CYBP CV, and if build-planB4D5BN CVB5 BP BR then there is no plan AP such that APBN D5 CYBP CV.

6 Symbolic Implementation and Experimental Results

We have implemented the planning algorithm and have performed some experimental evaluations. Though very preliminary, the experiments define some basic test cases for planning for CTL goals in non-deterministic domains, show that the approach is effective in practice with cases of significant complexity, and settle the basis for future comparisons.

We have implemented the algorithm inside MBP ([Cimatti et al., 1998]). MBP uses symbolic techniques based on BDDs [Burch et al., 1992] to overcome the problems of the explicit-state planning algorithm due to the huge size of realistic domains, and in particular of non-deterministic domains.

In order to provide a BDD-based implementation, the explicit algorithm presented in the previous section has to be revisited, taking into account the fact that BDDs work effectively on sets of states rather than on single states. For lack of space, we can not describe the symbolic BDD-based algorithm in details: further information on this algorithm, as well as on the test cases, can be found at the MBP home page http://sra.itc.it/tools/mbp.

One of the very few examples of planning for extended goals in non-deterministic domains that we have found in the literature is the "robot-moving-objects" search problem, presented in [Kabanza et al., 1997] to test the SIMPLAN planner for some LTL-like goals. The domain consists of a set of rooms connected by doors, of a set of objects in the rooms, and of a robot that can grasp the objects and carry them to different rooms. The non-determinism in the domain is due to the fact that (some of) the doors are defective and can close without an explicit action of the robot.

We have performed experiments with different extended goals. For lack of space we report only the results for the goal of moving the objects into given rooms and keeping them there (experiment 1 in [Kabanza et al., 1997]). In our framework, this goal is of the form BTBYBTBZCV. The problem is parametrized in the number of the possible objects to be moved and in the number of defective doors. The time required to build the plan is reported in Figure 5 (all tests were performed on a Pentium II 300 MHz with 512 Mb RAM of memory running Linux). The time scale is logarithmic and shows that the required time grows exponentially in the number of objects (this corresponds to an exponential growth in the size of the domain). Due to the usage of symbolic techniques, instead, the performance is not influenced by the nondeterminism. We remark that in the case of 5 objects the domain is quite complex: it has more than BDBC BK states.

The results reported in [Kabanza et al., 1997] show a complementary behavior: SIMPLAN scales well with respect to the number of objects, but the explicit state search suffers significantly in the case of non-deterministic domains. We remark, however, that the efficient behavior of SIMPLAN in the case of deterministic domains depends on the enforced domain-dependent search control strategies, that are able to cut the largest part of the search graph. Our experiments show that MBP outperforms SIMPLAN, if the latter is executed without control strategies. This result is not surprising: symbolic techniques have shown to be dramatically more efficient that explicit techniques in the case of huge search space.

7 Conclusions and RelatedWork

In this paper we have presented an approach to automatic planning in non-deterministic domains where the goals are expressed as CTL formulas. We have implemented the algorithm by using symbolic model checking techniques, which open up the possibility to deal with large state space.

Some future objectives are the following. The symbolic implementation is still a rather naive transcription of the explicit algorithm presented in the paper: further work in needed to develop a symbolic algorithm that fully exploits the potentiality of BDDs and of the symbolic exploration of huge state spaces. Moreover, we plan to perform an extensive test with different kinds of extended goals on a set of realistic domains, to show that the approach is indeed practical. Finally, in this paper we focus on the case of full observability. An extension of the work to the case of planning for extended goals under partial observability is one of the main objectives for future research.

The problem of planning for CTL goals has never been solved before. The starting point of the work presented in this paper is the framework of "Planning via Symbolic Model Checking" (see, e.g., [Cimatti et al., 1998; Daniele et al., 1999; Bertoli et al., 2001]). None of the previous works in this framework deals with temporally extended goals. The issue of "temporally extended goals" is certainly not new. However, most of the works in this direction restrict to deterministic domains, see for instance [de Giacomo and Vardi, 1999; Bacchus and Kabanza, 1998]. A work that considers extended goals in non-deterministic domains is described in [Kabanza et al., 1997]: see Section 6 for a comparison.

Extended goals make the planning problem close to that of automatic synthesis of controllers (see, e.g., [Asarin et al., 1995; Kupferman and Vardi, 1997]). However, most of the work in this area focuses on the theoretical foundations, without providing practical implementations. Moreover, it is based on rather different technical assumptions on actions and on the interaction with the environment.