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.

Swarm robotic systems are distributed systems wherein a set of robots cooperatively perform a task, without any centralized coordination [29]. Although individual robots are governed by relatively simple reactive controllers, interactions within the swarm may give rise to complex behaviors that were not explicitly programmed. Ultimately, these behaviors enable the swarm to achieve goals that would defy each single robot in isolation, or would require more expensive robots to achieve the same goals as effectively as the swarm does - see, e.g, [4, 33] for some examples. While understanding individual robot behavior is easy, predicting the overall swarm behavior is difficult, and thus engineering controllers for individual robots that will guarantee a desired swarm behavior is not a straightforward task. Traditionally, the analysis of swarms is carried out either by testing real robot implementations, or by computational simulations [20, 22]; however, these approaches provide little guarantees as they suffer from intrinsically incomplete coverage. As suggested by many authors, higher levels of assurance in swarm behavior can be obtained via formal methods [32, 30, 16, 5, 18, 23].