Decidable Reasoning About Time in Finite-Domain Situation Calculus Theories
<|reference_start|>Decidable Reasoning About Time in Finite-Domain Situation Calculus Theories: 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.<|reference_end|>
@article{hofmann2024decidable,
    title={Decidable Reasoning About Time in Finite-Domain Situation Calculus
  Theories},
    author={Till Hofmann, Stefan Schupp, Gerhard Lakemeyer},
    journal={arXiv preprint arXiv:2402.03164},
    year={2024},
    archivePrefix={arXiv},
    eprint={2402.03164},
    primaryClass={cs.AI cs.LO}
}