Decidable Reasoning About Time in Finite-Domain Situation Calculus Theories
CoRR(2024)
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 𝑡𝑖𝑚𝑒(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.
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.
MoreTranslated text
AI Read Science
Must-Reading Tree
Example
![](https://originalfileserver.aminer.cn/sys/aminer/pubs/mrt_preview.jpeg)
Generate MRT to find the research sequence of this paper
Chat Paper
Summary is being generated by the instructions you defined