In dynamic epistemic logic (Van Ditmarsch, Van Der Hoek, & Kooi, 2008) it is customary to use an action frame (Baltag & Moss, 2004; Baltag, Moss, & Solecki, 1998) to describe different views of a single action. In this article, action frames are extended to add or remove agents, we call these agent-update frames. This can be done selectively so that only some specified agents get information of the update, which can be used to model several interesting examples such as private update and deception, studied earlier by Baltag and Moss (2004); Sakama (2015); Van Ditmarsch, Van Eijck, Sietsma, and Wang (2012). The product update of a Kripke model by an action frame is an abbreviated way of describing the transformed Kripke model which is the result of performing the action. This is substantially extended to a sum-product update of a Kripke model by an agent-update frame in the new setting. These ideas are applied to an AI problem of modelling a story. We show that dynamic epistemic logics, with update modalities now based on agent-update frames, continue to have sound and complete proof systems. Decision procedures for model checking and satisfiability have expected complexity. For a sublanguage, there are polynomial space algorithms.
翻译:在动态认知逻辑(Van Ditmarsch、Van Der Hoek和Kooi,2008)中,惯常使用动作框架(Baltag和Moss,2004;Baltag、Moss和Solecki,1998)来描述同一动作的不同视角。本文将动作框架扩展为可添加或移除主体,称之为主体更新框架。该扩展具有选择性,仅使指定的部分主体获取更新信息,可用于建模若干典型案例,如私有更新与欺骗(此前由Baltag和Moss(2004)、Sakama(2015)、Van Ditmarsch、Van Eijck、Sietsma与Wang(2012)研究过)。克里普克模型与动作框架的乘积更新是描述执行动作后所得变换模型的简化方式。在新框架中,该概念被实质性扩展为克里普克模型与主体更新框架的和积更新。这些思想被应用于人工智能中的故事建模问题。研究表明:基于主体更新框架的更新模态的动态认知逻辑仍具有可靠且完备的证明系统;模型检测与可满足性的判定程序具有预期的复杂度;针对某子语言,存在多项式空间算法。