On-Line Execution of cc-Golog Plans

1 Introduction

Consider a robot which, while engaged in a delivery task, is to move from Room 6213 to Room 6205 (see Figure 1). In a modern robot architecture like XAVIER [Simmons et al., 1997] or RHINO [Burgard et al., 2000], the controller would issue a message to a low-level navigation process telling it the new destination (Rm6205), and the navigation process would then move the robot to its desired location, making use of intermediate goal points like those outside doorways (nodes 1 and 2 in the figure) for robustness.

Besides executing such plans, an intelligent robot controller should be able to reason about its actions, that is, consider, for example, whether it is better to first charge the batteries or to continue the delivery, which would involve projecting the outcome of the delivery task and checking whether the batteries would still have enough power afterwards. Moreover, projection is also valuable for the designer of robot controllers to find out whether a program under development is executable or whether it would satisfy certain goals after execution. In [Grosskreutz and Lakemeyer, 2000a], we proposed such a projection mechanism for ccGolog an extension of GOLOG [Levesque et al., 1997] featuring a model of time, continuous change, and the ability to wait for conditions (like arriving in Rm6205) to become true. While tasks like the above can be modelled quite naturally in cc-Golog, it so far remains unclear how to actually execute a cc-Golog plan or program (in this paper we use plan and program interchangeably). To get a sense of the problem, consider the actions of initiating moving just outside of Room 6213 and waiting to arrive there. In cc-Golog these actions would have the effect of setting the location of the robot to a continuous linear function of time to approximate the robot's trajectory and to advance time to the point when the goal location is reached, respectively. While this seems fine for the purpose of projection, which is sometimes also called off-line execution [de Giacomo and Levesque, 1999], those "effects" are simply inappropriate during actual on-line execution. For one, the robot has no control over the passage of time and, for another, the actual trajectory often follows a function quite different from the idealized approximation (see the curved vs. the straight (dotted) line in Figure 1). What is needed instead, it seems, are frequent sensor readings telling the robot about the current time and location, which should be used instead of the models of how time passes or how the robot moves. A waiting action would then simply reduce to a test whether the goal has been reached. Another minor complication is that actions that are part of the model of a low-level process such as navigation need to be ignored during execution except for an action that activates the process. Finally, while projection in cc-Golog so far is limited to a complete program starting in the initial state, one would often like to project on the fly during execution, similar to the search operator of [de Giacomo and Levesque, 1999]. However, for reasons of efficiency, we would like to go beyond that and allow for a restricted projection of a program, which only searches up to a (temporally) limited horizon. For instance, if the robot is in the middle of a delivery but near the docking station, we want to enable it to find out whether the coming activities would allow it to operate for at least another 5 minutes and, if not, decide to charge the batteries first.

In this paper, we show how all this can be done in ccGolog. For that we first show how a robot control architecture where a high-level controller communicates with lowlevel ✂ processes via messages can be modelled directly in ccGolog. The main advantage is that there is a clear separation of the actions of the high-level controller from those of the low-level processes. Then we discuss the changes necessary to use the same cc-Golog program both for on-line execution and projection. Finally, we show how a time-bounded projection mechanism can be defined and interleaved with execution.

The rest of the paper is organized as follows. In Section 2, we briefly review cc-Golog and the situation calculus on which cc-Golog is based. Then we describe how to model the robot control architecture and give an example of a model of a low-level navigation process. In Sections 4 and 5 we discuss the changes needed to allow on-line execution of cc-Golog programs and how on-line execution and projection can be interleaved. We end with a brief summary and discussion of related work.

2 Preliminaries

The Situation Calculus The semantics of cc-Golog is based on an extension of the situation calculus [McCarthy, 1963]. We will only go briefly over the basic situation calculus: all terms in the language are one of the following sorts: ordinary objects, actions, or situations; there is a special constant ✄ ☎ used to denote the initial situation, namely that situation in which no actions have yet occurred; there is a distinguished binary function symbol do where do✝ ✞ ✠ ☛ ✌ denotes the successor situation to ☛ resulting from performing the action ✞ ; relations whose truth values vary from situation to situation are called relational fluents, and are denoted by predicate symbols taking a situation term as their last argument; similarly, functions varying across situations are called functional fluents and are denoted analogously; finally, there is a special predicate Poss ✝ ✞ ✠ ☛ ✌ used to state that action ✞ is executable in situation ☛ ✒

Within this language, we can formulate theories which describe how the world changes as the result of the available actions. One possibility is a basic action theory of the following form [Levesque et al., 1998]:

• Axioms describing the initial situation, ✄ ☎ .
• Action precondition axioms, one for each primitive action ✞ , characterizing Poss ✝ ✞ ✠ ☛ ✌ .
• Successor state axioms (SSAs) , one for each fluent ✖ , stating under what conditions ✖ ✝ ✘ ✚ ✠ do ✝ ✞ ✠ ☛ ✌ ✌ holds as a function of what holds in situation ☛ ✒ These take the place of the so-called effect axioms, but also provide a solution to the frame problem.
• Domain closure and unique name axioms for the actions.
• Foundational, domain independent axioms.

Let us now consider extending this basic situation calculus by time and continuous change according to [Grosskreutz and Lakemeyer, 2000a]. Note that these extensions are intended for the purpose of projections only. In Section 4 we will discuss the necessary changes to allow on-line executions as well. We begin by adding two new sorts real and time. 1 Similar to Pinto and Reiter [Pinto, 1997; Reiter, 1996], we introduce a special unary functional fluent start connecting situations and time. The intuition is that start ✝ ☛ ✌ denotes the time when situation ☛ begins. (We defer the formal definition of start until after the discussion of the passage of time.)

1 For simplicity, the reals are not axiomatized and we assume their standard interpretations together with the usual operations and ordering relations. The sort time ranges over the reals as well.

As in [Pinto, 1997], continuous change is modelled based on the idea that a fluent like the position of a robot takes as value a function of time. For example, in the situation where a robot starts moving, its 2-dimensional location can be characterized (in a somewhat idealized fashion) by a linear function of time, starting at its actual position and moving toward its destination. We call functional fluents whose values are continuous functions continuous fluents. In order to represent the value of continuous fluents, we add to the language another sort t-function, whose elements are meant to be functions of time. We assume that there are only finitely many function symbols of type t-function and we require domain closure and unique names axioms for them, just as in the case of primitive actions. Furthermore, one needs to specify what values these functions have at any particular time ✜ . This is done with the help of the special binary function val. The following axiom illustrates the use of val, where the values of constant functions and a special kind of linear functions are defined.

While const ✝ ✚ ✠ ✢ ✌ always evaluates to the tuple ★ ✚ ✠ ✢ ✪ , linear ✝ ✚ ✠ ✢ ✠ ✫ ✬ ✠ ✫ ✮ ✠ ✜ ☎ ✌ is a linear function intended to approximate the movement of a robot in 2-dimensional space (we ignore the details of representing tuples of reals in logic).

Motivated by the fact that during the execution of plans time passes merely when the high-level controller is waiting, the fluent start changes its value only as a result of the special primitive action waitFor ✝ ❆ ✌ . The intuition is as follows. Normally, every action happens immediately, that is, the starting time of the situation after doing ✞ in ☛ is the same as the starting time of ☛ . The only exception is waitFor ✝ ❆ ✌ : whenever this action occurs, the starting time of the resulting situation is advanced to the earliest time in the future when ❆ becomes true.

The arguments of waitFor are restricted to so-called t-forms, which are special formulas involving continuous fluents with the situation argument suppressed (see [Grosskreutz and Lakemeyer, 2000a] for details).An example is ✝ battLevel ❈ ❉ ❋ ✌ . Given a t-form ❆ , ❆ ❍ ☛ ✠ ✜ ❏ denotes ❆ with every continuous fluent evaluated in situation ☛ at time ✜ . For example, ✝ battLevel ❈ ❉ ❋ ✌ ❍ ☛ ✠ ✜ ❏ becomes ✝ val ✝ battLevel ✝ ☛ ✌ ✠ ✜ ✌ ❈ ❉ ❋ ✌ . The following axiom defines the least time point after the start of ☛ where ❆ becomes true:

A waitFor ✝ ❆ ✌ -action is possible iff ❆ has a least time point:

Finally, the following successor state axiom for start captures the intuition that the starting time of a situation changes only as a result of a waitFor ✝ ❆ ✌ , in which case it advances to the earliest time in the future when ❆ holds.

Example To illustrate the use of these definitions, let us model ❢ how a robot's location changes as a result of primitive actions. For simplicity, we ignore the robot's orientation and represent its position by the continuous fluent robotLoc, which evaluates to a tuple of reals. There are two types of actions that affect the location of the robot: startGo ✝ ★ ✚ ✠ ✢ ✪ ✌ , which initiates moving the robot towards position ★ ✚ ✠ ✢ ✪ , 2 and endGo which stops the movement of the robot. We assume that startGo is only possible if the destination differs from the robot's current location. Then we obtain the following successor state axiom for robotLoc.

❪ ❫ ☛ ☛ ✝ ✞ ✠ ☛ ✌ ❲ ❍ robotLoc ✝ ❛ ❫ ✝ ✞ ✠ ☛ ✌ ✌ ✦ ❣ ✳ ❭ ✜ ✠ ✚ ✠ ✢ ✒ ✜ ✦ start ✝ ☛ ✌ ✽ val ✝ robotLoc ✝ ☛ ✌ ✠ ✜ ✌ ✦ ★ ✚ ✠ ✢ ✪ ✽ ❍ ❭ ✚ ✲ ✠ ✢ ✲ ✠ ✫ ✬ ✠ ✫ ✮ ✒ ✞ ✦ startGo ✝ ★ ✚ ✲ ✠ ✢ ✲ ✪ ✌ ✽ ✫ ✬ ✦ ✝ ✚ ✲ ✸ ✚ ✌ ❦ ❧ ✽ ✫ ✮ ✦ ✝ ✢ ✲ ✸ ✢ ✌ ❦ ❧ ✽ ❣ ✦ linear ✝ ✚ ✠ ✢ ✠ ✫ ✬ ✠ ✫ ✮ ✠ ✜ ✌ ❜ ✞ ✦ endGo ✽ ❣ ✦ const ✝ ✚ ✠ ✢ ✌ ❜ ❙ ✚ ✲ ✠ ✢ ✲ ✒ ✞ ❝ ✦ startGo ✝ ✚ ✲ ✠ ✢ ✲ ✌ ✽ ✞ ❝ ✦ endGo ✽ ❣ ✦ robotLoc ✝ ☛ ✌ ❏

where, ❧ ✒ ✦ a115 ✝ ✚ ✲ ✸ ✚ ✌ ✉ ✴ ✝ ✢ ✲ ✸ ✢ ✌ ✉ is a normalizing factor needed in order to ensure that the total 2-dimensional velocity does not exceed 1.

The variables ✚ and ✢ refer to the coordinates of the robot. After startGo ✝ ★ ✚ ✲ ✠ ✢ ✲ ✪ ✌ , robotLoc has as value a linear tfunction starting at the current position and moving toward ★ ✚ ✲ ✠ ✢ ✲ ✪ . After endGo, it is const ✝ ★ ✚ ✠ ✢ ✪ ✌ . Finally, if ✞ is neither a startGo nor a endGo action, robotLoc remains unchanged.

cc-Golog We now turn to cc-Golog, which offers constructs such as sequences, iteration and procedures to define complex actions. In addition, parallel actions are introduced with a conventional interleaving semantics.

✇ primitive action waitFor ✝ ❆ ✌ wait until condition ❆ becomes true ❆ ① test action ❍ ② ③ ✠ ② ✉ ❏ sequence if ✝ ❆ ✠ ② ③ ✠ ② ✉ ✌ conditional while ✝ ❆ ✠ ② ✌ loop withPol ✝ ② ③ ✠ ② ✉ ✌ prioritized execution until ② ✉ ends 3 proc ④ ✝ ✚ ✌ ② procedure definition

Using cc-Golog, it is possible to specify event-driven behavior quite naturally. For example, the following program specifies that the robot is to travel to Room 6205 and say "In Hallway" if it ever enters the hallway on its way.

Here the send action indicates that the robot assigns the room number to a register, which leads to an activation of the navigation process to head to that room, and then blocks execution until the register reached signals that the navigation process has completed successfully. The details of this architecture are found in Section 3.

The semantics of cc-Golog is specified similar to that of ConGolog [Giacomo et al., 2000]. Its main ingredients are a predicate ➈ ➉ ✞ ➋ ☛ ✝ ② ✠ ☛ ✠ ➌ ✠ ☛ ✲ ✌ , which defines single steps of computation, and another predicate ✖ ➍ ➋ ✞ ➎ ✝ ② ✠ ☛ ✌ . ✖ ➍ ➋ ✞ ➎ specifies which configurations ✝ ② ✠ ☛ ✌ are final, meaning that the computation can be considered completed. This is the case, roughly, when the remaining program is ➋ ➍ ➎ , but not if there is still a primitive action or test action to be executed. We leave out the details for reasons of space.

2 For simplicity, we model the robot as always traveling at speed 1m/s. In a more realistic model, we would also consider different velocities.

3 Unprioritized concurrency can be defined as well, but is omitted since we do not use it in the paper.

Intuitively, the predicate ➈ ➉ ✞ ➋ ☛ ✝ ② ✠ ☛ ✠ ➌ ✠ ☛ ✲ ✌ associates with a given program ② and situation ☛ a new situation ☛ ✲ that results from executing a primitive action in ☛ , and a new program ➌ that represents what remains of ② after having performed that action. For space reasons, we only list a few of the axioms for ➈ ➉ ✞ ➋ ☛ .

➈ ➉ ✞ ➋ ☛ ✝ ✇ ✠ ☛ ✠ ➌ ✠ ☛ ✲ ✌ ✳ Poss ✝ ✇ ✠ ☛ ✌ ✽ ➌ ✦ ➋ ➍ ➎ ✽ ☛ ✲ ✦ do ✝ ✇ ✠ ☛ ✌ ➈ ➉ ✞ ➋ ☛ ✝ ➋ ➍ ➎ ✠ ☛ ✠ ➌ ✠ ☛ ✲ ✌ ✳ FALSE ➈ ➉ ✞ ➋ ☛ ✝ ❆ ① ✠ ☛ ✠ ➌ ✠ ☛ ✲ ✌ ✳ ❆ ❍ ☛ ❏ ✽ ➌ ✦ ➋ ➍ ➎ ✽ ☛ ✲ ✦ ☛ 4 ➈ ➉ ✞ ➋ ☛ ✝ ☛ ➑ ➒ ✝ ② ③ ✠ ② ✉ ✌ ✠ ☛ ✠ ➌ ✠ ☛ ✲ ✌ ✳ ✖ ➍ ➋ ✞ ➎ ✝ ② ③ ✠ ☛ ✌ ✽ ➈ ➉ ✞ ➋ ☛ ✝ ② ✉ ✠ ☛ ✠ ➌ ✠ ☛ ✲ ✌ ❜ ❭ ➌ ✲ ✒ ➈ ➉ ✞ ➋ ☛ ✝ ② ③ ✠ ☛ ✠ ➌ ✲ ✠ ☛ ✲ ✌ ✽ ➌ ✦ ☛ ➑ ➒ ✝ ➌ ✲ ✠ ② ✉ ✌ ➈ ➉ ✞ ➋ ☛ ✝ withPol ✝ ② ③ ✠ ② ✉ ✌ ✠ ☛ ✠ ➌ ✠ ☛ ✲ ✌ ✳ ❨ ✖ ➍ ➋ ✞ ➎ ✝ ② ✉ ✠ ☛ ✌ ✽ ❭ ➌ ③ ✒ ➈ ➉ ✞ ➋ ☛ ✝ ② ③ ✠ ☛ ✠ ➌ ③ ✠ ☛ ✲ ✌ ✽ ➌ ✦ withPol ✝ ➌ ③ ✠ ② ✉ ✌ ✽ ❙ ➌ ✉ ✠ ☛ ✉ ✒ ➈ ➉ ✞ ➋ ☛ ✝ ② ✉ ✠ ☛ ✠ ➌ ✉ ✠ ☛ ✉ ✌ ❲ ☛ ✜ ✞ ➉ ✜ ✝ ☛ ✲ ✌ ❈ ☛ ✜ ✞ ➉ ✜ ✝ ☛ ✉ ✌ ❏ ❜ ❭ ➌ ✉ ✒ ➈ ➉ ✞ ➋ ☛ ✝ ② ✉ ✠ ☛ ✠ ➌ ✉ ✠ ☛ ✲ ✌ ✽ ➌ ✦ withPol ✝ ② ③ ✠ ➌ ✉ ✌ ✽ ❙ ➌ ③ ✠ ☛ ③ ✒ ➈ ➉ ✞ ➋ ☛ ✝ ② ③ ✠ ☛ ✠ ➌ ③ ✠ ☛ ③ ✌ ❲ ☛ ✜ ✞ ➉ ✜ ✝ ☛ ✲ ✌ ❯ ☛ ✜ ✞ ➉ ✜ ✝ ☛ ③ ✌ ❏

A transition of a primitive action requires it to be possible in the current situation, leaving nothing (➋ ➍ ➎ ) to be done afterwards. The execution of ② ✉ with policy ② ③ means that one action of one of the programs is performed, whereby actions which can be executed earlier are always preferred. If both ② ③ and ② ✉ are about to execute an action at the same time, the policy ② ③ takes precedence. 5

A final situation ☛ ✲ reachable after a finite number of transitions from a starting situation is identified with the situation resulting from a possible execution trace of program ② , starting in situation ☛ ; this is captured by the predicate ➓ ❫ ✝ ② ✠ ☛ ✠ ☛ ✲ ✌ , which is defined in terms of ➈ ➉ ✞ ➋ ☛ ➔ , the transitive closure of ➈ ➉ ✞ ➋ ☛ :

where the ellipsis stands for the universal closure of the conjunction of the following formulas:

➈ ✝ ➌ ✠ ☛ ✠ ➌ ✠ ☛ ✌ ➈ ➉ ✞ ➋ ☛ ✝ ➌ ✠ ☛ ✠ ➌ ✲ ✲ ✠ ☛ ✲ ✲ ✌ ✽ ➈ ✝ ➌ ✲ ✲ ✠ ☛ ✲ ✲ ✠ ➌ ✲ ✠ ☛ ✲ ✌ ❲ ➈ ✝ ➌ ✠ ☛ ✠ ➌ ✲ ✠ ☛ ✲ ✌

Given a program ➌ , proving that ➌ is executable in the initial situation then amounts to proving ↔ ↕ ✦ ❭ ☛ Do ✝ ➌ ✠ ✄ ☎ ✠ ☛ ✌ , where ↔ consists of the above axioms for cc-Golog together with a basic action theory in the situation calculus.

3 ARobot Control Architecture

As indicated in the introduction, in modern robot architectures like XAVIER [Simmons et al., 1997] and RHINO [Burgard et al., 2000], the high-level controller does not directly operate the robot's physical sensors and effectors. Instead, it activates and deactivates specialized processes like a navigation process, to which we will refer as low-level processes. The job of the high-level controller is then to combine the activation and deactivation of these routines in a way to fulfill the overall goal. It turns out that cc-Golog allows a logical reconstruction of this type of architecture in a fairly natural way. The overall architecture is illustrated in Figure 2.

4 Here, ➛ stands for a situation calculus formula with all situation arguments suppressed. ➛ ➜ ➝ ➞ will denote the formula obtained by restoring situation variable ➝ to all fluents appearing in ➛ .

5 Note that ➟ ➠ ➡ ➢ ➝ requires a reification of formulas and programs in the logical language. See [Giacomo et al., 2000] for how this can be done.

The communication between the low-level processes and the high-level plan is achieved through the special fluent reg. The high-level interpreter can affect the value of reg by means of the special action send ✝ id✠ val✌ which assigns reg✝ id✌ the value val. The intuition is that in order to activate a low-level process, the high-level controller executes a send action. For example, the execution of send✝ ❺ ❻ ❼ ❽ ❾ ❿ ✠ ❋ ➀ ➁ ➂ ✌ would tell the navigation process to start moving toward Room 6205.

On the other hand, the low-level processes can provide the high-level controller with information by means of the (exogenous) action ➃ ❻ ➤ ❶ ❹ ✝ id ✠ ✫ ✞ ➎ ✌ . For example, in order to inform the high-level controller that it has reached its destination, the low-level process would cause an exogenous ➃ ❻ ➤ ❶ ❹ ✝ ➃ ❻ ⑨ ➄ ➅ ❻ ❺ ✠ ❋ ➀ ➁ ➂ ✌ action. The following successor state axiom specifies how reg is affected by send and reply.

3.1 Modeling Low-level Processes as cc-Golog Procedures

To describe complex low-level processes like a navigation process, we model low-level processes as cc-Golog procedures. 6 Given a faithful characterization of the low-level processes in terms of cc-Golog procedures, we can then project the effect of the activation of these processes using their corresponding cc-Golog models. We stress that these procedures are not meant to be executed, but rather represent a model of the effects of the corresponding low-level process.

As an example, let us consider a low-level navigation process. It is activated through a send ✝ ❺ ❻ ❼ ❽ ❾ ❿ ✠ ➧ ✌ action, which assigns reg✝ ❺ ❻ ❼ ❽ ❾ ❿ ✌ the value ➧ and tells the process to travel to room ➧ . The process causes the robot to move towards ➧ until the destination is reached, where it informs the high-level controller of the arrival by means of an ➃ ❻ ➤ ❶ ❹ ✝ ➃ ❻ ⑨ ➄ ➅ ❻ ❺ ✠ ➧ ✌ action.

We model this behavior by the cc-Golog procedure navProc. navProc makes use of the following functions: ❻ ➩ ⑤ ❽ ➫ ➭ ✝ ➧ ✌ , ⑤ ⑥ ❼ ⑤ ❺ ❻ ✝ ➧ ✌ and ➄ ➯ ➃ ➃ ❻ ⑥ ❽ ❾ ➲ ➲ ❿ . ❻ ➩ ⑤ ❽ ➫ ➭ maps a room name ➧ to a location near the exit of room ➧ , and ⑤ ⑥ ❼ ⑤ ❺ ❻ to location within ➧ . currentRoom is a function whose value in ☛ is the name of the room the robot is in at the beginning of ☛ . We write ➳ ➲ ❽ ➲ ➵ ➲ ➄ ✝ ❛ ✌ as an abbreviation for ❍ startGo ✝ ❛ ✌ ✠ waitFor ✝ ➋ ➑ ✞ ➉ ✝ ❛ ✌ ✌ ❏ and ➎ ❫ ❫ ➸ ✝ ② ✌ for while ✝ TRUE ✠ ② ✌ .

6 This is similar to [Grosskreutz and Lakemeyer, 2000b], where a probabilistic programming language is used to model processes with uncertain outcome.

navProc ✒ ✦ ➎ ❫ ❫ ➸ ✝ ❍ reg ✝ ❺ ❻ ❼ ❽ ❾ ❿ ✌ ❝ ✦ ➄ ➯ ➃ ➃ ❻ ⑥ ❽ ❾ ➲ ➲ ❿ ① ✠ if ✝ ➄ ➯ ➃ ➃ ❻ ⑥ ❽ ❾ ➲ ➲ ❿ ❝ ✦ HALLWAY ✠ ➳ ➲ ❽ ➲ ➵ ➲ ➄ ✝ ❻ ➩ ⑤ ❽ ➫ ➭ ✝ ➄ ➯ ➃ ➃ ❻ ⑥ ❽ ❾ ➲ ➲ ❿ ✌ ✌ ✌ ✠ ➳ ➲ ❽ ➲ ➵ ➲ ➄ ✝ ❻ ➩ ⑤ ❽ ➫ ➭ ✝ reg ✝ ❺ ❻ ❼ ❽ ❾ ❿ ✌ ✌ ✌ ✠ ➳ ➲ ❽ ➲ ➵ ➲ ➄ ✝ ⑤ ⑥ ❼ ⑤ ❺ ❻ ✝ reg ✝ ❺ ❻ ❼ ❽ ❾ ❿ ✌ ✌ ✌ ✠ endGo ✠ ➃ ❻ ➤ ❶ ❹ ✝ ➃ ❻ ⑨ ➄ ➅ ❻ ❺ ✠ reg ✝ ❺ ❻ ❼ ❽ ❾ ❿ ✌ ✌ ❏ ✌

Initially, the navigation process is blocked until reg✝ ❺ ❻ ❼ ❽ ❾ ❿ ✌ is assigned a room name different from the one the robot is actually in. Then navProc executes a sequence of startGo actions, approximating the trajectory towards the destination room by a polyline with an edge near every door the robot has to travel through (see Figure 1).

3.2 Projection

We will now describe how to project a cc-Golog plan, taking into account the cc-Golog model of the low-level processes. Let ☛ be a situation, ➎ ➎ ➼ ➽ ➾ ➚ ➪ a model of the low-level processes, 7 and ② a cc-Golog program. A projection ☛ ✲ can then be identified with the situation that results from the concurrent simulation of ② and ➎ ➎ starting in ☛ .

Let AX ➶ ➶ be the set of foundational axioms of Section 2 together with the domain closure and unique names axioms for t-functions, the axioms required for t-form's, the axioms defining val, the precondition axiom for waitFor, and axioms stating that the robot is in Room 6213 together with other appropriate descriptions of the environment like a definition of inHallway in terms of coordinates on the map. Using ➹ ➘ ➴ ➴ , we can project the plan prg1 from Section 2. We write do ✝ ❍ ✞ ③ ✠ ✒ ✒ ✒ ✞ ➷ ❏ ✠ ☛ ✌ a shorthand for do ✝ ✞ ➷ ✠ ✒ ✒ ✒ ✠ do ✝ ✞ ③ ✠ ☛ ✌ ✒ ✒ ✒ ✌ .

AX ➶ ➶ ↕ ✦ ❪ ➉ ❫ ➬ ✝ ✄ ☎ ✠ prg1 ✠ navProc ✠ ☛ ✌ ✳ ☛ ✦ do ✝ ❍ send✝ ❺ ❻ ❼ ❽ ❾ ❿ ✠ ❋ ➀ ➁ ➂ ✌ ✠ startGo✝ ➎ ③ ✌ waitFor ✝ ➋ ➑ ✞ ➉ ✝ ➎ ③ ✌ ✌ ✠ startGo ✝ ➎ ✉ ✌ ✠ waitFor ✝ ⑤ ⑥ ⑧ ⑨ ❶ ❶ ❷ ⑨ ❹ ✌ ✠ say ✝ "In Hallway" ✌ waitFor ✝ ➋ ➑ ✞ ➉ ✝ ➎ ✉ ✌ ✌ ✠ startGo ✝ ➎ ➱ ✌ ✠ waitFor ✝ ➋ ➑ ✞ ➉ ✝ ➎ ➱ ✌ ✌ ✠ endGo ➃ ❻ ➤ ❶ ❹ ✝ ➃ ❻ ⑨ ➄ ➅ ❻ ❺ ✠ ❋ ➀ ➁ ➂ ✌ ❏ ✠ ✄ ☎ ✌

The projected execution trace includes a startGo ✝ ➎ ✃ ✌ and waitFor ✝ ➋ ➑ ✞ ➉ ✝ ➎ ✃ ✌ ✌ action for every node on the approximating trajectory, where the ➎ ✃ stand for coordinates corresponding to the nodes ➍ in Figure 1. Additionally, it includes a say ✝ "In Hallway" ✌ which is executed immediately after the hallway has been reached, which is assumed to happen just after leaving ➋ ➑ ✞ ➉ ✝ ➎ ③ ✌ . The execution trace ends with ➃ ❻ ➤ ❶ ❹ ✝ ➃ ❻ ⑨ ➄ ➅ ❻ ❺ ✠ ❋ ➀ ➁ ➂ ✌ , which completes the navigation task.

4 On-Line Execution of cc-Golog plans

Projections such as the above should be understood as a way of assessing whether a program is executable in principle. The resulting execution trace is not intended as input to the execution mechanism of the robot for several reasons. For one, many of the actions like startGo ✝ ➎ ③ ✌ only serve to model the navigation process and are not meant to be executed by the high-level controller at all. For another, actions that do belong to the high-level controller like waitFor ✝ ⑤ ⑥ ⑧ ⑨ ❶ ❶ ❷ ⑨ ❹ ✌ must be interpreted differently during on-line execution. This is because during projection waitFor advances time to the least a209 point where the condition is satisfied according to an idealized model of the world (like piece-wise linear trajectories). During actual execution, however, a waitFor should intuitively be treated simply as a test, where a condition like being at a certain location is matched against sensor readings reflecting the actual state of affairs.

7 In our example, the navigation process is the only low-level process, so we can simply use navProc. If there were more relevant low-level processes, ❐ ❐ ❒ ❮ ❰ a207 a208 would amount to the concurrent execution of the individual cc-Golog models.

In order to see how such sensor readings can be obtained, let us briefly look at how actual robots like the RHINO system deal with it. There we find a tight update loop between the low-level system and the high-level controller. This update loop periodically provides the high-level controller with an update of the low-level processes' estimate of continuous properties like the batteries' voltage level or the robot's position (typically several times a second). The period of time between two subsequent updates is so small that for practical purposes the latest update can be regarded as providing not only the correct current time but also accurate values of the continuous fluents at the current time.

Our solution is then to represent the updates by means of a new exogenous action ccUpdate and to treat waitFor's simply as special tests during on-line execution. Intuitively, the effect of ccUpdate is to set the value of the continuous fluents to the latest estimates of the low-level processes. The actual arguments of ccUpdate depend on the continuous fluents that are to be updated. In our example scenario, ccUpdate has four arguments: ✚ , ✢ , ➎ and ✜ , where ✚ and ✢ refer to the current position of the robot, ➎ to the current voltage level and ✜ to the current time. To get a sense of the effect of ccUpdate, let us consider a new version of the successor state axiom for robotLoc of Section 2 suitable for both on-line execution and projection. For simplicity, it is assumed that the actions startGo and endGo only occur during projection (as part of the model of the low-level navigation process).

❪ ❫ ☛ ☛ ✝ ✞ ✠ ☛ ✌ ❲ ❍ robotLoc ✝ ❛ ❫ ✝ ✞ ✠ ☛ ✌ ✌ ✦ ❣ ✳ ❭ ✜ ✠ ✚ ✠ ✢ ✒ ✜ ✦ start ✝ ☛ ✌ ✽ val ✝ robotLoc ✝ ☛ ✌ ✠ ✜ ✌ ✦ ★ ✚ ✠ ✢ ✪ ✽ ❍ ❭ ✚ ✲ ✠ ✢ ✲ ✠ ✫ ✬ ✠ ✫ ✮ ✒ ✞ ✦ startGo ✝ ★ ✚ ✲ ✠ ✢ ✲ ✪ ✌ ✽ ✫ ✬ ✦ ✝ ✚ ✲ ✸ ✚ ✌ ❦ ❧ ✽ ✫ ✮ ✦ ✝ ✢ ✲ ✸ ✢ ✌ ❦ ❧ ✽ ✽ ❣ ✦ linear ✝ ✚ ✠ ✢ ✠ ✫ ✬ ✠ ✫ ✮ ✠ ✜ ✌ ❜ ✞ ✦ endGo ✽ ❣ ✦ const ✝ ✚ ✠ ✢ ✌ ❜ ❭ ✚ ✲ ✠ ✢ ✲ ✠ ➎ ✲ ✠ ✜ ✲ ✒ ✞ ✦ ccUpdate ✝ ✚ ✲ ✠ ✢ ✲ ✠ ➎ ✲ ✠ ✜ ✲ ✌ ✽ ❣ ✦ const ✝ ✚ ✲ ✠ ✢ ✲ ✌ ❜ ❙ ✘ ✚ ✒ ✞ ❝ ✦ startGo ✝ ✘ ✚ ✌ ✽ ✞ ❝ ✦ ccUpdate ✝ ✘ ✚ ✌ ✽ ✞ ❝ ✦ endGo✽ ❣ ✦ robotLoc ✝ ☛ ✌ ❏

Note that ccUpdate simply "assigns" ❣ the constant function const ✝ ✚ ✲ ✠ ✢ ✲ ✌ , which reflects the idea that, during on-line execution, the linear approximation of the trajectory plays no role and that the actual values ★ ✚ ✲ ✠ ✢ ✲ ✪ should be used instead.

Besides updating the value of the continuous fluents, ccUpdate is of prime importance because it causes time or, better, the internal clock to advance during execution. Therefore, we need to modify the successor state axiom of the fluent start. In order to account for the fact that time advances differently in projections and during on-line execution, we need to explicitly distinguish between the two modes of operation. For that purpose, we introduce a special fluent ➲ ⑥ ❶ ⑤ ⑥ ❻ ✝ ☛ ✌ which can only change its truth value by the special actions setOnline and clipOnline, respectively. (Specifying the SSA for ❫ ➋ ➎ ➍ ➋ ➑ is easy and left out.) The SSA for start then becomes

❪ ❫ ☛ ☛ ✝ ✞ ✠ ☛ ✌ ❲ ❍ start ✝ ❛ ❫ ✝ ✞ ✠ ☛ ✌ ✌ ✦ ✜ ✳ ❨ ➲ ⑥ ❶ ⑤ ⑥ ❻ ✝ ☛ ✌ ✽ ❭ ❆ ✒ ✞ ✦ waitFor ✝ ❆ ✌ ✽ ltp ✝ ❆ ✠ ☛ ✠ ✜ ✌ ❜

➲ ⑥ ❶ ⑤ ⑥ ❻ ✝ ☛ ✌ ✽ ❭ ✚ a211 ✠ ✢ a211 ✠ ➎ a211 ✒ ✞ ✦ ccUpdate ✝ ✚ a211 ✠ ✢ a211 ✠ ➎ a211 ✠ ✜ ✌ ❜ ✜ ✦ start ✝ ☛ ✌ ✽ ✝ ❨ ➲ ⑥ ❶ ⑤ ⑥ ❻ ✝ ☛ ✌ ❲ ❙ ❆ ✒ ✞ ❝ ✦ waitFor ✝ ❆ ✌ ✌ ✽ ✝ ➲ ⑥ ❶ ⑤ ⑥ ❻ ✝ ☛ ✌ ❲ ❙ ✘ ✚ ✒ ✞ ❝ ✦ ccUpdate ✝ ✘ ✚ ✌ ✌ ❏ .

In other words, start ✝ ❛ ❫ ✝ ✞ ✠ ☛ ✌ ✌ is assigned the least time point when the waitFor-condition becomes true under off-line execution, or the time value returned by ccUpdate under on-line execution, or it remains the same. We remark that we could equivalently write two separate successor state axioms for the on-line and off-line case using the idea of guarded successor state axioms proposed in [Giacomo and Levesque, 1999]. While this would enhance the readability and modularity of the axioms, we do not pursue this idea further here for space reasons.

The precondition axiom for ccUpdate ensures that the starting time of legal action sequences is monotonically nondecreasing:

❪ ❫ ☛ ☛ ✝ ccUpdate ✝ ✚ ✠ ✢ ✠ ➎ ✠ ✜ ✌ ✠ ☛ ✌ ✳ ✜ ❘ start ✝ ☛ ✌ ✌

AwaitFor ✝ ❆ ✌ instruction is treated as a special kind of test during on-line execution: it succeeds immediately iff the condition ❆ is true at the beginning of the actual situation. To ensure this intended behavior, we modify the definition of ➈ ➉ ✞ ➋ ☛ for primitive actions:

Finally, we remark that another difference between projection and on-line execution is that during actual execution, whenever the high-level controller executes a send action, the interpreter should check whether this signals an activation of a low-level process and, as a side-effect, activate the actual low-level process if necessary.

On-Line Execution The situations which can result from the on-line execution of a plan have a special structure. Basically, they are made up of the sequence of robot actions as defined by the possible transitions (similar to the execution traces defined by ➈ ➉ ✞ ➋ ☛ ➔ ), however with an arbitrary number of exogenous actions between any two robot actions. Formally, the situations ☛ ✲ which can result from the execution of a program ② in situation ☛ can be characterized by the following predicate ➈ ➉ ✞ ➋ ☛ ➚ ✬ ➽ :

➈ ➉ ✞ ➋ ☛ ➚ ✬ ➽ ✝ ② ✠ ☛ ✠ ➌ ✠ ☛ ✲ ✌ ✳ ❙ ➈ ❍ ✒ ✒ ✒ ❲ ➈ ✝ ➌ ✠ ☛ ✠ ➌ ✲ ✠ ☛ ✲ ✌ ❏

where the ellipsis stands for the universal closure of the conjunction of the following formulas:

➈ ✝ ➌ ✠ ☛ ✠ ➌ ✠ ☛ ✌ ➈ ➉ ✞ ➋ ☛ ✝ ➌ ✠ ☛ ✠ ➌ ✲ ✲ ✠ ☛ ✲ ✲ ✌ ✽ ➈ ✝ ➌ ✲ ✲ ✠ ☛ ✲ ✲ ✠ ➌ ✲ ✠ ☛ ✲ ✌ ❲ ➈ ✝ ➌ ✠ ☛ ✠ ➌ ✲ ✠ ☛ ✲ ✌ ❻ ➩ ➲ ➳ ✝ ✞ ✌ ❲ ➈ ✝ ➌ ✠ ☛ ✠ ➌ ✠ ❛ ❫ ✝ ✞ ✠ ☛ ✌ ✌ , where ❻ ➩ ➲ ➳ ✝ ✞ ✌ ✳ ❭ ➍ ✠ ➋ ✠ ✘ ✚ ✒ ✞ ✦ ➃ ❻ ➤ ❶ ❹ ✝ ➍ ✠ ➋ ✌ ❜ ✞ ✦ ccUpdate ✝ ✘ ✚ ✌

Note that this differs from the original ➈ ➉ ✞ ➋ ☛ ➔ in Section 2 only in the last conjunct, which expresses that an arbitrary number of exogenous actions may occur between any ordinary transition. As an example, let us consider a possible on-line execution trace of prg1. prg1's first action is send ✝ ❺ ❻ ❼ ❽ ❾ ❿ ✠ ❋ ➀ ➁ ➂ ✌ , which results in an activation of the navigation process, which we then assume to provide the high-level controller with ccUpdate actions every .25 sec. The execution trace results in situation ✄ ➚ ✬ ➚ ➶ , where the ➸ ✃ ✠ ➒ ✃ stand for appropriate ✚ ✸ ✢ -coordinates along the path of the robot (we have left out the 3rd argument (voltage level) of ccUpdate a214 ).

✄ ➚ ✬ ➚ ➶ ✒ ✦ do ✝ ❍ send ✝ ❺ ❻ ❼ ❽ ❾ ❿ ✠ ❋ ➀ ➁ ➂ ✌ ✠ ccUpdate ✝ ➸ ③ ✠ ➒ ③ ✠ ➁ ✒ ➀ ➂ ✌ ✠ ccUpdate✝ ➸ ✉ ✠ ➒ ✉ ✠ ➁ ✒ ➂ ✌ ✠ ccUpdate ✝ ➸ ➱ ✠ ➒ ➱ ✠ ➁ ✒ a215 ➂ ✌ ✠ ccUpdate✝ ➸ a217 ✠ ➒ a217 ✠ a218 ✒ ➁ ✌ ✠ say ✝ "In Hallway" ✌ ✠ ✒ ✒ ✒ ✠ ccUpdate ✝ ➸ ➱ ☎ ✠ ➒ ➱ ☎ ✠ a215 ✒ ➂ ✌ ✠ ➃ ❻ ➤ ❶ ❹ ✝ ➃ ❻ ⑨ ➄ ➅ ❻ ❺ ✠ ❋ ➀ ➁ ➂ ✌ ❏ ✠ ✄ ☎ ✌ .

It is not hard to see that ✄ ➚ ✬ ➚ ➶ is a legal on-line execution trace of the introductory cc-Golog program prg1, provided the coordinates ★ ➸ a217 ✠ ➒ a217 ✪ are the first to satisfy inHallway and ★ ➸ ➱ ☎ ✠ ➒ ➱ ☎ ✪ is near the destination ( ➎ ➱ ). Note that waitFor no longer occurs in the action sequence since it is nowmerely a test. Let AX➶ ➶ ✬ be similar to AX➶ ➶ but with the new definitions of this section concerning ➈ ➉ ✞ ➋ ☛ , start, ccUpdate and robotLoc. Let a219 be ➹ ➘ ➴ ➴ a220 a221 ➲ ⑥ ❶ ⑤ ⑥ ❻ ✝ a222 ☎ ✌ . Then

a219 ↕ ✦ ❭ ➌ ✒ ➈ ➉ ✞ ➋ ☛ ➚ ✬ ➽ ✝ prg1 ✠ ✄ ☎ ✠ ➌ ✠ ✄ ➚ ✬ ➚ ➶ ✌ ✽ ✖ ➍ ➋ ✞ ➎ ✝ ➌ ✠ ✄ ➚ ✬ ➚ ➶ ✌

5 Interleaving Projection and On-Line Execution

[de Giacomo and Levesque, 1999] suggest that it is often useful to interleave on-line execution and projection. With our model of time we can take this idea one step further and define projection during on-line execution with the possibility to explicitly put a time-bound on the projection.

5.1 Projection in non-initial Situations

So far, we have only considered projection of cc-Golog in the initial situation. To see how things work in non-initial situation, let us again consider our example scenario, where projection makes use of a model of the navigation process. Suppose we are in the situation illustrated in Figure 3, resulting from the on-line execution of prg1. The controller begins execution by activating the navigation process through send✝ ❺ ❻ ❼ ❽ ❾ ❿ ✠ ❋ ➀ ➁ ➂ ✌ , after which the low-level process provides the high-level controller with a sequence of ccUpdates (the ccUpdates are indicated as black dots in the figure). The controller is now in situation ✄ ③ with

✄ ③ ✒ ✦ do ✝ ❍ send ✝ ❺ ❻ ❼ ❽ ❾ ❿ ✠ ❋ ➀ ➁ ➂ ✌ ✠ ccUpdate ✝ ➸ ③ ✠ ➒ ③ ✠ ➁ ✒ ➀ ➂ ✌ ✠ ccUpdate✝ ➸ ✉ ✠ ➒ ✉ ✠ ➁ ✒ ➂ ✌ ✠ ccUpdate ✝ ➸ ➱ ✠ ➒ ➱ ✠ ➁ ✒ a215 ➂ ✌ ✠ ccUpdate✝ ➸ a217 ✠ ➒ a217 ✠ a218 ✒ ➁ ✌ ❏ ✠ ✄ ☎ ✌ .

First, let us consider the value of the continuous fluent robotLoc in ✄ ③ . Let a219 be defined as before. Then

a219 ↕ ✦ robotLoc ✝ ✄ ③ ✌ ✦ const ✝ ➸ a217 ✠ ➒ a217 ✌ .

We can also infer that what remains from prg1 in ✄ ③ differs from the initial plan (because send ✝ ❺ ❻ ❼ ❽ ❾ ❿ ✠ ❋ ➀ ➁ ➂ ✌ has already been executed).

a219 ↕ ✦ ❭ ➌ ✒ ➈ ➉ ✞ ➋ ☛ ➚ ✬ ➽ ✝ prg1 ✠ ✄ ☎ ✠ ➌ ✠ ✄ ③ ✌ ✽ ➌ ✦ withPol ✝ ❍ waitFor ✝ ⑤ ⑥ ⑧ ⑨ ❶ ❶ ❷ ⑨ ❹ ✌ ✠ ☛ ✞ ✢ ✝ "In Hallway" ✌ ❏ ✠ ❍ reg✝ ➃ ❻ ⑨ ➄ ➅ ❻ ❺ ✌ ✦ ❋ ➀ ➁ ➂ ❏ ✌ ①

Given the updated value of robotLoc, we can now correctly project that the remaining plan will cause the robot to directly travel to its destination. Note the use of clipOnline, which forces a switch to projection mode.

a219 ↕ ✦ ❙ ➌ ✠ ☛ ✒ ➈ ➉ ✞ ➋ ☛ ➚ ✬ ➽ ✝ prg1 ✠ ✄ ☎ ✠ ➌ ✠ ✄ ③ ✌ ❲ Proj ✝ do ✝ ➄ ❶ ⑤ ➤ ➫ ⑥ ❶ ⑤ ⑥ ❻ ✠ ✄ ③ ✌ ✠ ➌ ✠ navProc✠ ☛ ✌ ✳ ☛ ✦ do ✝ ❍ startGo ✝ ➎ ✉ ✌ ✠ waitFor ✝ ⑤ ⑥ ⑧ ⑨ ❶ ❶ ❷ ⑨ ❹ ✌ ✠ say ✝ "In Hallway" ✌ ✠ waitFor ✝ ➋ ➑ ✞ ➉ ✝ ➎ ✉ ✌ ✌ ✠ startGo ✝ ➎ ➱ ✌ ✠ waitFor ✝ ➋ ➑ ✞ ➉ ✝ ➎ ➱ ✌ ✌ ✠ endGo ✠ ➃ ❻ ➤ ❶ ❹ ✝ ➃ ❻ ⑨ ➄ ➅ ❻ ❺ ✠ ❋ ➀ ➁ ➂ ✌ ❏ ✠ do ✝ ➄ ❶ ⑤ ➤ ➫ ⑥ ❶ ⑤ ⑥ ❻ ✠ ✄ ③ ✌ ✌ ❏

The reason why projections in non-initial situations of the example scenario are fairly straightforward is that we never have to remember the state the actual navigation process is in. More precisely, for any given position, the cc-Golog model of the navigation process yields an appropriate approximation of the remaining trajectory of the robot (as illustrated in the above projection). While many low-level processes used in mobile robots seem to have this property, we remark that processes where one needs to keep track of their internal state during execution can be dealt with in a way similar to [Grosskreutz, 2000]. The details, however, are outside the scope of this paper.

5.2 Projection Tests

In order to allow for a time-bounded lookahead, we define the predicate Proj ✝ ❆ ✠ ✜ ✠ ② ✠ ☛ ✌ , which is true, roughly, if ❆ holds at time ✜ in the projected execution of a plan ② in situation ☛ . Let ➎ ➎ ➼ ➽ ➾ ➚ ➪ refer to an appropriate model of the low-level processes, as before.

Proj ✝ ❆ ✠ ✜ ✠ ② ✠ ☛ ✌ ✳ ❭ ② ➔ ✠ ☛ ➔ ✒ ❆ ✝ ☛ ➔ ✌ ✽ start ✝ ☛ ➔ ✌ ❈ ✜ ✽ ➈ ➉ ✞ ➋ ☛ ➔ ✝ withPol ✝ ➎ ➎ ➼ ➽ ➾ ➚ ➪ ✠ ② ✌ ✠ ❛ ❫ ✝ ➄ ❶ ⑤ ➤ ➫ ⑥ ❶ ⑤ ⑥ ❻ ✠ ☛ ✌ ✠ ② ➔ ✠ ☛ ➔ ✌ ✽ ❍ ❙ ② ➔ ➔ ✠ ☛ ➔ ➔ ✒ ➈ ➉ ✞ ➋ ☛ ➔ ✝ ② ➔ ✠ ☛ ➔ ✠ ② ➔ ➔ ✠ ☛ ➔ ➔ ✌ ❲ start ✝ ☛ ➔ ➔ ✌ a224 ✜ ❜ ✖ ➍ ➋ ✞ ➎ ✝ ② ➔ ✠ ☛ ➔ ✌ ❏

Again, we use clipOnline to switch to projection mode. The disjunct involving ✖ ➍ ➋ ✞ ➎ covers the case where the projected plan ends before time ✜ . Using Proj within test conditions, a cc-Golog plan can check whether a possible behavior would lead to certain conditions, and thus deliberate over different possible subplans. In addition, the lookahead can be limited to a certain amount of time ✜ , which seems very useful in order to make quick decisions. A possible application of this test, illustrated by the following program, would be to check if the battery level is going to drop below 46V in the next 300 seconds if the robot comes close to the battery docking station.

withPol ✝ ❍ a225 ✞ ➍ ✜ ✖ ❫ ➉ ✝ ➋ ➑ ✞ ➉ a226 ✞ ✜ ✜ ➓ ❫ a227 a228 ➍ ➋ a229 ✄ ✜ ✞ ✜ ➍ ❫ ➋ ✌ ✠ if ✝ Proj ✝ deliverMail ✠ a230 ➁ ➁ ✠ a231 ✞ ✜ ✜ a232 ➑ ✫ ➑ ➎ ❈ ❉ ❋ ✌ ✠ chargeBatteries ✌ ❏ ✠ ❛ ➑ ➎ ➍ ✫ ➑ ➉ a233 ✞ ➍ ➎ ✌

6 Implementation

Although the definition of cc-Golog requires second-order logic, it is easy to implement a PROLOG interpreter for ccGolog, just as in the case of the original ConGolog. 8 In order to deal with the constraints implied by the waitFor instruction during projection, we have made use of the ECRC Common Logic a234 Programming System Eclipse 4.2 and its built-in constraint solver library clpr (similar to Reiter [Reiter, 1998]).

8 The subtle differences between the second order axiomatization of ConGolog and a PROLOG implementation are discussed in [Giacomo et al., 2000].

As for the on-line execution of cc-Golog plans, we have implemented a prototype runtime system that couples the ccGolog interpreter to the beeSoft execution system [Burgard et al., 2000]. The link between our PROLOG implementation and the beeSoft execution system is based on the High-Level Interface HLI [H¨ ahnel et al., 1998] which provides a uniform PROLOG interface to the low-level processes of beeSoft, along with a monitoring component which provides status update about the state of execution of the activated modules. In particular, our runtime-system handles high-level send actions, which are mapped to commands to the low-level processes, and periodically generates ccUpdate actions reflecting the lattest status updates of the low-level processes.

7 Summary and Discussion

In summary, we have extended cc-Golog so that it becomes suitable for both projections of plans and their on-line execution. In doing so, we also incorporated a model of a robot architecture typically found on modern mobile robots. Finally, we showed how to interleave on-line execution and a form of time-bounded projection.

As mentioned before, the idea of modeling both projection and on-line execution was first explored in [de Giacomo and Levesque, 1999]. However, the authors consider neither time nor the idea of low-level processes which interact with a highlevel controller in complex ways. Most importantly, there is no distinction between the effects on fluents during projection and on-line execution, a distinction we feel is necessary when it comes to modeling essential features of mobile robots such as their location at a given time. [Lesperance and Ng, 2000] have extended de Giacomo and Levesque's ideas in a direction which bears some resemblances to ours. They propose that during projection one also needs to consider a simulated environment which, for example, produces exogenous actions to inform the high-level controller that the destination is reached. However, their notion of a simulated environment remains fairly simple since they are not able to model temporally extended processes, and they also do not distinguish between the effects on fluents during projection and on-line execution. We feel that our proposal addresses some of these shortcomings and brings logic-based robot controllers yet another step closer to real world robotics.

The examples in this paper involving navigation tasks of a single robot were chosen mainly because of their simplicity and as such may not be too convincing as to why logicbased robot controllers with built-in projection mechanisms are beneficial or even necessary, especially at run-time. We believe that the advantages of projections will become much more apparent once robots engage in more complex tasks. Consider, for example, a multi-robot delivery scenario where a user makes a request to have a letter delivered by one of the robots. Then in order to determine which robot should deliver the letter, each robot might use projection to determine the cost that would arise if it were to carry out this job, and the task could then be assigned to the robot with a minimal cost estimate. On-the-fly projection becomes even more important when robots need to coordinate their activities. Suppose that two robots agree to meet somewhere at a certain time in the future. Until then they would probably want to carry out as much of their other duties as possible. Since tasks may not be interruptible at arbitrary times, each robot would be well-advised to check how much of the current task can be completed before heading off to the meeting point. To do so, some form of projection seems necessary. We plan to investigate these and other multi-robot scenarios in the future.