A complete proof system for a dynamic epistemic logic based upon finite $\pi$-calculus processes

The pi-calculus process algebra describes the interaction of concurrent and communicating processes. In this paper we present the syntax and semantics of a dynamic epistemic logic for multi-agent systems, where the epistemic actions are finite processes in the pi-calculus. We then extend the language to include actions from a specified set of action structures. We define a proof system for the extended language, and prove the completeness of the proof system. Thus any valid formula in the original language without action structures can be proved in the proof system for the extended language.