主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2018年第12期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
周从华,叶萌,王昌达,刘志锋.多智体系统中约简状态空间的限界模型检测算法.软件学报,2012,23(11):2835-2861
多智体系统中约简状态空间的限界模型检测算法
Bounded Model Checking Algorithm to Reduce the State Space in Multi-Agent Systems
投稿时间:2012-06-04  修订日期:2012-08-12
DOI:10.3724/SP.J.1001.2012.04304
中文关键词:  多智体系统  模型检测  限界模型检测  状态空间爆炸
英文关键词:multi-agent system  model checking  bounded model checking  state space explosion
基金项目:国家自然科学基金(61003288, 61111130184); 教育部博士点基金(20093227110005); 江苏省自然科学基金(BK2010192)
作者单位E-mail
周从华 江苏大学 计算机科学与通信工程学院,江苏 镇江 212013 chzhou@ujs.edu.cn 
叶萌 江苏大学 计算机科学与通信工程学院,江苏 镇江 212013  
王昌达 江苏大学 计算机科学与通信工程学院,江苏 镇江 212013  
刘志锋 江苏大学 计算机科学与通信工程学院,江苏 镇江 212013  
摘要点击次数: 3838
全文下载次数: 2840
中文摘要:
      为了形式化描述多智体系统中与概率、实时、知识相关的性质,提出了一种概率实时认知逻辑PTCTLK.模型检测是验证多智体系统是否满足PTCTLK 公式的主要技术,状态空间爆炸是该技术实用化的主要瓶颈,为此提出一种PTCTLK的限界模型检测算法.其基本思想是,在有限的局部可达空间中逐步搜索属性成立的证据,从而达到约简状态空间的目的.首先,将PTCTLK 的模型检测问题转换为实时算子的PBTLK 的模型检测问题;其次,定义PBTLK 的限界语义,并证明其正确性;然后,设计基于线性方程组求解的限界模型检测算法;最后,依据概率度量的演化规律,探索检测过程终止的判别准则.实例研究结果表明,与界模型检测相比,在属性为真的证据较短的情况下,限界模型检测完成验证所需空间更小.
英文摘要:
      In order to specify properties relating to probability, real time, and knowledge on multi-agent systems, a logic system PTCTLK is proposed. Model checking is an automatic technique for checking if a multi-agent system satisfies a PTCTLK formula. The state explosion problem is the key obstacle in checking the feasibility of the model. In this paper, a bounded model checking algorithm for PTCTLK is proposed. First the model checking of PTCTLK is reduced to the model checking of PBTLK, which does not contain real time operators. Second, the bounded semantics of PBTLK is defined and its correctness is proven. Third, the bounded model checking procedure of PBTLK is transformed into a linear equation. Finally, the paper discusses the law of increasing of probability measure, and some termination criterions are given. The case study shows that compared with the unbounded model checking, if the length of the witness is short, then the bounded model checking needs less space.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利