|
|||||
|
|
| 基于SPIN的LTL属性分解方法研究 | |
| 作者单位： | ;1.南京大学计算机软件新技术国家重点实验室;2.南京大学计算机科学与技术系 |
| 摘 要： | 提出一种基于模型检测工具SPIN的LTL属性分解方法以解决状态空间爆炸问题。根据逻辑和时序操作符常见的组合情况,讨论不同的属性分解模式,根据子属性构建的切片准则进行程序切片,利用SPIN对切片后的等价简化模型进行检测,从而将对原模型上属性的检测转化成对复杂度较低的子模型上各子属性的分别检测。实验结果表明,该方法具有一定的有效性。 |
| 关 键 词： | 线性时序逻辑属性 模型检测 属性分解 静态程序切片 |
STUDY ON SPIN-BASED LTL PROPERTY DECOMPOSITION |
|
| Abstract: | |
| Keywords: | |
| 本文献已被 CNKI 等数据库收录！ | |