Logics for Epistemic Actions: Completeness, Decidability, Expressivity

We build and study dynamic versions of epistemic logic. We study languages parameterized by an action signature that allows one to express epistemic actions such as (truthful) public announcements, completely private announcements to groups of agents, and more. The language L(Σ) is modeled on dynamic logic. Its sentence-building operations include modalities for the execution of programs, and for knowledge and common knowledge. Its program-building operations include action execution, composition, repetition, and choice. We consider two fragments of L(Σ). In L1(Σ), we drop action repetition; in L0(Σ), we also drop common knowledge. We present the syntax and semantics of these languages and sound proof systems for the validities in them. We prove the strong completeness of a logical system for L0(Σ) and the weak completeness of one for L1(Σ). We show the finite model property and, hence, decidability of L1(Σ). We translate L1(Σ) into PDL, obtaining a second proof of decidability. We prove results on expressive power, comparing L1(Σ) with modal logic together with transitive closure operators. We prove that a logical language with operators for private announcements is more expressive than one for public announcements.