Seminar session on Epistemic Protocols on Monday December 7th

In this talk, we report the ongoing work on dynamic epistemic logics with so-called ”future-shaping modalities” which constrain the possible actions in the future. The introduction of the new modalities is motivated by the analysis of epistemic protocols, where the meta knowledge of the protocol itself is crucial. We will demonstrate the use of such dynamic modalities with various of potential applications in, e.g., semantics of (pseudo) imperatives, dynamics of games, and information flow analysis.

We present a logic to describe communication channels and secret messages. Additionally, our logic can reason about communication protocols. We combine a Dynamic Epistemic Logic (DEL) perspective with ideas from Interpreted Systems (IS). Our framework models the communication channels underlying the information flow as well as the information flow itself. Our DEL-style actions allow us to model various communication actions such as message passing and group announcements. In particular we define an external informing action, which essentially announces the protocol the agents are supposed to follow, thus making it common knowledge that the future behaviour of the agents is constrained. Our framework is very flexible in modeling a variety of scenarios with different assumptions about the observational power of the agents. We propose a generic method of epistemic modeling where the initial model is simply the real world, and other worlds are generated on-the-fly. We show how our framework applies to some nice examples.

In my recent and on-going joint work with A. Baltag, we use the formalism of Dynamic-Epistemic logic to model and reason about the non-local informational dynamics in compound quantum systems. I will show how this combined logical formalism can express important features of quantum measurements and unitary evolutions of multi-partite quantum states, and I will give logical characterizations of various forms of entanglement (e.g. the Bell states, the GHZ states etc). As applications, I will use our logic to give a formal correctness proof for at least one of the following quantum protocols (Teleportation, Quantum Secret Sharing protocol, Superdense Coding, Quantum Key Distribution etc.). In the remainder of the talk I will sketch how this formalism can be extended to model how classical agents record the results of their quantum observations and perform actions. The final goal is to model all aspects of the classical-quantum interaction present in the mentioned quantum protocols.