Changing agents and ascribing beliefs in dynamic epistemic logic
This work addresses a foundational issue in formal logic for AI and multi-agent systems by enabling more flexible modeling of agent interactions, though it appears incremental as it builds on existing action frame frameworks.
The paper tackles the problem of modeling dynamic changes in the set of agents and their beliefs in dynamic epistemic logic by introducing agent-update frames, which extend action frames to add or remove agents selectively, and applies this to an AI story modeling problem, showing that the resulting logics have sound and complete proof systems with decision procedures of expected complexity, including polynomial space algorithms for a sublanguage.
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.