DROPS

Document

DOI: 10.4230/OASIcs.TIME.2026.11

Decidable Reasoning About Time in Finite-Domain Situation Calculus Theories

Authors: Till Hofmann, Stefan Schupp, and Gerhard Lakemeyer

Published in: OASIcs, Volume 146, 33rd International Symposium on Temporal Representation and Reasoning (TIME 2026)

Abstract

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.

Cite as

Till Hofmann, Stefan Schupp, and Gerhard Lakemeyer. Decidable Reasoning About Time in Finite-Domain Situation Calculus Theories. In 33rd International Symposium on Temporal Representation and Reasoning (TIME 2026). Open Access Series in Informatics (OASIcs), Volume 146, pp. 11:1-11:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{hofmann_et_al:OASIcs.TIME.2026.11,
  author =	{Hofmann, Till and Schupp, Stefan and Lakemeyer, Gerhard},
  title =	{{Decidable Reasoning About Time in Finite-Domain Situation Calculus Theories}},
  booktitle =	{33rd International Symposium on Temporal Representation and Reasoning (TIME 2026)},
  pages =	{11:1--11:22},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-448-2},
  ISSN =	{2190-6807},
  year =	{2026},
  volume =	{146},
  editor =	{Orlandini, AndreA and Pinchinat, Sophie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TIME.2026.11},
  URN =		{urn:nbn:de:0030-drops-277073},
  doi =		{10.4230/OASIcs.TIME.2026.11},
  annote =	{Keywords: Situation Calculus, Golog, timed automata, clocks, dense time, reachability, decidability, region abstraction, program realization}
}

Search Results

Documents authored by Schupp, Stefan

Decidable Reasoning About Time in Finite-Domain Situation Calculus Theories

Abstract

Cite as

Thanks for your feedback!

Could not send message