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.
翻译:公共观察逻辑(POL)是对代理人期望和代理人观察进行理性的动态缩略语逻辑的变体。代理人对手头的情况有一定的期望,这种期望是由有关议定书促成的,他们消除了他们的期望与其观察结果不符的可能世界。在这项工作中,我们调查了POL示范检查问题的计算复杂性,并证明了PSPACE的完整性。我们还研究了POL的各种合成碎片。我们举例说明了POL示范检查在核查互动系统不同特点和特点方面对系统不同期望和(匹配)观察的可适用性。最后,我们讨论了模式检查算法的执行情况。