Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Decidable Reasoning About Time in Finite-Domain Situation Calculus Theories

Till Hofmann, Stefan Schupp, Gerhard Lakemeyer

TL;DR

The paper tackles the undecidability of time-aware reachability in the Situation Calculus by showing that attaching real-valued time via $time(a)$ leads to undecidable reachability even with finite domains. It introduces clocked BATs, where clocks are real-valued fluents with restricted successor-state axioms and comparisons restricted to natural numbers, and augments the theory with a wait action to advance time. By combining regression with regionalization, the authors obtain a finite time-abstract transition system and prove decidability of reachability for clocked BATs over finite objects, and extend the approach to the realizability of Golog programs. This clock-based framework bridges SC with timed automata theory, enabling decidable verification of time-sensitive cyber-physical reasoning and offering a foundation for future work on bounded action theories and two-variable SC fragments. The results provide both theoretical and practical pathways for verifying time-aware action theories and Golog programs within finite domains.

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 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.

Decidable Reasoning About Time in Finite-Domain Situation Calculus Theories

TL;DR

The paper tackles the undecidability of time-aware reachability in the Situation Calculus by showing that attaching real-valued time via leads to undecidable reachability even with finite domains. It introduces clocked BATs, where clocks are real-valued fluents with restricted successor-state axioms and comparisons restricted to natural numbers, and augments the theory with a wait action to advance time. By combining regression with regionalization, the authors obtain a finite time-abstract transition system and prove decidability of reachability for clocked BATs over finite objects, and extend the approach to the realizability of Golog programs. This clock-based framework bridges SC with timed automata theory, enabling decidable verification of time-sensitive cyber-physical reasoning and offering a foundation for future work on bounded action theories and two-variable SC fragments. The results provide both theoretical and practical pathways for verifying time-aware action theories and Golog programs within finite domains.

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 fluent 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.
Paper Structure (20 sections, 3 theorems, 22 equations, 1 figure, 3 algorithms)

This paper contains 20 sections, 3 theorems, 22 equations, 1 figure, 3 algorithms.

Table of Contents

  1. Introduction
  2. Related Work
  3. The Situation Calculus
  4. Basic Action Theories
  5. Regression
  6. Reachability
  7. Clocks in the Situation Calculus
  8. Regression
  9. Regionalization
  10. Decidability
  11. Realizing Golog Programs
  12. Golog Transition Semantics
  13. Program Realization
  14. Conclusion
  15. Appendix
  16. ...and 5 more sections

Key Result

Proposition 1

Let $\nu\xspace_1$ and $\nu\xspace_2$ be two clock valuations over a set of clocks $\mathcal{C}$ such that $\nu\xspace_1 \cong_\mathcal{K}\xspace\xspace \nu\xspace_2$. Then for all $\tau \in \mathbb{R}_{\geq 0}\xspace$ there exists a $\tau' \in \mathbb{R}_{\geq 0}\xspace$ such that $\nu\xspace_1 + \

Figures (1)

  • Figure 1: Regions for a system with two clocks $c_1, c_2$ and max. constant of $\mathcal{K}\xspace = 2$, adapted from alur_timed_1999. Highlighted are examples for a point (red) satisfying $c_1 = 1 \wedge c_2 = 1$, a line segment (orange) satisfying $c_1 \in (1, 2) \wedge c_2 = 2$, and an open region (blue) satisfying $c_1 \in (1, 2) \wedge c_2 \in (0, 1) \wedge \mathop{\mathrm{fract}}\limits(c_2) \leq \mathop{\mathrm{fract}}\limits(c_1)$.

Theorems & Definitions (26)

  • Definition 1
  • proof : Proof Idea
  • proof : Proof Idea
  • proof : Proof Idea
  • Definition 2
  • Definition 3
  • Example 1
  • Definition 4
  • Definition 5
  • Definition 6: Time-abstract Bisimulation
  • ...and 16 more