Computational Complexity of Planning with Temporal Goals

1 Introduction

In the presence of complete information about the initial situation, a plan - in the sense of classical planning - is a sequence of actions that takes the agent from the initial situation to the state which satisfies a given goal. Traditionally, a goal is described as a fluent which must be true after all the actions. For such goals, the computational complexity of finding a plan has been well-studied [Bylander, 1994; Erol et al., 1995; Liberatore, 1997; Baral et al., 2000]. In the most natural formulation, the problem of finding polynomial length plans is NP-complete (for exact definitions of standard complexity terms such as NP-completeness, see, e.g., [Papadimitriou, 1994; Baral et al., 2000]).

In many real-life planning problems, the goal is represented in a much more complicated temporal form: e.g., in addition to having a desired fluent true at the end, we may want to keep certain fluents true at all times; for example, we may want to make sure that certain safety constraints are satisfied at all times. In this paper, we study the complexity of planning for such temporal goals. There exist two formalisms for describing temporal goals: Linear Temporal Logic (LTL) [Bacchus and Kabanza, 1998] in which we are allowed to refer to the actual past and future events, and Branching Temporal Logic CTL [Niyogi and Sarkar, 2000] in which we are also allowed to refer to events from the possible future. In this paper, we will describe the computational complexity of

Ra ´ul A. Trejo

ITESM Campus Edo. M´exico Atizapan, M´exico 52926 rtrejo@campus.cem.itesm.mx

planning in both logics. To the best of our knowledge this has not been done before.

Our complexity analysis will be based on the action description language a0 proposed in [Gelfond and Lifschitz, 1993]. The language a0 and its variants have made it easier to understand the fundamentals (such as inertia, ramification, qualification, concurrency, sensing, etc.) involved in reasoning about actions and their effects on a world, and we would like to stick to that simplicity principle here. To stick to the main point we consider the simplest action description, and do not consider features such as executability conditions. We now start with a brief description of the language a0 .

1.1 The language ✁ : brief reminder

In the language a0 , we start with a finite list of properties (fluents) ✂ ✄ ✆ ✞ ✞ ✞ ✆ ✂ ☛ which describe possible properties of a state. A state is then defined as a finite set of fluents, e.g., ☞ ✌ or ☞ ✂ ✄ ✆ ✂ ✑ ✌ . We are assuming that we have complete knowledge about the initial state: e.g., ☞ ✂ ✄ ✆ ✂ ✑ ✌ means that in the initial state, properties ✂ ✄ and ✂ ✑ are true, while all the other properties ✂ ✔ ✆ ✂ ✕ ✆ ✞ ✞ ✞ are false. The properties of the initial state are described by formulas of the type

✖ ✗ ✖ ✙ ✖ ✚ ✛ ✛ ✢ ✂ ✆

where ✂ is a fluent literal, i.e., either a fluent ✂ ✤ or its negation ✥ ✂ ✤ .

To describe possible changes of states, we need a finite set of actions. In the language a0 , the effect of each action ✦ can be described by formulas of the type

where ✂ ✆ ✂ ✄ ✆ ✞ ✞ ✞ ✆ ✂ ✯ are fluent literals. A reasonably straightforward semantics describes how the state changes after an action:

• ✱ If, before the execution of an action ✦ , fluent literals ✂ ✄ ✆ ✞ ✞ ✞ ✆ ✂ ✯ were true, and the domain description contains a rule "✦ ✧ ✚ ✩ ✪ ✫ ✪ ✂ ✖ ✭ ✂ ✄ ✆ ✞ ✞ ✞ ✆ ✂ ✯ ", then this rule is activated, and after the execution of the action ✦ , ✂ becomes true.
• ✱ If for some fluent ✂ ✤ , no activated rule enables us to conclude that ✂ ✤ is true or false, thismeans that the execution of action ✦ does not change the truth of this fluent; therefore, ✂ ✤ is true in the resulting state if and only if it was true in the old state.

Formally, a domain description a0 is a finite set of value propositions of the type " ✖ ✗ ✖ ✙ ✖ ✚ ✛ ✛ ✢ ✂ " (which describe the initial state), and a finite set of effect propositions of the type " ✦ ✧ ✚ ✩ ✪ ✫ ✪ ✂ ✖ ✭ ✂ ✄ ✆ ✞ ✞ ✞ ✆ ✂ ✯ " (which describe results of actions). The initial state ✁ ✂ consists of all the fluents ✂ ✤ for which the corresponding value proposition " ✖ ✗ ✖ ✙ ✖ ✚ ✛ ✛ ✢ ✂ ✤ " is contained in the domain description. (Here we are assuming that we have complete information about the initial situation.) We say that a fluent ✂ ✤ holds in ✁ if ✂ ✤ ☎ ✁ ; otherwise, we say that ✥ ✂ ✤ holds in ✁ . The transition function ✝ ✞ ✁ ✡ ☞ ✦ ✆ ✁ ✎ which describes the effect of an action ✦ on a state ✁ is defined as follows:

• ✱ we say that an effect proposition "✦ ✧ ✚ ✩ ✪ ✫ ✪ ✂ ✖ ✭ ✂ ✄ ✆ ✞ ✞ ✞ ✆ ✂ ✯ " is activated in a state ✁ if all ✏ fluent literals ✂ ✄ ✆ ✞ ✞ ✞ ✆ ✂ ✯ hold in ✁ ;
• ✱ we define ✑ ✒ ✡ ☞ ✦ ✆ ✁ ✎ as the set of all fluents ✂ ✤ for which a rule "✦ ✧ ✚ ✩ ✪ ✫ ✪ ✂ ✤ ✖ ✭ ✂ ✄ ✆ ✞ ✞ ✞ ✆ ✂ ✯ " is activated in ✁ ;
• ✱ similarly, we define ✑ ✔ ✡ ☞ ✦ ✆ ✁ ✎ as the set of all fluents ✂ ✤ for which a rule "✦ ✧ ✚ ✩ ✪ ✫ ✪ ✥ ✂ ✤ ✖ ✭ ✂ ✄ ✆ ✞ ✞ ✞ ✆ ✂ ✯ " is activated in ✁ ;
• ✱ if ✑ ✒ ✡ ☞ ✦ ✆ ✁ ✎ ✗ ✑ ✔ ✡ ☞ ✦ ✆ ✁ ✎ ✚ ✜ ✢ , we say that the result of the action ✦ is undefined;
• ✱ if the result of the action ✦ is defined in a state ✁ (i.e., if ✑ ✒ ✡ ☞ ✦ ✆ ✁ ✎ ✗ ✑ ✔ ✡ ☞ ✦ ✆ ✁ ✎ ✜ ✢ ), we define ✝ ✞ ✁ ✡ ☞ ✦ ✆ ✁ ✎ ✜ ☞ ✁ ✪ ✑ ✒ ✡ ☞ ✦ ✆ ✁ ✎ ✎ ✮ ✑ ✔ ✡ ☞ ✦ ✆ ✁ ✎ .

Aplan ✱ is defined as a sequence of actions ✲ ✦ ✄ ✆ ✞ ✞ ✞ ✆ ✦ ✯ ✳ . The result ✝ ✞ ✁ ✡ ☞ ✱ ✆ ✁ ✎ of applying a plan ✱ to the initial state ✁ ✂ is defined as

The planning problem is: given a domain a0 and a desired property, find a plan for which the resulting trajectory ✁ ✂ , ✁ ✄ ✹ ✺ ✻ ✜ ✝ ✞ ✁ ✡ ☞ ✦ ✄ ✆ ✁ ✂ ✎ , ✁ ✔ ✹ ✺ ✻ ✜ ✝ ✞ ✁ ✡ ☞ ✦ ✔ ✆ ✁ ✄ ✎ , etc., satisfies the desired property. In particular, if the goal is to make a certain fluent ✂ true, then the planning problem consists of finding a plan which leads to the state in which ✂ is true.

In addition to the planning problem, it is useful to consider the plan checking problem: given a domain, a desired property, and a candidate plan, check whether this action plan satisfies the desired property. It is known that in the presence of complete information about the initial situation, for fluent goals, plan checking is a tractable problem - i.e., there exists a polynomial-time algorithm for checking whether a given plan satisfies the given fluent goal [Bylander, 1994; Erol et al., 1995; Liberatore, 1997; Baral et al., 2000].

1.2 Temporal extensions: motivations

Let us give two examples of planning problems explaining why temporal extensions are desirable:

1. If we are planning a flight of an automatic spy miniplane, then the goal is not only to reach the target point (which can be described by the fluent ✾ ), but also to avoid detection; more formally, a fluent ✿ ("detected") must remain false all the time.
2. When planning a movement of a robot, we may want to require that not only the robot achieve its goal but also

that, whenever the robot strays from the desired trajectory, it should always be possible to bring the robot back to this trajectory (i.e., make the fluent ❀ ❁ ❂ ✾ ✦ ❄ ✞ ❆ ❂ ❀ ✾ ❉ true) by a single corrective action.

1.3 Linear temporal logic: brief reminder

In Linear Temporal Logic (LTL), in addition to the truth values of a fluent at the current moment of time, we can also refer to its truth values in the past and in the future. For this, LTL has several operators. Different authors use different notations for these operators. Since we will also analyze planning in branching time logic described in [Niyogi and Sarkar, 2000] as an extension of LTL, we will use notations from [Niyogi and Sarkar, 2000] for LTL operators.

LTL has four basic future operators:

• ✱ ❊ (neXt time in the future): ❊ ✱ is true at a moment time ❂ if ✱ is true at the moment ❂ ● ■ ;
• ✱ ❑ (Going to be always true): ❑ ✱ is true at the moment ❂ is ✱ is true at all moments of time ✁ ▼ ❂ .
• ✱ ❖ (sometime in the Future): ❖ ✱ is true at the moment ❂ if ✱ is true at some moment ✁ ▼ ❂ ;
• ✱ ◗ (Until): ✱ ◗ ❘ is true at the moment ❂ if ✱ is true at this moment of time and at all the future moments of time until ❘ becomes true.

Similarly, LTL has four basic past operators:

• ✱ ❚ (Previously): ❚ ✱ is true at a moment time ❂ if ✱ is true at the moment ❂ ❯ ■ ;
• ✱ ❲ (Has always been): ❲ ✱ is true at themoment ❂ if ✱ was true at all moments of time ✁ ❨ ❂ ;
• ✱ ❩ (Once or sometime in the past): ❩ ✱ is true at the moment ❂ if ✱ was true at some moment ✁ ❨ ❂ ;
• ✱ ❬ (Since): ✱ ❬ ❘ is true at the moment ❂ if ✱ is true at this moment of time and at all the past moments of time since the last time when ❘ was true.

We can combine several such operators: e.g., ❊ ✑ ✱ ✹ ✺ ✻ ✜ ❊ ❊ ❊ ✱ is true at a moment ❂ if ✱ is true at the moment ❂ ● ❫ .

In general, an LTL-goal is a goal which is obtained from fluents by using LTL operators and propositional connectives ❵ ("and"), ❛ ("or"), and ✥ ("not").

For example, the objective from our first planning problem can be easily formulated as the following LTL-goal: ❜ ✹ ✺ ✻ ✜ ✾ ❵ ✥ ✿ ❵ ❲ ☞ ✥ ✿ ✎ ✞

Comment. Some versions of LTL have additional operators, e.g., we may have interval operators in which moments of time ✁ ▼ ❂ or ✁ ❨ ❂ are restricted to a given interval [Bacchus and Kabanza, 1998; Niyogi and Sarkar, 2000].

1.4 Branching temporal logic: brief reminder

In the Branching Temporal Logic CTL [Emerson, 1990; Niyogi and Sarkar, 2000], in addition to LTL operations, we have two additional operators ❝ and ❞ which describe possible futures:

• ✱ ❝ ✱ (Exists path) is true at the state ✁ at the time ❂ if there exists a possible evolution of this state forwhich ✱ is true at this same moment ❂ .

• ✱ ❞ ✱ (All paths) is true at the state ✁ at the time ❂ if for all possible evolutions of this state, ✱ is true at this same moment ❂ .

For example, the requirement that, no matter what action we apply to the state ✁ , a fluent ✂ will always stay true, can be described as ❞ ☞ ❊ ✂ ✎ .

Similarly, we can describe in this language the fast maintainability requirement from our second planning problem: no matter what action we apply to the state ✁ , if a fluent ✂ stops being true after this action, we can always make the property ✂ true by applying appropriate correcting action.

In CTL, this fast maintainability requirement can be formulated as follows:

• ✱ Once we have already reached the next state ✁ a0 , the possibility to get ✂ back by applying a single correcting action means that either ✂ is already true, or there is a path in which ✂ will be true at the next moment of time ( ❊ ✂ ), i.e., that ✂ ❛ ❝ ☞ ❊ ✂ ✎ .
• ✱ So, the fast maintainability requirement means that every possible immediate future state ✁ a0 satisfies the above property ✂ ❛ ❝ ☞ ❊ ✂ ✎ , i.e., in CTL notations, that

Comment. The description of more general temporal logics can be found in [Gabbay et al., 1994].

2 Results

2.1 What kind of planning problems we are interested in

Informally speaking, we are interested in the following problem:

• ✱ given a domain description (i.e., the description of the initial state and of possible consequences of different actions) and a goal (i.e., a fluent which we want to be true),
• ✱ determine whether it is possible to achieve this goal (i.e., whether there exists a plan which achieves this goal).

We are interested in analyzing the computational complexity of the planning problem, i.e., analyzing the computation time which is necessary to solve this problem.

Ideally, we want to find cases in which the planning problem can be solved by a tractable algorithm, i.e., by an algorithm ✁ whose computational time ❂ ✂ ☞ ☎ ✎ on each input ☎ is bounded by a polynomial ✱ ☞ ✝ ☎ ✝ ✎ of the length ✝ ☎ ✝ of the input ☎ : ❂ ✂ ☞ ✡ ✎ ☞ ✱ ☞ ✝ ☎ ✝ ✎ (this length can be measured bit-wise or symbol-wise). Problems which can be solved by such polynomial-time algorithms are called problems from the class P (where P stands for polynomial-time). If we cannot find a polynomial-time algorithm, then at least we would like to have an algorithm which is as close to the class of tractable algorithms as possible.

Since we are operating in a time-bounded environment, we should worry not only about the time for computing the plan, but we should also worry about the time that it takes to actually implement the plan. If a (sequential) action plan consists of a sequence of ✎ ✔ ✏ actions, then this plan is not tractable. It is therefore reasonable to restrict ourselves to tractable plans, i.e., to plans ✑ whose duration ✒ ☞ ✑ ✎ is bounded by a polynomial ✱ ☞ ✝ ☎ ✝ ✎ of the input ☎ .

With this tractability in mind, we can now formulate the above planning problem in precise terms:

• ✱ given: a polynomial ✱ ☞ ❁ ✎ ✓ ❁ , a domain description a0 (i.e., the description of the initial state and of possible consequences of different actions) and a goal statement ❜ (i.e., a statement which we want to be true),
• ✱ determine whether it is possible to tractably achieve this goal, i.e., whether there exists a tractable-duration plan ✑ (with ✒ ☞ ✑ ✎ ☞ ✱ ☞ ✝ a0 ✝ ● ✝ ❜ ✝ ✎ ) which achieves this goal.

We are interested in analyzing the computational complexity of this planning problem.

2.2 Complexity of the planning problemwith goals expressible in Linear Temporal Logic

Theorem 1. For goals expressible in Linear Temporal Logic (LTL), the planning problem is NP-complete.

Comments.

• ✱ Since the planning problem is NP-complete even for simple (non-temporal) goals [Bylander, 1994; Erol et al., 1995; Liberatore, 1997; Baral et al., 2000], this result means that allowing temporal goals from LTL does not increase the computational complexity of planning.
• ✱ This result is in good accordance with the fact that the decidability problem for linear temporal logic is also NP-complete [Emerson, 1990].
• ✱ For readers' convenience, all the proofs are placed in the special Proofs section.

The proof of Theorem 1 is based on the following result:

Theorem 2. For goals expressible in Linear Temporal Logic (LTL), the plan checking problem is tractable.

We give the proofs of Theorems 1 and 2 for the version of Linear Temporal Logic which only uses eight basic temporal operators. However, as one can easily see from the proofs, these result remains true if we allow more sophisticated temporal operators, e.g., interval operators of the type ✘ ✙ ✛ ✜ ✣ ✤ meaning that the fluent is true in some future moment of time from the interval ✲ ❂ ✆ ✁ ✳ [Bacchus and Kabanza, 1998; Niyogi and Sarkar, 2000].

2.3 Complexity of the planning problemwith goals expressible in Branching Temporal Logic

Theorem 3. For goals expressible in Branching Temporal Logic CTL, the planning problem is PSPACE-complete.

Comment. This result is in good accordance with the fact that the decidability problem for most branching temporal logics is also PSPACE-complete [Gabbay et al., 1994].

For the Branching Temporal Logic, not only planning, but even plan checking is difficult:

Theorem 4. For goals expressible in Branching Temporal Logic CTL, the plan checking problem is PSPACE-complete.

Theorems 3 and 4 mean that allowing temporal goals from CTL can drastically increase the computational complexity of planning. These results, however, are not that negative because most safety and maintainability-type conditions can be expressed in a simple subclass of CTL. Namely, in the maintainability conditions like the one above, we do not need to consider all possible trajectories, it is sufficient to consider trajectories which differ from the actual one by no more than one (or, in general, by nomore than a0 ) states. In this case, the planning problem becomes much simpler:

Definition 1. Let a0 ▼ ✁ be a positive integer. We say that an expression in CTL is a0 -limited if this expression remains true when in all operators ❝ and ❞ , we only allow possible trajectories differ from the actual trajectory in no more than a0 moments of time.

For example, the above maintainability statement (1) means that all possible 1-deviations from the actual trajectory are maintainable and therefore, this statement is 1-limited.

Theorem 5. Let a0 ▼ ✁ be an integer. For a0 -limited goals expressible in Branching Temporal Logic CTL, the planning problem is NP-complete.

Theorem 6. Let a0 ▼ ✁ be an integer. For a0 -limited goals expressible in Branching Temporal Logic CTL, the plan checking problem is tractable.

2.4 Conclusions

Our first conclusion is that if, instead of traditional goals which only refer to the state of the system at the last moment of time, we allow goals which explicitly mention the actual past and actual future states, the planning problem does not become much more complex: it stays on the same level of complexity hierarchy.

Our second conclusion is that if we allow goals which refer to potential future, the planning problem can become drastically more complicated. Thus, we should be very cautious about such more general goals.

3 Proofs

Proof of Theorems 1 and 2. We already know that the planning problem is NP-complete even for the simplest possible case of LTL-goals: namely, for goals which are represented simply by fluents [Bylander, 1994; Erol et al., 1995; Liberatore, 1997; Baral et al., 2000]. Therefore, to prove that the general problem of planning under LTL-goals is NPcomplete, it is sufficient to prove that this general problem belongs to the class NP.

Indeed, it is known [Papadimitriou, 1994] that a problem belongs to the class NP if the corresponding formula ✘ ☞ ☎ ✎ can be represented as ✆ ✑ ✝ ☞ ✑ ✆ ☎ ✎ , where ✝ ☞ ✑ ✆ ☎ ✎ is a tractable property, and the quantifier runs over words of tractable length (i.e., of length limited by some given polynomial of the length of the input).

For a given planning situation ☎ , checking whether a successful plan exists or not means checking the validity of the formula ✆ ✑ ✝ ☞ ✑ ✆ ☎ ✎ , where ✝ ☞ ✑ ✆ ☎ ✎ stands for "the plan ✑ succeeds for the situation ☎ ". According to the above definition of the class NP, to prove that the planning problem belongs to the class NP, it is sufficient to prove the following two statements:

• ✱ the quantifier runs only over words ✑ of tractable length, and
• ✱ the property ✝ ☞ ✑ ✆ ☎ ✎ can be checked in polynomial time.

The first statement immediately follows from the fact that in this paper, we are considering only plans of polynomial (tractable) duration, i.e., sequential plans ✑ whose length ✝ ✑ ✝ is bounded by a polynomial of the length ✝ ☎ ✝ of the input ☎ : ✝ ✑ ✝ ☞ ✱ ☞ ✝ ☎ ✝ ✎ , where ✱ ☞ ❁ ✎ is a given polynomial. So, the quantifier runs over words of tractable length.

Let us now prove the second statement - that plan checking can be done in polynomial time. (This statement constitutes Theorem 2.) Once we have a plan ✑ of tractable length, we can check its successfulness in a situation ☎ as follows:

• ✱ we know the initial state ✁ ✂ ;
• ✱ take the first action from the action plan ✑ and apply it to the state ✁ ✂ ; as a result, we get the state ✁ ✄ ;
• ✱ take the second action from the action plan ✑ and apply it to the state ✁ ✄ ; as a result, we get the state ✁ ✔ ; etc.

At the end, we get the values of all the fluents at all moments of time. On each step of this construction, the application of an action to a state requires linear time; in total, there are polynomial number of steps in this construction. Therefore, computing the values of all the fluents at all moments of time indeed requires polynomial time.

Let us now take the desired goal statement ❜ and parse it, i.e., describe, step by step, how we get from fluents to this goal statement ❜ .

For example, for the above spy-plane goal statement ❜ ✠ ✾ ❵ ✥ ✿ ❵ ❲ ☞ ✥ ✿ ✎ , parsing leads to the following sequence of intermediate statements: ❜ ✄ ☛ ✜ ✥ ✿ , ❜ ✔ ☛ ✜ ✾ ❵ ❜ ✄ , ❜ ✑ ☛ ✜ ❲ ❜ ✄ , and finally, ❜ ✠ ❜ ✕ ☛ ✜ ❜ ✔ ❵ ❜ ✑ .

The number of the resulting intermediate statements cannot exceed the length of the goal statement; thus, this number is bounded by the length ✝ ❜ ✝ of the goal statement.

Based on the values of all the fluents at all moments of time, we can now sequentially compute the values of all these intermediate statements ❜ ✤ at all moments of time:

• ✱ When a new statement is obtained from one or two previous ones by a logical connective (e.g., in the above example, as ❜ ✕ ☛ ✜ ❜ ✔ ❵ ❜ ✑ ), then, to compute the value of the new statement at all ✒ moments of time, we need ✒ logical operations.
• ✱ Let us now consider the case when a new statement is obtained from one or two previously computed ones by using one temporal operations: e.g., in the above example, as ❜ ✑ ☛ ✜ ❲ ❜ ✄ ). Then, to compute the truth value of ❜ ✑ at each moment of time, we may need to go over all other moments of time. So, to compute ❜ ✤ for each moment of time ❂ , we need ☞ ✒ steps. Hence, to compute the truth value of ❜ ✤ for all ✒ moments of time, we need ☞ ✒ ✔ steps.

In both cases, for each of ☞ ✝ ❜ ✝ intermediate statements, we need ☞ ✒ ✔ computations. Thus, to compute the truth value of the desired goal statement, we need ☞ ✒ ✔ a0 ✝ ❜ ✝ computational steps. Since we look for plans for which ✒ ☞ ✱ ☞ ✝ a0 ✝ ● ✝ ❜ ✝ ✎ for some polynomial ✱ ☞ ❁ ✎ , we thus need a polynomial number of steps to check whether the given plan satisfies the given goal.

So, we can check the success of a plan in polynomial time, and thus, the planning problem indeed belongs to the class NP. The theorems are proven.

Proof of Theorem 3. This proof follows the same logic as proofs of PSPACE-completeness of other planning problems; see, e.g., [Littman, 1997] and [Baral et al., 2000].

By definition, the class PSPACE is formed by problems which can be solved by a polynomial-space algorithm. It is known (see, e.g., [Papadimitriou, 1994]) that this class can be equivalently reformulated as a class of problems for which the checked formula ✝ ☞ ☎ ✎ can be represented as ✁ ✑ ✄ ✆ ✑ ✔ ✞ ✞ ✞ ✝ ☞ ✑ ✄ ✆ ✑ ✔ ✆ ✞ ✞ ✞ ✆ ✑ ✂ ✆ ☎ ✎ , where the number of quantifiers a0 is boundedby a polynomial of the length of the input, ✝ ☞ ✑ ✄ ✆ ✞ ✞ ✞ ✆ ✑ ✂ ✆ ☎ ✎ is a tractable property, and all a0 quantifiers run over words of tractable length (i.e., of length limited by some given polynomial of the length of the input). In view of this result, it is easy to see that for CTL-goals, the planning problem belongs to the class PSPACE. Indeed, all the operators of CTL can be described by quantifiers over words of tractable length, namely, either over paths (for operators ❞ and ❝ ) or over moments of time (for LTL operators). A plan is also a word of tractable length. Thus, the existence of a plan which satisfies a given CTL-goal can be described by a tractable sequence of quantifiers running over words of tractable length. Thus, for CTL-goals, the planning problem does belong to PSPACE.

To prove that the planning problem is PSPACE-complete, we will show that we can reduce, to the planning problem, a problem known to be PSPACE-complete: namely, the problem of checking, for a given propositional formula ✘ with the variables ✡ ✄ ✆ ✞ ✞ ✞ ✆ ✡ ✯ ✆ ✡ ✯ ✒ ✄ ✆ ✞ ✞ ✞ ✆ ✡ ☛ , the validity of the formula ☎ of the type ✆ ✡ ✄ ✁ ✡ ✔ ✆ ✡ ✑ ✁ ✡ ✕ ✞ ✞ ✞ ✘ ✞ This reduction will be done as follows. Consider the planning problem with two actions ✦ ✒ and ✦ ✔ , and ✎ ❁ ● ■ fluents ✡ ✄ ✆ ✞ ✞ ✞ ✆ ✡ ☛ , ❂ ✂ ✆ ❂ ✄ ✆ ✞ ✞ ✞ ✆ ❂ ☛ . These actions and fluents have the following meaning:

• ✱ the meaning of ❂ ✤ is that we are at moment of time ✆ ;
• ✱ the action ✦ ✒ , when applied at moment ❂ ✤ ✔ ✄ , makes ✆ -th variable ✡ ✤ true;
• ✱ the action ✦ ✔ , when applied at moment ❂ ✤ ✔ ✄ , makes ✆ -th variable ✡ ✤ false.

The corresponding initial conditions are:

• ✱ ✖ ✗ ✖ ✙ ✖ ✚ ✛ ✛ ✢ ✥ ✡ ✤ (for all ✆ );
• ✱ ✖ ✗ ✖ ✙ ✖ ✚ ✛ ✛ ✢ ❂ ✂ ; ✖ ✗ ✖ ✙ ✖ ✚ ✛ ✛ ✢ ✥ ❂ ✤ (for all ✆ ▼ ✁ ).

The effect of actions if described by the following rules (effect propositions):

• ✱ for ✆ ✜ ■ ✆ ✎ ✆ ✞ ✞ ✞ ✆ ❁ , the rules

describe howwe assign values to the variables ✡ ✤ ;

The corresponding goal is designed as follows:

• ✱ first, we replace in the above quantified propositional formula ☎ , each existential quantifier ✆ ✡ ✤ by ❝ ❊ , each universal quantifier ✁ ✡ ✤ by ❞ ❊ ; let us denote the result of this replacement by ✘ a0 ;
• ✱ then, we add ❵ ❂ ✂ to the resulting formula ✘ a0 ;
• ✱ finally, we add ❚ ☛ in front of the whole thing - creating ❚ ☛ ☞ ✘ a0 ❵ ❂ ✂ ✎ .

For example, for a formula ✆ ✡ ✄ ✁ ✡ ✔ ✘ , this construction leads to the following goal: ❚ ✔ ☞ ❝ ❊ ☞ ❞ ❊ ☞ ✘ ✎ ✎ ❵ ❂ ✂ ✎ ✞ This reduction leads to a linear increase in length, so this reduction is polynomial-time.

To complete the proof, we must show that this is a "valid" reduction, i.e., that the resulting planning problem is solvable if and only if the original quantified propositional formula is true.

To prove this equivalence, let us first remark that, by definition of the operator ❚ ("previous"), the goal formula ❚ ☛ ☞ ✘ a0 ❵ ❂ ✂ ✎ is true at a moment ❂ if and only if the formula ✘ a0 ❵ ❂ ✂ holds at a moment ❂ ❯ ❁ . Since, due to our rules, ❂ ✂ is only true at the starting moment of time ❂ ✜ ✁ , the goal can only be true if ❂ ✜ ❁ . Thus, to check whether we can achieve the goal, it is sufficient to check whether we can achieve it at the moment ❁ , i.e., after a sequence of ❁ actions. In this case, the validity of the goal is equivalent to validity of the formula ✘ a0 at the initial moment ❂ ✜ ✁ .

Let us now show that the validity of the formula ✘ a0 at the moment ❂ ✜ ✁ is indeed equivalent to the validity of the above quantified propositional formula. We will prove this equivalence by induction over the total number of variables ❁ .

Induction base: For ❁ ✜ ✁ , we have no variables ✡ ✤ at all, so ✘ is either identically true or identically false. In this case, ✘ a0 simply coincides with ✘ , so they are, of course, equivalent.

Induction step: Let us assume that we have proven the desired equivalence for all quantified propositional formulas with ❁ ❯ ■ variables; let us prove it for quantified proposi-

tional formulas with ❁ variables.

Indeed, let a quantified propositional formula ☎ of the above type be given. There are two possibilities for the first variable ✡ ✄ of this formula:

• ✱ it may be under the existential quantifier ✆ ✡ ✄ ; or
• ✱ it may be under the universal quantifier ✁ ✡ ✄ .

■ ✠ . In the first case, the formula ☎ has the form ✆ ✡ ✄ ☛ , where for each ✡ ✄ , ☛ is a quantified propositional formulawith ❁ ❯ ■ variables ✡ ✔ ✆ ✞ ✞ ✞ ✆ ✡ ☛ . According to our construction, the CTL formula ✘ a0 has the form ❝ ☞ ❊ ✌ a0 ✎ , where ✌ a0 is the result of applying this same construction to the formula ☛ .

To show that ✘ a0 is indeed equivalent to ☎ , we will first show that ✘ a0 implies ☎ , and then that ☎ implies ✘ a0 .

■ ✞ ■ ✠ ✞ Let us first show that ✘ a0 implies ☎ .

Indeed, by definition of the operator ❝ , if the formula ✘ a0 ✠ ❝ ☞ ❊ ✌ a0 ✎ holds at themoment ❂ ✜ ✁ thismeans that there exists a path for which, at moment ❂ ✜ ✁ , the formula ❊ ✌ a0 is true.

By definition of the operator ❊ ("next"), the fact that the formula ❊ ✌ a0 is true at the moment ❂ ✜ ✁ means that the formula ✌ a0 is true at the next moment of time ❂ ✜ ■ .

By the time ❂ ✜ ■ , we have applied exactly one action which made ✡ ✄ either true or false, after which the value of this variable ✡ ✄ does not change. Let us select the value ✡ ✄ as "true" or "false" depending on which value was selected along this path.

The moment ❂ ✄ can be viewed as a starting point for the planning problem corresponding to the remaining formula ☛ . By induction assumption, the validity of ✌ a0 at this new starting moment is equivalent to the validity of the quantified propositional formula ☛ . Thus, the formula ☛ is true for this particular ✡ ✄ , hence the original formula ☎ ✠ ✆ ✡ ✄ ☛ is also true. So, ✘ a0 indeed implies ☎ .

■ ✞ ✎ ✠ ✞ Let us now show that ☎ implies ✘ a0 .

Indeed, if ☎ ✠ ✆ ✡ ✄ ☛ is true, this means that there exists a value ✡ ✄ for which ☛ is true. By the induction assumption, this means that for this same ✡ ✄ , the goal formula ✌ a0 is also true at the new starting moment ❂ ✜ ■ . Thus, for any path which starts with selecting this ✡ ✄ , the formula ❊ ✌ a0 is true at the previous moment ❂ ✜ ✁ . Since this formula is true for some path, by definition of the operator ❝ , it means that the formula ❝ ☞ ❊ ✌ a0 ✎ is true at the moment ❂ ✜ ✁ , and this formula is exactly ✘ a0 .

Thus, ☎ does imply ✘ a0 , and hence ☎ and ✘ a0 are equivalent.

• ✎ ✠ ✞ The second case, when ✡ ✄ is under the universal quantifier ✁ ✡ ✄ , can be handled similarly.

The induction step is proven, and thus, by induction, the equivalence holds for all ❁ .

Thus, the reduction is valid, and the corresponding planning problem is indeed PSPACE-complete. Q.E.D.

Proof of Theorem 4. Similarly to the proof of Theorem 3, we can show that plan checking belongs to the class PSPACE, so all we need to prove is the desired reduction. From the proof of Theorem 3, one can see that the exact same reduction will work here as well, because in this reduction, the equivalence between ☎ and ✘ a0 did not depend on any action plan at all. The equivalence used in the proof of Theorem 3 is based on the analysis of possible trajectories and does not use the actual trajectory at all.

Thus, we can pick any action plan (e.g., a sequence consisting of ❁ actions ✦ ✒ ), and the desired equivalence will still hold. Q.E.D.

Proof of Theorems 5 and 6. For trajectories of duration ✒ , with a0 possible actions at each moment of time, there are no more than ✒ a0 a0 possible trajectories differing in one state, no more than ☞ ✒ a0 a0 ✎ ✔ trajectories differing in two states, etc. In general, whatever number a0 we fix, there is only a polynomial number ( ☞ ☞ ✒ a0 a0 ✎ ✂ ) of possible trajectorieswhich differ from the actual one in ☞ a0 places.

Therefore, for fixed a0 , we can explicitly describe the new operators ❝ and ❞ by enumerating all such possible trajectories. Thus, similarly to the proof of Theorems 1 and 2, we can conclude that for a0 -planning, plan checking is tractable and the corresponding planning problem is NP-complete.

Acknowledgments

This work was supported by NASA (grant NCC5-209 and a Research on Intelligent Systems grant), by the AFOSR grant F49620-00-1-0365, by the grant W-00016 from the U.S.- Czech Science and Technology Joint Fund, and by the NSF grants IRI 9501577, 0070463, and 9710940Mexico/Conacyt.

The authors are thankful to the anonymous referees for valuable comments.