Decidable Reasoning About Time in Finite-Domain Situation Calculus Theories
CoRR(2024)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要