Document Open Access Logo

Decidable Reasoning About Time in Finite-Domain Situation Calculus Theories

Authors Till Hofmann , Stefan Schupp , Gerhard Lakemeyer

PDF

File

Thumbnail PDF
PDF
OASIcs.TIME.2026.11.pdf
  • Filesize: 0.8 MB
  • 22 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Situation Calculus
  • Golog
  • timed automata
  • clocks
  • dense time
  • reachability
  • decidability
  • region abstraction
  • program realization

Metrics

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 Get BibTex

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) https://doi.org/10.4230/OASIcs.TIME.2026.11

Author Details

Till Hofmann
  • RWTH Aachen University, Germany
  • University of Oxford, UK
Stefan Schupp
  • TU Wien, Austria
Gerhard Lakemeyer
  • RWTH Aachen University, Germany

Funding

This research was supported by the EU ICT-48 2020 project TAILOR (No 952215). Travel funding to present this paper was provided by the EU project euroFMX (No 101299128).

References

  1. Rajeev Alur. Timed automata. In Nicolas Halbwachs and Doron Peled, editors, Computer Aided Verification (CAV), Lecture Notes in Computer Science, pages 8-22, Berlin, Heidelberg, 1999. Springer. URL: https://doi.org/10.1007/3-540-48683-6_3.
  2. Rajeev Alur, Costas Courcoubetis, Thomas A. Henzinger, and Pei-Hsin Ho. Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In Robert L. Grossman, Anil Nerode, Anders P. Ravn, and Hans Rischel, editors, Hybrid Systems, Lecture Notes in Computer Science, pages 209-229, Berlin, Heidelberg, 1993. Springer. URL: https://doi.org/10.1007/3-540-57318-6_30.
  3. Rajeev Alur and David L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183-235, April 1994. URL: https://doi.org/10.1016/0304-3975(94)90010-8.
  4. Rajeev Alur and P. Madhusudan. Decision Problems for Timed Automata: A Survey. In Marco Bernardo and Flavio Corradini, editors, Formal Methods for the Design of Real-Time Systems, Lecture Notes in Computer Science, pages 1-24. Springer, Berlin, Heidelberg, 2004. URL: https://doi.org/10.1007/978-3-540-30080-9_1.
  5. Vitaliy Batusov, Giuseppe De Giacomo, and Mikhail Soutchanski. Hybrid temporal situation calculus. In Marie-Jean Meurs and Frank Rudzicz, editors, Advances in Artificial Intelligence, Lecture Notes in Computer Science, pages 173-185, Cham, 2019. Springer. URL: https://doi.org/10.1007/978-3-030-18305-9_14.
  6. Patricia Bouyer, Catherine Dufourd, Emmanuel Fleury, and Antoine Petit. Updatable timed automata. Theoretical Computer Science, 321(2):291-345, August 2004. URL: https://doi.org/10.1016/j.tcs.2004.04.003.
  7. Béatrice Bérard and Catherine Dufourd. Timed automata and additive clock constraints. Information Processing Letters, 75(1):1-7, July 2000. URL: https://doi.org/10.1016/S0020-0190(00)00075-2.
  8. Jens Claßen and Gerhard Lakemeyer. A logic for non-terminating Golog programs. In Proceedings of the 11th International Conference on Principles of Knowledge Representation and Reasoning (KR), pages 589-599. AAAI Press, 2008. URL: https://aaai.org/papers/KR08-058-a-logic-for-non-terminating-golog-programs/.
  9. Jens Claßen, Martin Liebenberg, Gerhard Lakemeyer, and Benjamin Zarrieß. Exploring the boundaries of decidable verification of non-terminating Golog programs. In Proceedings of the 28th AAAI Conference on Artificial Intelligence (AAAI), pages 1012-1019. AAAI Press, 2014. URL: https://doi.org/10.1609/AAAI.V28I1.8875.
  10. Giuseppe De Giacomo, Yves Lespérance, Matteo Mancanelli, and Gianmarco Parretti. Reactive synthesis for Golog specifications in the propositional situation calculus. In Proceedings of the 22nd International Conference on Principles of Knowledge Representation and Reasoning (KR), 2026. Google Scholar
  11. Giuseppe De Giacomo, Yves Lespérance, and Hector J. Levesque. ConGolog, a concurrent programming language based on the situation calculus. Artificial Intelligence, 121:109-169, 2000. URL: https://doi.org/10.1016/S0004-3702(00)00031-X.
  12. Giuseppe De Giacomo, Yves Lespérance, Hector J. Levesque, and Sebastian Sardina. IndiGolog: A high-level programming language for embedded reasoning agents. In Multi-Agent Programming. Springer, 2009. URL: https://doi.org/10.1007/978-0-387-89299-3.
  13. Giuseppe De Giacomo, Yves Lespérance, and Fabio Patrizi. Bounded situation calculus action theories and decidable verification. In Thirteenth International Conference on the Principles of Knowledge Representation and Reasoning, May 2012. Google Scholar
  14. Giuseppe De Giacomo, Yves Lespérance, and Fabio Patrizi. Bounded situation calculus action theories. Artificial Intelligence, 237:172-203, August 2016. URL: https://doi.org/10.1016/j.artint.2016.04.006.
  15. Alberto Finzi and Fiora Pirri. Representing flexible temporal behaviors in the situation calculus. In Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI), pages 436-441, 2005. URL: http://ijcai.org/Proceedings/05/Papers/1562.pdf.
  16. Michael Gelfond, Vladimir Lifschitz, and Arkady Rabinov. What Are the Limitations of the Situation Calculus? In Automated Reasoning: Essays in Honor of Woody Bledsoe, pages 167-179. Springer Netherlands, Dordrecht, 1991. URL: https://doi.org/10.1007/978-94-011-3488-0_8.
  17. Yilan Gu and Mikhail Soutchanski. A description logic based situation calculus. Annals of Mathematics and Artificial Intelligence, 58(1):3-83, February 2010. URL: https://doi.org/10.1007/s10472-010-9176-z.
  18. Till Hofmann and Jens Claßen. LTLf synthesis on first-order agent programs in nondeterministic environments. In Proceedings of the 39th AAAI Conference on Artificial Intelligence (AAAI), volume 39, pages 14976-14986, 2025. URL: https://doi.org/10.1609/aaai.v39i14.33642.
  19. Till Hofmann, Stefan Schupp, and Gerhard Lakemeyer. Decidable reasoning about time in finite-domain situation calculus theories, 2026. URL: https://doi.org/10.48550/arXiv.2402.03164.
  20. Robert Kowalski and Marek Sergot. A logic-based calculus of events. New Generation Computing, 4(1):67-95, March 1986. URL: https://doi.org/10.1007/BF03037383.
  21. John McCarthy. Situations, actions, and causal laws. Technical Report, Stanford University, 1963. Google Scholar
  22. Rob Miller. A case study in reasoning about actions and continuous change. In Proceedings of the 12th European Conference on Artificial Intelligence (ECAI), page 21, 1996. Google Scholar
  23. Marvin Minsky. Computation: finite and infinite machines. Prentice-Hall, Englewood Cliffs, N.J, 1967. Google Scholar
  24. Erik T. Mueller. Event Calculus. In Frank van Harmelen, Vladimir Lifschitz, and Bruce Porter, editors, Foundations of Artificial Intelligence, volume 3 of Handbook of Knowledge Representation, pages 671-708. Elsevier, January 2008. URL: https://doi.org/10.1016/S1574-6526(07)03017-9.
  25. Joël Ouaknine and James Worrell. On the decidability and complexity of Metric Temporal Logic over finite words. Logical Methods in Computer Science, 3(1):1-27, February 2007. Publisher: Episciences.org. URL: https://doi.org/10.2168/LMCS-3(1:8)2007.
  26. Javier Pinto and Raymond Reiter. Reasoning about time in the situation calculus. Annals of Mathematics and Artificial Intelligence, 14(2-4):251-268, 1995. URL: https://doi.org/10.1007/BF01530822.
  27. Fiora Pirri and Ray Reiter. Some contributions to the metatheory of the situation calculus. Journal of the ACM, 46(3):325-361, 1999. URL: https://doi.org/10.1145/316542.316545.
  28. Raymond Reiter. Natural Actions, Concurrency and Continuous Time in the Situation Calculus. In Proceedings of the 5th International Conference on Principles of Knowledge Representation and Reasoning (KR), pages 2-13, San Francisco, CA, 1996. Morgan Kaufmann Publishers Inc. Google Scholar
  29. Raymond Reiter. Knowledge in action: logical foundations for specifying and implementing dynamical systems. MIT Press, 2001. Google Scholar
  30. Kristof Van Belleghem, Marc Denecker, and Danny De Schreye. On the relation between situation calculus and event calculus. The Journal of Logic Programming, 31(1):3-37, April 1997. URL: https://doi.org/10.1016/S0743-1066(96)00123-9.
  31. Benjamin Zarrieß and Jens Claßen. Decidable verification of Golog programs over non-local effect actions. In Dale Schuurmans and Michael Wellman, editors, Proceedings of the thirtieth AAAI conference on artificial intelligence (AAAI 2016), pages 1109-1115. AAAI Press, 2016. URL: https://doi.org/10.1609/AAAI.V30I1.10109.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact