--- title: "Synthesizing Plant Controllers Using Real-time Goals" authors: - "Michel Barbeau" - "Froduald Kabanza" - "Richard St-Denis" doi: "" url: "https://ijcai.org/proceedings/1995/103" pdf: "https://ijcai.org/proceedings/1995/0103.pdf" venue: "Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence" year: 1995 pages: "791-799" track: "Knowledge Base Technology" keywords: --- # Synthesizing Plant Controllers Using Real-time Goals Michel Barbeau, Froduald Kabanza, Richard St-Denis *Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence*, pages 791-799. ## Abstract This paper introduces a novel planning method for reactive agents. Our planning method handles, in a single framework, issues from AI, control theory, and concurrency that have so far been considered apart. These issues are mostly controllability, safety, bounded liveness, and real time. Our approach is founded on the supervisory control theory and on Metric Temporal Logic (MTL) . The highlights of our method consist of a new technique for incrementally checking MTL goal formulas over sequences of states generated by actions and a new method for backtracking during search by taking into account uncontrollable actions. ## Full text ## 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- Figure 1: A model of control ![Image](https://ijcai.org/proceedings/1995/fulltext/103/image_000000_026faade852a7a1ee8692e0537addd35db27f83780c7ef021b81a051b58809dc.png) 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 ``` Figure 2: Progression algorithm for BMTL formulas . 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 3: Prologue to the planning algorithm 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