Decidable Verification of Golog Programs:
    Situation Calculus Meets Description Logic

                         Gerhard Lakemeyer

  RWTH Aachen University, Ahornstr. 55, 52056 Aachen, Germany
               gerhard@cs.rwth-aachen.de



Abstract. In the area of reasoning about action and change, one of the
best understood formalisms is the situation calculus, which was originally
proposed by John McCarthy in the late fifties. In its modern form, due to
Ray Reiter, the situation calculus provides a solution to the frame prob-
lem and is also the basis for the action programming language Golog,
which is used, among other things, to control the high-level behavior of
robots. When considering the verification of temporal properties of Golog
programs, one quickly runs into undecidability because of the expressive-
ness of the situation calculus. To tackle this problem we have teamed up
with Franz Baader and his group, and we have been able to show that
decidable verification can be obtained when the base logic is restricted
to a Description Logic (DL). In this talk, I will begin by introducing a
modal variant of the situation calculus and Golog. I will then define the
verification problem and show how decidability can be achieved with the
help of DL.