# Decidable Reasoning About Time in Finite-Domain Situation Calculus Theories

arXiv: https://arxiv.org/abs/2402.03164 · HTML: https://mlsanity.com/paper/2402.03164/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 2 of its 31 references that are in the map.
- First posted on arXiv 5 Feb 2024.

## Builds on (most cited first, 2 of 2)

- [Bounded Situation Calculus Action Theories](https://mlsanity.com/paper/1509.02012/) (2015)
- [Hybrid Temporal Situation Calculus](https://mlsanity.com/paper/1807.04861/) (2018)

## Abstract (arXiv)

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 function mathittime(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 when the domain contains only finitely many 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. With this restriction, we can show that the reachability problem for finite-domain basic action theories is decidable. Finally, we apply our results to Golog program realization by presenting a decidable procedure for determining an action sequence that is a successful execution of a given program.