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 fties. In its modern form, due to Ray Reiter, the situation calculus provides a solution to the frame problem 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 veri cation of temporal properties of Golog programs, one quickly runs into undecidability because of the expressiveness 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 veri cation 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 de ne the veri cation problem and show how decidability can be achieved with the help of DL.