Arbitrary Public Announcement Logic with Mental Programs
Tristan Charrier, François Schwarzentruber · 2015
rennes.fr We propose a variant of arbitrary public announcement logic which is decidable. In this variant, knowledge accessibility relations are defined by programs. Technically, programs are written in dynamic logic with propositional assignments. We prove that both the model checking problem and the satisfi-ability problem are decidable and AEXPpol-complete where AEXPpol is the class of decision problems decided by alter-nating Turing machines running in exponential time where the number of alternations is polynomial. Whereas arbitrary public announcement logic is undecidable, our framework is decidable and we provide a proof-of-concept to show its ex-pressiveness: we use our framework to reason about epis-temic properties and arbitrary announcements when agents are cameras located in the plane.