基于时态认知逻辑的Web服务模型检测

传统模型检测技术主要采用时态逻辑描述被验证的规范,人们较少注意多智能体认知逻辑的模型检测问题.而在分布式系统领域,系统和协议的规范很适合用认知逻辑来描述.Web服务是一个典型的分布式系统.把Web服务组合建模为多智能体系统,并成功采用我们实现的时态认知逻辑符号模型检测工具MCTK验证了SAS股票分析服务实例.同时采用WSAT,WS-Engineer和SPIN 3个模型检测工具在相同实验环境下验证了该实例,实验结果表明我们的Web服务模型检测方法不仅比这3个模型检测工具更高效,而且支持认知逻辑规范的验证,这是这3个模型检测工具所不具备的.     

多智体系统时态认知规范的模型检测算法

模型检测技术一直以来主要是检验用时态逻辑描述的规范,人们很少注意认知逻辑的模型检测问题,而在分布式系统领域,系统和协议的规范已广泛地采用知识逻辑来描述.着重研讨了时态认知逻辑的模型检测算法.在SMV(symbolic model verifier)模型检测器的基础上,根据知识的语义和集合理论,提出了多种检验知识和公共知识的算法,从而使SMV的检测功能由时态逻辑扩充到时态认知逻辑.这些方法也适用于其他以状态集合作为输出的模型检测方法和工具的功能扩充.     

Web服务的形式化验证

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

基于标记Büchi自动机的时态描述逻辑ALC-LTL模型检测

时态描述逻辑将描述逻辑的刻画能力引入到命题时态逻辑中,适合于在语义Web环境下对相关系统的时态性质进行刻画.为了对这些时态性质进行高效的验证,在ALC-LTL的基础上研究了时态描述逻辑的模型检测问题.一方面,使用时态描述逻辑ALC-LTL公式来表示待验证的时态规范;另一方面,在对系统建模时借助描述逻辑ALC对领域知识进行刻画.针对上述扩展后得到的模型检测问题,提出了基于自动机的ALC-LTL模型检测算法.模型检测算法由3个阶段组成:首先将时态规范的否定形式和系统模型分别构造成标记büchi自动机;接下来构造这两个自动机的乘积自动机,并将关于ALC的推理机制融入到乘积自动机的构造过程中;最后对该乘积自动机进行判空检测.与LTL模型检测相比,时态描述逻辑ALC-LTL的模型检测引入了描述逻辑的刻画和推理机制,可以在语义Web环境下对语义Web服务等复杂系统的时态性质进行刻画和验证.     

多主体系统时态认知规范的"On the Fly"模型检测算法研究

时态认知逻辑已被广泛应用于分布式系统和协议的规范描述，模型检测时态认知规范已成为一个新的研究领域，因此着重研讨时态认知规范的“On the Fly”模型检测算法．在“On the Fly”模型检测时态逻辑描述规范的基础上，根据自动机理论、深度优先方法和知识的语义，提出了“On the Fly”模型检测时态认知规范的算法，该算法在模型检测带有知识算子的时态规范时，在找到一个反例之前，往往只需构造系统的部分甚至小部分状态空间，从而避免了时态认知规范的模型检测中内存不足和状态爆炸等问题，实现了“On the Fly”模型检测时态认知规范，并且算法的复杂性是多项式时间的．最后，通过该方法在验证TMN密码协议中的应用来作为一个例子说明该方法的有效性．     

一种Web服务组合的认知模型检测方法

由于Web服务及其协同的动态性,开放多变的互联网运行环境,以及松耦合的服务开发模式所导致的开发和运行过程不确定性,使得Web服务组合的正确性和可靠性等可信性质难以得到保证.将Web服务组合抽象为多主体系统,提出业务流程执行语言BPEL的形式模型BSTS,设计并实现了从BPEL到BSTS的B2S转化算法,以及从BSTS到多主体系统模型检测工具MCMAS输入语言ISPL的S2I转化算法,从而实现Web服务组合的自动形式化建模,使得我们不仅可以验证Web服务组合的时态逻辑规范,而且还可以验证认知与合作等多主体系统特有的逻辑规范.我们实现了相关的模型检测工具原型MCWS,并用其对一个贷款核准服务实例进行建模和验证,实验结果显示了MCWS的有效性.     

基于有界限模型检验的服务建模与自动组合

针对面向服务架构(SOA)体系的Web服务数量快速增长现状,为实现大规模服务场景下高效自动组合Web服务来满足用户复杂需求问题,提出一种基于有界模型检验的Web服务组合方法.其中,Web服务被建模为有限状态自动机,众多Web服务构成服务社区,Web服务组合需求由线性时态逻辑公式描述,通过有界模型检验器的系统化搜索,该方...     

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

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

多智能体系统时态认知规范高效符号模型检测的算法研究

Clarke和McMillan提出了利用mu演算和OBDDs符号模型检测时态逻辑的方法.这些方法是非常有效的,能用于验证许多具有极大状态空间的实际系统(状态个数可以超过1020).但是,这些方法不能检测知识逻辑.而时态认知逻辑能更精确地描述分布式领域中系统和协议的规范.文章首先讨论了Kripke结构和mu演算的扩展,然后提出了利用扩展mu演算和OBDDs符号模型检测时态认知逻辑的方法.     

时态认知逻辑CTL＊K的符号化模型检查算法

时序认知逻辑是由时序逻辑和认知逻辑组合而成的逻辑,主要应用于多主体系统的规范定义.大多数时序认知逻辑是基于CTL的,表达能力有限.并且已知的一些模型检查算法存在内存不足和状态爆炸等问题.讨论了基于CTL*的时态认知逻辑cTL*K的语法、语义和模型,它能够在表达力很强的时态逻辑CTL*基础上描述智能体的知识、目标等意向特征.并给出了CTL*K的模型检查算法,其核心思想就是将CTL*K公式的检查问题转化为CTL*公式的模型检查问题,可以使检查的系统规模得以大幅度提高.并且将算法编码后容易集成到NuSMV模型检查器.     

基于多Agent的Web服务动态合成的研究

现有基于传统工作流的Web服务合成的研究,不能很好满足Web服务合成动态、分布 式的要求。将Web服务动态合成技术和多Agent技术结合,着重于合成服务流程执行阶段的监控和 异常处理,给出了基于多Agent技术的Web服务动态合成系统的框架MAS WS,描述了其中的关键技 术,包括Agent联邦动态组建、主动协作、服务流程分层管理、流程规划与执行交叉进行等,并分析了 MAS WS的优势。     

基于多agent协同的Web服务复合系统研究

主要研究和设计了一种基于多agent协同的Web服务复合系统(CoWEB).通过对"Web服务复合"这种新型分布计算应用模型特点和需求进行分析,提出了使用agent构建CoWEB系统的优势.接着,通过对CoWEB系统三个功能层的主要结构设计,以及系统整体特点的论述,表明该系统能较好地适应Web服务环境,并能较好地解决Web服务特有的异构、自治和动态性问题,得以实现可靠灵活的Web服务复合应用.     

基于Web使用挖掘的个性化学习推荐系统

针对当前E learning推荐系统存在的问题，引入多Agent（MAS）系统，提出一种基于Web使用挖掘的集成MAS与Web services的分布式智能推荐系统模型。该模型能动态生成基于用户使用信息的个性化链接页面，有效地帮助学员找到所需的资源信息。提出了一种基于最近最少使用策略的系统推荐算法，包括系统整体实现算法、系统聚类算法及推荐算法。实时性能分析显示该系统运行性能良好。     

Improving the security level of the FUSION@ multi-agent architecture

The use of architectures based on services and multi-agent systems has become an increasingly important part of the solution set used for the development of distributed systems. Nevertheless, these models pose a variety of problems with regards to security. This article presents the Adaptive Intrusion Detection Multi-agent System (AIDeMaS), a mechanism that has been designed to detect and block malicious SOAP messages within distributed systems built by service based architectures. AIDeMaS has been implemented as part of FUSION@, a multi-agent architecture that facilitates the integration of distributed services and applications to optimize the construction of highly-dynamic multi-agent systems. One of the main features of AIDeMaS is that is employs case-based reasoning mechanisms, which provide it with great learning and adaptation capabilities that can be used for classifying SOAP messages. This research presents a case study that uses the ALZ-MAS system, a multi-agent system built around FUSION@, in order to confirm the effectiveness of AIDeMaS. The preliminary results are presented in this paper.     

认识逻辑(1):关于知识和信念的逻辑框架

知识和信念是人工智能领域研究中经常涉及到的两个重要概念。本文讨论了知识和信念的涵义与关系，定义了认识逻辑系统ＥＩ，讨论了它的语法和语义，证明了认识逻辑ＥＬ不但是可靠的而且是完备的，认为逻辑ＥＬ不但可以用来描述人类的认识过程，还可以用于对常识推理以及分布式系统的形式化描述。     

B2B collaboration through web services-based multi-agent system

Web services open a door for better B2B collaboration in large distributed environment such as Internet. Process-oriented systems like workflow management systems have been taking the main role for web service-based B2B collaboration in such an environment. However, conventional workflow management systems don’t offer complete solutions for B2B collaborations considering many unsolved issues such as security, trust and complex and flexible interaction handling. In this paper, we propose a web service-based multi-agent platform, which can be used as a complementary solution for B2B collaborations. It fits naturally into the B2B interaction model and provides a very loosely coupled open system architecture.     

一个基于偏序事件结构的Web服务模型及其形式化组装

随着Internet的发展,服务化和Web化趋势使得一个基于Web的分布式软件服务计算环境正在形成;同时随着大规模应用需求的不断涌现,单个的Web服务往往不能很好地满足一些复杂的应用。因此Web服务之间的集成组装就显得尤为重要。分析Web服务的交互和协同行为可以发现,分布性和并发性是基于软件服务分布计算系统的本质特征。这就往往使得组装的正确性难以得到保证,从而需要提供一定的手段加以支持;同时,基于软件服务分布计算系统的效率问题也值得关注。我们认为,利用偏序关系对这些问题加以处理是一种理想和有效的手段;而同时我们发现,在服务的组装中,服务与服务之间存在着一种自然的偏序关系。本文基于此,从形式化的角度研究了软件服务及其组装,提出了一种基于偏序事件多集的Web服务的形式化模型。本文从服务内部事件而不仅仅是服务的角度来考察并发问题,这使服务内和服务问的更多的事件可以并行执行,并使得组装后的系统可以更高效地进行实施,从而使得Web服务的并发拉度变细;在此基础上给出了一种服务组装语言和规则,以确保在组装过程中出现的局部变化不影响整体的Web服务的正确组装,从而能够从形式化的角度来规范Web服务的集成组装,使其正确性和效率能够得到保证。     

基于工作流的电信业务开发系统模型

随着Web服务技术的发展,Web服务已经成为集成电信网、移动网、互联网上分布和异构应用的通用技术。基于流程的Web服务组合语言未考虑业务规则的分离,不支持流程中不确定的动态部分的抽象和封装,因此该文提出了将规则系统应用到工作流中的业务开发系统模型,从而为服务提供商进行电信新业务开发和生成提供了快速有效的途径。