33学位论文_基于多智能体系统模型检测与抽象技术的Web服务组合验证文档

我们还可以从另外个方面来说明这种缺点。

解释系统中状态迁移关系由动作协议和迁移三个部分组成，协议是定义在状态集合和动作集合上二元关系，每个单独的状态上系统有个特定的动作集合，迁移是定义在协议和状态集合上的二元关系或者看成是定义在状态集合，动作集合和状态集合上的三元关系。

可见，解释系统表示迁移关系时必须枚举整个状态空间，形式化程度不高。

另外，解释系统中的动作集合可能使状态空间更大。

任何个计算机软件系统都是运行的，因此其必然有个运行轨迹。

多智能体系统的运行轨迹称为路径，是种全局状态的有限或无限序列。

定义如，华侨大学硕士学位论文华侨大学硕士学位论文目录目录第章引言国内外服务组合验表示个迁移的概率，则对于，有，，其中表示的规模即元素个数。

多智能体系统也是个有限状态并发系统，其结构是个五元组，元组中的前四个元素与传统模型检测中并发系统结构元组中的元素相同，只不过语义有所变化第五个元素是个表示认知可达关系的集合。

具体见如下定义。

定义多智能体系统的结构为以下的五元组其中是系统中多智能体的集合，其中的每个智能体，或称为主体，都足够聪明从而能从其当前已掌握的信息来进行推理。

中的主体用编号到表示，其中是中主体的数目。

是系统全局状态有限集合。

全局状态对应于普通并发系统的系统状态。

对于任意，全局状态在其上的分量为它在该全局状态下的局部状态，系统全局状态集合在其上的分量为它的局部状态集合。

我们用表示主体的局部状态集合，用表示主体在全局状态下的局部状态。

有，是系统初始全局状态的有限集合。

初始全局状态即系统在开始运行时处于的状态。

对于任意，在其上的分量是它的初始局部状态集合。

我们用表示智能体的初始局部状态集合。

有华侨大学硕士学位论文对于每个中的元素，由系统的全局状态和智能体的局部状态的关系可知，这个元素在任意智能体的分量都是该智能体的初始局部状态。

是系统的全局状态迁移关系，也是个传递的关系。

根据以上全局状态与智能体局部状态间的关系可知，对于每个，的定义如下，即为智能体的局部状态迁移关系。

由于只作用于全局状态在智能体分量上，因此可用，表示，。

是系统全局状态集合上的标签函数，值域是原子命题集合的幂集。

有令对于每个，即为的分量，也即为定义在该智能体局部状态集体上的标签函数。

对任意，是全局状态间的认知可达关系。

它的定义为，对于任意两个，，当且仅当，即从式可知，认知可达关系是种自反对称和传递的关系，所以它是种等价关系。

表示在全局状态和下，智能体所掌握的关第章基础理论于系统的信息是完全致的，从下文知识的定义也可知，在这两个全局状态下，智能体通过推理所得知的知识也必然样。

在这种情况，我们把全局状态和称为在彼此状态下的可能世界。

对每个主体集合可以定义等于，定义为的传递闭包。

以上定义了多智能体系统的结构。

在不产生歧义的情况，今后本文是出现的多智能体系统均是多智能体系统的结构，并且在出现全局状态之处，我们也可能会简写为状态。

等使用种解释系统，作为多智能体系统的形式模型，相对于我们的结构，解释系统的缺点是形式化程度或者说是抽象的程度不高。

解释系统是使得计算机的将其建模成的代价更低，从这点可以看出它是种比结构更接近于多智能体系统在机器内部表示的语言，文献指出，种语言如果越接近机器内部的表示，也就是越接近具体语言，抽象程度也越低。

我们还可以从另外个方面来说明这种缺点。

解释系统中状态迁移关系由动作协议和迁移三个部分组成，协议是定义在状态集合和动作集合上二元关系，每个单独的状态上系统有个特定的动作集合，迁移是定义在协议和状态集合上的二元关系或者看成是定义在状态集合，动作集合和状态集合上的三元关系。

可见，解释系统表示迁移关系时必须枚举整个状态空间，形式化程度不高。

另外，解释系统中的动作集合可能使状态空间更大。

任何个计算机软件系统都是运行的，因此其必然有个运行轨迹。

多智能体系统的运行轨迹称为路径，是种全局状态的有限或无限序列。

定义如下。

定义多智能体系统的条路径是个全局状态的有限序列，其中，是个自然数，表示路径长度，且华侨大学硕士学位论文或者无限序列其中，是个自然数，且，由于多智能体系统是有限状态系统，无限路径的尾端必有环，因此，无限路径除了满足以上条件外，还满足更直观地，无限路径可以表示为，，通常我们用符号表示路径，用表示该路径的第个状态首状态为第个状态，表示的从开始的后缀。

多智能体系统是个无限运行下去的系统，系统在任何个状态上都发生迁移，或者迁移到其他状态，或者迁移到该状态本身，因此系统所有的运行路径都是无限路径，我们定义的有限路径是无限路径的前缀。

时态认知逻辑本文验证服务组合的时态认知性质。

因而，在本文中，主要考虑的逻辑是时态认知逻辑。

由于服务组合性质的验证是基于模型检测多智能体，我们在多智能体系统语义的基础上定义时态认知逻辑的语义。

时态认知逻辑属于现代逻辑中的模态逻辑，与经典逻辑相异。

它包含了时态逻辑和认知逻辑。

给普通的谓词逻辑添加必要和可能算子，便得到了模态逻辑。

给模型逻辑以种时序上的解释，便得到了时态逻辑，。

时态逻辑体系大致可以分为两大流派，即线性时态逻辑和分支时态逻辑。

比较两种时态逻辑时采用了特定的时态结构和特定的比较原则，且限定了分支时态逻辑公式的语法和语义，从而得出了不被第章基础理论赞成的结论，即在证明并发程序的些性质时线性时态逻辑要优于分支时态逻辑，而在证明非确定性的些性质时分态时序逻辑要优于线性时态逻辑，且在些方面，线性时态逻辑要比分支时态逻辑强。

和，对分支时态逻辑的语法和语义作适当的扩充，克服了上述缺点，并且融两种时态逻辑于个语言之中，从而又克服了对时态逻辑公式的二义性解释。