动态认知逻辑与通信行动

可在www.sciencedirect.com在线获取理论计算机科学电子笔记344（2019）67-82www.elsevier.com/locate/entcs具有交流行为的动态认知逻辑Mario Roberto Folhadela Benevides1PESC/COPPE-仪器deMatem'atica/DCC里约热内卢联邦大学里约热内卢，巴西Saab Lima2PESC/COPPE里约热内卢里约热内卢，巴西摘要本文提出了一种动态认知逻辑与通信行动，可以同时执行。 不像Ditmarsch，Hoek和Kooi[15]介绍的并发认知动作逻辑，其中并发机制是所谓的真正并发，这里我们使用基于过程演算的方法，如CCS和CSP，以及动作模型逻辑。我们的方法使得证明的合理性，完整性和可判定性，从其他方法不同。我们提出了一个axiomatisation和证明的合理性，完整性和可判定性可以使用减少的方法。关键词：认知逻辑，动态逻辑，动作模型，动态认知逻辑，并发动作，通信动作。1引言多智能体认知逻辑在计算机科学中已经被研究[6]，以表示和推理智能体（或智能体组）的动态逻辑旨在推理动作（程序）及其结果[8]。动态认知逻辑[16]被认为是对改变代理（或代理组）认知状态的行为进行推理改变Agent的知识和信念的行为第一个动态认知逻辑由[11]和[7]独立提出。它被称为公共通告逻辑（PAL）。还有许多其他方法，但在这项工作中使用的是[1，2]提出的动作模型逻辑。1电子邮件：mario@cos.ufrj.br2电子邮件：isaque@cos.ufrj.brhttps://doi.org/10.1016/j.entcs.2019.07.0051571-0661/© 2019作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。68M.R.福尔哈德拉贝内维德斯岛Macalam Saab Lima / Electron. Notes Theor. Comput. Sci. 344（2019）67-82并发动态认知逻辑是在[15]中提出的，它的目的是用并发的认知动作来扩展VanDitmarsch在[14]在这个扩展中，他们使用一种称为“真并发”的机制来处理并发，在[12]中提出的一个有趣的工作，题为通信和知识的逻辑，提出了一个用于建模消息传递情况的框架，该框架结合了动态epistemic语义和基于历史的方法的属性另一项启发我们将沟通行为表示为私人认知行为的工作是[7]。例如：假设有两个学生在等待老师发回作业的消息，其中一个学生不知道另一个学生是否收到或回复了消息。为了表示这一点，我们需要建模以下动作：教师发送消息（发送动作），每个学生独立地接收（接收动作）和响应（响应动作）消息。我们还需要保证：接收动作不能在发送动作之前执行，响应动作不能在接收动作之前执行，学生动作可以并发执行。我们可以使用动作模型逻辑来建模吗？由于这是一个非常小的例子，可以说这可以通过使用先决条件和非确定性选择来模拟所有可能的路径来完成。现在想象一下100名学生的情况做模型可不容易这项工作提出了一种方法来处理并发和通信的动态认知逻辑。我们使用基于动作模型和过程演算的方法与[15]不同的是，它在认知动作逻辑之上实现了并发，我们扩展了动作模型来处理并发和通信。可靠性、完备性和可判定性的证明可以使用归约方法来完成。为了便于证明可靠性、完整性和可判定性，我们限制了并发方法。我们不像[ 15 ]中那样处理相反，我们采用了在CCS和CSP等进程代数中使用的交织（所有可能路径的非确定性选择由于我们是基于在动作模型中，我们可以使用前置条件来限制必须在另一个动作之后执行的动作。我们不处理常识，因为这会使证明变得有点棘手。在第2、3、4节中，我们简要介绍了多智能体认知逻辑、动作模型逻辑和并发动态认知逻辑。接下来，我们介绍了我们在本文中提出的动态认知逻辑。最后一部分是结论。2多智能体认知逻辑本节介绍多智能体认知逻辑S5a。本节的所有定义和定理都基于[16]。M.R.福尔哈德拉贝内维德斯岛Macalam Saab Lima / Electron. Notes Theor. Comput. Sci. 344（2019）67-82692.1语言与语义定义2.1认知语言由命题符号的可数集合Φ、施事的有限集合A、每个施事a的模态Ka以及布尔连接词<$和<$组成。公式定义如下：：：= p|不|¬ϕ|ϕ1∧ϕ2|Ka其中p∈Φ，a∈ A.定义2.2多智能体认知框架是一个元组F=（S，Ra），其中：• S是一个非空的状态集合;• Ra是S上的二元关系，对每个主体a∈ A;定义2.3多主体认知模型是一对M=（F，V），其中F是框架，V是赋值函数V：Φ→ 2S。我们称一个有根的多智能体认知模型（M，s）为认知状态。定义2.4给定一个多智能体认知模型M= R（S，Ra），V满意度的概念M，s|定义如下：1. M，s| = p i s∈ V（p）2. M，s|=<$φ i M，s| = φ3. M，s| = φ i M，s| = φ和M，s|=4. M，s| = Kaφ i对于所有sJ∈S：sRasJ <$M，sJ|= φ2.2公理化(i) 所有命题重言式的实例，(ii) Ka（n→n）→（Kan→Kan），(iii) Ka→，(iv) Ka→KaKa（+内省），(v) <$Ka→Ka<$Ka（−内省），推理规则M.P.，→/U.G./Ka定理2.5 S5a在语义上是可靠的和完备的。例2.6这个例子来自[16]。假设我们有一个纸牌游戏，有三张牌：0，1和2，三个玩家a，b和c。每个玩家收到一张牌，并且不知道其他玩家的牌。我们使用命题符号0x， 1x， 2x表示x∈ {a，b，c}，意思是我们通过每个玩家在该状态下拥有的牌来命名每个状态，例如012是玩家a拥有牌0，玩家b拥有牌1，70M.R.福尔哈德拉贝内维德斯岛Macalam Saab Lima / Electron. Notes Theor. Comput. Sci. 344（2019）67-82玩家C有牌23。下面的认识模型表示每个主体4的认识状态。Hexa1 =（S，R），V：• S={ 012， 021， 102， 120， 201， 210}• R={（012，012），（012，021），（021，021），. 个文件夹• V（0a）={ 012， 021}，V（1a）={ 102， 120}，.图1.一、EpistemicModelHexa13动作模型本节的所有定义和定理都基于[16]。3.1语言与语义定义3.1一个动作模型M是一个结构S，A，P，其中：• S是动作点或事件有限域;•A是S上的一个等价关系，对每个智能体a∈ A;• pre：S<$→ L是一个前置条件函数，它为每个s ∈ S分配一个前置条件。有根的动作模型是一个具有区别状态（M，s）的动作模型。注意，S与S不同，M与M不同，s与s不同。定义3.2动作模型语言由一个可数的命题符号集Φ、一个有限的主体集A、布尔连接词<$和<$、一个模态Ka（每个主体a ∈ A） 和一个模态[α]组 成 。公式定义如下：：：= p|不|¬ϕ|ϕ1∧ϕ2|Ka|[α] δ，α：：=（M，s）|α1，α2|α1∪α2其中，p∈Φ，a∈ A，（M，s）是根动作模型，且<$α<$Particip <$[<$α]定义3.3给定一个认知状态（M，s），M= S，Ra），Va，和一个有根的行动模型 （ M ， s ） ， M=S ， Ra ， pre a 。 在 （ M ， s ） 中 执 行 （ M ， s ） 的结果是（M<$M，（s，s）），其中M <$M=N（SJ，RaJ），VJ，使得：3带下划线的状态名称表示当前状态4我们省略了图中的反射循环M.R.福尔哈德拉贝内维德斯岛Macalam Saab Lima / Electron. Notes Theor. Comput. Sci. 344（2019）67-8271（Ⅲ）7.（M，s）;（MJ，sJ）i（M;MJ，（s，sJ））行动模型的组成6. <$α<$β）i <$<$α）<$<$β）(i) SJ={（s，s）使得s∈S，s∈S，且M，s| = pre（s）}(ii) （s，s）RaJ（t，t）i ∈（sRatands∈at）(iii) （s，s）∈VJ（p）i <$s∈V（p）定义3.4根动作模型给定有根动作模型（M，s），其中M= S，S，P，P，和（MJ，sJ），其中MJ=，它们的组成是动作模型（M;MJ，（s，sJ）），其中M;MJ=⟨SJJ,∼JJ,preJJ⟩:• SJJ={（s，sJ）使得s∈S，sJ∈SJ}• （s，sJ）<$JaJ（t，tJ）i <$（s<$atandsJ<$JatJ）• preJJ（s，sJ）=<$（M，s）<$preJ（sJ）定义3.5给定一个有根的认知状态（M，s），M =S，Ra），Va，和一个有根的行动模型（M，s），M = S，R a，pre a。满意度的概念M，s |=从2.4扩展而来，定义如下1，2，3，4与定义2.4相同5. M，s |=[（M，s）] φ i <$M，s |= pre（s）M M，（s，s）|= φ什么事？ 是一个动作模型上的迭代。3.2公理化认知逻辑公理第2.2节的公理（i）、（ii）、（iii）、（iv）和（v），动作模型逻辑公理(i)[（M，s）]pParticipate（pre（s）→p），(vii)[（M，s）]<$φ参与（pre（s）→<$[（M，s）]φ）（viii）[（M，s）]（φ）Participate（[（M，s）]φ[（M，s）]）(ix)[（M，s）]KaφParticipate（pre（s）→satKa[（M，t）]φ）（x）[（M，s）][（MJ，sJ）]φParticipate[（M，s）;（MJ，sJ）]φ(xi)[（M，s）<$（MJ，sJ）]φ参与[（M，s）]φ<$[（MJ，sJ）]φ推理规则M. P.，/Ka72M.R.福尔哈德拉贝内维德斯岛Macalam Saab Lima / Electron. Notes Theor. Comput. Sci. 344（2019）67-82 没有共同知识的行为模型逻辑语言中的每个公式都等价于认知逻辑语言中的一个公式[16]。M.R.福尔哈德拉贝内维德斯岛Macalam Saab Lima / Electron. Notes Theor. Comput. Sci. 344（2019）67-8273实施例3.6实施例2.6的延续假设现在代理a想要执行向代理出示她的卡的动作B. 实际上，我们有三个动作，代理a向代理展示牌0，1或2B.智能体a和b可以区分这三种行为，但智能体c不能。这种情况可以用下面的动作模型来表示图二. 表演的动作模型• S={sh0，sh1，sh2}•a={（s，s）|s∈S}•b={（s，s）|s∈S}•c=S×S• pre（sh0）= 0a• pre（sh1）= 1a• pre（sh2）= 2a如果在例2.6的认知模型上，代理人a执行向代理人b出示她的卡片的动作，我们得到：图3.第三章。Hexa1表演结束后这个新的认知模型，如图3所示，是由图1的认知模型和图2的行动模型的乘积得到的。重要的是要注意，乘积之后的状态数是18（6× 3），但大多数都被抛出，因为它们不满足前提条件。4认知动作与并发动态认知逻辑本节简要介绍[15]和[16]中介绍的工作。认知动作是多智能体认知逻辑的扩展，用于处理新信息（更新），如动作模型，但它使用不同的方法来处理新信息。并发动态认知逻辑提出了一种处理认知动作并发性74M.R.福尔哈德拉贝内维德斯岛Macalam Saab Lima / Electron. Notes Theor. Comput. Sci. 344（2019）67-82（2）8.<$α; αJ）=<$α）<$<$αJ）4.1语言与语义4.1认知动作语言由命题符号的可数集合Φ、施事的有限集合A、布尔联结词<$和<$、每个施事a∈ A的模态Ka和模态[α]组成。公式和动作定义如下：：：= p|不|¬ϕ|ϕ1∧ϕ2|Ka|[α] α，α：：=？α|LBβ|（α！α）|（αα）|（α; β）|（α1<$α2）其中p∈Φ，a∈ A，B <$A，L表示学习，LBβ表示α是一个测试，（α！α）称为左局部选择，（α<$α）称为右局部选择，（α; β）是顺序复合（先α后β），（α1<$α2）是非确定性选择。定义4.2给定认知模型M=S，Sa，Va，状态s∈S。满意度的概念M，s |=从2.4扩展而来，定义如下1，2，3，4与定义2.4相同5. M，s |= [α] φi ∈ （MJ，sJ）：（M，s）[α]（MJ，sJ）蕴涵（MJ，sJ）|= φ6. （M，s）[？φ]（MJ，sJ）i <$MJ=<$[φ]M，<$，V<$[φ]M<$且sJ=s7. （M，s）[LGφ]（MJ，sJ）i <$MJ=<$SJ，<$J，VJ<$and（M，s）[φ]sJ9.α<$αJ）=<$α）<$<$αJ）10.第一！αJ= α并发动态认知逻辑语言在认知动作语言的动作中增加了并发表达式运算符。这些行动的定义如下：α：：=？α |LBβ|（α！α）|（αα）|（α; β）|（α1<$α2）|（α1<$α2）其中（α1<$α2）表示并发执行。例4.3为了说明认知行动语言的使用，我们考虑第3节中提出的纸牌游戏。认知模型与图1所示相同。“代理a向代理b出示她的卡”的动作（L（b）？0aL（b）？1a/b？2a）;（L（a，b，c）？（Kb0a<$Kb 1a<$Kb 2a））这意味着代理A告诉代理B她的卡，然后所有代理都知道代理B知道代理A持有的卡。执行此操作后，产生的认知模型与图3相同。M.R.福尔哈德拉贝内维德斯岛Macalam Saab Lima / Electron. Notes Theor. Comput. Sci. 344（2019）67-8275i、ji、ji、j5具有交流作用的动态认知逻辑5.1进程演算在本节中，我们提出了一个非常小的过程（程序）演算的程序的动态认知逻辑与通信行动（DELWCA）。”[17]这是他的灵感。令A ={1，.，n}，由i，j. 是一个有限的集合，的代理，AMS={a1，a2，a3.. . }被一铁镍铁矿设置的行动模型和N={c1，c2，c3，...，c1，c2，c3，.. . 是一组有限的通信动作。 按照惯例，带有一条上划线的通信动作表示输出，没有上划线的通信动作表示输入。 通信操作可以组合在一起， 通过将输出通信动作与其相应的输入（[c1，c1]=a1）。两个通信动作的连接的动作模型结果被称为静默动作，由τs（. ），其可以被解释为代理i和j之间的通信的结果。定义5.1语言可以定义如下。η：：= α| α.η|η1; η2|η1 + η2，其中α∈AMS<$Nπ：：= η |β.π |π1; π2|π1+ π2|η1η2···ηn其中n =|一|并且ηi表示由代理i执行的程序。我们用π和η表示进程（程序），α和β表示动作模型和通信动作。Prefix操作符表示进程将首先执行动作α，然后表现为π。求和（或非确定性选择）运算符+表示过程将做出非确定性选择，以表现为π1或π2。 并行复合算子表示过程η1，.，nn，由代理1，...，n分别可以独立地进行或者可以通过公共信道通信。我们用ieπ→απj表示过程π能实现απα，之后，beh ave作为πJ。我们用π→απ来表示π的过程是成功的在执行动作α之后完成。 一个过程完成时，没有可能的β√剩下的动作让它去执行。例如，β →。 当一个进程在内部完成时，我们写的并行组合、顺序组合或非确定性选择π代替π|π，π，π + π。 我们也写而不是|- 是的像[9]一样，我们需要限制代理执行某些操作。在我们的例子中，我们5作为无声的行动τ s（. ）被解释为私有动作模型，索引s表示动作的根模型τ s（. ）.76M.R.福尔哈德拉贝内维德斯岛Macalam Saab Lima / Electron. Notes Theor. Comput. Sci. 344（2019）67-82i、j我们的进程演算的语义可以由转换规则给出，其中π和η是过程规范，而πJ和ηJ是过程规范或η。的τs（. ）动作代表一种内部沟通从代理人i到代理人j的动作。α√α→αα.π→ παπ1→π1′απ1; π2→π1′; π2απ1→π1′απ1+π2→π1′βπ2→π2′βπ1+π2→π2′α对于所有i，j∈A，ηi→ηi ′α（η1. 我的天 ηn）→（η1 我... n）C c对于所有i，j∈ A，ηi→ηi′，ηj → ηj ′τi，j（. ）（η1. 我的天 你好... n）→（η1π... 我... 你好... n）表1过渡关系例5.2继续纸牌游戏的例子。现在假设游戏是在线的，玩家a向玩家b和c发送消息p。所以在消息p之后，玩家b和c知道所有的牌。这个问题可以模拟如下：• π1=cab（p）;cac（p）+cac（p）;cab（p）• π2 = cab（. ）.β• π3 = cac（. ）.γ• π1 <$2 <$3=（π1<$π2<$π3）给定程序π1、π2和π3，最初我们有两个可能的动作：a和b之间的通信或a和c之间的通信。假设a和b之间的通信首先发生，那么我们将有两个可能的动作：a和c之间的通信或动作β等等。我们可以使用并行组合来表示：π1ǁπ2ǁπ3τacγβ◦J布拉奇布拉奇◦ _sβ◦Jγ布拉奇zvτabzvβ布拉奇γ◦Jβ布拉奇τab◦Jz_rvzγ布拉奇zvτab布拉奇β布拉奇见图4。过程π1<$π2<$π3τacτacγγβM.R.福尔哈德拉贝内维德斯岛Macalam Saab Lima / Electron. Notes Theor. Comput. Sci. 344（2019）67-8277ααα→i1我221221112于是：• π11213（K2p<$K3p）为真• π11213（K2p<$K3p）为真• π11213（K2p<$K3p）为假5.2互模拟互模拟的概念是任何进程代数中的一个关键概念。它是具有相似行为的过程之间的等价关系。直觉是两个双相似过程不能被外部观察者区分开利用互模拟的概念，我们可以将任何过程转换为等价的过程，该过程是所有可能行为的总和，这就是扩展定律（定理5.5）states.tab：semccsCCS中的τ动作有两种可能的语义：它可以被视为是可观察的，就像通信动作一样，或者它可以被视为是不可见的。我们采用第一个，因为它更一般，更适合我们的形式主义。只要τ作用是可观测的，互模拟关系就被称为强的。定义5.3（[9]）设k是所 有 过 程 的集合。 一个 集合Z ×是一个如果（π1，π2）∈Z，则强互模拟对所有α∈AMS意味着：α• 若π1→πJ，则存在πJ∈Z使得π2→πJ且（πJ，πJ）∈Z;α• 若π2→πJ，则存在πJ∈Z使得π1→πJ且（πJ，πJ）∈Z;• π1→α π当且仅当π2→απ。定义5.4（[9]）两个过程π和πJ是强双相似的（或简单的双相似），用ππJ表示，如果存在强互模拟Z使得（π，πJ）∈Z。现在，我们介绍扩展律，它在语义的定义和我们逻辑的公理化中非常重要我们提出了一个特殊的情况下，扩展法律，这是适合我们的需要。膨胀定律的最一般情况在[9]中给出。定理5.5（[9]）[展开律（EL）]设π =（η1≠. n）。然后π∼Σα。（η1. 我... n）+n'我τi，j（. ）的。（η1. 我... 你好... n）'Jηiαη'C（η→ηi）（ηC→ηj）其中α是动作模型，τi，j是由两个通信动作组合而成的私有动作模型。我们用 E x p （ π ） 表示这种双相似性的右侧。 我们也用0表示扩展为空的过程，即， re是no（ηi→cηJ），（ηj→cnjJ）和（ηk→αηJ）对于任意i，j，k∈{1，.， n}。K78M.R.福尔哈德拉贝内维德斯岛Macalam Saab Lima / Electron. Notes Theor. Comput. Sci. 344（2019）67-82i、ji、j=c.A+α.A和B=c.B+β.B证据这可从表1和定义5.3和5.4中得出。这个定理最一般情况的详细证明可以在[9]中找到。Q膨胀定律是CCS过程的一个非常有用的性质。 它的直觉过程可以重写为所有可能行为的总和defJ JJdefJ JJ过程（A→B）等价于，使用扩展定律，（A至B） α。（AJJ<$B）+ β。（A<$BJJ）+ τAB。（AJ<$BJ）5.3语言在本节中，我们将介绍DELWCA语言。定义5.6DELWCA语言由一个可数命题符号的集合Φ、一个在5.1节中定义的程序集合A、一个有限的主体集合A、布尔连接词<$和<$、每个程序π∈ <$的模态<$π<$（如5.1节中定义的）和每个主体a的模态Ka组成。公式定义如下：：：= p|不|¬ϕ|ϕ1∧ϕ2|⟨π⟩ϕ|Ki其中p∈ Φ，π∈ φ，i∈ A和φπφ意味着存在一个π的执行，导致φ为真的状态。5.4语义对于通信动作（N中的动作），我们需要放宽动作模型中的关系是等价关系的事实，我们只需要它们是关系。在这种情况下，所有的动作模型的定义（定义3.1）、动作模型的执行（产品）（定义3.3）、动作模型的组成（定义3.4）都可以很容易地进行调整。定义5.7设A是所有智能体的集合，i，j ∈ A。所述动作模型τs（τ）=（M，s），其中M= τS，τ s，pre τ s，定义如下：• S={s，t}•i={（s，s），（t，t）}• {（s，s），（t，t）}• 对于所有k∈ A\{i，j}，k={（s，t），（t，t）}• pre（s）=0• pre（t）=T图五. τs的动作模型为了获得DELWCA的满意度定义，我们必须在定义3.5中增加以下条件：假设我们有一个进程A中选择一个选项。M.R.福尔哈德拉贝内维德斯岛Macalam Saab Lima / Electron. Notes Theor. Comput. Sci. 344（2019）67-82791n i，j1J Jnic1J分（η 我... （m））={λτ （。））; 我... 我的天你好... ǁηJ我）），对于所有（η我→ηi）&（ηj→c1ηJ）}{<$α）;<$（η1<$.. 你好... 对于所有的（ηi→αηJ）}5.4.1公理化(i) 所有命题重言式的实例，认知逻辑公理第2.2节的公理（i）、（ii）、（iii）、（iv）和（v），行动模型公理第3.2节公理（六）、（七）、（八）和（九），PDL公理(x) [π]（φ→π）→（[π]φ→[π]π）（K公理）(xi) [π1][π2]φ参与[π1;π2]φ（合成）(xii) [π1+π2]φ参与[π1]φ[π2]φ（非确定性选择）(xiii) [α.π]φ参与[α][π]φ（前缀）6(xiv) [α.π]φ参与（α）→[π]φ并发动作公理(xv)[η1]... ηn] φParticipate [Exp（η1 n）]φ推理规则M.P.，→/U.G./[π]命题5.8<$[α;π2]φ参与[α][π2]φ参与[α.π2]φ参与（α）→[π2]φ例5.9一位导师Ane（1）和她的两个学生Bob（2）和Cathy（3）在自己家里的电脑上工作。 主管想预约“明天下午4点”的会议。她异步地向鲍勃和凯茜发送一条消息。我们假设管理程序分别使用信道c12和c13与Bob和Cathy通信。我们分别用进程π1、π2和π3表示Anne、Bob和Cathy，用π1 <$2 <$3表示他们的平行合成。• π1=c12（p）;c13（p）+c13（p）;c12（p）• π2 = c12（. ）6需要注意的是，Prefix是Composition的一个特例。80M.R.福尔哈德拉贝内维德斯岛Macalam Saab Lima / Electron. Notes Theor. Comput. Sci. 344（2019）67-82ǁǁ• π3 = c13（. ）• π1 <$2 <$3=（π1<$π2<$π3）我们有两个可能的运行过程π1 <$2 <$3，如图6中的树所示。π1π2π3τ12τ13◦ s，τ13布拉奇z轴τ12布拉奇见图6。过程π1<$π2<$π3让命题符号p代表认知模式在乞讨时的M j如图7所示。u2，3vpp图第七章初始认知模型M0τ12和τ13的作用模型见图8和图9。见图8。行动模式τ12见图9。τ13的行动模型假设τ12在τ13之前执行。在执行τ12之后，我们得到图10中的认知模型图。图10. 认知模型M1=M0<$τ12M.R.福尔哈德拉贝内维德斯岛Macalam Saab Lima / Electron. Notes Theor. Comput. Sci. 344（2019）67-8281需要注意的是，在状态us1Ane和Bob知道pM1，us1K1pK2p，但Cath 在第二次沟通τ13之后，我们有了图11的认识模型。图十一岁认知模型M2=M1<$τ13=M0<$τ12<$τ13从 图 11 中 我 们 可 以 注 意 到 ， 在 状 态 us1s2Ane ， Bob 和 Cath 知 道 pM2 ，us1s2K1pK2pK3p，正如预期的那样。 如果我们执行运行τ13; τ 12，我们得到模型M3，如图12所示。图12个。认知模型M3=M0<$τ13<$τ12我们可以从图12中看出，Ane、Bob和Cath知道pM3，us1s2n。K1pK2pK3p如预期。5.5可靠性、完备性和可判定性5.5.1健全性我们需要证明所有的公理都是有效的。公理i到xiii是动态认知逻辑文献中的标准，可以在[16]中找到。我们只证明公理6的有效性。82M.R.福尔哈德拉贝内维德斯岛Macalam Saab Lima / Electron. Notes Theor. Comput. Sci. 344（2019）67-82引理5.10 [η1] η n] φ Participate [Exp（η1 n）] φ是有效的。证据 这个证明直接遵循表1和定理1的规则。五点五Q在[3]中可以找到详细的可靠性证明。5.5.2完整性完备性的证明类似于[13]动态认知逻辑中引入的公共声明和动作模型逻辑的证明。我们证明了DELWCA中的每个公式与Epistemic逻辑中的公式等价的完备性.为了实现这一点，我们只需要提供一个转换函数，将每个DELWCA公式转换为一个公式，而无需通信操作和并发性。完整性的详细证明可以在[3]中找到。5.5.3判定性可判定性直接从S5a的可判定性得出。6结论在这项工作中，我们提出了一个动态认知逻辑与通信动作，可以同时执行。为了实现这一点，我们提出了一个PDL一样的语言的行动，并开发了一个小的过程演算。我们表明，它很容易建模的通信和并发问题与建议的动态认知逻辑。它的主要特征是扩展规则，允许表示并行组合运算符。这种方法类似于[4，5]中介绍的方法。我们把通信行为表示为私有行为模型，其中的关系不是等价关系。我们提出了一个公理化，并证明了完备性使用减少技术。作为未来的工作，我们想调查的扩展与共同的知识和/或迭代运算符，研究其他类型的通信，代理不可靠或不信任，扩展到动态认知逻辑与后条件和改变DEMO，或创建一个新的模型，以处理并发和通信。引用[1] Baltag，A.和L.Moss，认知程序的逻辑，Synthese（2004），pp.165-224。[2] Baltag，A.，L.莫斯和索莱茨基，公共知识的逻辑，公共公告和私人suppition，in：I.吉尔博，主编，第七届理性与知识的理论方面会议（TARK98），1998年，第100页. 43比56[3] Benevides，M.和I. Lima，Dynamic epistemic logic with communication actions，Technical Report1902.01164，ArXiV（2019）。URLhttp://arxiv.org/abs/1902.01164M.R.福尔哈德拉贝内维德斯岛Macalam Saab Lima / Electron. Notes Theor. Comput. Sci. 344（2019）67-8283[4] Benevides，M.和L. Schechter，CCS程序的命题动态逻辑，在：第十五届逻辑，语言，信息和计算研讨会论文集，LNAI5110（2008），pp. 83比97[5] Benevides，M.和L. Schechter，A propositional dynamic logic for concurrent programs based on the π-calculus，in：Proceedings of Methods for Modalities，Electronic Notes in Theoretical Computer ScienceENTCS262（2010），pp. 49比64[6] 费金河，J. Halpern，Y.摩西和M.Vardi，[7] Gerbrandy ， J. and W. Groeneveld ， Reasoning about information change ， Journal of Logic ，Language，and Information（1997）. 147比169[8] Harel，D.，“动态逻辑”，《哲学逻辑手册》，多德雷赫特：赖德尔，第2卷，1984年，D. Gabbay和F. 冈纳[9] 米尔纳河，“Communication and Concurrency,” Prentice Hall,[10]Peleg，D.，并发动态逻辑中的通信，计算机与系统科学杂志35（1987年）。[11] Plazza，J. A.，“Logics of Public Communications,” Proceedings of the 4[12] Sietsma，F.，“沟通和知识的逻辑，”博士。论文，阿姆斯特丹大学（CWI-ILLC）（2012）。[13]van Bentham，J.，J. van Eijck和B.P. Kooi，沟通和变化的逻辑，Inf.Comput. 204（2006），pp. 1620-1662年。[14] van Ditmarsch，H.， M. Pauly和G.Sandu，ESSLI，2001年。[15] van Ditmarsch ， H. ， W. van der Hoek 和 B. Kooi ， “ 并 发 动 态 认 知 逻 辑 ” ， Kluwer ， Ed. V.F. 的Hendricks等人，，第二卷。322，2003年。[16] van Ditmarsch，H.，W. van der Hoek和B. Kooi，[17] 范格拉布尔克河J.，线性时间分支时间谱i：具体的顺序过程的语义，在：A. P.J.A. Bergstra和S. Smolka，编辑，Handbook of Process Algebra，第1章，Elsevier，2001页。3-99