多智能体系统中基于模型检查的验证技术探索与初步实施

理论计算机科学电子笔记123（2005）5-17www.elsevier.com/locate/entcs多Agent系统穆斯塔法·布拉赫拉1阿尔及利亚Biskra大学计算机科学系Mohamed Benmohamed阿尔及利亚君士坦丁大学计算机科学系摘要多智能体系统越来越复杂，其验证和确认问题也越来越重要。在本文中，我们将展示如何一个众所周知的和有效的验证技术，模型检查，可以推广到处理多智能体系统。本文探讨了一种特殊类型的多智能体系统，其中每个智能体被视为具有信念（B），愿望（D）和意图（I）的三种心理态度。我们使用一个多模态分支时间逻辑BDICTL，与语义，是在传统的决策理论和一个可能的世界框架。该方法的初步实施显示出有希望的结果。关键词：代理，多代理系统，多模态分支时间逻辑，形式化规范和验证，模型检测。1介绍在复杂动态环境中执行高级管理和控制任务所需的系统（特别是安全关键控制）的设计在商业上越来越重要。这些系统包括对空中交通系统、电信网络、商业过程、航天器和医疗服务的管理和控制。经验1电子邮件：mbourahla@hotma il. 网2 电子邮件地址：ibnm@yahoo.fr1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.04.0426M. Bourahla，M.Benmohamed/Electronic Notes in Theoretical Computer Science 123（2005）5应用传统的软件技术来开发这样的系统已经表明，它们的构建、验证和维护非常困难并且非常昂贵。面向代理的系统，基于一个完全不同的观点的计算实体，或者说是一个质的变化，在这一立场的前景许多不同的方法已经成为面向代理系统研究的候选者[1，4，8，10，11]。一个这样的体系结构将系统视为具有信念（信念可以被视为系统状态的信息组成部分）、欲望（欲望可以被认为代表系统的动机状态）和意图（系统的意图捕获系统的审议组成部分）的某些心理态度的理性主体。因此，BDI代表的信息，动机，和deliberative状态的代理。这些心理态度决定了系统为了描述系统状态的信念、愿望和意图成分，使用了基于可能世界的命题形式。因此，可能世界模型[8]由一组可能世界组成，其中每个可能世界都是树结构。在一个可能世界中的一个特定的指数被称为一个情况。我们将每一种情境与一组信念可及的世界、欲望可及的世界和意图可及的世界联系在一起;直观地说，这些世界分别是行动者相信是可能的、欲望是可能的、意图是可能实现的。在本文中，我们解决的问题，验证这种形式主义是越来越重要。多主体时态逻辑[8]被引入到提升最成功的验证技术之一，模型检查[2]，用于多智能体系统的验证。多智能体时序逻辑BDICTL在一个框架内结合了时序逻辑的各个方面，用于推理有限状态自动机的时序演化，以及与智能体相关的方面，如信念，愿望和意图。扩展标准时态逻辑模型检查技术，然后使用相关工具来处理逻辑的多代理方面的问题是可能世界及其之间关系的具体化。我们的贡献的本质是提出一种方法，通过这种方法我们可以帮助减少指定时间。 这种方法是基于自动合成的代理人的心理态度。每一种精神状态都将是一个索引，指向一个新创造的世界，使用不同的代理人的规范。为了说明我们的方法，我们设计了一个子语言指定多智能体系统。规范将以代理人为导向。开发了一个用于构造多智能体系统中各智能体状态空间的工具.然后提出了一种合成智能体的算法M. Bourahla，M.Benmohamed/Electronic Notes in Theoretical Computer Science 123（2005）57∨¬∃ ⇔ ∧ ∃ ∃具体的多智能体系统模型。综合的结果是一个可能世界模型。最后，我们采用标准的模型检测方法对这些多智能体系统模型进行了分析。实现了一个用于验证多智能体系统的符号模型检测工具。初步结果非常有希望。本文的结构如下。在第二节中，我们描述了多主体时态逻辑（BDI-CTL）.在第3节中，我们提出了具体化子语言及其底层直觉，并将语言和语义定义为时态逻辑。在第4节中，我们提出了相应的多智能体结构的合成算法。在第五节中，我们提出了模型检测的扩展通用算法。最后，在第6节中，我们概述了结果，讨论了未来的工作，并得出一些结论。2多Agent时态逻辑我们考虑的时态逻辑BDICTL[8]是计算树逻辑CTL [5]的扩展，该逻辑已被广泛用于并发程序的推理。扩展了分支时间逻辑CTL，使之能表示主体的心理状态或信念-愿望-意图状态。 这个逻辑可以用来对行为人以及他们的信念、欲望和行动如何能使他们的欲望得到满足进行推理。BDICTL的语法如下。：：= true|p|p|ϕ∨ϕ|X| ∃Gϕ| ∃ϕU ϕ|B i|I I I|D i.这种语言的原语包括原子命题的非空集合AP，命题连接词和模态算子B（agent believes）、D（agent desires）和I（agent intends）以及CTL的时态算子。CTL时态运算符有：X（可能在下一个时刻成立）、U（可能在未来某个时刻成立，直到那时才成立）和G（可能在所有未来时刻成立）。时间算子的特征是紧U惠（紧（紧U惠X紧（紧U惠）和紧G（XG.）。 我们有算子B i、I i和D i，这意味着智能体i分别有信念、欲望和意图。这个文法并不是以最简洁的形式给出的，并且存在等价规则来用不同的运算符表达相同的公式;例如，<$F <$（不可避免）等价于<$G<$<$。在实践中，通过使用这个等价规则，可以写出一个公式，使得否定只出现在原子命题的层次上。这种形式的公式被称为负范式（NNF形式）。传统的信念可能世界语义学认为每个世界8M. Bourahla，M.Benmohamed/Electronic Notes in Theoretical Computer Science 123（2005）50120通过连接这些世界的信念-可及性关系B，成为命题和模型信念的集合。一个公式在一个世界中被认为是可信的，当且仅当它在其所有可信任的世界中为真[6]。可达性关系B是在索引处的世界与在时间点处的世界之间的关系一系列世界的联系直觉上，一个智能体相信一个世界中某个特定指数的公式，当且仅当这个公式在其所有可信任的世界中为真。我们认为每个可能世界都是一个树结构，有一个单一的过去和一个分支的未来[3]。公式的求值是关于一个世界和一个状态的。因此，一个状态就像一个索引，指向一个特定的树结构或智能体的世界。信念-可达性关系将一个状态下的可能世界映射到其他可能世界。愿望-可及性关系和意图-可及性关系以类似的方式表现。更正式地说，我们对Kripke结构有以下定义。定义2.1 Kripke结构被定义为元组K=W，S，{Sw：w∈W}，{Rw：w∈W}，{Iw：w∈W}，L，B，D，I，其中W是可能世界的集合，S是状态的集合，Sw是每个世界w∈W（S=Ww∈WSw）中的状态的集合，Rw是全树关系，即，Rw<$Sw×Sw，Iw 是一组初始状态（Iw<$Sw），L：W×S→2AP是一个函数，它为每个世界w∈W标记，每个状态s∈Sw在该状态下为真的原子命题集，B，D和I是世界W和状态S（即OW×S×W），其中O是B、D或I之一。我们也定义一个世界是另一个世界的子世界，如果其中一个世界包含较少的路径，但它们彼此相同更正式地说，我们有以下定义。定义2.2世界wJ是世界w的子世界，记为wJ±w，当且仅当(i) SwJSw，IwJIw，RwJRw，(ii) 其中，L（wJ，s）=L（w，s），(iii) <$s ∈ SwJ，（wJ，s，v）∈ B i <$（w，s，v）∈ B;对D和I也是如此。BDICTL的语义包括两个维度：认知维度和时间维度。一个公式的真值既取决于认识世界w，也取决于时间状态s。一对（w，s）（也记为sw）称为BDICTL公式求值的情况。位置之间的关系传统上被称为可及性关系（信仰）或后继关系（时间）。BDI CTL模型M被表示为Kripke结构。我们把世界w中的模型M记为Mw.世界w ∈ W中从s w开始的迹（路径）是状态的无限序列ρ w=s w sw ···使得s w=s w，并且M. Bourahla，M.Benmohamed/Electronic Notes in Theoretical Computer Science 123（2005）59∈我我的天一期+1我J我JW对每一个i≥ 0，n ∈R w. 迹ρw的第（i+ 1）个状态记为ρw[i]. 从模型Mw的状态sw开始的路径集合定义为：Mw（s w）={ρ w|ρ w[0]= s w}。对于任意BDICTL-模型Mw和状态sw∈Sw，存在一个无穷大的连通性，根标为sw的截断树，使得Sw，sw是树中的弧，如果且仅当εs w，s wε ∈R w. 公式的满足，表示为|= M，给出关于模型M，世界w和状态s。表达s| = Mw被解读为• S|=Mw pi∈L（w，s）• S|=Mwpi s|=Mw p• S|=Mwi s|=Mw/s|=Mw• S|=Mw <$X <$i <$$> ρw∈ <$Mw（s）.ρw[1]|=Mw• S|=Mw<$G <$i <$$> ρw∈ <$Mw（s）. j ≥ 0.ρw[j]|=Mw• S|=Mw <$$> U <$i <$$> ρw∈ <$Mw（s）. （φj ≥ 0.ρw[j]）|=Mw<$）<$（k，0 ≤ k< j. ρw[k]|=Mw）• S|=MwBi（n）iv，（w，s，v）∈ B. sJ∈ v.sJ|=Mv• S|=MwDi（n）iv，（w，s，v）∈ D. sJ∈ v.sJ|=Mv• S|=Mw Ii（v）i <$<$v，（w，s，v）∈ I. sJ∈ v.sJ|=Mv一个公式在M v中是有效的，记为|= Mv，if s| = Mv对于每个状态s Sv。一个公式是有效的，如果它在每一个状态、每一个世界、每一个结构（模型）中都为真。3多智能体系统多代理系统包含有限数量的代理。代理的基本形式是 多代理系统中的每个代理都被假设为具有从一组代理标识符中提取的唯一名称。主要会期确定其行为的代理是程序主体P。 程序体的基础是一种简单的命令式语言，包含迭代（循环）、序列（构造函数）、选择（if、then、else语句的一种形式）、选择（|构造函数）和赋值运算符。允许代理A通过do指令执行集合Actions = α中的任何一个，外部行动。 考虑外部行为的最简单方法是作为Java等编程语言中的本地方法。它们为代理提供了一种执行操作的方法，这些操作不仅检查代理的内部状态，还检查其外部环境。do指令的基本形式是do α，其中α∈Actions是要执行的外部操作。当10M. Bourahla，M.Benmohamed/Electronic Notes in Theoretical Computer Science 123（2005）5|||||||ǁ ǁ ···ǁ我们通过将消息发送建模为要执行的外部动作来合并通信。在传统的编程语言中，if语句中的条件只允许依赖于程序变量。不寻常的是，我们允许if语句中的条件是BDICTL逻辑的任意公式（允许任何可接受的公式作为条件）。为了更具体地说明这一点，请考虑以下几点：if Bj pthen r：=p else r：=false这个想法是，如果执行这个指令的代理相信代理j相信p，那么执行指令的代理将p的值分配给r。如果执行该指令的代理相信不是代理j相信p而是它相信<$p的情况，则它将值false赋给r。注意这里使用的词的形式：执行这个if指令的主体必须相信j相信p;条件不取决于j实际上相信什么，而是取决于执行语句的主体相信j相信什么。正如这个例子所说明的，条件因此可以指其他代理人的精神状态。循环构造的一般形式，如在常规编程语言中，是循环P endloop，其中P是程序。给定代理的集合{A1，···，An}，它们通过并行组合运算符““：A 1An组合成注意也就是说，没有信念算子的嵌套，也没有生成新代理的机制。形式上，多智能体系统的抽象语法由下面的语法定义。Init：：= initp，其中p∈APP：：= do αp：= true或false if_then_Pif_then_Pelse_P_loop_P_endloopPJ; JPPJJP代理：：=代理A是初始化PMAS：：=代理人···代理人例3.1为了阐明这种语法，让我们考虑以下涉及两个代理的场景：一个接收方rcv和一个发送方snd。SND连续地从其传感器读取关于特定主题的新闻（例如，标准输入）。一旦阅读了新闻，snd只有在它认为rcv没有关于该主题的正确知识时才通知rcv（这是为了最小化网络上的传输）。一旦收到消息，rcv向snd确认这一事实。代理snd是代理rcv是initp∈AP：p：=falseinitp：=falseM. Bourahla，M.Benmohamed/Electronic Notes in Theoretical Computer Science 123（2005）511¬∧¬∧¬∧¬¬¬¬ ∧ ¬¬∧¬∧∀ ∈loop循环return（p）; return（m）;如果p Brcv p那么如果（m = inform（snd，rcv，p））那么do putmsg（inform（snd，rcv，p））;p：=true如果p Brcv p，则执行putmsg（inform（rcv，snd，Brcv p））;执行putmsg（inform（snd，rcv，p））;如果（m = inform（snd，rcv，p）），则publicvoid run（m）;如果（m = inform（rcv，snd，Brcv p）），则执行putmsg（inform（rcv，snd，Brcvp））;B rcv p：=真B rcvp：= false;endloopif（m = inform（rcv，snd，B rcv p））thenBrcvp：= trueB rcv p：=false; endloop代理协议是initp AP：p：=false回路p∈AP：p：=false;{BsndFdo（putmsg（inform（snd，rcv，p）：=trueBrcvFdo（getmsg（inform（snd，rcv，p）：=true个文件夹|{1}snd Fdo（putmsg（inform（snd，rcv，<$p）：=trueBrcvFdo（getmsg（inform（snd，rcv，<$p）：=true}的情况;p∈AP：p：=false;{BrcvFdo（putmsg（inform（rcv，snd，Brcv p）：=trueBsndFdo（getmsg（inform（rcv，snd，Brcv p）：=true个文件夹|{1}RCV 请将您的请求发送给我们。RCV <$p）：=trueBsndFdo（getmsg（inform（rcv，snd，Brcv <$p）：=trueen}dloop因此，我们有三个代理：snd，rcv和一个允许它们交互的网络（通信协议）协议上面的例子分别给出了snd、rcv和通信协议协议的描述。在这些描述中，信息交换的新闻主题是命题原子p的真值。inf（snd，rcv，p）返回一条包含发送方snd、接收方rcv和内容p的消息（inf是FIPA（智能物理代理基础）原语）。putMSG和getMSG是用于（从通信信道）发送和获取消息的原语read允许从标准输入读取。Brcv是用于表示其他代理感知的rcv的信念的算子，并且对于Bsnd是对偶的。请注意，通信协议具有关于rcv和snd的信念，因此必须具有它们如何行为的表示我们假设这种表示与rcv和snd实际上是一致的，如上所述。这使我们能够模拟这样一个事实，即通信协议正确地遵循snd和rcv的行为。snd也相信BB12M. Bourahla，M.Benmohamed/Electronic Notes in Theoretical Computer Science 123（2005）5∀∀···→接收器我们假设snd（原则上不知道rcv如何工作）只知道rcv可以处于两种 状 态 之 一 ， p 要 么 为 真 要 么 为 假 。 在 这 个 例 子 中 ， Bsnd Fdo（）（Brcv Fdo（））直观地表示snd（rcv）将必然达到一种状态，在这种状态下，它将刚刚执行与相对应的动作。代理程序协议编码了这样一个事实，即协议实现了snd和rcv之间的信息流，以及它总是传递它被要求传递的消息。我们可能需要证明的一些性质是：(i) 代理活动属性，例如，该SND将最终相信RCV相信P或相信<$P。其表达|= Mwsnd<$F（Brcvp<$Brcv <$p）。其中w是代理所看到的世界。(ii) 整体系统活性属性，例如，如果它相信p，那么在未来SND会相信RCV会相信p。其表达|= MBsnd（p）FBsndF Brcvp.3.1形式语义多智能体程序的语义将被定义为BDICTL的公式，它表征了系统的可接受计算和系统中智能体的[[init p]]Init=Bselfp，p∈AP[[do α]]P=Iselfα，α∈作用[[p：=e]]P=XBself[[e]]Bexp[[ifnthen P]]P=Bselfn[[P]]P[[if n then P1else P2]]P=Bselfnn n[[P1]]Pn（Bself<$nn n <$Bself nn）n n[[P2]]P[[loop P endloop]]P=[[P;loop P endloop]]P[[P1;P2]]P=[[P1]]P[[P2]]P[[P1|P2]] P=[[P1]] P[[P2]] P[[agent A is init P]]Agent=（[init]]Init[[P]]P）[A›→self][[A1···An]]MAS=[[A1]]Agent···[[An]]AgentMAS代理程序的语义功能是根据功能定义的（]]Bexp：Bexp B，它给出布尔表达式的语义。剩下的四个语义功能如上所定义。其思想是语义由一组定义归纳地定义，每个定义对应于语言中的每个构造。声明初始化语句和程序体P的集合。我们捕捉语义M. Bourahla，M.Benmohamed/Electronic Notes in Theoretical Computer Science 123（2005）513O×M在[init]]Init[[P]]P中，系统地将占位符名称self替换为名称A。系统A1···An的语义简单地说是组件智能体Ai的语义与一些背景假设AMAS的结合。背景假设的想法是，这些捕获的多智能体系统的一般属性，而不是由语言的语义捕获。4多Agent系统我们将开发一种算法来构建定义2.1中定义的多智能体结构首先，我们需要为每个代理指定构建一个结构，然后我们将合成这些结构。一开始，多智能体系统将具有形式为K=W={w1，···，wn}，S={S w 1，···，S w n}，R ={R w 1，···，R w n}，I ={I w 1，···，I w n}，L，B = N，D = N，I =其中n是代理的数量。然后，我们将使用世界w∈W和标记函数L来计算集合B、D和I。最后，将使用以下算法构造表示多智能体系统的Kripke结构K。初始Kripke结构K直接从代理指定生成。在每一个世界中，都有一个形式为O i（其中O代表B、D或I）的BDI运算符的有限集合。这个集合被认为是原子命题AP的一部分。让我们称TrueBDI（w，v）（s）为世界w（当前施事体）的BDI原子的集合，其形式为Oi，在s为真（TrueBDI（w，v）（s）=BDI（w，v）<$L（w，s））。v是代理i的世界。相容关系（w，v） BDI（w，v）Sv将世界w的BDI原子的真值约束到世界v中的真值。与s相容的世界v的状态是这些状态属于在s处为真的BDI原子上与TrueBDI（w，v）（s）兼容的状态集合的交集我们将相容关系扩展到一组BDI原子A <$BDI（w，v）上的关系，如下所示。O（w，v）（A）=Oi∈AO（w，v）（Oi）因此，与w的状态s兼容的v的状态集合将简单地表示为O（w，v）（TrueBDI（w，v）（s））。根据所考虑的BDI运算符的种类，兼容关系可以具有不同的属性。多智能体可能世界的模型是由相邻子世界之间相容关系的特殊结构构成的。定义4.1BDICTL模型M是一个可能的世界结构，如果对于每个14M. Bourahla，M.Benmohamed/Electronic Notes in Theoretical Computer Science 123（2005）5∈M∈M ←MM ←M字w，w的每个BDI原子Oi∈ w和每个s Sw，则以下条件成立。(i) 如果Oi∈L（w，s），则SJ∈ O（w，v）（TrueBDI（w，v）（s））蕴涵sj在v中可达，且SJ|= Mv.(ii) 如果Oi∈ L（w，s），则对某个可达状态SJ∈ O（w，v）（TrueBDI（w，v）（s）），SJ|=Mv <$。根据BDI的语义，条件1告诉我们世界v中与给定状态s兼容的状态是什么（满足TrueBDI（w，v）（s）），即在状态处为真的BDI的参数必须在通过兼容关系从它可到达的所有状态中为真。另一方面，条件2告诉我们世界w的哪些状态实际上符合BDI的语义，即根据BDI算子的语义将真值分配给BDI原子的状态。4.1合成多Agent结构在本节中，我们提出了一种合成算法，该算法可以从一组独立生成的结构中自动构建合适的多智能体Kripke结构，用于每个智能体指定和一组选定的BDI原子，从而在建模阶段节省大量时间。合成算法报道如下。它接受一组表示为世界结构的代理和一组BDI原子的输入。直观地说，每个世界的算法计算与世界的每个BDI运算符相关联的相容性关系作为第这是根据定义4.1的条件1完成的第二步是实现相同定义的条件2。这个想法是检查当前世界中是否存在某些BDI原子的否定与其他BDI原子在该状态下为真的状态。条件2告诉我们，在多智能体结构中，没有这样的状态是允许的，因为它们对应于BDI原子的不可能组合。因此，我们需要摆脱世界结构中的所有这些国家。一旦这两个步骤在每个世界上完成，所产生的结构实际上是一个多智能体结构。算法1BUILD-MODEL（w，M）对于每一个i 代理标识符设v为智能体i的世界结构如果BDI（w，v） ≠，则设wv是世界w的施事所看到的施事i的世界构建模型（wv，）CR（w，v，）end ifendforreturn（M）M. Bourahla，M.Benmohamed/Electronic Notes in Theoretical Computer Science 123（2005）515←O←∈|/∈|←∈ {| ∈}|←∈ {|∈}O−}初始调用是BUILD-MODEL（top，M），其中top是Kripke结构（在我们的示例中，是协议代理）。在算法的最后，M将包含以w为根的结构的相容关系。算法BUILD-MODEL递归地从根为w的世界树的深度开始下降，并与当前世界w下一层的所有世界建立兼容性关系（下面的算法）。相容性关系的创建使用算法MAS-Sat（w，n）（在下一节中描述），该算法计算世界w中满足公式n的状态集。算法2-CR（w，v，M）{/* 定义4.1的条件1 */对于每个Oi∈BDI（w，v），[[]]vMAS-Sat（v，）（w，v）（Oi）[[]]v端/* 定义4.1的条件2 */坏州←坏对于每个Oi∈BDI（w，v），[[]]v←MAS-Sat（v，）BadBDI ← {A <$BDI（w，v）\ {Oi<$}| O（w，v）（A）<$[[<$$>]]v=<$}BadStates ← BadStates <${s ∈ Sw|TrueBDI（w，v）（s）BadBDI}端SwJ←JSw\Bad StatesJ如果Rw（Rw限制于Sw）是全树关系，则substitutewithSwJ，RwJ，IwSwJinMelse从M中删除w返回（M）}5BDICTL模型检验在本节中，我们提出了标准CTL模型检测算法[2]的扩展。给定一个BDICTL-公式和一个具有有限状态集（Sw）的BDICTL-模型世界Mw，模型检查算法MAS-Sat（w，n）（如下所示）从满足BDICTL公式的世界w计算状态集。这个集合被表示为[]]w，并且以递归的方式计算，即，通过为的每个子公式计算集合[]]w。为了决定是否S| = Mw<$我们只需要检查s是否∈ [[<$]] w。算法3MAS-Sat（w，ω）{case}p p AP：[[]]ws p L（w，s）OjOjAP：[[]]ws OjL（w，s）OjOjAP：设v是智能体j的世界，设wv是智能体j的世界，由世界w[[]]wv←MAS-Sat（wv，）的智能体所看到的世界1（w，v）（[[]]wv）← {A BDI（w，v）|O（w，v）（A）[[]]wv}16M. Bourahla，M.Benmohamed/Electronic Notes in Theoretical Computer Science 123（2005）5（w，v）∃ ←∩ ∃∃ ← ∪∩ ∃←{∈|∃ ⟨⟩ ∈∧∈个文件夹[[]]w← {s∈Sw|TrueBDI（w，v）（s）O−1（[[]]wv）}<$：[[]]w←Sw\MAS-Sat（w，）ψ∨γ:[[ϕ]]w ←MAS-Sat(w, ψ) ∪MAS-Sat(w,γ)X[[]]wsQs，sRwsQ G：[[]]wνZ. （[[]]wX Z）（Uγ）：[[]]wµZ. （[[]]w（[[γ]]wXZ））endcasereturn（[[]]w）}6结论我们提出了一种新的方法来验证多智能体系统，基于使用可能世界来描述系统，模态时态逻辑来指定属性，以及基于模型检查技术的决策过程。一个贡献是一个强制性的多智能体编程语言的介绍，并为这种语言的BDICTL逻辑方面的正式语义。多智能体程序用于系统地构造智能体状态空间。我们的主要贡献是综合这些状态空间使用代理人的心理态度，以产生可能的世界结构。这些可能世界将被决策程序用来解决验证问题。目前，我们正在研究在许多方面的扩展。一个是扩展的语言，以支持其他类型的表达，特别是算术表达式，通过合并一个工具，用于抽象的程序使用的框架，谓词抽象。另一个问题，这是我们的注意力是爆炸问题的技术，如基于等价的最有趣的扩展之一是处理心理态度之间的函数依赖关系的情况，其中心理态度被认为是一个或多个其他心理态度的函数引用[1] Bratman，M.E、D. Israel和M.E. Pollack，Plans and resource bounded practicalreasoning，Computational Intelligence，4（1988），349[2] Clarke，E.M.，O. Grumberg和D.A. Peled，MIT Press，（1999）.[3] 科恩山口R.，和H.J. Levesque，意图是承诺的选择，人工智能，42（1990），213-261。[4] 道尔·J Rationality and its roles in reasoning，Computational Intelligence，8（2）（1992），376- 409.[5] 埃默森一、和J. Srinivasan，分支时间时序逻辑，线性时间，分支时间和部分顺序在逻辑和模型的并发性，Springer-Verlag，123M. Bourahla，M.Benmohamed/Electronic Notes in Theoretical Computer Science 123（2005）517[6] Halpern J. Y. ， 和 Y. O. MosesA guide to completeness and complex for modal logics ofknowledge and belief，Arti ficial Intelligence，54（1990），319[7] 拉奥美国，和M. [1] George J.，Decision procedures for BDI logics，Journal of Logic andComputation，8（3）（1998），293[8] 拉奥美国，和M.P. 陈文辉，“基于BDI架构的智能体建模”，第二届知识表示与推理原理国际会议论文集，北京，1991。[9] 拉 奥 美 国 ， 和 M. P. George ， An abstract architecture for rational agents ， KnowledgeRepresentation and Reasoning，439[10] 罗 森 沙 因 湾 J. ， 和 L.P. Kaelbling ， The synthesis of digital machines with proposableepistemic properties，Proceedings of the First Conference on Theoretical Aspects of Reasoningabout Knowledge，Morgan Kaufmann，1986。[11] Shoham Y. Agent 0：一种简单的Agent语言及其解释器，第九届全国人工智能会议论文集（AAAI91），704[12] Woodridge M.，代理的计算接地理论，第四届多代理系统国际[13] Woodridge M.，和M. Fisher，时态信念逻辑的决策过程，第一届时态逻辑国际会议论文集，1994。