  Representing time is crucial for cyber-physical systems and has been studied
extensively in the Situation Calculus. The most commonly used approach
represents time by adding a real-valued fluent $\mathit{time}(a)$ that attaches
a time point to each action and consequently to each situation. We show that in
this approach, checking whether there is a reachable situation that satisfies a
given formula is undecidable, even if the domain of discourse is restricted to
a finite set of objects. We present an alternative approach based on
well-established results from timed automata theory by introducing clocks as
real-valued fluents with restricted successor state axioms and comparison
operators. %that only allow comparisons against fixed rationals. With this
restriction, we can show that the reachability problem for finite-domain basic
action theories is decidable. Finally, we apply our results on Golog program
realization by presenting a decidable procedure for determining an action
sequence that is a successful execution of a given program.
