Synthesizing Plant Controllers Using Real-time Goals

1 Introduction

A reactive plan is a program that specifies the actions to be executed by an agent that continuously reacts to the occurrence of discrete events from its environ­ ment. The automatic synthesis of reactive plans is a key component in the design of autonomous systems. It is of interest in AI planning [Georgeff and Lansky, 1987; Drummond and Bresina, 1990; Dean et al., 1993], con­ trol theory [Ramadge and Wonham, 1989; Makungu et al., 1994], and concurrency theory [Emerson, 1990]. In these areas, the terms control rules, supervisor, and re­ active programs are respectively used to denote reactive plans. However, the paradigms used to generate such plans vary widely. In AI planning, the focus is on repre­ senting and reasoning about actions in an efficient and natural way. This has led researchers in this field to con­ centrate on heuristic search techniques. Unfortunately, little research in AI planning has taken into account the concepts of controllable actions and liveness goals.

In the area of control theory, the emphasis has been on reasoning about the issues of controllability and ob­ servability of actions [Ramadge and Wonham, 1989]. A

This work was supported by the Canadian Government through its NSERC programs.

key characteristic of models of actions in this field is that they distinguish between controllable and uncontrollable actions. This facilitates reasoning about controllability issues.

In concurrency, modal temporal logic has been recog­ nized as a useful tool for dealing with liveness properties. For instance, real-time modal temporal logic can express bounded-time response properties of the form "each oc­ currence of event e leads to satisfaction of condition c within 5 time units" [Alur and Henzinger, 1993]. One interesting development in this area is model checking [Emerson, 1990]. In this approach, verifying a program is viewed as evaluating the truth of a temporal formula on a temporal structure representing the program.

In this paper, we describe a method for generating reactive plans. Our method borrows concepts and con­ cerns from all the three areas outlined above. From AI planning, we take the concern of reasoning about actions and using heuristic search to generate plans. From con­ trol theory, we borrow the concept of controllable action. As in concurrency theory, we are also concerned with the representation and reasoning about real time, safety, and liveness goals.

To be more specific, our planner takes as input a goal, a description of the primitive actions of a reactive agent, which are controllable, and those of its environment, which are uncontrollable . The planner returns a reac­ tive plan for achieving the goal. Note that both the agent and its environment are referred to as the process or plant in control theory. We generate plans essentially by searching among sequences of states that represent executions of primitive actions, checking whether they satisfy the goal or not. Reactive plans are more or less immediately extracted from satisfactory sequences. We describe goals using Metric Temporal Logic (MTL) for­ mulas [Alur and Henzinger, 1993].

Recent research has investigated connections between AI planning, control, and concurrency. This includes work on representation of AI control programs [Nilsson, 1994], a recent book by Dean and Wellman on plan­ ning and control [Dean and Wellman, 1991], work on the integration of planning and concurrency ideas [Godefroid and Kabanza, 1991; Kabanza, 1990], and work on the synthesis of controllers in temporal logic frame­ works [Thistle and Wonham, 1986; Fusaoka et al., 1983]. We view our contribution to this research in three re­ spects. First, our planner integrates concepts and con­ cerns from the above three fields deeper than any ex­ isting comparable framework. Hence, besides its more general capabilities, our planner contributes to a better understanding of issues in the boundaries of these fields.

Second, we introduce a method for checking MTL goals over state sequences on the fly (i.e., incremen­ tally). In contrast to other techniques for checking sim­ ilar real-time formulas (e.g., [Alur and Benzinger, 1993; Alur et al., 1993]), our technique does not require an explicit storage of the state-transition graph over which formulas are checked. Rather, our planner generates and checks state sequences on the fly. This allows us to gen­ erate plans using a standard forward-chaining search. It also lets our planner generate plan control rules incre­ mentally. In this way, our planner can be considered as having anytime capability. According to Dean and Boddy [Dean and Body, 1988], an anytime algorithm is one that can be stopped at different stages of its pro­ cessing and yield an approximate, but useful, result.

Third, we introduce a search technique, called control­ directed backtmcking. This technique uses selective back­ tracking to states from which the planner can expand controllable paths. We use an example to demon­ strate that this approach can allow the planner to prune the search space significantly. This search technique is reminiscent of, but quite different from, the mech­ anisms used in dependency-directed backtmcking [Stall­ man and Sussman, 1978] and partial-order search using Mazurkiewicz's tmces [Godefroid and Kabanza, 1991].

Although our planning approach applies to standard MTL and more general logics, due to space limitations, we will describe it only for a restricted class of MTL formulas called bounded-time MTL formulas (BMTL). Even with this restriction, our planner handles prob­ lems that are beyond the scope of comparable AI plan­ ning or control-theoretic frameworks. For example, as was mentioned above, our planner treats various types of bounded-time goals.

The remainder of this paper is organized in three parts, beginning with the description of our model of actions and plans. This is followed by a brief overview of MTL and a description of our planning method.

2 Actions and Plans

We adopt the following model of plans from Ramadge and Wonham 1 [Ramadge and Wonham, 1989]. A pro­ cess is modeled as a spontaneous generator of sequences of actions. The set of actions A of the process are par­ titioned into two disjoint subsets Au and Ac. The actions in Au are uncontrollable, while those in Ac are controllable. Hence, the evolution of the process can be controlled by prohibiting the occurrence of some con­ trollable actions at certain points. A control input is a subset 1 of A satisfying the condition Au ~ I· If a E /, then a is permitted to occur. Let L denote the set of sequences of actions that can be generated by the pro­ cess and r ~ 2.A represent the set of all control inputs. A plan is a map f : L -+ r yielding, for each sequence w E L of generated actions, the control input f( w) to be applied to the process at that point . Language LJ de­ notes the sequences of actions generated by the process under the supervision of f. Let f be the empty string, a E A, and wE A*. The language L1 is formally defined as follows:

1 As was mentioned in the introduction, we use the term "plan" as a synonym for supervisor.

1. f E L1 and
2. wa E LJ iff wE LJ, a E f(w), and wa E L.

In our framework, the process consists of a reactive agent and its environment, both performing primitive actions (see Figure 1). The actions performed by the agent are controllable, whereas those performed by the environ­ ment are uncontrollable. ·We model the interaction be­ tween the agent and its environment by interleaving their actions.

--j Supervisor r-

Actions There are varwus models of actions in the · fields of AI, concurrency, and control theory. Repre­ sentations of actions in planning are mostly based on STRIPS-like models [Fikes and Nilsson, 1972] . Models of actions in concurrency and control theory are often based on state-transition machines such as automata or Petri nets. Nevertheless, all these models are more or less theoretically equivalent. For example, a state-transition model can be derived from a STRIPS-like formalism by generating the states reachable from one or several ini-· tial states. Hence, without loss of generality, we assume a STRIPS-like formalism in this paper.

The STRIPS model of actions includes two basic con­ cepts, namely, world state and primitive action. A world state is defined as a set of propositions. Propositions model facts about states of the agent and its environ­ ment. Every primitive action is described by a precondi­ tion (a conjunction of propositions enabling the action), a delete-list (a list of propositions retracted by the execu­ tion of the action), and an add-list (a list of propositions asserted by the execution of the action). Note that, in general, variables are used to describe schemata of in­ stances of actions.

For the sake of clarity, we use the following functions to manipulate actions. Let S denote a world state and a an action. The transition function &(a, S) returns the successor world state of S after execution of action a. The function Controllable(a) returns true if a is con­ trollable, otherwise it returns false. The function &(a, S) is defined only when a is enabled in S. When it is de­ fined, the result of &(a, S) is obtained by removing from S the propositions in the delete-list of a and then adding the propositions in the add-list of a.

Operational representation of a plan For conve­ nience, we adopt the following automaton representa­ tion of a plan f . A plan is represented by a pair (R, cp) , where R = (Y, A,~, Yo) is a finite-state automaton 2 and cp : Y -+ r is an output map yielding, for each state of R, the control input to be applied to the process at that point . A pair (R, cp) represents a plan f if for every wE LJ , cp(~(w,y0 )) = f(w) . Intuitively, the value off on the sequence of actions w is obtained by the applica­ tion of w to R, causing R to move from its initial state y0 to the state y = ~ ( w, Yo) , and then calculating the control input cp(y) .

3 Metric Temporal Logic

In this section, we summarize the MTL formulas that we use to describe goals [Alur and Henzinger, 1993].

Syntax MTL formulas are constructed from an enu­ merable collection of propositional symbols, the boolean connectives 1\ (and) and ..., (not), and the temporal modalities U-x (until), o_x (always) , where ,...... denotes =, ~ , or ~, and x is an integer. The formula forma­ tion rules are (1) every propositional symbol pis a for­ mula, and (2) if 11 and !2 are formulas, then so are ...,11, 111\/2, D_x 11, and h U-x 11. 3 The following abbrevi­ ations are standard: <> -x f = true U -x f (eventually f) and 11-+ 12 = ...,11 V 12 (11 implies /2) .

Semantics MTL formulas are interpreted over mod­ els of the form M = (S, 1r , 7), where S is an infinite sequence of states so, s1 , ... ; 1r is a function that takes a proposition and a state as input and returns true if the proposition holds in the state; and 7 is a function that associates a time stamp with each state. As usual, we write (M, s) I= f if state s in model M satisfies formula f . In addition to the standard rules for the boolean con­ nectives, we have that, for a state s; in a model M, a propositional symbol p, and formulas 11 and h :

2 In this paper, all the states of automata are accepting.

3 Note that the standard MTL also has a congruence mod­ ulo constraint and a next modality [Alur and Henzinger, 1993] .

• (M, s;) I= p iff 1r(p, s;) = true;
• (M, s;) I= o_x 11 iff Vj such that /(sj ) ,...... T(si)+x , (M,sj ) I= 11 ;
• (M, s;) I= 11 U-x h iff 3j such that T(sj ) ,...... T(si)+ x, (M, Sj) I= /2, and (M, sk) I= 11 Vk, i ~ k < j.

Finally, we say that the model M (or sequence of states S E M) satisfies a formula f if (M, so) I= f.

Bounded-time MTL Formulas As was mentioned in the introduction, we describe our planning algorithm only for bounded-time MTL formulas. These formulas are defined in terms of normalized MTL formulas. A normalized MTL formula is one in which only proposi­ tional symbols are negated. 4 A bounded-time MTL for­ mula is a normalized MTL formula in which every until modality is of the form U ~x .

Example 3.1 The formula <><1o D>o p (i.e., p holds within 10 time units and remains tr-;ie afterwards) ex­ presses a classical goal requirement in AI planning and stability in control theory [Fusaoka et al., 1983] . In Fig­ ure 7, the formula g1 expresses the safety (mutual ex­ clusion) requirement that c(i) and m(i), 1 ~ i ~ 4, are never true simultaneously. The formula g2 expresses the liveness requirement that c(2) and c( 4) become simulta­ neously true infinitely often, at intervals shorter than 5 time units. ·

4 Planning Method

4.1 Global view

Given a set of primitive actions, an initial state, and a goal, our planner searchs for sequences of world states , starting from the initial state, and checking on the fly whether or not sequences of states expanded so far sat­ isfy the goal. Reactive plans are extracted from sat­ isfactory sequences. Our search process differs from a classical forward-chaining exploration in three respects. First, the check of MTL goals requires that we actu­ ally search in a space of pairs where each pair consists of a world state and an MTL formula, rather than sim­ ply a space of world states. Second, transitions corre­ sponding to uncontrollable actions are subject to special treatment. Third, when we reach a sink, we backtrack taking into account the fact that some transitions are uncontrollable. As will be illustrated, our backtracking mechanism can lead to considerable savings compared to blind backtracking.

To check formulas over state sequences on the fly , we associate an MTL formula to each world state. The formula attached to a state must be satisfied by each sequence starting from this state. The planner uses a mechanism of progressing MTL subformulas through world states to compute the formulas to be attached to states. Intuitively, progressing an MTL formula through a world state consists in checking that the present re­ quirement conveyed by the formula is satisfied in this state. If so, a formula representing the future require­ ment is returned, otherwise false is returned. Hence, given a current world state and an action, the formula representing the future requirement is paired with the successor world state obtained by applying the action to the current world state.

4 For any MTL formula, we can obtain an equivalent nor­ malized formula by using logical equivalences to propagate the negation symbol inwards.

4.2 Formula Progression

The formula progression algorithm is described in Fig­ ure 2. The function Prog accepts as input an MTL for­ mula f , a world states, a real number t , and a function 1r(p, s) , which returns true only if the proposition p holds in the world state s. It returns an MTL formula repre­ senting the progression off through s. This algorithm is characterized by the following theorem.

function Prog(f ,s,t,1r) 1. case f 2. p (p a proposition) : 1r(p, s ); 3. ·h : ·Prog(fl , s,t,1r); 4. h 1\ h : Prog(fl, s, t, 1r) 1\ Prog(h , s, t , 1r) ; 5. h V h : Prog(fl , s, t, 1r) V Prog(h , s, t , 1r) ; 6. D=.x fl : if x- t > 0 then o=(.x-t) h 7. else Prog(ft, s, t , 1r) ; 8. Ds, ft : if x- t > 0 then Prog(ft, s, t, 1r) A o:S;(.x-t) It 9. else Prog(ft, s, t, 1r); 10. o~"' ft: if x- t > 0 then o~(.x-t) It 11. else Prog(ft,s,t,7r)I\D>oft ; 12. ft U=.x h : - 13. if x- t > 0 then Prog(ft , s, t, 1r)l\ It U=(.x-t} h 14. else Prog(h, s, t , 1r); 15. hU<.x h: 16. if-x- t > 0 then Prog(h, s, t, 1r)V 17. (Prog(fl, s, t, 1r)l\ It Us(.x-t} h) 18. else Prog(h , s, t, 1r); end

Theorem 4.1 Let M = (S, 1r , 7) be any MTL model and let s; be the ith state in the sequence of states S . Then, we have for any MTL formula f , (M, s;) I= f if and only if (M, Si+l) I= Prog(f, Si+l, /(s;+l)-T(s;), 1r) .

The time difference /(si+l) - T(s;) corresponds to the duration of the action that leads to s;+l from s;. For the sake of simplicity, we assume that each action takes 1 time unit .

4.3 The Planning Algorithm

We can now detail the algorithm of our planner. The input consists of an initial world state x0 , a set of prim­ itive actions A, the transition function~ . an MTL goal g, and the function 1r (see Figure 3). It outputs a plan (R, <p) . For the sake of clarity, the planning algorithm is divided into three parts: the prologue (Figure 3) , search process (Figure 4) , and epilogue (Figure 5).

• function Planner( in xo, f> , A, g, 1r , out (R, cp)) 1. fo ~ Prog(g,xo,0,1r); 2. if fo = false then return the empty solution; 3. [xo, fo].pct ~ {}; [xo, fo].pre ~ {}; 4. [xo , fo].status ~undefined; 5. [xo , fo] .controllable ~ false; 6. CLOSED~ {} ; OPEN~ {[xo,/o]};

7. repeat select [x ,!] in OPEN; 8. [x, !] . controllable ~ true; 9. CLOSED~ CLOSED U {[x, f]}; OPEN~ OPEN\ {[x , f]} ; 10. for each a in A such that f>(a , x) is defined do I* Expand the state [x, f] *I 11. x' ~a( a, x); f' ~ Prog(f, x', 1, 1r) ; 12. iff' = false or ([x', !'] E CLOSED and 13. [x', f'].status =sink) 14. then if not Controllable( a) I* [x, f] becomes sink *I 15. [x, !].controllable ~false; Sink([x , J]); 16. break; 17. else 18. €(a, [x, f]) ~ [x', !']; 19. if (x', f']lt CLOSED and (x', f']lt OPEN then /* Initialization of a new state *I 20. [x', !'] .pet~{}; [x', f1 .pre ~ {}; 21. [x , !].status~ undefined; 22. [x', !'].controllable ~ false; 23. OPEN~ OPEN U {[x', f']}; 24. if Controllable( a) then 25. [x', f'].pct ~ [x', f1 .pct U {[a, [x,J]]} ; 26. else 27. [x', !'] .pre~ [x', !'].pre U {[x , !]}; 28. [x , !].controllable ~false; 29. if [x, !].controllable =true then I* Check for a trivial satisfactory state *I 30. if not Has_Eventually([x, f]) 31. then Satisfactory([x , f]); 32. until OPEN = {}; I* Check for non trivial satisfactory states *I 33. Check_Non..TriviaLSatisfactory..States();

Figure 4: Search process of the planning algorithm

Prologue The prologue consists in initializing a search graph that implements an intermediate automaton M = (X x F, A, ~ ~ [xo, fo]) , where F is a set of bounded-time MTL formulas derived from g using the formula progres­ sion algorithm. The set of states X x F is partitioned into expanded and unexpanded states. Initially, the set of expanded states, CLOSED, is empty; the set of unex­ panded states, OPEN, contains the initial state [x0, f0], where fo = Prog(g, xo , 0, 1r) . Note that Prog(g, x0 , 0, 1r) returns a formula equivalent to g, since the time differ­ ence used is 0. The purpose is to check that the present requirement of g is satisfied in x0 .

Overview of the Search Process The search pro­ cess repeatedly selects a state [x , f] from OPEN and proceeds as follows . For each action enabled in x, it

I* Compute the reactive plan (supervisor) *I 34. if [xo, fo].status =satisfactory 35. then R f- {CLOSED,at, A, ~·at, [xo, fo]) ; 36. else return the empty solution; f* Compute the feedback function <p *I 37. for each [x,J] in CLOSED, at do 38. for each a in A do 39. if <5(a, x) is defined and ~·at(a, [x, f]) is defined 40. then <p([x,f]) f- <p([x,f])U{a}; end

computes a successor [x', J'], where x' = 8(a , x) and f' = Prog(f, x', 1, 1r) .

Epilogue The epilogue derives a plan (R, <p) from the intermediate automaton M as follows. First, the plan­ ner removes the states that are not satisfactory from M to obtain the automaton R (lines 34-35). Then <pis ob­ tained by including in <p(s) an action a for each transition (s, a, s') of R (lines 37-40) . Hence, a crucial step in our planning process is to determine satisfactory states.

Example 4.1 Let us consider the maze example pic­ tured in Figure 6 (taken from [Ramadge and Wonham, 1989]) . The maze has five rooms. There are a cat and a mouse moving from one room to another through door­ ways. Every doorway is either for the exclusive passage of the cat (c1, ... , c7) or the mouse (m1 , ... , m5) . Door­ way c7 is bidirectional and uncontrollable, while oth­ ers are unidirectional and controllable (i.e., they can be closed) . The goal of this process consists of two require­ ments. First, the cat and the mouse must never occupy the same room simultaneously. Second, after leaving their initial rooms (room 2 for the cat and room 4 for the mouse) , they must return within 5 time units. These requirements are specified by formula fo in Figure 7 (this formula is also commented on in Example 3.1).

Figure 7 details the expansion of the search graph (i .e. , automaton M) for this example. Every state of the graph is composed of a world state, which is a pair consisting of the cat and mouse positions, and an MTL formula. For clarity in the figure , we only indicate for­ mulas for some states of the graph. The initial state is [(2, 4) , fo] . The formulas fi , 1 ~ i ~ 5, are defined in Figure 7. A proposition c( i) ( m( i)) means that the cat (mouse) is in room i. The initial formula fo is the result of progressing the goal 91 1\ 92 through the world state (2, 4) with a time difference of 0. States are expanded by applying actions as explained above. For instance, [(0, 4), 11] is produced by applying action c3 to obtain the world state (0, 4) and by progressing fo through (0, 4), using a time difference of 1, to get 11 · Note that the eventually modality in 11 is bounded by 4, which con­ veys the fact that one unit of time has elapsed. The expansion of [(0, 4), 11] into [(1, 4), h) by applying the action c1 is similar.

The expansion of [(1,4),/2] into [(2,4),/o] by apply­ ing c2 deserves more comment . Following lines 15-18 of the formula progression algorithm, the progression of <><3 (c(2) 1\ m(4)) , which is a conjunct of /2, through (f 4) yields true V <:>9(c(2) 1\ m(4)), which is simplified as true. In this way, the progression of h through (2, 4) yields J0 , hence closing a cycle. Note that the infinite ex­ ecution represented by this cycle satisfies fo . In general, as explained below, each cycle generated by our search process is necessarily satisfactory.

In Figure 7, solid lines represent transitions of the plan. Dashed lines represent paths that have been ex­ plored then rejected when the planner has determined that they lead to sinks. For instance, state [(3, 3), /s] is a sink because it violates the subgoal 91 of fo . This violation causes the progression of /3 through (3, 3) to return false, i.e., fs . From such trivial sinks, the planner derives less trivial ones. For example, state [(1, 3), /3] also becomes a sink because action c7 is uncontrollable.

Dotted lines represent parts of the search space that are not explored by our search process due to the use of the dependency-directed backtracking technique ex­ plained below. ·

Determining Satisfactory States and Sinks We extend the notion of controllable action to a notion of controllable state. A state is controllable if it is expanded (i.e., it is in CLOSED) and all its outgoing transitions are due to controllable actions. Each state is attached with a slot, controllable, indicating whether it is controllable or not. This slot is set to false for each newly created state. To each state is also attached a status that indicates whether the state is sink, satisfactory, or still undefined. The status of each newly created state is set to undefined. Then, the search process updates the status of expanded states based on the following definitions.

Definition 4.1 A sink is ( 1) a state of the form [ x, false) or (2) a state from which there is an outgoing uncon­ trollable transition to a sink or (3) a state involving an eventually modality and from which there is no enabled action or all enabled actions lead to sinks.

Condition 1 constitutes a basic case for determining sinks. It is implemented by the lines 14-16 of the planner's algorithm. Condition 2 constitutes one of two re­ cursive cases for determining sinks and is implemented in part by the function Sink . This function is described in Figure 8 and is discussed below. Condition 2 is also handled in part concurrently with Condition 3 by the procedure Check..Non_ Trivial...Satisfactory_States . This is further explained below.

Definition 4.2 A state is satisfactory if ( 1) it is control­ lable and does not involve an eventuality modality or (2) it is in a cycle not containing a sink or (3) there exists at least one transition to a satisfactory state and every outgoing uncontrollable transition leads to a satisfactory state.

Condition 1 specifies the most trivial of two basic cases for determining satisfactory states. It is implemented by the lines 29-31. Condition 2 constitutes the other less trivial basic case that needs further explanation. Each formula progression decreases the timing constraints of bounded-time eventualities by the duration of the ap­ plied action. That is, each progression yields a formula different from the current one. Hence, the search process cannot reach an ancestor state on the current path, i.e., it cannot close a cycle, unless all the eventualities have been achieved. Theorem 4.1 implies that each path ter­ minated by such a cycle satisfies the goal formula. Note that if we had unbounded-time eventualities, it would be possible to reach a cycle without achieving all the eventu-

function Sink(s); 1. s.status +- sink; 2. Mark_Useless(s); 3. for each s' in s.pre do 4. if s'.status f; sink then Sink(s'); end

alities, since the progression of an unbounded-time even­ tuality does not necessarily change it. Also note that a bounded-time eventuality cannot be progressed indefi­ nitely without being achieved, since sooner or later its timing constraint will reach 0, resulting in a sink.

Condition 2 is implemented in the function Check..Non_ Trivial...Satisfactory_States. The recursive case is handled by the procedure Satisfactory (Figure 9), which is called each time a basic satisfactory state has been identified. Because of space constraints, we de­ scribe Check..Non_ Trivial..Satisfactory_States informally. Essentially, Condition 2 must label all satisfactory states of the automaton M . When all the satisfactory states have been identified, the remaining states still labeled undefined become sinks. In this way, the planner also takes into account Condition 3 for sinks.

Control Directed Backtracking Search The idea of this search technique is to avoid expanding descen­ dants of nontrivial sinks. Indeed, such expansions are useless. For example, in Figure 7, when the expan­ sion has reached the sink [(3, 3), f 5], through the uncon­ trollable transition c7, state [(1, 3), h] also becomes a sink. It then becomes useless to expand descendants of [(1, 3), h] that cannot be reached through at least one path from the initial state.

To implement this idea, we need to attach backpointers to states to indicate their immediate parents: s .pre ~ 2(XxF) contains the set of immediate parents of s for which the transition to s is caused by an uncontrollable action; s.pct ~ 2(.Acx(XxF)) contains the set of control­ lable transitions incoming to s. Hence, if [a, s'] E s.pct, then state s can be avoided by disabling a at s', since a is controllable.

The control-directed backtracking mechanism is then implemented by the function Sink (see Figure 8). Given a sink s, this function explores, backwards, all ancestors of s reachable through a path formed only of uncon­ trollable transitions. Each state met in this traversal is marked "sink" and all its descendants are marked "use­ less" provided that their predecessors are sink or marked "useless" (the function Mark_Useless runs over descen­ dants of s , marking them "useless" until we meet a state already marked "useless" or for which at least one pre­ decessor is not marked "useless"). A state marked "use­ less" is removed from OPEN.

Note, however, that this process might mark states for which all the incoming transitions have not yet been generated. Hence, when these currently missing tran­ sitions are generated, the "useless" mark are removed. The overhead incurred by these removals can be avoided by deleting states rather than marking them. Deleted states would then be re-expanded when reached again by further expansions. In this way, we replace the over­ head due to updating the "useless" marks by the over­ head incurred by re-expanding states. The problem here is comparable to the management of backpointers in the search algorithm A · [Rich and Knight, 1991] (pp. 7679): one can either keep and update backpointers on expanded nodes, or re-expand them. Both strategies are incomparable in terms of performance.

5 Conclusion

In this paper, we have described a new planning method based on an original control-directed backtracking tech­ nique and a procedure for checking MTL goal formulas incrementally. Our framework generates plans of reac­ tive systems that take into consideration safety, liveness, and real-time constraints as well as controllable actions in a uniform way. Note that the computation of the feedback function t.p does not need to be done after the construction of the entire automaton R. Instead, we could detect satisfactory states at different stages of ex­ pansion and immediately update the function t.p accord­ ingly. This means that the processing done in the func­ tion Check_Non_Trivial..Satisfactory..States has to be in­ terleaved with the expansion process. In this way, t.p is produced incrementally. This gives anytime capability to our planner [Dean and Body, 1988].

As a matter of facts, the search process explained in the previous section can be seen as generating the prod­ uct of two timed automata (or timed transition graphs): one automaton accepting all the world-state sequences, and the other accepting the legal sequences (satisfying the MTL formula). The product automaton is simply a search graph in which world-states correspond to states in the world-state automaton and MTL formulas corre­ sponds to states in the MTL automaton. Our search pro­ cess computes this product on the fly . Thus, rather than specifying the transitions of the world-state automaton explicitly, we use a STRIPS-like action language to specify them succintly and then recursively apply actions to gen­ erate them only when they become relevant in the search process. Similarly, rather than specifying the transitions of the MTL automaton explicitly, we progress formu­ las to generate them only when they become relevant in the search process. Recently, Brandin and Wonham have proposed an approach in which the transitions of the two automata are specified explicitly [Brandin and Wonham, 1994]. Our approach has at least two advan­ tages with respect to their work. First, in our planner only world-states and MTL formulas that are relevant in the product are generated. In the Brandin and Won­ ham's approach, sink states and all potential time tran­ sitions must be specified explicitly in the input automata since their relevance can only be determined when con­ structing the product. Second, MTL specifications are declarative and are maintained as such during our search process. We think that this will facilitate debugging of controller specifications. For example, sink states rise when an MTL always modality is made false or the dead­ line of an eventually modality expires. These modalities provide information in a declarative form about unde­ sired states in the process being controlled.

We are investigating different complementary strate­ gies for coping with state explosion. Recent work in AI planning shows that forward-chaining search can be made effective using such strategies [Bacchus and Ka­ banza, 1995]. At the same time, work in control theory has demonstrated that a forward-chaining exploration can become effective with real-world problems using ef­ ficient implementation or modular techniques [Balemi et al., 1993; Brandin, 1994]. In the same trend, we intend to investigate the application of AI planning goal-regression techniques ([Rich and Knight, 1991]) to generate search control knowledge that specifies the relevance of actions to a given goal. With this knowledge, forward-chaining will explore the more relevant parts of the search space before the less relevant ones. The usual goal-regression techniques in AI planning deal only with goals of achiev­ ing state conditions. Our approach to handle general MTL goals is being influenced by two observations. On the one hand, an MTL eventually modality expresses a condition to be achieved. Thus, we could parse an MTL formula to extract the sub-formulas expressing condi­ tions to be achieved and then apply goal-regression tech­ niques to determine the relevance of actions to these con­ ditions. On the other hand, an MTL always modality expresses a condition to be maintained. Each uncontrol­ lable action that could falsify such a condition is rele­ vant since it might lead to sinks. Such relevant actions could also be determined using goal-regression . It thus seems possible to interleave the goal-regression processes of computing relevant actions and the forward-chaining one of generating accessible states. The challenge will be to study the tradeoffs between these processes and the ef­ fectiveness of their combination on real-world problems. In the same line of inquiry, we are also interested in ab­ straction over large numbers of states during search.