Decidable Reasoning About Time in Finite-Domain Situation Calculus Theories

要約

時間の表現はサイバーフィジカルシステムにとって非常に重要であり、状況微積分において広範囲に研究されてきた。最もよく使われるアプローチは、実数値フルエント$mathit{time}(a)$を追加することによって時間を表現し、各アクションに時間点を付け、その結果、各状況に時間点を付ける。このアプローチでは、与えられた式を満たす到達可能な状況が存在するかどうかをチェックすることは、たとえ言説のドメインがオブジェクトの有限集合に制限されていたとしても、決定不可能であることを示す。我々は、制限された後継状態公理と比較演算子を持つ実数値フルエントとしてクロックを導入することで、時限オートマトン理論の確立された結果に基づく代替アプローチを提示する。それは固定された有理数との比較のみを可能にするものである。この制限により、有限領域基本作用素理論の到達可能性問題が決定可能であることを示すことができる。最後に、与えられたプログラムの実行に成功する作用列を決定するための決定可能な手続きを提示することにより、Gologプログラム実現に関する我々の結果を適用する。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, DeepL