论文标题
关于验证智能代理的期望和观察
On verifying expectations and observations of intelligent agents
论文作者
论文摘要
公众观察逻辑（POL）是动态认知逻辑的一种变体，以理论代理人期望和代理观察。代理人对当前情况有一定的期望，这些期望是由相关协议驱动的，并且消除了他们的期望与他们的观察结果不符的可能世界。在这项工作中，我们研究了POL的模型检查问题的计算复杂性，并证明其PSPACE完整性。我们还研究了POL的各种句法片段。我们体现了POL模型检查在验证系统的不同期望和（匹配）观察结果方面的不同特征和特征中的适用性。最后，我们提供了有关模型检查算法的实现的讨论。
Public observation logic (POL) is a variant of dynamic epistemic logic to reason about agent expectations and agent observations. Agents have certain expectations, regarding the situation at hand, that are actuated by the relevant protocols, and they eliminate possible worlds in which their expectations do not match with their observations. In this work, we investigate the computational complexity of the model checking problem for POL and prove its PSPACE-completeness. We also study various syntactic fragments of POL. We exemplify the applicability of POL model checking in verifying different characteristics and features of an interactive system with respect to the distinct expectations and (matching) observations of the system. Finally, we provide a discussion on the implementation of the model checking algorithms.
