基于群体的公告逻辑PPAL的定义与性质

可在www.sciencedirect.com在线获取理论计算机科学电子笔记348（2020）105-123www.elsevier.com/locate/entcsPopulational Announcement Logic（PPAL）Vitor Machado马查多1，2 Mario Benevides马里奥·贝内维德斯1，3里约热内卢联邦大学数学研究所巴西里约热内卢摘要Populational Announcement Logic（PPAL）是标准公共公告逻辑（PAL）的变体，具有模糊语义，其中我们拥有人口和群体而不是特定的代理。定义了语义和公告逻辑，并给出了一个例子。我们表现出类似PAL公理和他们的证明的有效性，也提供了一个证明的可判定性。我们简要地讨论了模型检查和比较框架与概率逻辑。我们的结论是，PPAL相对于PAL的主要优势是与先前定义的代理人一起工作的灵活性保留字：认知逻辑，模态逻辑，知识表示1介绍认知逻辑试图提供对知识表示模型进行推理的方法[18]。C. I. 刘易斯在1918年出版了《符号逻辑概论》一书后来在1951年，冯·赖特它被认为是关于模态逻辑的第一个重要工作进一步的发展是动态逻辑，它对动作及其结果进行推理[12]。动态认知逻辑（DEL）被认为是对改变代理人的知识和信念的行为进行推理。它对证明某件事是否是知识不感兴趣，而是从所说的知识中推断出某件事。第 一 个 动 态 认 知 逻 辑 是 由 [17] 和 [10] 独 立 提 出 的 ， 被 称 为 公 共 声 明 逻 辑（PAL），一种允许简单公共声明的1我们要感谢研究机构CNPq、CAPES和FAPERJ的支持。2电子邮件：vmachado@cos.ufrj.br3电子邮件地址：mario@cos.ufrj.brhttps://doi.org/10.1016/j.entcs.2020.02.0071571-0661/© 2020作者。出版社：Elsevier B.V.这是CC BY许可下的开放获取文章（http://creativecommons.org/licenses/by/4.0/）。106诉Machado，M.Benevides/理论计算机科学电子笔记348（2020）105改变其代理人知识状态的行为。后来[2，3]提出了动作模型逻辑方法，允许更复杂的推理。在文献[11]中，Häajek研究了模态逻辑S5的一个模糊变量 它介绍了这种变体的Kripke模型，并展示了演绎系统和完备性证明。然而，它并没有提供任何类型的模型更新（即公告）机制。一个相关的方法，也对代理群体的原因，虽然在一个非常不同的方式，被称为术语模态逻辑[8]，其发展动态术语模态逻辑[13]。这种逻辑以类似于Lambda演算和其他演算的方式进行变量绑定和替换。在术语模态逻辑中， 其他代理，允许复杂的代理命名。它包含公式，例如x（second year student（x）→ [x] knows calculus（x）），意思是“每一个二年级的学生x都知道微积分”;1.1动机和目标这项工作的目的是指定PAL的变化，其中的知识是跨人口和群体的人口，而不是离散的代理人，因为它通常是这样做。这背后的动机是提供一个框架，能够处理的应用程序，其中一个打算的原因，知识的进化在人口，而不是个别代理。它是专门为模型检查而设计的，因为它不需要事先指定代理（或在这种情况下的种群），相反，这些种群可以在执行过程中由语言的声明运算符定义。为了实现这一点，我们引入并定义了PAL的一个“模糊”变体，允许向其代理（称为“种群”和“组”）进行我们形式化的模型，语言和语义，并提供类似于PAL公理公理。然后，我们证明了逻辑是可判定的，并证明了模型检测的复杂性。我们给出了一个例子，其中给出了一个初始模型，并作出了一些公告，修改它，以说明其适用性的情况下，知识在人群中的进化公告。1.2路线图在第2节中，我们介绍了公共公告逻辑（PAL），这是这项工作的基础。在第三节中，我们介绍了人口公告逻辑（PPAL），解释了它的目的和相对于PAL的区别，并定义了它的语言，语义和模型。我们还提供了类似于PAL公理的公理，并证明了它们的有效性。在本节中，我们仍然证明了PPAL是可判定的，并演示了模型检查的复杂性，并简要介绍了实际的模型检查器实现。第4节提供了PPAL的两个基本示例，展示了该模型在公告后如何演变第五节A诉Machado，M.Benevides/理论计算机科学电子笔记348（2020）105107PPAL和概率逻辑之间的快速比较，概述它们之间的相似性和差异。第六部分是结论，最后的一些评论和未来的工作。2公告逻辑（PAL）在这里，我们将简要地提供公共声明逻辑的定义，这是多智能体认知逻辑的扩展，在计算机科学中已经研究过它是第一个实际的动态认知逻辑，由Plaza在[17]中开发。2.1语言与语义该语言在BNF表示法中如下：：= p| ¬ϕ|ϕ1∧ϕ2|Ka|[φ]其中p∈Φ，可数个命题符号的集合，a∈ A，有限个一组代理人。类似于命题逻辑，运算符和→公告[φ]的情态运算符具有预期的含义：“在公开宣布φ的效果是模型中的一个限制，只包含φ为真的状态定义2.1给定一个多智能体认知模型M=S，S，V，S，满足的概念M，S|定义如下：• M，s| = p i s∈V（p）• M，s|=<$φ iM，s| = φ• M，s| =φiM，s|=φ和M，s|=• M，s| = Kaφ i <$$>sJ∈S：s<$asJ<$M，sJ|= φ• M，s| =[φ] iM，s| =公司简介|φ，s|=其中M|φ是通过限制M仅具有状态而获得的新模型，其中φ保持不变。3Populational Announcement Logic（PPAL）在本节中，我们将介绍人口公告逻辑（PPAL）。 与PAL相比，它最显著的特点是， 而不是代理人。它的工作原理就像PAL的“模糊”版本，其中公告作用于部分人口，因此明确谈论私人或公共公告没有意义。应当指出，在向全体人民发布公告的有限情况下，人民保护党的行为与人民保护党发布公告的行为相似。这使我们具有更大的灵活性，因为我们可以预先定义系统的种群。此外，它允许以更自然的方式表达部分知识。108诉Machado，M.Benevides/理论计算机科学电子笔记348（2020）105G⎧⎪⎨0如果G=0，作为动机，考虑下面的例子：一位著名的政治家涉嫌洗钱和贿赂。选举即将到来，这位政治家希望再次当选，但如果人们知道对他的两项指控，他们就不太愿意投票给他。然而，并非所有人都知道这些指控。有了PPAL，我们可以模拟只有一定数量的人口看到的电视节目所做的公告，然后我们可以断言人口对政治家的整体认识。例如，公式[l] 0. 3KG（l b）（1）表示对0的一小部分进行的宣布。3，该政治家实际上犯有洗钱罪（l），以及随后的知识断言G是否知道该政治家是否腐败（犯有洗钱罪和贿赂罪）。我们将在第4节中回到这个例子。3.1人口和群体定义3.1总体是指个体的集合。 人口P的大小P∈R>0。它被定义为一个实数，因为公告将人口分为两个人口的一组，它们的大小将是人口大小的分数请注意，虽然人口代表许多个体，但实际的个体从未直接表达或引用，这与DEL不同。个体仅由人口的规模来代表。这样做的动机归结为这样一个事实，即我们最感兴趣的是代表和使用人口或人口的一部分的知识，因此没有目的在模拟实际的个人。接下来，我们将定义群体的概念定义3.2群G可以是空的、一个总体或一组不相交的群：G：= 1000|P | {G0, G1,..., Gn}（2）群G的大小定义为：G=P如果G=P，如果G={G0，G1， . ，Gn}。之所以对“组”和“总体”有两种定义，有了组，就可以在发布声明后保留对两个拆分诉Machado，M.Benevides/理论计算机科学电子笔记348（2020）105109GnGnG2G例如，如果对一个种群P发出了一个通知，然后它变成了一个群G={P1，P2}，这个群通过保留它的大小来表示原始种群，但是现在由两个不同的种群组成，一个收到了通知，另一个由于逻辑中的公告适用于人口或群体的一小部分，它们的工作方式类似于私人公告。因此，使用了多世界方法。每个群体都有自己的模型，代表其当前对世界的认识定义3.3总体P，MP=T，G，V的模型由一组状态T，一个赋值函数V：Φ→ 2T（它将Φ中的命题符号映射到T 的子集中），以及T上的一族二元关系表示d={P，G，1，G，2，...，其中Gi是P所知道的群。例如，表示群G的怀疑的关系将包含在集合G 中。请注意，我们将关系定义为一个集合，因为这些关系将在群模型定义中进行并运算，而且它们的顺序并不重要。定义3.4模型MG，对于群G ={G1，G2，...，Gn}定义为GiG1模型集MGi=T，，V，作为M=T，∪···∪你好，V。3.2语法和语义本节介绍PPAL的语法和语义。我们从定义语言开始，然后从语义上定义逻辑的每个运算符。定义3.5该语言在BNF表示法中如下：：：=p|¬ϕ|ϕ1∧ϕ2|ϕ1∨ϕ2|ϕ1→ϕ2|KG|BG|[2001]第2（3）条规则其中r∈U = [0，1]，G表示群，p∈ Φ.模态运算符具有以下预期含义：• K G和BG：• [101] r102：“在宣布r 101之后，r 102为真，以供个人采取行动”。后者描述了一个部分公告，定义了两个新的群体，其中只有一个群体收到了公告的信息。现在我们可以定义算子的语义了，我们从定义3.3中引入的赋值函数V开始。 为了实现这一点，我们定义一个评价函数e：p×（MG，s）→U如下：e（p，（MG，s））= 1，如果s∈V（p），否则为0（4）其中p∈Φ，MG是G的模型，s是状态，U是单位区间[0，1].110诉Machado，M.Benevides/理论计算机科学电子笔记348（2020）105下面，我们给出一些关于模糊函数的性质，这些模糊函数用于满意度的定义。在这一点上，我们选择不定义特定的模糊语义，而是为每个操作定义类可以选择满足以下性质的任何同样重要的是要注意，这项工作与模型检查有关，因此满意度的概念就足够了。由于这个原因，我们没有定义结果关系。3.3模糊否定一元运算NOT：U→U是模糊否定，如果：• return（0）;• return（1）;• x≤y→NOT（y）≤NOT（x）。例如，一个可能的求反函数是NOT（x）= 1−x。3.4模糊连接一个二元运算AND：U2→U是一个模糊合取，如果：• （x，y，y）=AND（y，x）;• y≤z→AND（x，y）≤AND（x，z）;• A ND（x，A ND（y，z））=A ND（A ND（x，y），·z）A;ND（x，1）=x.这些也精确地定义了t-范数函数类，它们被广泛用于模糊逻辑中，因为它们被认为是例如，可能的合取函数是AND（x，y）=min{x，y}。3.5模糊析取一个二元运算OR：U2→U是一个模糊析取，如果：• （x，y）=OR（y，x）;• OR（x，OR（y，z））=OR（OR（x，y），z）;• y≤z→OR（x，y）≤OR（x，z）;• OR（x，0）= x.这些也精确地定义了t-连续函数类，类似于t-范数类。例如，可能的析取函数是OR（x，y）=max{x，y}。3.6模糊蕴涵一个二元运算IMP：U2→U是一个模糊蕴涵，如果：• x≤y→IMP（x，z）≥IMP（y，z）;• y≥z→IMP（x，y）≥IMP（x，z）;• x > y→y≤IMP（x，y）≤x;• x≤y→IMP（x，y）= 1。诉Machado，M.Benevides/理论计算机科学电子笔记348（2020）105111例如，一个可能的蕴涵函数是IMP（x，y）= min{1，1 −x + y}，也称为L-ukasiewicz蕴涵。112诉Machado，M.Benevides/理论计算机科学电子笔记348（2020）105⎩⎨G1if∈sJ∈T|sGsJ→E如果G/=P，则G′B（M，（MS，s），GJ）∈GG′ B（M，（M S，s），Gj），K（M，S，s），G）=MS，s'（），3.7模糊知识断言三元运算K：F ×（MS，s）×G→U，其中F是PPAL的公式集合，如果：• 如果G=P，则n ∈sJ∈T|sGsJ[E• 如果G=P，则n ∈sJ∈T|sGsJ[E′（S）= 1→K（S，（MS，s），P）= 1];′（<$s）= 1→K（k，（MS，s），P）=0];• K（k，（MS，s），G）≤maxG′∈G{K（k，（MS，s），GJ）};• K（k，（MS，s），G）≥minG′∈G{K（k，（MS，s），GJ）}.例如，可能的知识断言函数是如果G=/P，则G′∈GG′K（G，（MS，s），GJ）000元，否则直觉上，它意味着一个群体的知识等于它所包含群体的加权平均知识，当群体是一个单一的群体时，它等于1，并且在通过连接到状态s的每个状态中都为真，否则等于0。 一个单一的人口知道的东西，只有当它是真实的，在每一个可以想象的世界，这个人口考虑。3.8模糊信念断言三元运算B：F ×（MS，s）×G→U，其中F是PPAL的公式集合，如果：• 如果G=P，则n ∈sJ∈T|sGsJ[E• 如果G=P，则n ∈sJ∈T|sGsJ[E′（S）= 1→B（S，（MS，s），P）>0];′（<$s）= 1→B（n，（MS，s），P）1];<• 如果G=P，则 ∈ 不|sK（S，（MS，s），P）];sJ[EMS，s′（π）= 1 → B（m，（MS，s），P）=• B（n，（MS，s），G）≤maxG′∈G{B（n，（MS，s），GJ）};• B（n，（MS，s），G）≥minG′∈G{B（n，（MS，s），GJ）}.例如，一个可能的群体信念断言函数是B（M，S，s），G）=s′∈Ns⎩GEMS，s′（ε）Ns如果G1=0，其中Ns=s′∈T|sGs′0否则。sJ是s通过关系G 的 邻 居。它在功能上类似于K，但允许区间[0， 1]中的任何数例如，如果在经由NRG连接到状态s的状态的一半中，则NRG值为1，并且MS，sMS，sMS，sMS，sG⎪诉Machado，M.Benevides/理论计算机科学电子笔记348（2020）105113Rr在另一半中为0，则B（M，S，S），P）= 0。5.与K类似，一个群的信念等于它所包含的群的加权平均信念有了这些函数，我们可以引入满意度定义如下：EMG，s（p）=e（p，（MG，s））EMG，s（<$）=NOT（EMG，s（<$））EMG，s（）=AND（EMG，s（），EMG，s（））EMG，s（）=OR（EMG，s（），EMG，s（））EMG，s（n→n）=IMP（EMG，s（n），EMG，s（n））EMG，s（KG'n）=K（n，（MG，s），G'）EMG，s（BG'）=B（，（MG，s），G'）EMG，s（[]）=IMP（EM，s（），EM，s（））RG其中，G1，G2，使得G={G1，G2}MG={MG1，MG2}MG1 = MG|MG2= MGG1=Gr G2=G（1−r）MG|=|MG ， s| = MG ， sJ|{\fn 黑 体 \fs19\bord1\shad1\1cHD8AFAF\4cHC08000\b0}.也就是说，它是一个新的模型，从MG通过保持只有状态之间的关系，在他们两个都成立。3.9一些有效性在本节中，我们证明了一些公式对于我们的语义是有效的。所有这些公式都类似于PAL公理。定义3.6我们说一个公式f是有效的，如果对所有的评价函数e，所有的群G和所有的状态s，EMG，s（f）= 1。3.9.1有效公式在这一节中，我们证明了PAL（公理）的一些有效公式，当用PPAL重写时仍然有效。定理3.7下列公式在PPAL中有效。(i) [φ]rpParticipate（φ→p）;(ii) [φ]r<$n→（φ→<$[φ]r <$n）;(iii) [φ]r（χ）Participate（[φ]r[φ]rχ）;(iv) [φ]rKG<$Participate（φ→KG[φ]r<$）;(v) 如果φ是有效的，则推断[] rφ也是有效的。这些证明都是通过直接应用评价函数和算子定义得到的，除了iv需要我们假设建议的算子实现。为了便于可视化，我们将形式为e（m，（MG，s））的函数简单地写为e（m），并且EG（m）代替EMG，s（m）。证据 式i.EG（[φ]p→（φ→p））=IMP（EG（[φ]p），EG（φ→p））=IMP（e（p，（MGn，s）），IMP（e（φ），e（p））（5）G114诉Machado，M.Benevides/理论计算机科学电子笔记348（2020）105由于MG和MG中的估值函数V相同，我们可以有把握地说，e（p，（MG，s））=e（p），给出IMP（e（p），IMP（e（φ），e（p））（6）诉Machado，M.Benevides/理论计算机科学电子笔记348（2020）105115R给定p是一个命题，我们考虑每种情况，并使用3.6中定义的规则：• p= 1·IMP（1，IMP（e（φ），1））=IMP（1， 1）= 1;• p= 0·IMP（0，IMP（e（φ），0））=IMP（0， 0）= 1;类似地，我们可以证明←方向也是有效的：• p= 1· IMP（IMP（e（φ），1），1）=IMP（1， 1）= 1;• p= 0· IMP（IMP（e（φ），0），0）=IMP（0， 0）= 1;因此，[φ]rpParticipate（φ→p）是有效的。Q证据式II.EG（[φ]r<$$>→（φ→<$[φ]r<$））=IMP（EG（[φ]r<$$>），EG（φ→<$[φ]r<$））R r=IMP（EG（<$），IMP（EG（φ），EG（<$[φ]）=IMP（NOT（EG（）），IMP（EG（φ），NOT（EG（[φ]）s=IMP（NOT（EG（）），IMP（EG（φ），NOT（EG（）（七）考虑以下情况：• NOT（EG（φ））≥EG（φ）· 根据3.6节的第四条规则，IMP（EG（φ），NOT（EG（φ）= 1。· 我们仍然使用IMP（NOT（EG（）），1），它再次由3.6中的第四条规则，必须等于1。• NOT（EG（φ）））=IMP（IMP（EG（φ），NOT（EG<$（φ），NOT（EG<$（φ）（十四）给定NOT（EG（）） 0。诱导步骤：(i) EMG，s（<$N）=NOT（EMG，s（<$N））：对于U中的任何输入，NOT计算为U中的值。由于EMG，s（ε）可由假设判定，因此该公式是可判定的。EMG，s（n→n），EMG，s（n→ n）和EMG，s（n→ n）都是可判定的，因为它们的论元相同;(ii) EMG，s（KG′j）=K（k，（MG，s），GJ）：120诉Machado，M.Benevides/理论计算机科学电子笔记348（2020）105R(a) 当GJ= 0时，它是平凡可判定的，因为它的求值总是等于0;(b) 当GJ=P时，它是可判定的，因为该公式是通过计算EMG，s′（ε），这是可由假设判定的;(c) 在GJ={GJ0，GJ1， . ，GJn}，|GJI|严格小于|GJ|因为根据定义，群GJ由一组不相交的群组成。因此，s（KG′i<$）

下载后可阅读完整内容，剩余1页未读，立即下载