This paper demonstrates the undecidability of a number of logics with quantification over public announcements: arbitrary public announcement logic (APAL), group announcement logic (GAL), and coalition announcement logic (CAL). In APAL we consider the informative consequences of any announcement, in GAL we consider the informative consequences of a group of agents (this group may be a proper subset of the set of all agents) all of which are simultaneously (and publicly) making known announcements. So this is more restrictive than APAL. Finally, CAL is as GAL except that we now quantify over anything the agents not in that group may announce simultaneously as well. The logic CAL therefore has some features of game logic and of ATL. We show that when there are multiple agents in the language, the satisfiability problem is undecidable for APAL, GAL, and CAL. In the single agent case, the satisfiability problem is decidable for all three logics. This paper corrects an error to the submitted version of Undecidability of Quantified Announcements, identified by Yuta Assami . The nature of the error was in the definition of the formula cga (X) (see Subsection 5.2) which is corrected in this version.
翻译:本文证明了若干具有量化公共宣告的逻辑的不可判定性:任意公共宣告逻辑(APAL)、群体宣告逻辑(GAL)以及联盟宣告逻辑(CAL)。在APAL中,我们考虑任意宣告的信息性后果;在GAL中,我们考虑一组智能体(该组可以是所有智能体集合的真子集)同时(且公开地)进行宣告所导致的信息性后果,因此这比APAL更具限制性。最后,CAL与GAL类似,区别在于我们现在同时量化了不在该组内的智能体可能作出的任何宣告。因此,CAL具有博弈逻辑和ATL的某些特征。我们证明,当语言中存在多个智能体时,APAL、GAL和CAL的可满足性问题都是不可判定的。在单智能体情况下,这三种逻辑的可满足性问题都是可判定的。本文修正了已提交版本《量化宣告的不可判定性》中的一个错误,该错误由Yuta Assami指出。错误的本质在于公式cga(X)的定义(见第5.2小节),本版本已对此进行了更正。