Reasoning about the Interaction of Knowledge, Time and Concurrent Actions in the Situation Calculus

1 Introduction

The aim of this paper is to develop a uni£ed approach for axiomatizing the interaction of knowledge, sensing, time, and concurrency. Actions have preconditions which may include knowledge preconditions. Sensing actions alter knowledge. The knowledge produced depends upon the relative time at which sensing actions occur and also whether or not other sorts of actions occur concurrently. All of this interacts with the agent's evolving knowledge of time.

Consider a robot gathering knowledge about its environ­ ment. It moves about while concurrently panning the camera and at various points senses the environment for the presence of objects with various characteristics. The knowledge ob­ tained through sensing (positions of objects of various sizes, shapes and colors) depends upon the position of the robot at a particular point in time, the angle of the camera, etc. For many purposes, the results of sensing actions that occur at the same time are important. Not only do we have the need for two distinct concurrent sensing actions in binocular stereop­ sis, but also in the simultaneous use of other features such as texture gradients and shading to achieve knowledge of depth relationships. Here it is relative, not absolute time, that is important.

Furthermore, speci£cation of an agent's ability to achieve a goal in general involves requiring that the agent know what to do to arrive at a goal state [Moore, 1980; Lesperance et al., 2000]. As the ability to achieve particular goals will often involve the ability to perform concurrent actions, the integra­ tion of knowledge and concurrency is an important step in fully formalizing these aspects of ability.

We develop our framework within the situation calcu­ lus - a £rst-order formalism for representing and reasoning about the effects of actions. The language is based upon the dialect of the situation calculus used in the Cognitive Robotics Group at the University of Toronto. Certainly, an­ other formalism could have been used. Within A.I. numer­ ous varying formalisms are available for nrepresenting and reasoning about action (to name a few, [Shanahan, 1995; Baral et al., 1997]). Knowledge has been incorporated into a number of these (for example, [Lobo et al., 2001; Thielscher, 2000]). Outside of A.I. proper, there is also [Fa­ gin et al., 1995] on the interaction of knowledge and time.

But by working in the situation calculus, we are able to extend previous work on reasoning (by regression and theo­ rem proving) to cover the language developed here as well. Furthermore, our work is suitable to be incorporated into the robot programming languages GOLOG and CONGOLOG. It can then be used to specify agents that must reason about the interactions of time, knowledge, and concurrent actions (in­ cluding sensing actions).

The situation calculus [McCarthy and Hayes, 1969] is a language for modeling dynamically changing worlds. Changes to the world are the results of actions, while pos­ sible world histories consisting of sequences of actions are represented by situations. The situation calculus can be used for agent planning via goal regression. Reiter [Reiter, 1991] proposed a simple solution to the frame problem, an approach to axiomatization within the situation calculus. Al­ though this approach to the frame problem requires certain simplifying assumptions, it has proven to be useful and is the foundation for both goal regression and the programming lan­ guage GOLOG. Goal regression was extended by Scher! and Levesque[Scherl and Levesque, 2003] to apply to an agent who can sense properties of the external world (e.g., read numbers on a piece of paper or determine the shape of an object).

This paper 1 combines and extends the work of Scher! and Levesque [Scher! and Levesque, 2003] incorporating the model of concurrency and time presented by Reiter [Re­ iter, 2001]. At the same time, Reiter's simple solution to the frame problem is preserved. The real dif£culty is to per­ form the synthesis in such a way that the important distinc­ tion between indexical and objective time [Lesperance and Levesque, 1995] is preserved.

If the agent currently knows the absolute time, then he knows the absolute time after executing an action. But if he doesn't know the absolute time, then he only knows that he began executing the action some number of time units ago, unless of course he reads a clock. While maintaining these properties, the results presented here allow the representation of the various ways in which actions (including sensing ac­ tions and possibly other concurrent actions) interact with time and knowledge. The method of regression is also extended to work with this augmented language.

Section 2 gives a quick introduction to the situation calcu­ lus and Section 3 does the same for the foundational axioms. The representation of knowledge and sensing actions are cov­ ered in Section 4. Concurrency is integrated into the frame­ work in Section 5. Section 6 covers some additional con­ structs of the language and illustrates their representational power. A number of properties of the formulation are dis­ cussed in Section 7. Regression is covered in Section 8. Fi­ nally, Section 9 is the conclusion.

2 Situation Calculus and the Frame Problem

Space does not permit a full exposition of the background material on the situation calculus. The framework developed in [Reiter, 2001] is followed and full details may be found there or in [Scher!, 2003] . We assume that the frame problem has been handled by utilizing successor state axioms.

3 Foundational Axioms

Following [Lin and Reiter, 1994; Reiter, 2001] the founda­ tional axioms for the situation calculus are utilized. These axioms provide us with a de£nition of s ~ s', which says that there is a sequence of zero or more executable actions that move from situation s to situation s'. Again, space does not permit full development of this material here. Full details may be found in [Reiter, 2001; Scher!, 2003].

4 An Epistemic 'Fluent

Scher! and Levesque [Scher! and Levesque, 2003] adapt the standard possible-world model of knowledge to the situation calculus, as £rst done by Moore[Moore, 1980]. Informally, one can think of there being a binary accessibility relation over situations, where a situation s' is understood as being accessible from a situations if as far as the agent knows in sit­ uation s, he might be in situation s'. So something is known in s if it is true in every s' accessible from s, and conversely something is not known if it is false in some accessible situa­ tion.

1 An earlier version of some of this work has appeared in [Zim­ merbaum and Scher!, 2000].

To treat knowledge as a ouent, they introduce a binary rela­ tion K( s', s), read as "s' is accessible from s" and treat it the same way we would any other ouent. In other words, from the point of view of the situation calculus, the last argument to K is the of£cial situation argument (expressing what is known in situations), and the £rst argument is just an auxiliary like they in BROKEN(y, s). 2

The notation Knows(P(now), s) (read as P is known in situations) can then be introduced as as an abbreviation for a formula that uses K. For example

The special indexical now is instantiated with a situation vari­ able upon expansion.

The approach also handles actions that make known the denotation of a term. For this case, one needs the notation Kref(T(now), s) de£ned as follows:

In general, there may be many knowledge-producing ac­ tions, as well as many ordinary actions. To characterize all of these, we have following the presentation in [Scher! and Levesque, 2003], a function SR (for sensing result), and for each action a, a sensing-result axiom of the form:

This result is "YES" if "Q" is true and "NO'' otherwise. The symbols are given in quotes to indicate that they are not Du­ ents. The sensing result function for SENSEQ is axiomatized as follows:

For ordinary actions, the SR result is always the same, with the speci£c result not being signi£cant. For example, we could have:

In the case of a READr action that makes the denotation of the term T known, we would have:

Therefore, T has the same denotation in all worlds s" such that K(s", DO(READn s)), and so Kref(T, DO( REA Dr, s)) is true.

The form of the successor state axiom for K without con­ currency is as follows:

The relation Kat a particular situation DO(a, s) is completely determined by the relation at s and the action a.

2 Note that using this convention means that the arguments to K are reversed from their normal modal logic use.

5 Concurrency

As originally de£ned in the situation calculus [McCarthy and Hayes, 1969], actions had to occur sequentially, with one action completed before another could begin. Furthermore, there was no facility to deal with the continuous passage of time. This contrasted with other formalisms such as the event calculus which could naturally handle concurrent actions and continuous time.

5.1 Concurrency with Knowledge

The work of Pinto [Pinto, 1994] and Reiter [Reiter, 2001] proposed an approach to dealing with concurrency, natural actions and continuous time while still maintaining the so­ lution to the frame problem. Reiter [Reiter, 2001] de£ned a new sort concurrent, sets of simple actions. Variables a, a', .. represent the sort actions and c, c', ... represent the sort concurrent. In Reiter's notation, the time of an action's occurrence is the value of that action's temporal argument. Thus an action has the form A(x, t) and for each action an axiom of the form TIME(A(x, t)) = tis required to indicate the time of the action.

Concurrent actions are sets of ordinary actions that are taken to represent instantaneous acts. An action with dura­ tion is represented by two instantaneous actions - a start ac­ tion and an end action. Additionally, the foundational axioms are modi£ed to rule out the possibility of prior actions having later times.

So if we want to represent a PRESSING action with duration (as in pressing a button that keeps a light on), the approach is to de£ne two actions; STARTPRESS and ENDPRESS. We also must introduce a ouent PRESSING. The needed succes­ sor state axiom is as follows:

This approach to representing actions with duration is some­ thing that we make use of here.

But, the use of a temporal argument for actions is problem­ atic in the presence of knowledge. Given our successor state axiom for K, it would require the agent to know the time after any action, even if it was unknown in the previous situation. To avoid this, we can not represent time as an argument to the instantaneous actions.

Instead, we represent the instantaneous actions and asso­ ciated times as a tuple of the form < a, t > with functions ACTION and TIME de£ned, returning the £rst and second ele­ ments of the tuple:

These pairs, represented by variables p, p', ... are elements of the sort action-time pairs. Concurrent Actions are now a set of such tuples. The sort action contains actions without a temporal argument.

We also have the following

which is needed to relate the time of the action/time pair to the start of a situation. There may also be an axiom giving the start time of the initial situation So. We also de£ne a variant notation:

We adopt, without signi£cant change, Reiter's requirement that concurrent actions be coherent, that is there is at least one action-time pair p in the collection, and the time of all pairs in the collection is the same:

A set of action-time pairs are coherent if each of them have the same time component.

The de£nition of time can readily be extended to sets of concurrent actions and this allows us to de£ne the function start of a situation resulting from the execution of a concur­ rent action.

The predicate Poss(c, s) means that it is possible to exe­ cute concurrent action c in situation s.

If it is possible to execute a concurrent actions, then it is co­ herent and each of the simple actions is possible.

We implicitly assume an additional sort ranging over time points which can be integers, rationals or reals; depending on how one wants to model time. The standard Arabic numerals are used to represent time points. Additionally, the symbols for addition and subtraction are interpreted as the usual oper­ ations on numbers (integers, reals etc.)

5.2 Precondition Interactions

We need to be able to conclude when a particular concurrent action c is possible in a situation c in order for the machinery being developed in the rest of this paper to work. Unfortu­ nately, Sentence 15 does not suf£ce. The conditional can not be changed to a biconditional because of the precondition in­ teraction problem [Pinto, 1994; 1998].

This issue needs to be handled by the axiomatizer of the domain. For example, the axiomatizer might provide the fol­ lowing axiom:

As discussed in [Pinto, 1994; 1998], the axiomatization of PRECINT is domain dependent and can be done at increasing levels of detail.

For the purposes of this paper, the point here is that what­ ever solution is used for the precondition interaction problem in the ordinary situation calculus carries over to the case of knowledge and sensing.

5.3 Successor State Axiom forK with Concurrency

The Successor State Axiom for K using concurrency can be stated in several alternative ways depending on what condi­ tions one wishes to apply regarding the agent's knowledge of time. We continue to require that the relation K at a particular situation oo( c, s) is completely determined by the relation at s and the set of concurrent actions c.

The following successor state axiom models an agent who knows how much time is passing 3 . This is an agent who has an accurate clock.

After executing a set of concurrent actions c in situation s, as far as the agent knows, it could be in a situation s" iff s" is the result of performing c' in some previously accessible situation s', provided that c is possible in s' and that s' is identical to s in terms of what is being sensed. Furthermore, it is required that the concurrent action c' being performed in all situations accessible from s be identical to c in terms of the individual actions that make up the set.

Note that it is not required that the TIME of the actions in all the accessible situations be identical. If this were the case, it would force the agent to know the objective time after execut­ ing any action. Rather, it is only required that the difference between the start of the current situation and the start of the previous situation be the same in all accessible situations (in­ cluding the actual situation). This requirement does ensure that the agent knows how much time is passing, but the ob­ jective time is only known if it was known before the action has occurred.

5.4 Concurrency and Sensing

One can readily imagine cases of sensing actions where the desired result of sensing (knowing whether or not some proposition holds) depends upon some other action occurring concurrently. For example, the light needs to be turned on while the camera is clicked. If the light is off, then sensing produces no knowledge.

Consider representing, the requirement that the light switch be pressed while SENSEp occurs for the knowledge of whether or not P holds to result from the execution of SENSEp. We need to de£ne a predicate SCOND.

----- Now the successor state axiom forK needs to be modi£ed to include SCOND as well.

30ther possibilities are considered in [Scher!, 2003].

For every action an appropriate ScaN axiom needs to be written. For most actions, the action is simply:

6 The Language and Examples

6.1 Further Constructs

We need some way to refer to the current time without speci­ fying the value of the current time. To achieve this we use the special indexical term now. Upon expansion the term is re­ placed with the appropriate situation term. So, START(now) can be used to refer to the current time. Here we illustrate by example. The agent's knowing the objective time is expressed as :Jt Know( start( now) = t, s). This expands into

We augment our language with a number of additional ex­ pressions. These are based on ideas developed by Lesperance and Levesque [Lesperance and Levesque, 1995] and require the use of the notion of precedence of situations as de£ned earlier. Note that we distinguish between the < relation on integers used to represent time points and the -< relations on situations as de£ned in the foundational axioms for the situation calculus.

The macro Happened is introduced to allow one to talk about an action occurring at a particular time point.

It speci£es that an action occurred prior to s and it was time t at some point during the action's duration.

The macro Wasat is introduced to allow one to assert that a auent was true at a particular point in time.

It speci£es that P held at s' and twas the time of s' or s' pre­ ceded t and no other situation after s' preceded t . Here we introduce another special indexical then which is needed to ensure that the correct situation is substituted into the situa­ tion argument of the predicate which is the middle argument to Wasat.

7 Properties of the Formulation

First of all, we show that the distinction between indexical and objective time is preserved.

Proposition 1 (Persistence of Ignorance of Objective Time)

For all situations s, if -.::Jt Know( START( now) = t, s) then in do( c, s) where c is any concurrent action it is also the case that -.3t Know( START( now) = t, s) unless there is some a E c with an SR axiom equivalent to the following: SR(a, s) = r = r = TIME(s)

Proposition 2 (Persistence of Knowledge of Objective Time)

For all situations s, if3t Know( start( now) = t, s) then in do( c, s) where c is any concurrent action it is also the case that 3t Know( start( now) = t , s)

Even if agents do not know the objective time, they do know how much time has passed since the last occurrence of a par­ ticular action or the last time at which a particular ouent was true.

Proposition 3 (Knowledge of Indexical Time 1)

For every, Act such that Act occurs in s, 3t Knows(::Jt'Happened(t', Act , now) 1\

Proposition 4 (Knowledge of Indexical Time 2) For every P such that there is some s' -< s such that P( s') holds,

Additionally, the crucial results of [Scher! and Levesque, 2003] carry over to the case considered here. These include

Proposition 5 (Default Persistence of Ignorance) For an action o: and a situation s, if -.Knows(P, s) holds and the axiomatization entails

and

then

holds as well.

Proposition 6 (Knowledge Incorporation) For a !-.:now/edge-producing action o:, a Duent or the negation of a Duent F, a ouent or the negation of a Duent P, and a situation s, if the axiomatization entails

and also

and

hold, then

holds as well.

Proposition 7 (Memory) For all Duents P and situations s, ifKnows(P, s) holds then Knows(P, DO( a:, s)) holds as long as the axiomatization entails

These results ensure that actions only affect knowledge in the appropriate way.

8 Reasoning

A regression operator n is de£ned relative to a set of suc­ cessor state axioms e. Space limitations here only allow a sketch of the regression operators. Full details may be found in [Scher!, 2003].

The operators satisfy the following regression theorem:

Theorem 1 For any ground situation term s 9 r and formula G:

Here :F is the initial axiomatization of the domain and :Fss is the set of successor state axioms.

8.1 Regression Operators

The regression operator n is de£ned relative to a set of suc­ cessor state axioms e. The £rst four parts of the de£nition of the regression operator Re concern ordinary (i .e. not knowledge-producing) actions [Reiter, 2001]. They are ex­ actly the same as those in [Reiter, 2001]. Additionally, it is necessary to correctly regress the equality predicate as dis­ cussed in [Scher! and Levesque, 2003; Reiter, 2001].

Additional steps are needed to extend the regression op­ erator to knowledge-producing actions. Two de£nitions are needed for the speci£cation to follow. When cp is an arbitrary sentence and sa situation term, then cp [s] is the sentence that results from instantiating every occurrence of now in cp with s'. The reverse operation cp- 1 is the result of instantiating every occurrence of s' in cp with now.

Step v covers the case of regressing the Knows operator through a non-knowledge-producing action. Step vi covers the case of regressing the Knows operator through a knowl­ edge producing action. In the de£nitions below, s' is a new situation variable.

1. Whenever c does not contain a knowledge-producing ac­ tion,

1. Whenever c does contain a knowledge-producing action, Re[Knows(W, oo(c, s))] =

The special function trans replaces c with a c' that has the identical action in each of the action-time pairs. But it re­ places the time portion with a relative time. This is an ex­ pression of the form (3 = TIME( now)). So, if c occurs in a situation term of the form DO(c, s) and TIME( c) is 7 and START(s) is 4, then the 7 in the time part of every action­ time pair inc would be replaced by (3 =TIME( now)). These are properly handled by the operators for regressing equality predicates.

The regression operators for Happened and Wasat follow: viii.

ix.

R[Wasat(t, W, oo(c, s))] = (Wasat(t, W,s) 1\ t < START(s)) V (W(s) 1\ t 2 START(s) 1\ t < START(DO(c, s)))

The end result of regression is a sentence (possibly much larger) in a language without actions. The language is a modal language with both temporal and epistemic operators.

9 Conclusions

The results reported in this paper can be combined with Concurrent, Temporal Golog or RGolog[Reiter, 2001] or CONGOLOG[Giacomo eta!., 1997] to specify and control an agent (such as the robot discussed in Section I) that con­ currently moves about its environment and performs various actions including sensing actions. Future work will address the issue of developing a good theorem proving method for the language resulting from regression. This method needs to combine modal theorem proving with a method for solving integer constraints.

Acknowledgments

Numerous helpful discussions have been held with Yves Lesperance on many of the topics covered in this paper. Use­ ful suggestions made by Patrick Doherty, Daniele Nardi, and a number of anonymous reviewers of earlier versions of this paper have been incorporated. Additional thanks are due to Steve Zimmerbaum with whom the initial stages of this work were carried out. This research was partially supported by NSF grants SES-9819116 and CISE-9818309.