2026-10-10T21:18:06Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:27707 2026-10-10T19:48:19Z ddc:004 open_access

Decidable Reasoning About Time in Finite-Domain Situation Calculus Theories Hofmann, Till Schupp, Stefan Lakemeyer, Gerhard Situation Calculus Golog timed automata clocks dense time reachability decidability region abstraction program realization 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 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 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Till Hofmann and Stefan Schupp and Gerhard Lakemeyer 2026 Is Part Of OASIcs, Volume 146, 33rd International Symposium on Temporal Representation and Reasoning (TIME 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/OASIcs.TIME.2026.11 urn:nbn:de:0030-drops-277073 https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TIME.2026.11 eng https://creativecommons.org/licenses/by/4.0/legalcode