离散时间区间时序逻辑可满足性的判定
On the Decidability of Satisfiability of Discrete TITL Formulae作者机构：西安电子科技大学计算机学院陕西西安710071 郑州大学信息工程学院河南郑州450052
出 版 物：《电子学报》 (Acta Electronica Sinica)
年 卷 期：2010年第38卷第5期
页 面：1039-1045页
核心收录：
学科分类：08[工学] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）]
基 金：国家863高技术研究发展计划(No.2007AA010408) 河南省重大科技攻关计划(No.092101220104) 陕西省科技攻关计划(No.2009K01-36)
主 题：模型检查 离散时间区间时序逻辑 时间正则图 可满足性判定
摘 要：目前还没有模型检查的方法自动检测模型是否满足时间区间时序逻辑描述的性质.我们约束时间域到离散时间,证明了离散时间区间时序逻辑的可满足性是可判定的,因而是可模型检查的.提出了时间正则图模型,通过从离散时间区间时序逻辑到时间正则图的构造,提出了基于该逻辑的判定算法,该算法可以推广到其它的时序逻辑模型检查,并优于现有的基于自动机的时序逻辑判定方法.
维普期刊数据库
同方期刊数据库