In this paper, we study two problems: determining action model equivalence and minimizing the event space of an action model under certain structural relationships. The Kripke model equivalence is perfectly caught by the structural relationship called bisimulation. In this paper, we propose the generalized action emulation perfectly catching the action model equivalence. Previous structural relationships sufficient for the action model equivalence, i.e. the bisimulation, the propositional action emulation, the action emulation, and the action emulation of canonical action models, can be described by various restricted versions of the generalized action emulation. We summarize four critical properties of the atom set over preconditions, and prove that any formula set satisfying these properties can be used to restrict the generalized action emulation to determine the action model equivalence by an iteration algorithm. We also construct a new formula set with these four properties, which is generally more efficient than the atom set. The technique of the partition refinement has been used to minimize the world space of a Kripke model under the bisimulation. Applying the partition refinement to action models allows one to minimize their event spaces under the bisimulation. The propositional action emulation is weaker than bismulation but still sufficient for the action model equivalence. We prove that it is PSPACE-complete to minimize the event space of an action model under the propositional action emulation, and provide a PSPACE algorithm for it. Finally, we prove that minimize the event space under the action model equivalence is PSPACE-hard, and propose a computable method based on the canonical formulas of modal logics to solve this problem.
翻译:本文研究了两个问题:判定动作模型等价性,以及在特定结构关系下最小化动作模型的事件空间。Kripke模型等价性可由称为互模拟的结构关系完美刻画。本文提出了广义动作模拟,该关系能完美刻画动作模型等价性。先前足以判定动作模型等价性的结构关系(即互模拟、命题动作模拟、动作模拟以及典范动作模型的动作模拟)均可由广义动作模拟的各类受限版本描述。我们总结出前提条件集上原子命题集的四个关键性质,并证明任何满足这些性质的公式集均可通过迭代算法,利用对广义动作模拟的限制来判定动作模型等价性。我们还构造了一个具有这四个性质的新公式集,其效率通常优于原子命题集。划分精化技术已被用于在互模拟关系下最小化Kripke模型的世界空间。将该技术应用于动作模型,可在互模拟关系下最小化其事件空间。命题动作模拟弱于互模拟,但仍足以判定动作模型等价性。我们证明在命题动作模拟关系下最小化动作模型事件空间是PSPACE完全的,并给出了一个PSPACE算法。最后,我们证明在动作模型等价关系下最小化事件空间是PSPACE困难的,并提出了一种基于模态逻辑典范公式的可计算方法来解决该问题。