首页> 外文学位 >Model-checking of distributed autonomous agents using logic programming.
【24h】

Model-checking of distributed autonomous agents using logic programming.

机译:使用逻辑编程对分布式自治代理进行模型检查。

获取原文
获取原文并翻译 | 示例

摘要

Systems of autonomous agents providing automated services over the Web are fast becoming a reality. Often these multi-agent systems (MAS) are constructed using procedural architectures providing a framework for connecting agents that perform specific tasks. The designer codes the tasks for each agent and uses the framework to connect the agents into a MAS. The Cougaar Cognitive Agent Architecture is an example of such a framework. This approach does not provide easy verification of global properties of constructed agent systems. An alternate approach to building MAS describes the agent system in a declarative language that directly translates to a logical model. Languages such as AgentSpeak, based on the semantics of the Belief-Desire-Intention (BDI) paradigm for describing agents, use this approach. This approach allows for easy verification of logical properties of the MAS, but requires that the logical model be implemented using a special purpose interpreter or compiler. Also fault tolerance and inter-agent communications are not addressed by declarative agent languages. Frameworks like Cougaar incorporate these features in the framework infrastructure so that the designer can assume a certain level of service.; I outline here a methodology based on logic programming for modeling procedural agent frameworks using the Cougaar Architecture as an example. This methodology directly translates Cougaar systems into a state transition system. I then show how global properties of a Cougaar system can be specified as temporal logic formulae and outline a GCTL* temporal logic model checker which can be used to verify these properties. Within the community studying MAS, BDI logic is the preferred logic for expressing properties of MAS. This is a multi-modal logic which adds modalities for beliefs, desires, and intentions to CTL* logic. I also show how the GCTL* model checking system can be extended to BDI logic. The BDI extension to the model checker allows for direct verification of BDI logic properties of an MAS. I contrast BDI models to Cougaar models and suggest ways in which they may be integrated. Finally, I present a four agent Cougaar system for resource bound order processing and illustrate some verified properties of this system.
机译:通过Web提供自动化服务的自治代理系统正在迅速成为现实。通常,这些多代理系统(MAS)是使用过程体系结构构建的,该体系结构提供了用于连接执行特定任务的代理的框架。设计人员为每个代理编码任务,并使用框架将代理连接到MAS。 Cougaar认知代理体系结构就是这种框架的一个示例。此方法无法轻松验证已构建代理系统的全局属性。构建MAS的另一种方法是使用声明性语言描述代理系统,该声明性语言直接转换为逻辑模型。诸如AgentSpeak之类的语言基于用于描述代理的Belief-Desire-Intention(BDI)范式的语义而使用。这种方法可以轻松验证MAS的逻辑属性,但是需要使用专用解释器或编译器来实现逻辑模型。声明性代理语言也未解决容错和代理间通信。诸如Cougaar之类的框架将这些功能合并到框架基础结构中,以便设计人员可以承担一定级别的服务。我在这里概述一种基于逻辑编程的方法,该方法使用Cougaar体系结构作为示例来对过程代理框架进行建模。这种方法直接将Cougaar系统转换为状态转换系统。然后,我将展示如何将Cougaar系统的全局属性指定为时间逻辑公式,并概述可用于验证这些属性的GCTL *时间逻辑模型检查器。在研究MAS的社区中,BDI逻辑是表达MAS属性的首选逻辑。这是一种多模式逻辑,它为CTL *逻辑增加了信念,愿望和意图的模式。我还将展示如何将GCTL *模型检查系统扩展到BDI逻辑。模型检查器的BDI扩展允许直接验证MAS的BDI逻辑属性。我将BDI模型与Cougaar模型进行了对比,并提出了整合它们的方法。最后,我提出了一种用于资源绑定订单处理的四代理Cougaar系统,并说明了该系统的一些经过验证的属性。

著录项

  • 作者

    Pokorny, Louis Robert.;

  • 作者单位

    State University of New York at Stony Brook.;

  • 授予单位 State University of New York at Stony Brook.;
  • 学科 Computer Science.
  • 学位 Ph.D.
  • 年度 2005
  • 页码 81 p.
  • 总页数 81
  • 原文格式 PDF
  • 正文语种 eng
  • 中图分类 自动化技术、计算机技术;
  • 关键词

  • 入库时间 2022-08-17 11:41:44

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号