Arbitrary arrow update logic

In this paper we introduce arbitrary arrow update logic (AAUL). The logic AAUL takes arrow update logic, a dynamic epistemic logic where the accessibility relations of agents are updated rather than the set of possible worlds, and adds a quantifier over such arrow updates. We investigate the relative expressivity of AAUL compared to other logics, most notably arbitrary public announcement logic (APAL). Additionally, we show that the model checking problem for AAUL is PSPACE-complete. Finally, we introduce a proof system for AAUL, and prove it to be sound and complete.

Authors

• Hans van Ditmarsch
• Wiebe van der Hoek
• Barteld Kooi
• Louwe B. Kuijer

Keywords

• Modal logic
• Knowledge representation
• Arrow update logic
• Dynamic epistemic logic
• Arbitrary arrow update logic
• Arbitrary announcement logic