arXiv：cs.AI· Till Hofmann, Stefan Schupp, Gerhard Lakemeyer·· 19 小时前
有限域情境演算理论中时间推理的可判定性研究
Decidable Reasoning About Time in Finite-Domain Situation Calculus Theories
AI 导读
针对情境演算中常用的为每个动作附加实值 time(a) 函数来表示时间的方法，论文证明即使域中只有有限多个对象，判断是否存在满足给定公式的可达情境也是不可判定的。作者借鉴时间自动机理论，引入时钟作为带受限后继状态公理和比较算子的实值 fluent，证明有限域基本动作理论的可达性问题可判定，并给出确定 Golog 程序成功执行动作序列的可判定过程。
正文
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 $\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 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.
| Subjects: | Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO) |
| Cite as: | arXiv:2402.03164 [cs.AI] |
| (or arXiv:2402.03164v3 [cs.AI] for this version) | |
| https://doi.org/10.48550/arXiv.2402.03164 arXiv-issued DOI via DataCite |
|
| Related DOI: | https://doi.org/10.4230/OASIcs.TIME.2026.11
DOI(s) linking to related resources |
Submission history
From: Till Hofmann [view email]
[v1]
Mon, 5 Feb 2024 16:32:12 UTC (78 KB)
[v2]
Mon, 21 Sep 2026 20:54:55 UTC (583 KB)
[v3]
Tue, 13 Oct 2026 14:15:35 UTC (569 KB)
来源：arXiv：cs.AI · arxiv.org