基于广义可能性度量的模糊线性时间属性定量模型检测

Yongming Li

基于广义可能性度量的模糊线性时间属性定量模型检测

计算机科学中的逻辑 2016-01-26 v1

作者: Yongming Li

摘要

基于可能性度量的线性时间属性模型检测在先前工作（Y. Li and L. Li, Model checking of linear-time properties based on possibility measure, IEEE Transactions on Fuzzy Systems, 21(5)(2013), 842-854）中已被研究。然而，先前工作考虑的线性时间属性是经典且定性的，系统的可能性信息完全未被考虑。本文研究基于广义可能性度量的模糊线性时间属性定量模型检测。系统模型以及系统需遵循的属性均使用可能性信息描述，以识别模型/属性中的不确定性。系统由广义可能性Kripke结构（简称GPKS）建模，属性由模糊线性时间属性描述。具体地，引入并研究了GPKS中关于可达性、总是可达性、约束可达性、重复可达性和持久性的模糊线性时间属性。引入GPKS中的模糊正则安全属性和模糊 $\omega-$ 正则属性，并深入研究了使用模糊有限自动机验证模糊正则安全属性和模糊 $\omega-$ 正则属性。已证明有限GPKS中模糊正则安全属性和模糊 $\omega-$ 正则属性的验证可转化为本文引入的乘积GPKS中(总是)可达性属性和重复可达性(持久性)属性的验证。给出了若干例子以说明本文提出的方法。

关键词

定量模型检测广义可能性度量模糊线性时间属性广义可能性Kripke结构模糊正则安全属性模糊ω-正则属性模糊有限自动机可达性属性

引用

@article{arxiv.1601.06504,
  title  = {Quantitative Model Checking of Linear-Time Properties Based on Generalized Possibility Measures},
  author = {Yongming Li},
  journal= {arXiv preprint arXiv:1601.06504},
  year   = {2016}
}

备注

arXiv admin note: text overlap with arXiv:1409.6466

基于广义可能性度量的模糊线性时间属性定量模型检测

摘要

关键词

引用

备注

相关论文