Logic-Based Subsumption Architecture

1 Introduction

In [Brooks, 1986], Rodney Brooks provided a decompo­ sition of the problem of robot control into layers corre­ sponding to levels of behavior, rather than a sequential, functional form. Within this setting, he introduced the idea of subsumption, that is, that more complex layers not only depend on lower , more reactive layers, but could also influence their behavior. The resulting architecture was one that could simultaneously service multiple, po­ tentially conflicting goals in a reactive fashion, giving precedence to high-priority goals.

Because of its realization in hardware, the architecture lacks declarativeness, making it difficult to implement higher-level reasoning and making its semantics unclear. The increasing hardware complexity with new layers in­ troduces scaling problems. And, relying on hardware specifications, the architecture is specifically oriented to­ wards robot control and is not applicable to software­ based intelligent agents. The problem of extending simi­ lar architectures to more complex tasks and goals and to agents that are not necessarily physical has already been raised and discussed in general terms by [Minsky, 1985] and [Stein, 1997], but to our knowledge, no practical AI architecture has been developed along these lines.

In this paper we describe an architecture that is mod­ eled in the spirit of Brooks' subsumption architecture but relies on a logical framework and has wider applica­ bility and extendibility in the manner described above. Our Logic-Based Subsumption Architecture (LSA) in­ cludes a set of First-Order Logic (FOL) theories, each corresponding to a layer in the sense of Brooks' archi­ tecture. Each layer is supplied with a separate theorem prover, allowing the system of layers to operate concur­ rently. We use nonmonotonic reasoning to model the connections between the theories. In addition, by allow­ ing the layers to make nonmonotonic assumptions, we have made each layer's performance independent of the performance of other layers, thus supporting reactivity.

We demonstrate our architecture by modeling four layers for the task of robot control, the bottom two of which are Brooks' first two layers. We show empirically that the layer in greatest need of reactivity is sufficiently fast (0.1- 0.3 seconds per control-loop cycle). This result shows that general-purpose theorem provers can be used in intelligent agents without sacrificing reactivity.

The remainder of the paper is organized as follows: After giving a brief introduction to Brooks' system and behavioral decomposition, we describe the LSA and give formal semantics to the approach using circumscription. We then describe the robot control system we have im­ plemented using the architecture. We conclude with a discussion of implementation issues, comparisons to re­ lated work and a description of future directions.

2 Subsumption and Decomposition

2.1 Brooks' Subsumption Architecture

Brooks showed that it is often advantageous to decom­ pose a system into parallel tasks or behaviors of increas­ ing levels of competence rather than the standard func­ tional decomposition. Whereas a typical functional de­ composition might resemble the sequence

sensors ---+ perception ---+ modeling ---+ planning ---+ task recognition ---+ motor control,

Brooks would decompose the same domain as avoid objects < wander < explore< build maps < monitor changes < identify objects < plan actions < reason about object behavior where < denotes increasing levels of competence. Po­ tential benefits from this approach include increased ro­ bustness, concurrency support, incremental construction and ease of testing.

In general, the different layers are not completely in­ dependent. In the decomposition above, wandering and exploring depend on the robot's ability to avoid objects. But the system may be able to service multiple goals in parallel, despite the dependence. The goals of one layer will occasionally conflict with those of another layer, in which case higher-priority goals should override lower­ priority ones. Consequently, the subsumption architec­ ture provides mechanisms by which higher, more compe­ tent layers may observe the state of lower layers, inhibit their outputs and override their inputs, thus adjusting their behavior. High-priority tasks in lower layers (such as reflexively halting when an object is dead ahead) will still have a default precedence if the designer disallows any tampering with these particular tasks.

Brooks implemented a control system of layers corre­ sponding to the first three levels of competence described above (avoidance, wandering and exploration). The first two layers are shown in Figure 1. Briefly, the avoid layer endows the robot with obstacle avoidance capabil­ ities by moving it in directions that avoid obstacles as much as possible and forcing it to stop if a head-on col­ lision is imminent. The wander layer causes the robot to move around aimlessly when '·. is not otherwise occu­ pied. The explore layer gives the robot some primitive goal-directed behavior by periodically choosing a loca­ tion in the distance and heading the robot towards it if idle. While in explore mode, this layer inhibits the wander layer so that the robot remains on track towards its destination. When either the wander or the explore layer is active, it overrides the default heading computed by the avoid layer, but the avoid layer still ensures that the robot does not have a collision. We refer the reader to [Brooks, 1986] for further details.

2.2 Behavioral Decomposition

The first important idea we borrow from Brooks' ar­ chitecture is that of decomposing the domain along be­ havioral lines rather than along the standard, sequential functional lines. A Logic-Based Subsumption Archi­ tecture (LSA) is composed of a sequence of FOL the­ ories. Each represents a layer with an axiomatization of the layer's behavior, that is, the layer's inputs , out­ puts (goal), state and any dependencies between them. The inputs are axioms coming from either the sensors or higher layers. The outputs are proved · theorems de­ termined by running a separate theorem prover for that layer only. These outputs may be sent to lower layers or to the robot effectors.

Because the axiomatization of a layer is usually much smaller than that of the whole system, each cycle is less computationally expensive than running one theorem prover over the whole compound axiomatization, leading to an overall higher performance. Another advantage of the layer-decoupling is the possibility of achieving more reactive behavior. As in Brooks' system, lower layers controlling basic behaviors are trusted to be autonomous and do not need to wait on results from higher layers (they assume some of them by default) before being able to respond to situations. Because these layers typically have simpler axiomatizations, and given the default as­ sumptions, the cycle time to compute their outputs can be shorter than that of the more complex layers.

2.3 Subsumption Principles

Of course, the layers are not fully independent. We adopt the view that, together with the task-based decompo­ sition idea, the coupling approach represented by sub­ sumption in the subsumption architecture is an impor­ tant and natural paradigm for intelligent agents in gen­ eral, and robot control in particular (see [Stein, 1997]). We want each layer in an LSA to be able to communicate with those underneath it in the hierarchy.

In general, however, when one layer overrides another, the two disagree on what some particular input should be. In a classical logic setting, the two corresponding theories will be inconsistent. We need to formalize the higher-layer theory's precedence over the lower layer's in such a way that (a) if there is no conflict, both layers keep their facts and the higher layer asserts its relevant conclusions in the lower layer, and (b) if there is conflict, the lower layer tries to give up some assumptions to ac­ commodate the higher layer's conclusions. A number of techniques developed in the logic community are appli­ cable, e.g., nonmonotonic techniques and belief revision. We have chosen to use circumscription, although other approaches may be equally interesting and appropriate.

3 Logical Subsumption

This section describes in detail how we implement the principles discussed above.

3.1 Basic Machinery

We distinguish three parts of the logical theory associ­ ated with each layer: (1) the Body of the layer, (2) the Sensory and Input Latches, and (3) the Output. The Body of the layer is the invariant theory for that layer.

The Latches are used to accept the input and replace it at the beginning of every cycle (rather than accumulate it) . The Output is the set of goal sentences proved from the layer's theory (including the latches).

The processing loop of each layer proceeds as follows: First, collect any pertinent sensor data and assert it in the form of logical axioms. Simultaneously, assert any inputs from higher-level theories. The theorem prover of that layer then attempts to prove the layer's goal. Upon reaching the conclusions, transmit the relevant ones ei­ ther to the layer below or (in the case of layer 0) to the robot manipulators. Figure 2 illustrates this process.

3.2 Circumscription-Based Subsumption

In the logical paradigm, McCarthy's circumscription [McCarthy, 1986] is one of the first major nonmonotonic reasoning tools. McCarthy's circumscription formula

says that in the theory A, with parameter relations and function sequences P, Z, P is a minimal element such that A(P, Z) still holds while Z is allowed to vary in order to allow P to become smaller.

Take, for example, the theory T block(Bl) 1\ block(B2 ). The circumscription of block in T, varying nothing, is Circ[T; block;] = T 1\ \fp [T[block/p] =? ·(p < block)] and is equivalent to \fx (block(x) {:} (x = B1 Vx = B2 )). By minimizing block, we have concluded that there are no other blocks in the world besides those mentioned in the original theory T.

In the LSA, we use circumscription for two distinct tasks: assuming defaults in the layers and giving seman­ tics to the system of layers as one big logical system.

To implement the idea of subsumption, we let each layer make default "assumptions" about the inputs that later may be adjusted by other (higher-level) layers. These assumptions take the form of the Closed-World Assumption (CWA) by minimizing a predicate in the layer's input language (Extended CWA, a generalization of CWA, was shown to be equivalent to circumscription [Gelfand et al. , 1989]).

More formally, let Layer; be the theory of layer i, and C;, a set of predicates in £(Layer;), for which we wish to assert CWA. Then, subsumption is achieved for layer i by using the parallel circumscription policy

When implemented, this formula often can be substi­ tuted with a simple (external to the logic) mechanical in­ terference determining the value of the minimized pred­ icates; we discuss this issue in section 5.

3.3 Semantics for LSA

If we ignore the time differences between the theorem provers in different layers and consider the entire system of layers as one logical theory, we can give the system a simple semantics. Let Layer; be the theory of layer i (including any CWA as a FOL schemata), G;(x) be the goal formula of layer i (i.e., the formula that we try to prove in that layer) and �~ (!; ( x)) be its translation to Layer;_1 's input. We call such a system of layers T a layered theory. For <p E £(Layer;), we write T f- <p if the mechanical entailment we described above derives <p.

Let tp':[b = \fx.·ab;(x) =? (G;(x) =? �~(f;(x))), where every ab; is a relation symbol that does not show in T.

Definition 3.1 (Semantics for Layered Theories) M is a model of the layered theory T (written M Fe T) iff it is a first-order model of the circumscriptions

This semantics assumes (1) we are interested in the set of results <p E £(Layer;) for some i (as opposed to <p E £(Layer; U Layerj), for example) and (2) all the symbols in the various theories are different (e.g., the symbol1 actually has the name L0 .1 in layer 0 and L2 .1 in layer 2).

Let £{ be the FOL language including only G;, =, and the constant and function symbols of £(Layer;). For a sentence ¢> E £{, let ¢' be the translation of ¢> by replacing G with G' and every term t by t' = J;(t). The following theorem validates the semantics for our proof­ theoretic system of transferring goals from one layer to another.

Theorem 3.2 (Completeness) Assume that T { Layer;};<m is a layered theory and <p is a formula in the language l(Layer0 ). IfT f- <p, then there is k 2': 0 and a sequence of sentences i.pk, ... , tpo s. t. <p = tpo, Layerk f= i.pk, and 1 ::=:; Vi ::=:; k <p; E £{ and Layer;-1 f= <p~ =? l.pi-1· Our LSA obeys this semantics, assuming that transfer­ ring a single instantiation of the goal between any pair of layers is sufficient. In case one layer proves only a disjunction of goal instantiations, we need to refine our LSA to support such a transfer, but this refinement can be done for any size of disjunctions. Additionally, there is no need to consider quantification in our LSA since we assume skolemization of the clauses (see Section 5).

We omit the proof for lack of space, but mention that it relies on Craig's Interpolation Theorem for FOL and on the following lemma.

Lemma 3.3 If Circ[Layer1 U Layer0 U { <p~b}; ab1; .C}Layero)] ~ Vx-.ab1(x), then there is a formula <P E .C 1 , negative in G1 , s. t. Layer1 ~ <P and Layero F ¢'.

Furthermore, if Layer~ is the result of adding all such <P 's to Layer1, then Circ[ Layer~ U Layer0 U {<p~b}; ab1; .C(Layero)] F Vx-.ab(x).

For soundness, we need to assume that the set of layers of T is consistent with {<pi, \lx-.abi(x )}i<n and that all the circumscriptions in Fe for T have sm-ooth preference relations (i.e., every model is either minimal or has a minimal model that is preferred to it) .

Theorem 3.4 (Soundness) Assume that there are <pk, ... , rl s.t .. ~ ;:::_l and Layerk F <pk ~nd k ;::: Vi > l, <pi E Li, posttwe m Gi, and Layeri F <pi+l => <pi, where <p~ is the translation of <pi from layer i to layer i - 1. Then, T Fe <p1.

4 A Model of Brooks' System

We briefly describe the logical theories for a control sys­ tem we have implemented for a robot operating in a multi-story office building. The first two layers corre­ spond roughly to the first three layers in Brooks' system. For simplicity, we list only selected axioms from the the­ ories and refer the reader to the full version of the paper for the complete system.

We assume the architecture is used to control a cylin­ drical robot with sonar sensors on its perimeter and wheels that control its motion. We also assume that it is able to determine its current location and orientation.

4.1 LAYER 0: Obstacle-avoidance

Layer 0 takes its input, asserted in the form of the axiom schema SonarReading(sonar _number) = dist, from the physical sonars and translates it into a map of objects, recording their distance and direction (relative to the robot) 1 . It may also discover "virtual" objects by way of layer 1 's subsumption latch.

Vdist, dir. (3sonar _number. SonarReading(sonar _number) = dist/\ Sonar Direction( sonar _number) = dir/\ dist ;::: 0 1\ dir > -1r 1\ dir ~ 1r) => (3obj. Object( obj) 1\ L ;tance( obj) = dist/\ Direction ( obj) = dir) .

Layer 0 checks to see if it has detected objects lying directly in front of it, and halts the robot if it has.

ObjectAhead {::::::::} (3obj. (Object( obj) 1\ Distance( obj) < MIN _DIST 1\ Direction ( obj) = dir 1\ dir > - f 1\ dir < f) .

ObjectAhead => HaltRobot.

1 The robot's 0-radians reference point is straight ahead, the front sonar is numbered 0, and the sonars are numbered consecutively, counter-clockwise from 0 to NSONARS- 1.

Using the map, layer 0 executes the function GetForce, computing the combined "repulsive force" exerted on the robot by the detected objects as Force_direction and Force_strength. It uses the former to specify a heading angle for the robot away from this force. Once headed in the right direction, the robot is commanded to move away at a speed proportional to the strength of the force, slowing down as it moves farther away from the objects.

Heading_angle = (Force_direction mod 27r)- 1r.

Heading_speed = Force_strength.

N eedTurn (Heading _angle) => Turn (Heading _angle).

-.HaltRobot 1\ -.NeedTurn(Heading_angle)/\ NeedFwd(Heading_speed) => Fwd(Heading_speed) . HaltRobot V NeedTurn(Heading_angle) => Fwd(O) .

During each cycle of layer 0, it applies the CWA to the symbols HaltRobot, Object, Distance, Direction in the input language. It then uses its theorem prover to try to prove Fwd(speed) and Turn(angle), where speed and angle are instantiated by the proof. The results are translated into the appropriate actuator commands.

4.2 LAYER 1: Destination-seeking

Layer 1 supports simple movements towards a goal lo­ cation, more closely resembling the exploration layer of Brooks' system than the wandering layer. Given a particular pair of coordinates specified by the input M oveCmd from layer 2 and given the robot's current location, 2 it makes a simple calculation to find in which of the eight quadrants surrounding the robot this goal position is, and asserts the existence of a "virtual push­ ing object" in the opposing quadrant .

Object( PUSH _OBJECT).

Vxo,yo,x,y. CurrLoc = {xo ,Yo} 1\ MoveCmd(x,y) => HasPushObject(Quadrant(xo - x, Yo - y)).

\/quad. HasPushObject(quad) => Direction(PUSH _OBJECT) = quad* NQ~ADS 1\

Distance(PUSH _OBJECT) = PUSH _QBJ _DIST.

During each cycle, layer 1 's theorem prover at­ tempts to prove Object(obj), Direction(obj) = dir, and Distance(obj) = dist, and introduces them into layer O's input latch if successful. The avoidance capabilities of layer 0 effectively push the robot away from the object in the direction of the goal, although it may deviate from a direct path if there are physical objects in the vicinity.

4.3 LAYER 2: Mid-Level Planning

Layer 2 performs two tasks: (1) translate logical loca­ tions into Cartesian coordinates and (2) reason in the situation calculus [McCarthy and Hayes, 1969] about us­ ing the elevators.

2 These coordinates are with respect to the fixed coordi­ nate system of the domain.

The inputs for this layer are the current location data from the robot (CurrLandmark) and the out­ put from layer 3 (TargetLandmark). During each cy­ cle, it tries to plan for the next landmark and prove M oveCmd (next _landmark).

Cartesian(RM218, [0, 0]).

Vx, y , lm. ·NeedElevPlan 1\ TargetLandmark(lm)l\ Cartesian(lm, [x, y]) =? MoveCmd(x, y).

Vx , y , lm, s11 , inter, s1 . N'eedElevPlanl\ TargetLandmark(lm) 1\ At( ROBOT, lm, su )I\ FirstSit(su, sl) 1\ At( ROBOT, inter, sl)l\ Cartesian(inter, [x, y]) =? MoveCmd(x , y).

The situation calculus theory includes three fluents: the two elevators' locations and the robot's location (we explicitly state frame axioms). Since the domain and depth are small, planning here is simple.

4.4 LAYER 3: High-level planning

Layer 3 performs high-level robot motion planning using situation calculus. Here there is only one fluent (the robot's location); thus, deeper reasoning can be per­ formed in a reasonable time.

The input for this layer is the current location of the robot. The goal is TargetLandmark(landmark).

Room(RM218) 1\ Room(ELEV1) ... Corridor(C2A1) 1\ Corridor(C2AELEV) ... InCorridor(Front(RM218) , C2A1) . ..

Vl,l',s.At(ROBOT,l,s) 1\ VConnected(l,l') ==> At( ROBOT, l', Result(M oveTo(l'), s)).

Vl.Room(l) =? VLinked(l , Front(l)) .

5 Implementation Issues

We have implemented the above theory using the PTTP theorem prover ([Stickel, 1988], [Stickel, 1992]) on a Sun Spare station, running Quintus Prolog as the underlying interpreter for PTTP. PTTP (Prolog Technology The­ orem Prover) is a model-elimination theorem prover. Given a theory made of clauses (not necessarily dis­ junctive) without quantifiers, PTTP produces a set of Prolog-like Horn clauses, makes sure only sound unifi­ cation is produced, and avoids the negation-as-failure proofs that are produced by the Prolog inference algo­ rithm. It is sound and complete.

We subjected our system to a battery of experiments in a simulated office building environment . Figure 3 summarizes the results for three scenarios of varying dif­ ficulty: (1) planning a path towards a location on the same floor as the robot, (2) creating a plan that requires a low-level plan for using the elevator, and (3) planning a path towards a location on a different floor . In each scenario, we . experimented with various robot orienta­ tions and obstacle positions in the robot's vicinity. For each layer, we measured the number of inference steps and time taken to prove its goal. 3

Layer 0, the critical layer, achieved its results in an average of 0.1 seconds when a turn action was required, and 0.3 seconds when a forward action was required. (Because of space concerns, we have included in Figure 3 only the data for cases of the former kind.) Layers 1, 2, and 3 worked fairly fast , although the long planning involved in Scenario 1 took more than 10 seconds (for a depth of 30 in the proof space). However, because we rely on the speed of only layer 0, safety is not compromised; the avoidance capabilities ensure that the robot does not fall off a cliff while planning a way to avoid the cliff edge.

We attribute the speed achieved to three optimiza­ tions. First, we used a few semantic attachments in Layer 0. In particular, the predicate GetForce was em­ bodied in a C function that returns the force vector [Strength , Direction]. It calls Prolog's bagof operator to collect all the objects for which existence proofs can be found, then computes the sum of the forces contributed by each object. This CWA is achieved by limiting proofs to be no longer than a specified constant (after some ex­ perimentation, we settled on a constant of 20.)

Second, we applied caching to the proof of GetForce. Since every proof "re-proved" GetForce many times, this improved the performance of Layer 0 significantly (from approximately 10 seconds to 0.1 seconds per proof) .

Third, we divided the planning so that layer 2 executes "local planning" for the elevator domain. This allowed layer 3 to avoid an explosion of the proof space, which otherwise would have occurred since there are four prin­ cipal actions as well as a number of frame axioms asso­ ciated with the robot and the elevator. The separation also helped prevent complex unifications .

6 Related Work

Compared to other approaches to agent architecture and robot control using logic, LSA is the only one using full FOL theorem provers for the low-level control loop and the first one to propose an architecture built on theorem provers that is suitable for realizing complex tasks.

[Shanahan, 1996] describes a map-building process us­ ing abduction, but then implements his theory in an al­ e;orithm that is proved to have his abductive semantics. lBaral and Tran, 1998] define control modules to be of a form of Stimulus-Response (S-R) agents (see [Nilsson, 1998]), relating them to the family of action languages A (e.g., [Gelfond and Lifschitz, 1993], [Giunchiglia et al., 1997]). They provide a way to check that an S-R module is correct with respect to an action theory in A or An and provide an algorithm to create an S-R agent from an action theory. [Levesque et al., 1997], [Giacomo et al., 1998], and other work in the GOLOG project have a planner that computes/plans the GOLOG program off­ line, only later letting the robot execute the GOLOG

3 We do not list averages or standard deviations for layers 2 and 3 because their performances are independent of both the robot's orientation and sonar readings.

program on-line. Here again, logic is used only to give semantics for GO LOG programs by way of situation cal­ culus ([McCarthy and Hayes, 1969]).

None of this work uses FOL theorem provers for con­ trolling robots at run-time. To our knowledge, there has been no such system since Shakey [Nilsson, 1984].

7 Conclusion

We have shown that theorem provers can be used for robot control by employing them in a layered architec­ ture. We demonstrated that the architecture and the versatility of theorem provers allow us to realize complex tasks, while keeping individual theories simple enough for efficient theorem proving. Furthermore, we have grounded our proposal by giving it formal semantics based on circumscription.

At this time, the system is implemented in four layers on a simulating computer. Besides installing the system on a mobile robot, our future work plan includes adding layers that create maps and layers that reason about and update explicit beliefs about the world. We are currently working on incorporating vision sensory capabilities and implementing concurrency.

This work is a first step towards our long-term goal of creating a general logic-based AI architecture that is efficient and scalable, and that supports reactivity.

8 Acknowledgments

We wish to thank Mark Stickel for allowing us to use his PTTP sources (both for PROLOG and LISP) and providing helpful answers to our inquiries regarding its use. This research was supported by an ARPA (ONR) grant N00014-94-1-0775 and by a National Physical Sci­ ence Consortium (NPSC) fellowship.