命题投影时序逻辑并发建模与自动验证
Modeling and verification of concurrent systems using propositional projection temporal logic作者机构：西安电子科技大学计算机学院陕西西安710071 郑州大学信息工程学院河南郑州450052
出 版 物：《华中科技大学学报（自然科学版）》 (Journal of Huazhong University of Science and Technology(Natural Science Edition))
年 卷 期：2010年第38卷第8期
页 面：77-80页
核心收录：
学科分类：08[工学] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）]
基 金：国家高技术研究发展计划资助项目(2007AA010408) 中国高校基本科研业务专项资金资助项目(JY10000903014) 河南省重大科技攻关计划资助项目(092101210104) 陕西省科技攻关计划资助项目(2009K01-36)
主 题：模型检测 时序逻辑 可计算性与判定性 命题投影时序逻辑 并发模型 统一逻辑框架
摘 要：针对目前尚无模型检测方法对区间并发模型进行区间性质的自动验证的情况,采用命题投影时序逻辑中具有特定结构的一类公式来建立系统的区间并发模型,该逻辑的任意公式可以描述模型需要满足的区间性质,通过归约为已有的逻辑公式可满足性判定算法,证明了命题投影时序逻辑统一框架模型检测是可判定的,从而得到了其自动验证方法,并给出了一个验证实例.
维普期刊数据库
同方期刊数据库