命题投影时序逻辑并发建模与自动验证  

Modeling and verification of concurrent systems using propositional projection temporal logic

作　　者：朱维军[1,2] 张海宾[1] 周清雷[2] 

机构地区：[1]西安电子科技大学计算机学院,陕西西安710071 [2]郑州大学信息工程学院,河南郑州450052

出　　处：《华中科技大学学报（自然科学版）》2010年第8期77-80,共4页Journal of Huazhong University of Science and Technology(Natural Science Edition)

基　　金：国家高技术研究发展计划资助项目(2007AA010408);中国高校基本科研业务专项资金资助项目(JY10000903014);河南省重大科技攻关计划资助项目(092101210104);陕西省科技攻关计划资助项目(2009K01-36)

摘　　要：针对目前尚无模型检测方法对区间并发模型进行区间性质的自动验证的情况,采用命题投影时序逻辑中具有特定结构的一类公式来建立系统的区间并发模型,该逻辑的任意公式可以描述模型需要满足的区间性质,通过归约为已有的逻辑公式可满足性判定算法,证明了命题投影时序逻辑统一框架模型检测是可判定的,从而得到了其自动验证方法,并给出了一个验证实例.There exists no model checking method that can check automatically the interval properties for the interval models. Thus, a class of propositional projection temporal logic （PPTL） formulas with special structures is found to be able to describe the interval concurrent models. Besides, PPTL formulas can describe the interval properties too. By being reduced to the decidability problem of PPTL formulas, the model checking problem based on uniform framework of PPTL is proved to be decidable. And the automatic verification processes are given. An example is also given to illustrate the approach.

关 键 词：模型检测 时序逻辑 可计算性与判定性 命题投影时序逻辑 并发模型 统一逻辑框架 

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