###
Journal of Software:2012.23(11):2835-2861

多智体系统中约简状态空间的限界模型检测算法
周从华,叶萌,王昌达,刘志锋
(江苏大学 计算机科学与通信工程学院,江苏 镇江 212013)
Bounded Model Checking Algorithm to Reduce the State Space in Multi-Agent Systems
ZHOU Cong-Hua,YE Meng,WANG Chang-Da,LIU Zhi-Feng
(School of Computer Science and Telecommunication Engineering, Jiangsu University, Zhenjiang 212013, China)
Abstract
Chart / table
Reference
Similar Articles
Article :Browse 4388   Download 3112
Received:June 04, 2012    Revised:August 12, 2012
> 中文摘要: 为了形式化描述多智体系统中与概率、实时、知识相关的性质,提出了一种概率实时认知逻辑PTCTLK.模型检测是验证多智体系统是否满足PTCTLK 公式的主要技术,状态空间爆炸是该技术实用化的主要瓶颈,为此提出一种PTCTLK的限界模型检测算法.其基本思想是,在有限的局部可达空间中逐步搜索属性成立的证据,从而达到约简状态空间的目的.首先,将PTCTLK 的模型检测问题转换为无实时算子的PBTLK 的模型检测问题;其次,定义PBTLK 的限界语义,并证明其正确性;然后,设计基于线性方程组求解的限界模型检测算法;最后,依据概率度量的演化规律,探索检测过程终止的判别准则.实例研究结果表明,与无界模型检测相比,在属性为真的证据较短的情况下,限界模型检测完成验证所需空间更小.
Abstract: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.
文章编号:     中图分类号:    文献标志码:
基金项目:国家自然科学基金(61003288, 61111130184); 教育部博士点基金(20093227110005); 江苏省自然科学基金(BK2010192) 国家自然科学基金(61003288, 61111130184); 教育部博士点基金(20093227110005); 江苏省自然科学基金(BK2010192)
Foundation items:
Reference text:

周从华,叶萌,王昌达,刘志锋.多智体系统中约简状态空间的限界模型检测算法.软件学报,2012,23(11):2835-2861

ZHOU Cong-Hua,YE Meng,WANG Chang-Da,LIU Zhi-Feng.Bounded Model Checking Algorithm to Reduce the State Space in Multi-Agent Systems.Journal of Software,2012,23(11):2835-2861