型检测中并发系统结构元组中的元素相同，只不过语义有所变化第五个元素是个表示认知可达关系的集合。具体见如下定义。定义多智能体系统的结构为以下的五元组其中是系统中多智能体的集合，其中的每个智能体，或称为主体，都足够聪明从而能从其当前已掌握的信息来进行推理。中的主体用编号到表示，其中是中主体的数目。是系统全局状态有限集合。全局状态对应于普通并发系统的系统状态。对于任意，全局状态在其上的分量为它在该全局状态下的局部状态，系统全局状态集合在其上的分量为它的局部状态集合。我们用表示主体的局部状态集合，用表示主体在全局状态下的局部状态。有，是系统初始全局状态的有限集合。初始全局状态即系统在开始运行时处于的状态。对于任意，在其上的分量是它的初始局部状态集合。我们用表示智能体的初始局部状态集合。有华侨大学硕士学位论文对于每个中的元素，由系统的全局状态和智能体的局部状态的关系可知，这个元素在任意智能体的分量都是该智能体的初始局部状态。是系统的全局状态迁移关系，也是个传递的关系。根据以上全局状态与智能体局部状态间的关系可知,对于每个，的定义如下,即为智能体的局部状态迁移关系。由于只作用于全局状态在智能体分量上，因此可用,表示,。是系统全局状态集合上的标签函数，值域是原子命题集合的幂集。有令对于每个，即为的分量，也即为定义在该智能体局部状态集体上的标签函数。对任意，是全局状态间的认知可达关系。它的定义为，对于任意两个,，当且仅当，即从式可知，认知可达关系是种自反对称和传递的关系，所以它是种等价关系。表示在全局状态和下，智能体所掌握的关第章基础理论于系统的信息是完全致的，从下文知识的定义也可知，在这两个全局状态下，智能体通过推理所得知的知识也必然样。在这种情况，我们把全局状态和称为在彼此状态下的可能世界。对每个主体集合可以定义等于，定义为的传递闭包。以上定义了多智能体系统的结构。在不产生歧义的情况，今后本文是出现的多智能体系统均是多智能体系统的结构，并且在出现全局状态之处，我们也可能会简写为状态。等使用种解释系统,作为多智能体系统的形式模型，相对于我们的结构，解释系统的缺点是形式化程度或者说是抽象的程度不高。解释系统是使得计算机的将其建模成的代价更低，从这点可以看出它是种比结构更接近于多智能体系统在机器内部表示的语言，文献指出，种语言如果越接近机器内部的表示，也就是越接近具体语言，抽象程度也越低。我们还可以从另外个方面来说明这种缺点。解释系统中状态迁移关系由动作协议和迁移三个部分组成，协议是定义在状态集合和动作集合上二元关系，每个单独的状态上系统有个特定的动作集合，迁移是定义在协议和状态集合上的二元关系或者看成是定义在状态集合，动作集合和状态集合上的三元关系。可见，解释系统表示迁移关系时必须枚举整个状态空间，形式化程度不高。另外，解释系统中的动作集合可能使状态空间更大。任何个计算机软件系统都是运行的，因此其必然有个运行轨迹。多智能体系统的运行轨迹称为路径，是种全局状态的有限或无限序列。定义如下。定义多智能体系统的条路径是个全局状态的有限序列,其中，是个自然数，表示路径长度，且华侨大学硕士学位论文或者无限序列其中，是个自然数，且,由于多智能体系统是有限状态系统，无限路径的尾端必有环，因此，无限路径除了满足以上条件外，还满足更直观地，无限路径可以表示为，，通常我们用符号表示路径，用表示该路径的第个状态首状态为第个状态，表示的从开始的后缀。多智能体系统是个无限运行下去的系统，系统在任何个状态上都发生迁移，或者迁移到其他状态，或者迁移到该状态本身，因此系统所有的运行路径都是无限路径，我们定义的有限路径是无限路径的前缀。时态认知逻辑本文验证服务组合的时态认知性质。因而，在本文中，主要考虑的逻辑是时态认知逻辑。由于服务组合性质的验证是基于模型检测多智能体，我们在多智能体系统语义的基础上定义时态认知逻辑的语义。时态认知逻辑属于现代逻辑中的模态逻辑，与经典逻辑相异。它包含了时态逻辑和认知逻辑。给普通的谓词逻辑添加必要和可能算子，便得到了模态逻辑。给模型逻辑以种时序上的解释，便得到了时态逻辑,。时态逻辑体系大致可以分为两大流派，即线性时态逻辑和分支时态逻辑。比较两种时态逻辑时采用了特定的时态结构和特定的比较原则，且限定了分支时态逻辑公式的语法和语义，从而得出了不被第章基础理论赞成的结论，即在证明并发程序的些性质时线性时态逻辑要优于分支时态逻辑，而在证明非确定性的些性质时分态时序逻辑要优于线性时态逻辑，且在些方面，线性时态逻辑要比分支时态逻辑强。和,对分支时态逻辑的语法和语义作适当的扩充，克服了上述缺点，并且融两种时态逻辑于个语言之中，从而又克服了对时态逻辑公式的二义性解释。他们对此设计出的时态逻辑语言是和。知识模态逻辑从八十年代中期开始逐步被应用到分布式系统的形式规范,用于精确地描述个智能体的知识。随后，在时态逻辑中加入知识模态算子的时态知识也被广泛地应用分布式系统的知识推理。和首先在年提出用模型检测的方法进行知识推理，但是他们的知识逻辑中没有时态组件。和于年提出了模型检测时态知识逻辑的方法，从而把时态组件引入知识逻辑。和将这个模型检测问题转化为线性时态逻辑模型检测问题。年和开发了个时态知识逻辑的符号模型检测器。和在年提出个基于的时态知识逻辑的符号模型检测方法。年苏开乐和骆翔宇等提出的符号化模型检测时态知识逻辑方法除了能验证和验证的之外，还能验证。模型检测时态认知规范的方法不属于本文的内容，因此本文没有在模型检测的方法上进行研究。本文采用的模型检测方法为苏开乐等在年提出的方法和骆翔宇年在其博士论文里提出的方法。由于本文后续章节的需要，下面将介绍基于的时态认识逻辑的语法和语义。定义本文的的语法为学校代码分类号研究生学号密级硕士学位论文基于多智能体系统模型检测与抽象技术的服务组合验证作者姓名指导教师学科计算机应用技术研究方向形式化方法所在学院计算机科学与技术学院论文提交日期二零四年三月三十日学位论文独创性声明本人声明兹呈交的学位论文是本人在导师指导下完成的研究成果。论文写作中不包含其他人已经发表或撰写过的研究内容，如参考他人或集体的科研成果，均在论文中以明确的方式说明。本人依法享有和承担由此论文所产生的权利和责任。论文作者签名签名日期学位论文版权使用授权声明本人同意授权华侨大学有权保留并向国家机关或机构送交学位论文的复印件和电子版，允许学位论文被查阅和借阅。本人授权华侨大学可以将本学位论文的全部内容或部分内容编入有关数据库进行检索，可以采用影印缩印或扫描等复制手段保存和汇编本学位论文。论文作者签名指导教师签名签名日期签名日期摘要摘要面向服务的体系结构的出现和发展使得服务成为当今服务及软件开发的发展趋势。由于功能有限的单的服务在多数情况下不能满足用户的需求，出现了将多种服务按种特定的组合集成个面向具有不同需求用户的有统接口的服务的技术。然而，服务组合的可信性质受到了来自于服务本身或者其运行环境各个因素的威胁。针对服务的可信性质，研究者们在不断地寻求对验证服务组合的方法。目前验证服务组合方法多是形式化方法。相对于传统的形式化方法，模型检测的优点是验证的全自动化和验证所给出的证据和反例。其另个不太易见的优点是，它不需要在验证所涉及逻辑的全体论域中推理待验证公式是否成立，而只需将待检测系统的形式化模型作为论域。在众多用模型检测检验服务组合性质的技术中，多智能体系统模型检测的优势在于，它不但能验证时态公式，还能验证认知公式。状态爆炸问题是模型检测面临的主要的问题之，也当在模型检测多智能体系统的主要瓶颈之列。抽象作为解决状态爆炸问题的种优化手段，受到了许多研究者的青睐，其研究成果也不断出现。本文探索种多智能体系统模型检测图状反例向导的抽象，并将之应用于服务组合验证中，这是任何以往的服务组合验证工作都没有做到的。另外，以往的反例向导的抽象或者未针对多智能体系统，或者所用形式化模型的形式化程度较本文的结构形式化程度低。本文的方法论在文中获得了数学上严格证明。并且，通过实验证明了该方法论在性能上的优越性。论文的主要研究工作概括如下提出多智能体系统的结构，提出并证明了其抽象模型和种获得初始抽象系统的近似方法。提出了多智能体系统模型检测的种图状反例，给出并证明了图状反例的些性质。提出种图状反例向导的多智能体系统模型检测抽象精化方法。根据我们的分析，服务组合中常用的规范是。采用了以往的将描述的服务组合业务流程转化多智能体系统的种方法。华侨大学硕士学位论文形成个基于多智能体系统模型检测及其图状反例向导的抽象与精化技术的服务组合验证方法论。关键词服务组合验证多智能体系统模型检测图状反例抽象与精化状态爆炸问题华侨大学硕士学位论文