支持Stutter-不变性的命题区间时序逻辑  

Stutter-invariant propositional interval temporal logic

作　　者：杨琛[1,2,3] 段振华[1,2] 

机构地区：[1]西安电子科技大学计算理论与技术研究所,陕西西安710071 [2]西安电子科技大学综合业务网理论及关键技术国家重点实验室,陕西西安710071 [3]武汉大学软件工程国家重点实验室,湖北武汉430072

出　　处：《西安电子科技大学学报》2011年第2期151-156,共6页Journal of Xidian University

基　　金：国家自然科学基金重大国际合作项目资助项目(60910004);国家自然科学基金资助项目(60433010;60873018);国家重点基础研究发展计划(973)资助项目(2010CB328102);武汉大学软件工程国家重点实验室开放基金资助项目(SKLSE20080713);中央高校基本科研业务费专项基金资助项目(JY10000903004)

摘　　要：为了将命题区间时序逻辑(PITL)应用于组合验证,并降低组合产生的状态爆炸风险,提出了支持Stutter-不变性的命题区间时序逻辑PITLst.PITLst继承了PITL的结构相关性,可表达所有PITL能够表达的Stutter-不变性质,支持模块抽象约简系统规模,降低了状态爆炸风险.自动加油站模型的组合验证实例表明,PITLst可有效应用于组合验证技术.To apply the propositional interval temporal logic（PITL） in compositional verification with minor risk of state-exlopsion,a stutter-invariant PITL（PITLst） is proposed,which is structure-related since it inherits the structural relativity of PITL operators much like constructs of imperative programming,such as chop operator for sequential composition and projection opertor for iteration,thus when used as a specification language PITLst can specify the structure of concurrent systems.Moreover,it is shown that PITLst can express all stutter-invariant properties expressible in PITL,so it surpports modular abstraction for compositional verification.In this way,the overall system is of small size,so the risk of state-explosion is accordingly reduced.In addition,an automatic gas station system,as an example,is compositionally verified against PITLst properties,which illustrates that PITLst well supports compositional verfication.

关 键 词：模型检测 时序逻辑 状态爆炸 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]