Positive Announcements
- PDF / 850,299 Bytes
- 43 Pages / 453.543 x 680.315 pts Page_size
- 10 Downloads / 149 Views
Positive Announcements
Abstract. Arbitrary public announcement logic (APAL) reasons about how the knowledge of a set of agents changes after true public announcements and after arbitrary announcements of true epistemic formulas. We consider a variant of arbitrary public announcement logic called positive arbitrary public announcement logic (APAL+ ), which restricts arbitrary public announcements to announcement of positive formulas. Positive formulas prohibit statements about the ignorance of agents. The positive formulas correspond to the universal fragment in first-order logic. As two successive announcements of positive formulas need not correspond to the announcement of a positive formula, APAL+ is rather different from APAL. We show that APAL+ is more expressive than public announcement logic PAL, and that APAL+ is incomparable with APAL. We also provide a sound and complete infinitary axiomatisation. Keywords: Dynamic epistemic logic, Multi-agent systems, Universal formulas.
1.
Introduction and Overview
Public announcement logic (PAL) [20,25] extends epistemic logic with operators for reasoning about the effects of specific public announcements. The formula [ψ]ϕ means that “ϕ is true after the truthful announcement of ψ”. This means that, when interpreted in an epistemic model with designated state, after submodel restriction to the states where ψ is true (this includes the designated state, and ‘truthful’ here means true), ϕ is true in that restriction. Arbitrary public announcement logic (APAL) [5] augments this with operators for quantifying over public announcements. The formula ϕ means that “ϕ is true after the truthful announcement of any formula that does not contain ”. Quantifying over the communication of information as in APAL has applications to epistemic protocol synthesis, where we wish to achieve epistemic goals by communicating information to agents, but where we do not know of a specific protocol that will achieve the goal, and where we may not even know if such a protocol exists. In principle, synthesis problems can be solved
Presented by Yde Venema; Received March 5, 2018
Studia Logica https://doi.org/10.1007/s11225-020-09922-1
c Springer Nature B.V. 2020
H. van Ditmarsch et al.
by specifying them as formulas in the logic, and applying model-checking or satisfiability procedures. However in the case of APAL, while there is a PSPACE-complete model-checking procedure [1], the satisfiability problem is undecidable in the presence of multiple agents [18]. We consider a variant of APAL called positive arbitrary public announcement logic (APAL+ ), we obtain various semantic results relating refinements to positive formulas, we give various rather surprising expressivity results, and we give a non-surprising axiomatization. In APAL the arbitrary public announcements quantify over quantifier-free formulas, that are equivalent to epistemic formulas (basic modal logic). Whereas in APAL+ the arbitrary public announcements quantify over quantifier-free positive formulas: + ϕ means that “ϕ is true aft
Data Loading...
