In multiagent systems, the knowledge available to individual agents is subject to perpetual change: first, the truth of propositions may vary from one state of an agent to the next; second, the propositions that an agent is aware of may change; and third, an agent’s awareness of other agents may change. It is a challenging task to formally model such worlds of varying knowledge and awareness.

This paper addresses this problem with the dynamic logic of individual local awareness (DLILA), which extends modal logic with the concept of “awareness” of agents and propositions, and with the logic operators “becoming aware of” and “forgetting,” which modify the awareness of an agent. A bisimulation relation relates two models if they cannot be distinguished according to the current awareness; this relation is lifted into the logical language by corresponding quantifiers. Thus, not only the standard notions of implicit knowledge (accessible to an agent) and explicit knowledge (of which the agent is also aware), but also a novel notion of speculative knowledge (of which the agent is becoming aware of) can be defined. The authors then introduce special variants of DLILA, investigate an alternative version of “becoming aware of,” and elaborate further how to combine change of knowledge with change of awareness.

The paper gives many motivating examples to illustrate the abstract notions; it is thus also suitable for nonspecialists. However, algorithmic aspects that would be important for implementations of the logic are not addressed, which leaves room for further work.