基于可能性测度的线性时间性质模型检测
计算机科学中的逻辑
2016-09-27 v2
摘要
我们研究基于可能性测度的可能Kripke结构中的LTL模型检测。首先，介绍了可能Kripke结构及其相关可能性测度的概念，然后研究了有限可能Kripke结构中可达性和重复可达性线性时间性质的模型检测。引入了标准安全性和ω-正则性质，详细研究了使用有限自动机验证正则安全性和ω-正则性质。结果表明，有限可能Kripke结构中正则安全性和ω-正则性质的验证可以转化为本文引入的乘积可能Kripke结构中可达性和重复可达性性质的验证。给出了若干例子说明所提出的方法。
引用
@article{arxiv.1203.2241,
title = {Model-Checking of Linear-Time Properties Based on Possibility Measure},
author = {Yongming Li and Lijun Li},
journal= {arXiv preprint arXiv:1203.2241},
year = {2016}
}
备注
22pages,5 figures