异构多智能体系统模型检查

近几年,模型检查作为一种自动化系统验证方法,已被应用于多智能体系统的验证.由此延伸出的规约描述语言——交替时态逻辑（ATL）,也被给予了高度关注.根据智能体是否可以看到全局信息分为不完全信息和完全信息;根据智能体是否可以记录历史信息分为无记忆能力和无限记忆能力,提出了四种经典的策略类型.这些策略类型是通过ATL的语义进行刻画的.然而,在一个多智能体系统中,考虑完全信息和无限记忆能力时,所有智能体都只能选择这一种策略类型;在考虑不完全信息或无记忆能力时,仅在联合模态操作<>φ和的[[A]]φ里出现的智能体具备这种策略类型,而其他智能体还是完全信息和无限记忆能力策略类型.这可能会导致嵌套联合模态操作中智能体策略类型的不一致,且智能体策略类型取决于逻辑公式和逻辑的语义.而在实际多智能体系统中,智能体的策略类型往往取决于系统本身,且不同智能体具有不同的策略类型,即智能体策略类型是异构的,这种多智能体系统被称为异构多智能体系统.针对这些问题,本文提出了一种在语法层对智能体策略类型进行刻画的系统模型,即带类型解释系统.带类型解释系统在已有的解释系统中为每个智能体引入\"策略类型\"这一属性,允许不同智能体具备不同的策略类型.带类型解释系统可用于异构多智能体系统的建模.针对新提出的系统模型,对ATL语义进行了研究,设计了ATL模型检查算法,实现了相应的模型检查工具ShTMC.     

多智能体系统中的协商模型

目前,对多智能体系统的应用多是以开放的、复杂的、变化的网络为平台,为了更好地与环境相匹配,同对提高智能体之间协商的效率,从全局与单个智能体两方面着手,提出了一种新的MAS全局模型,并相应地提出了全局协调Agent的三维模型以及智能体之间的协商模型。通过这一系列模型的模拟实现,证明了此协商模型是正确的与接近自然的。从理论上基本上解决了与当前流行的基于网络的各种先进的智能系统,分布式问题求解等领域的衔接,因而有一定的指导意义并具有广阔的发展前景。     

基于黑板模型的多智能体合作学习

Q学习算法要求智能体无限遍历每个状态-动作转换,因此在涉及状态-动作空间非常大的应用问题时,导致收敛速度非常慢。借助多智能体的合作学习,智能体之间基于黑板模型的方法通过开关函数相互协调合作,可以更快地定位那些有效的状态-动作转换,避免了无效的更新,从而以较小的学习代价加快了Q表的收敛速度。     

钢铁工业过程多智能体系统研究

结合钢铁工业过程的特点，通过分析冶金过程工业智能控制的发展状况，提出了采用多Ａｇｅｎｔ技术，建立钢铁工业多智能体系统，从而实现钢铁工业的分布式智能控制，分析了系统建立的必要性和可行性，并给出了该系统的结构和实现方法。     

多智体系统时序认知规范的SPIN模型检测

SPIN模型检测器主要用来检测线性时序逻辑描述的规范,而多智体系统的规范采用时序认知逻辑描述比较方便。本文着重讨论了如何利用SPIN模型检测线性时序认知逻辑的方法,根据局部命题的理论,将模型检测知识算子和公共算子表述的规范规约为模型检测线性时序逻辑的问题,从而使SPIN的检测功能由线性时序逻辑扩充到线性时序认知逻辑。本文通过一个RPC协议分析实例来说明模型检测线性时序认知逻辑的方法。     

基于观测器的线性时变时滞多智能体系统一致性

针对系统状态不可测和具有通信时延的线性多智能体系统,提出一种基于观测器的一致性控制算法.设计观测器用于解决智能体状态不可测的问题,在观测器的基础上,提出一种控制协议来实现带时变时延的线性多智能体系统一致性.利用模型转换的方式将原系统转换为新的模型系统,在此基础上,构造Lyapunov-Krasovskii函数并分析系统稳定性,通过求解线性矩阵不等式获取控制器系数矩阵.最后通过Matlab数值仿真验证所提出方法的有效性.     

基于多智能体协商的电子市场原料配置模型

基于市场交互机制建立了多智能体之间的协商模型,每个企业看作自利智能体运行生产规划算法购置原料并安排生产,市场智能体作为中间人通过市场规则对智能体的个体选择进行综合并将综合后的结果反馈给每个智能体,这一机制较好地总结了各个终端智能体的个体信息,从而优化个体行为。给出了电子市场原料配置的定价算法和分配算法。仿真试验结果表明,基于市场机制的多智能体协商方法使得每个智能体的效用都有所改善,从而改善了系统的全局收益。     

群智能在多智能体系统中的应用研究进展

群智能算法是受群居性昆虫群体的集体行为启发而设计的分布式问题求解方法,将它应用到多智能体系统,旨在提高系统的鲁棒性、灵活性和自适应性。以群智能在多智能体系统中的应用为线索,首先介绍群智能的核心机制,然后从多智能体系统通信机制、协作技术、学习问题及体系结构建立这几个方面总结群智能理论在多智能体系统中的已有工作。最后分析和讨论了群智能方法在多智能体系统应用中存在的问题,并提出今后的工作展望。     

精确估计下的多智能体系统漏斗复合控制

针对一类具有时变扰动的非线性多智能体系统, 研究其在有向拓扑下的一致性跟踪问题, 提出一种基于精确估计的复合自适应预设有限时间(PFT)漏斗控制方法. 首先, 构建一种新的PFT漏斗控制, 使跟踪误差约束在PFT漏斗边界内. 其次, 采用神经网络(NN)逼近系统的未知非线性, 并利用NN逼近信息设计扰动观测器, 建立基于NN和扰动观测器的复合估计模型, 将得到的预测误差引入NN权值的复合更新律中, 实现对未知非线性和时变扰动的精确估计. 然后, 利用动态面技术和误差补偿机制, 在解决传统反步法“计算爆炸”问题的同时, 消除滤波器误差对系统的影响. 最后, 通过Lyapunov稳定性理论证明闭环系统所有信号均为有界的, 并通过仿真实验验证控制方法的有效性.     

一种基于多智能体的电力零售市场模型

使用多智能体技术,建立了一种电力零售市场的模型.该模型包括了4类市场成员智能体:电力交换公司智能体、发电公司智能体、电力零售商智能体和电力用户智能体.     

Verification of heterogeneous multi-agent system using MCMAS

The focus of the paper is how to model autonomous behaviours of heterogeneous multi-agent systems such that it can be verified that they will always operate within predefined mission requirements and constraints. This is done by using formal methods with an abstraction of the behaviours modelling and model checking for their verification. Three case studies are presented to verify the decision-making behaviours of heterogeneous multi-agent system using a convoy mission scenario. The multi-agent system in a case study has been extended by increasing the number of agents and function complexity gradually. For automatic verification, model checker for multi-agent systems (MCMAS) is adopted due to its novel capability to accommodate the multi-agent system and successfully verifies the targeting behaviours of the team-level autonomous systems. The verification results help retrospectively the design of decision-making algorithms improved by considering additional agents and behaviours during three steps of scenario modification. Consequently, the last scenario deals with the system composed of a ground control system, two unmanned aerial vehicles, and four unmanned ground vehicles with fault-tolerant and communication relay capabilities.     

Tableau-based automata construction for dynamic linear time temporal logic*

We present a tableau-based algorithm for obtaining a Büchi automaton from a formula in Dynamic Linear Time Temporal Logic (DLTL), a logic which extends LTL by indexing the until operator with regular programs. The construction of the states of the automaton is similar to the standard construction for LTL, but a different technique must be used to verify the fulfillment of until formulas. The resulting automaton is a Büchi automaton rather than a generalized one. The construction can be done on-the-fly, while checking for the emptiness of the automaton. We also extend the construction to the Product Version of DLTL.*This research has been partially supported by the project MIUR PRIN 2005 ‘Specification and verification of agent interaction protocols’.     

一种基于投影时序逻辑模型检测的入侵检测方法

基于时序逻辑模型检测的入侵检测技术降低了误用检测的漏报率,然而却几乎不能描述并发攻击和分段攻击,因而对这些复杂的攻击模式漏报率仍很高。本文针对该问题,提出了一种基于投影时序逻辑模型检测的入侵检测方法。对若干复杂攻击实例的检测表明,新方法可有效降低对并发攻击和分段攻击的漏报率。     

有界模型检测同步多智体系统的时态认知逻辑

提出在同步的多智体系统中验证时态认知逻辑的有界模型检测(bounded model checking,简称BMC)算法.基于同步解释系统语义,在时态逻辑CTL*的语言中引入认知模态词,从而得到一个新的时态认知逻辑ECKL_n.通过引入状态位置函数的方法获得同步系统的智能体知识,避免了为时间域而扩展通常的时态认知模型的状态及迁移关系编码.ECKL_n的时态认知表达能力强于另一个逻辑CTLK.给出该算法的技术细节及正确性证明,并用火车控制系统实例解释算法的执行过程.     

工作流模型检测研究

研究了利用模型检测技术对WPDL描述的工作流模型的正确性的检测方法，提出了工作流模型的正确性检测指标及其CTL*公式描述，以及博弈算法实现工作流模型的正确性检测，该方法的特点是具有较强的检测指标描述能力及高效的检测算法。     

Web服务的形式化验证

将Web服务组合建模为多智能体系统,采用时态知识逻辑模型检测工具MCTK刻画贷款协议Web服务实例,并验证相关的时态知识规范。在同一实验环境下,采用另一种时态知识逻辑模型检测工具MCMAS进行建模,并验证该实例。实验结果表明,基于MCTK的Web服务模型检测方法比基于MCMAS的方法更有效。     

一种自动的形式化验证技术-模型检测

模型检测是针对有限状态系统行为的逻辑性质的一种自动验证技术,已有许多工业应用.其主要缺陷是空间爆炸问题.本文通过一简单实例介绍其基本思想、检测步骤和相关理论,给出一些处理状态空间爆炸问题的优化技术,并与其它验证方法进行了比较,最后简单介绍了软件模型检测的新进展.     

一个命题投影时序逻辑符号模型检测器

现有模型检测工具的形式化规范语言,如计算树逻辑(computation tree logic,简称CTL)和线性时序逻辑(linear temporal logic,简称LTL)等的描述能力不足,无法验证ω正则性质.提出了一个命题投影时序逻辑(propositional projection temporal logic,简称PPTL)符号模型检测工具——PLSMC(PPTL symbolic model checker)的设计与实现过程.该工具基于著名的符号模型检测系统NuSMV,实现了PPTL的符号模型检测算法.PLSMC的规范语言PPTL具有完全正则表达能力,这使得定性性质和定量性质均可被验证.此外,PLSMC可以有效地缓解模型检测工具中容易发生的状态空间爆炸问题.最后,利用PLSMC对铁路公路交叉道口护栏控制系统的安全性质和周期性性质进行验证.实验结果表明,PPTL符号模型检测工具扩充了NuSMV系统的验证能力,使得时间敏感、并发性和周期性等实时性质可以被描述和验证.     

QRDChecker:一个QRDC模型检验工具

反应式系统通常是不终止的,其行为定义为系统状态的无限序列的集合.形式化验证时,检验需求一般使用时序逻辑给出.当使用诸如LTL(linear temporal logic)这样的逻辑时,由于这类逻辑的模型同样是无限序列,系统与需求之间的满足性关系可以简单定义为集合的包含关系.但是,当使用时段时序逻辑(interval temporal logic)作为说明逻辑时,由于逻辑模型的有限性,使得上面的满足关系不再适用.称这类有限序列集合表达的性质为有限性性质.对于不同的有限性性质,它们对应的满足性关系是有区别的.针对两类有限性定义了它们各自的满足性关系,并将这两种关系统一为一个更一般的满足性关系.在此基础上,提出模型检验这两类性质的算法,并将其实现为一个针对时段时序逻辑QRDC(quantified RDC (restricted duration calculus))的检验工具QRDChecker.QRDChecker可以检验QRDC公式在连续时间模型和离散时间模型下的有效性.在离散时间条件下,它还可以将QRDC公式转换成模型检验系统Spin能够接受的自动机的形式,从而可以检查反应式系统是否满足用QRDC公式表达的性质.