| 离散时间区间时序逻辑可满足性的判定 |
| |
| 引用本文： | 朱维军,张海宾,周清雷.离散时间区间时序逻辑可满足性的判定[J].电子学报,2010,38(5):1039-1045. |
| |
| 作者姓名： | 朱维军 张海宾 周清雷 |
| |
| 作者单位： | 1.西安电子科技大学计算机学院，陕西西安 710071；2.郑州大学信息工程学院，河南郑州 450052 |
| |
| 基金项目： | 国家高技术研究发展计划(863计划)，河南省重大科技攻关计划，陕西省科技攻关计划 |
| |
| 摘 要： | 目前还没有模型检查的方法自动检测模型是否满足时间区间时序逻辑描述的性质.我们约束时间域到离散时间,证明了离散时间区间时序逻辑的可满足性是可判定的,因而是可模型检查的.提出了时间正则图模型,通过从离散时间区间时序逻辑到时间正则图的构造,提出了基于该逻辑的判定算法,该算法可以推广到其它的时序逻辑模型检查,并优于现有的基于自动机的时序逻辑判定方法.
|
| 关 键 词： | 模型检查 离散时间区间时序逻辑 时间正则图 可满足性判定 |
| 收稿时间： | 2009-6-9 |
| 修稿时间： | 2009-9-24 |
On the Decidadiliyt of Satisfiability of Discrete TITL Formulae |
| |
| ZHU Wei-jun,ZHANG Hai-bin,ZHOU Qing-lei.On the Decidadiliyt of Satisfiability of Discrete TITL Formulae[J].Acta Electronica Sinica,2010,38(5):1039-1045. |
| |
| Authors: | ZHU Wei-jun ZHANG Hai-bin ZHOU Qing-lei |
| |
| Affiliation: | 1.School of Computer Science,Xidian University.Xi'an,Shaanxi 710071,China;2.School of Information Engineering,Zhengzhou University,Zhengzhou,Henan 450052,China |
| |
| Abstract: | There is no method available for checking whether a model satisfies a property described by a timed interval temporal logic (TITL) formula.In this paper,we formalize a novel model named timed normal form graph (TNFG).In addition,we give a procedure to construct TNFG from discrete TITL formula,and prove that the satisfiability of discrete TITL is decidable.The new method can be also used for other types of temporal logic and it is superior to the existing approaches. |
| |
| Keywords: | model checking discrete timed interval temporal logic timed normal form graph satisfiability checking |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《电子学报》浏览原始摘要信息 |
|
点击此处可从《电子学报》下载全文 |
|
