The Dynamic Logic of Epistemic Programs

Abstract: Epistemic programs are programs for jointly updating every agent's state of knowledge (or 'belief') in a multi-agent system (i.e. programs for "interactive learning", or for inducing belief changes among the agents). They can be intuitively understood as computing the epistemic effect of exchanges of information ("communication").

I present examples of such programs, and give a general semantics for them, in terms of "epistemic program models". I introduce various natural operations with epistemic programs, and a dynamic logic to reason about them. I present a complete and decidable proof system for this logic, and discuss further extensions of this work. I sketch how the logic could be used (e.g. in cryptographic communication protocols) to prove the partial correctness of a given communication strategy with respect to given epistemic goals (and given epistemic preconditions).

This presentation is based on joint work with L. Moss and S. Solecki, as well as on my own extensions of this work.

Go back to the current seminar programme.