Reasoning about Concurrent Execution Prioritized Interrupts, and Exogenous Actions in the Situation Calculus

1 Situation Calculus

There are a number of ways of making the planning task pre­ cise, but perhaps the most appealing is to formulate a specifi­ cation in terms of a general theory of action. One candidate language for formulating such a theory is the situation cal­ culus [10]. We will not go over the language here except to note the following components: there is a special constant S0 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( a, s) denotes the suc­ cessor situation to s resulting from performing the action a; 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; finally, there is a special predicate Pass( a, s) used to state that action a is executable in situations.

1 1n [ 13; 4] a direct use of such approaches to model concurrent (complex) actions in AI is investigated.

Within this language, we can formulate domain theories which describe how the world changes as the result of the available actions. One possibility is a theory of the following form [14]:

• Axioms describing the initial situation, S0 .
• Action precondition axioms, one for each primitive ac­ tion a, characterizing Pass( a, s).
• Successor state axioms, one for each fluent F, stating under what conditions F(x, do( a, s)) holds as function of what holds in situations. These take the place of the so-called effect axioms, but also provide a solution to the frame problem [14].
• Unique names axioms for the primitive actions.
• Some foundational, domain independent axioms.

For any domain theory of this sort, we have a very clean spec­ ification of the planning task, which dates back to the work of Green [5]:

Classical Planning: Given a domain theory Axioms as above, and a goal formula ¢(s) with a single free-variables, the planning task is to find a sequence of actions a such that:

where do([a1, .. . , an], s) is an abbreviation for

and where Legal( [ a1 , . . . , an], s) stands for

In other words, the task is to find a sequence of actions that is executable (each action is executed in a context where its precondition is satisfied) and that achieves the goal (the goal formula¢ holds in the final state that results from performing the actions in sequence).

2 Golog

As presented in [9], Golog is logic-programming language whose primitive actions are those of a background domain theory. It includes the following constructs:

In its most basic form, the high-level program execution task is a special case of the above planning task:

Program Execution: Given a domain theory Axioms as above, and a program a, the execution task is to find a sequence of actions a such that:

where Do( a, s, s') is an abbreviation for a formula of the situation calculus which says that program a when executed starting in situation s has s' as a legal terminating situation.

In [9], a simple inductive definition of Do was presented, con­ taining rules such as:

one for each construct in the language.

The kind of semantics Do associates to programs is some­ times called evaluation semantics [6] since it is based on the complete evaluation of the program. With the goal of eventu­ ally handling concurrency, it is convenient to give a slightly more refined kind of semantics called computational seman­ tics [6], which is based on "single steps" of computation, or transitions. 4 A step here is either a primitive action or test­ ing whether a condition holds in the current state. We begin by introducing two special predicates, Final and Trans , where Final(a, 's) is intended to say that program a may legally ter­ minate in situations, and where Trans( a , s, a', s') is intended to say that program a in situation s may legally execute one step, ending in situation s' with program a' remaining.

Final and Trans will be characterized by a set of equiv­ alence axioms, each depending on the structure of the first argument. It will be necessary to quantify over programs and so, unlike in [9], we need to encode Golog programs as first­ order terms, including introducing constants denoting vari­ ables, and so on. This is laborious but quite straightforward [8].5 We omit all such details here and simply use programs within formulas as if they were already first-order terms.

2 Here, ¢ stands for a situation calculus formula with all situa­ tion arguments suppressed; ¢( s) will denote the formula obtained by restoring situation variable s to all tluents appearing in ¢. Because there are no exogenous actions or concurrent processes in Golog, waiting for¢ amounts to testing that ¢holds in the current state.

3 For space reasons, we ignore these here.

4 Both types of semantics belong to the family of structural oper­ ational semantics introduced in [12].

5 0bserve that Final and Trans cannot occur in tests, hence self­ reference is disallowed.

The equivalence axioms rF for Final are as follows (uni-

versally closing on s): 6

Final(nil, s) ::::: TRUE Final( a, s) :::::FALSE Final(¢?, s) ::::: FALSE Final([a1;a2],s) = Final(a1,s) /\Final(a2,s) Final([a1 I a2],s) = Final(a1,s) V Final(a2,s) Final(1rx.a, s) = 3x.Final(a, s) Final( a*, s) ::::: TRUE Final(if ¢ then a 1 else a 2 , s) = ¢( s) 1\ Final( a1, s) V --.¢( s) 1\ Final( a2, s) Final( while¢ do a, s) = ¢(s) 1\ Final( a, s) V -.¢(s)

The equivalence axioms rr for Trans are as follows (univer­ sally closing on s, 6, s'):

Trans( nil, s, 6, s') = FALSE Trans( a, s, 6, s') = Poss(a, s) 1\ 6 = nil 1\ s' = do(a, s) Trans(¢?, s, 6, s') = ¢(s) 1\6 =nil 1\ s' = s Trans([a1; a2], s, 6, s') = Final(a1,s) 1\ Trans(a2,s,6,s') V 36'.6 = (6'; a2) 1\ Trans(a1, s, 6', s') Trans([a1 I a2], s, 6, s') = Trans( a1, s, 6, s') V Trans( a2, s, 6, s') Trans(1rx.a, s, 6, s') = 3x.Trans(a, s, 6, s') Trans( a*, s, 6, s') = 36'.6 = (6';a*) 1\ Trans(a,s,6',s') Trans(if ¢then a 1 else a 2 , s, 6, s') = ¢(s) 1\ Trans(a1,s,6,s') V --.¢( s) 1\ Trans( a2, s, 6, s') Trans( while¢ do a, s, 6, s') =

It is easy to verify, by induction on the structure of the first argument, the following:

Theorem 1: For each Go log program a, there exist two situation calculus formulas <Pu (s ).and Ill u (s, 6, s'), not men­ tioning Final and Trans, such that:

With Final and Trans in place, we may give a new definition of Do as:

where Trans* is the transitive closure of Trans, defined as the (second-order) situation calculus formula:

where the ellipsis stands for:

6 It is convenient to include a special "empty" program nil.

In other words, Do( a, s, s') holds if it is possible to repeat­ edly single-step the program a, obtaining a program 6 and a situation s' such that 6 can legally terminate in s'. We then get the following result: 7

Theorem 2: The two definitions of Do are equivalent in that for any non-nil Go!og program a and situations sands':

3 Concurrency

We are now ready to define ConGolog, an extended version of Golog that incorporates a rich account of concurrency. We say 'rich' because it handles:

• concurrent processes with possibly different priorities,
• high-level interrupts,
• arbitrary exogenous actions.

As is commonly done in other areas of computer science, we model concurrent processes as interleavings of the primitive actions in the component processes. A concurrent execution of two processes is one where the primitive actions in both processes occur, interleaved in some fashion. So in fact, we never have more than one primitive action happening at the same time. As discussed in [I; 15], to model actions that in­ tuitively could occur simultaneously, e.g. actions of extended duration, we use instantaneous start and stop (i.e. clipping) actions, where once again interleaving is appropriate.

An important concept in understanding concurrent execu­ tion is that of a process becoming blocked. If a deterministic process a is executing, and reaches a point where it is about to do a primitive action a in a situation s but where Poss( a, s) is false (or a wait action ¢?, where cp(s) is false), then the overall execution need not fail as in Golog. In ConGolog, the current interleaving can continue successfully provided that a process other than a executes next. The net effect is that a is suspended or blocked, and execution must continue elsewhere. 8

The ConGolog language is exactly like Golog except with the following additional constructs:

( a1 II a2) denotes the concurrent execution of the actions a1 and a2. ( a1 )) a2) denotes the concurrent execution of the ac­ tions a1 and a2 with a1 having higher priority than a2. This restricts the possible interleavings of the two processes: a2 executes only when a 1 is either done or blocked. The next construct, all, is like nondeterministic iteration, but where the instances of a are executed concurrently rather than in se­ quence. Finally, < ¢> -+ a> is an interrupt. It has two parts: a trigger condition¢ and a body, a. The idea is that the body a will execute some number of times. If ¢ never becomes true, a will not execute at all. If the interrupt gets control from higher priority processes when¢ is true, then a will ex­ ecute. Once it has completed its execution, the interrupt is ready to be triggered again. This means that a high priority interrupt can take complete control of the execution. For ex­ ample, < TRUE --7 ringBell > at the highest priority would ring a bell and do nothing else. With interrupts, we can easily write controllers that can stop whatever task they are doing to handle various concerns as they arise. They are, dare we say, more reactive.

7 See [6] for hints on the proof of this theorem.

8 Just as actions in Golog are external (e.g. there is no internal variable assignment), in ConGolog, blocking and unblocking also happen externally, via Pass and wait actions. Internal synchroniza­ tion primitives are easily added.

We now show how Final and Trans need to be extended to handle these constructs. (We handle interrupts separately below.) For Final, the extension is straightforward:

Observe that the last clause says that it is legal to execute the a in all zero times. For Trans, we have the following:

In other words, you single step (a1 II a 2 ) by single stepping either a1 or a 2 and leaving the other process unchanged. The (a1 )) a2) construct is identical, except that you are only allowed to single step a2 if there is no legal step for a1 . 9 This ensures that a1 will execute as long as it is possible for it to do so. Finally, you single step all by single stepping a, and what is left is the remainder of a as well as all itself. This allows an unbounded number of instances of a to be running.

Observe that with (a1 II a2), if both a1 and a2 are always able to execute, the amount of interleaving between them is left completely open. It is legal to execute one of them completely before even starting the other, and it also legal to switch back and forth after each primitive or wait action. It is not hard to define, however, new concurrency constructs llmin and llmax that require the amount of interleaving to be minimized or maximized respectively. We omit the details.

Exogenous actions are primitive actions that may occur without being part of a user-specified program. We assume that in the background theory, the user declares using a predi­ cate Exo which actions can occur exogenously. We then mod­ ify the specification of Trans for primitive actions and wait actions from Golog as follows:

9 lt is true, though not immediately obvious, that Trans· remains properly defined even with these axioms containing negative occur­ rences of Trans. See [I] for details.

and similarly for test actions. So while executing a program, exogenous actions whose preconditions are satisfied can oc­ cur before any primitive action or while waiting for any con­ dition to become true.

Finally, regarding interrupts, it turns out that these can be explained using other constructs of Condolog:

To see how this works, first assume that the special flu­ ent Interrupts_running is always true. When an in­ terrupt < ¢ --7 a> gets control, it repeatedly executes a until ¢ becomes false, at which point it blocks, releas­ ing control to anyone else able to execute.. Note that ac­ cording to the above definition of Trans, no transition oc­ curs between the test condition in a while-loop or an if­ then-else and the body. In effect, if ¢ becomes false, the process blocks right at the beginning of the loop, un­ til some other action makes ¢ true and resumes the loop. To actually terminate the loop, we use a special primi­ tive action stop_interrupts, whose only effect is to make I nterrupts_running false. Thus, we imagine that to execute a program a containing interrupts, we would actually execute the program {start-interrupts ; (a )) stop_interrupts)} which has the effect of stopping all blocked interrupt loops in a at the lowest priority, i.e. when there are no more actions in a that can be executed.

4 A reactive multi-elevator controller

We illustrate the use of the concurrency primitives using a reactive elevator controller example. The example will use the following terms (where e stands for an elevator):

• ordinary primitive actions: goDown(e) move elevator down one floor goU p( e) move elevator up one floor buttonReset( n) turn off call button of floor n toggleFan(e) change the state of elevator fan ring Alarm ring the smoke alarm
• exogenous primitive actions: reqElevator(n) call button on floor n is pushed changeTemp(e) the elevator temperature changes detectSmoke the smoke detector first senses smoke resetAlarm the smoke alarm is reset
• primitive fluents : floor(e, s) = n temp(e, s) = t FanOn(e, s) ButtonOn(n, s)
• Smoke(s) the elevator is on floor n, 1 :S n :S 6 the elevator temperature is t the elevator fan is on call button on floor n is on smoke has been detected
• defined fluents: def TooH ot(e, s) = temp(e, s) > 3 TooCold(e, s) d;j temp(e, s) < -3

We begin with the following basic action theory for the above primitive actions and fluents:

• initial state: floor(e, So) = 1 Button0n(3, So) ·FanOn(So) temp(e, So) = 0 Button0n(6, So)

• exogenous actions:

Va.Exo(a) = a= detectSmoke V a= resetAlarm V a= changeTemp(e) V 3n.a = reqElevator(n) · precondition axioms: Poss(goDown(e), s)=:floor(e, s) =f. 1 Poss(goUp(e), s)=:floor(e, s) =f. 6 Poss(buttonReset(n), s)=:TRUE Poss(toggleFan(e), s)=:TRUE Poss(ringAlarm)=:TRUE Poss(reqElevator(n), s):=(1 :S n :S 6) 1\ ·ButtonOn(n, s) Poss(changeTemp, s)=:TRUE Poss(detectSmoke, s)=:·Smoke(s) Poss(resetAlarm, s)=:Smoke(s) · successor state axioms: Poss(a,s) ::J [floor(e , do( a, s)) = n=: (a= goDown(e) 1\ n = floor(e, s)- 1) V (a= goUp(e) 1\ n = floor(e, s) + 1) V (n = floor(e , s) 1\ a =f. goDown(e) 1\ a =f. goUp(e))] Poss(a,s) ::J [temp(e,do(a,s)) = t= (a= changeTemp(e) 1\ FanOn(e, s) 1\ t = temp(e, s)- 1) V (a= changeTemp(e) 1\ ·FanOn(e, s) 1\ t = temp(e, s) + 1) V (t = temp(e, s) 1\ a =f. changeTemp(e))] Poss(a, s) ::J [FanOn(e,do(a, s))=: (a= toggleFan(e) 1\ ·FanOn(e, s)) V (a =f. toggleFan(e) 1\ FanOn(e, s))] Poss(a, s) ::J [ButtonOn(n, do( a, s))=: a= reqElevator(n) V (ButtonOn(n, s) 1\ a =f. buttonReset(n))] Poss(a, s) ::J [Smoke(do(a, s))=: a = detectSmoke V (Smoke(s) 1\ a =f. resetAlarm)]

Note that many fluents are affected by both exogenous and programmed actions. For instance, the fluent ButtonOn is made true by the exogenous action reqElevator (i.e. some­ one calls for an elevator) and made false by the programmed action buttonReset (i.e. when an elevator serves a floor).

Now we are ready to consider a basic elevator controller. It might be defined by something like:

while 3n.Button0n(n) do 1rn.{ BestButton(n)?; serveFloor(e, n)}; while floor( e) =f. 1 do goDown(e)

The fluent BestButton would be defined to select among all buttons that are currently on, the one that will be served next. For example, it might choose the button that has been on the longest. For our purposes, we can take it to be any ButtonOn. The procedure serveFloor( e, n) would consist of the actions the elevator would take to serve the request from floor n. For our purposes, we can use:

de f serveFloor(e, n) = while floor( e) < n do goUp(e); while floor( e) > n do goDown(e); buttonReset ( n)

We have not bothered formalizing the opening and closing of doors, or other nasty complications like passengers.

Using this controller a, we would get execution traces like

Axioms f= Do( a, So, do([u, u , r3, u, u, u, r6, d, d, d, d, d], So))

where u = goUp(e) , d= goDown(e), rn = buttonReset(n) . In this particular run, there were no exogenous actions.

This controller does have a big drawback, however: if no buttons are on, the first loop terminates, the elevator returns to the first floor and stops, even if buttons are pushed on its way down. It would be better to structure it as two interrupts:

< 3n.Button0n(n) -+ 1rn.{ BestButton(n)?; serveFloor(e, n)} > <floor(e) =f-1-+ goDown(e)>

with the second at lower priority. So if no buttons are on, and you're not on the first floor, go down a floor, and reconsider; if at any point buttons are pushed exogenously, pick one and serve that floor, before checking again. Thus, the elevator only quits when it is on the first floor with no buttons on.

With this scheme, it is easy to handle emergency or high­ priority requests. We would add

<3n.EButtonOn(n)-+ 1rn.{EButtonOn(n)?; serveEFloor(e, n)} >

as an interrupt with a higher priority than the other two (as­ suming suitable additional actions and fluents).

To deal with the fan, we can add two new interrupts:

<TooHot(e) 1\ ·FanOn(e)-+ toggleFan(e) > <TooCold(e) 1\ FanOn(e)-+ toggleFan(e) >

These should both be executed at the very highest priority. In that case, while serving a floor, whatever that amounts to, if the temperature ever becomes too hot, the fan will be turned on before continuing, and similarly if it ever becomes too cold. Note that if we did not check for the state of the fan, this interrupt would loop repeatedly, never releasing control to lower priority processes.

Finally, imagine that we would like to ring a bell if smoke is detected, and disrupt normal service until the smoke alarm is reset exogenously. To do so, we add the interrupt:

<Smoke -+ ring Alarm>

with a priority that is less than the emergency button, but higher than normal service. Once this interrupt is triggered, the elevator will stop and ring the bell repeatedly. It will han­ dle the fan and serve emergency requests, however.

Putting all this together, we get the following controller:

(<TooHot(e) 1\ ·FanOn(e)-+ toggleFan(e)> II <TooCold(e) 1\ FanOn(e)-+ toggleFan(e)>) )) < 3n.EButtonOn(n) -+ 1rn.{EButtonOn(n)?; serveEFloor(e, n)} >)) <Smoke -+ ring Alarm> )) <3n.Button0n(n)-+ 1rn.{ BestButton(n)?; serveFloor(e, n)} > )) <floor(e) =f. 1-+ goDown(e)>

Note that this elevator controller uses 5 different levels of pri­ ority. It could have been programmed in Golog without inter­ rupts, but the code would have been a lot messier.

Now let us suppose that we would like to write a controller that handles two independent elevators. In ConGolog, this can be done very elegantly using (u1 II u2 ), where u1 is the above program with e replaced by elevator1 and u2 is the same program withe replaced by elevator2 . This allows the two processes to work completely independently (in terms of priorities). 10 For n elevators, we would use (u1 II · · · II un) ­ In some applications, it is useful to have an unbounded num­ ber of instances of a process running concurrently. For exam­ ple in an FTP server, we may want an instance of a manager process for each active FTP session. This can be programmed using the ull concurrent iteration construct.

Finally, if it is desirable to have the elevator continue work­ ing indefinitely, we can do so by adding an interrupt:

at the lowest possible priority, where wait is a no-op in terms of fluents. So if everything else is satisfied, the elevator sim­ ply waits until a higher priority interrupt is triggered exoge­ nously. Such programs never terminate, so semantics based on Do cannot be used, but their behavior can nonetheless be specified using Trans [1].

5 Discussion

With all of this procedural richness, it is important not to lose sight of the logical framework. ConGolog is indeed a pro­ gramming language, but one whose execution, like planning, depends on reasoning about actions. Thus, a crucial part of a ConGolog program is the declarative part: the precondition axioms, the successor state axioms, and the axioms charac­ terizing the initial state. This is central to how the language differs from superficially similar "procedural languages". A ConGolog program together with the definition of Do and some foundational axioms about the situation calculus is a formal logical theory about the possible behaviors of an agent in a given environment.U And this theory must be used ex­ plicitly by a ConGolog interpreter.

We have developed a prototype ConGolog interpreter in Pro log (see [ 1]). Indeed, a simple if somewhat inefficient interpreter can be lifted directly from Final, Trans, and Do introduced above. 12 For example, for (u1 )) u2), we would have the following two Pro log clauses for Trans:

trans(prioConc(Sigmal,Sigma2) ,Sl,

prioConc(Delta,Sigma2),S2) :­

trans(Sigmal,Sl,Delta , S2).

trans(prioConc(Sigmal,Sigma2) ,Sl,

prioConc(Sigmal,Delta) ,S2)

trans(Sigma2,Sl,Delta , S2) ,

not trans(Sigmal,Sl,_,_).

Our implementation requires that the program's precondition axioms, successor state axioms, and axioms about the initial state be expressible as Prolog clauses. This is a limitation of the implementation, not the theory.

10 0f course, when an elevator is requested on some floor, both el­ evators may decide to serve it. It is easy to program a better strategy that coordinates the elevators: when an elevator decides to serve a floor, it immediately makes a fluent true for that floor, and the other elevator will not serve a floor for which that fluent is already true.

11 Although with a different emphasis, this approach is shared by [2] where a logical formalism is proposed for concurrent database transactions.

12 Exogenous actions can be simulated by generating them proba­ bilistically or by asking the user at runtime when they should occur.

In summary, we have shown how, given a basic action the­ ory describing an initial state and the preconditions and ef­ fects of a collection of primitive actions, it is possible to com­ bine these in complex ways appropriate for providing high­ level control. The semantics of these complex actions ends up deriving directly from that of the underlying primitive ac­ tions. In this sense, we inherit the solution to the frame prob­ lem provided by successor state axioms for primitive actions.

There are, however, many areas for future research. Among them, we mention: 1) incorporating sensing actions, that is, actions whose effect is not to change the world so much as to provide information to be used by the agent at runtime; 2) handling non-termination, that is, developing ac­ counts of program correctness (fairness, liveness etc.) appro­ priate for controllers expected to operate indefinitely.