The use of Dynamic Epistemic Logic (DEL) in multi-agent planning has led to a widely adopted action formalism that can handle nondeterminism, partial observability and arbitrary knowledge nesting. As such expressive power comes at the cost of undecidability, several decidable fragments have been isolated, mainly based on syntactic restrictions of the action formalism. In this paper, we pursue a novel semantic approach to achieve decidability. Namely, rather than imposing syntactical constraints, the semantic approach focuses on the axioms of the logic for epistemic planning. Specifically, we augment the logic of knowledge S5$_n$ and with an interaction axiom called (knowledge) commutativity, which controls the ability of agents to unboundedly reason on the knowledge of other agents. We then provide a threefold contribution. First, we show that the resulting epistemic planning problem is decidable. In doing so, we prove that our framework admits a finitary non-fixpoint characterization of common knowledge, which is of independent interest. Second, we study different generalizations of the commutativity axiom, with the goal of obtaining decidability for more expressive fragments of DEL. Finally, we show that two well-known epistemic planning systems based on action templates, when interpreted under the setting of knowledge, conform to the commutativity axiom, hence proving their decidability.

翻译：动态认知逻辑（DEL）在多智能体规划中的应用，催生出一种广泛采用的行动形式化框架，该框架能够处理非确定性、部分可观测性及任意知识嵌套。然而，这种表达能力以不可判定性为代价，因此已有若干可判定子片段被分离出来，主要基于行动形式化框架的句法限制。本文探索了一种新颖的语义方法来实现可判定性。具体而言，我们并未施加句法约束，而是关注认知规划逻辑的公理。我们通过增加一个被称为（知识）交换性的交互公理来扩展知识逻辑S5$_n$，该公理限制了智能体对其他智能体知识的无界推理能力。随后，我们做出了三方面贡献。首先，我们证明了由此产生的认知规划问题是可判定的，在此过程中我们证明了该框架允许对共同知识进行有限非不动点刻画——这一结果本身具有独立意义。其次，我们研究了交换性公理的不同推广形式，旨在为更富表达力的DEL子片段获得可判定性。最后，我们展示了两个基于行动模板的著名认知规划系统，在知识设定下进行解释时符合交换性公理，从而证明了它们的可判定性。