基于广义可能性测度的可达性问题的模型检测  

Model Checking of Reachability Problems Based on Generalized Possibility Measures

作　　者：马占有[1,2] 李永明[1] 

机构地区：[1]陕西师范大学计算机科学学院,陕西西安710062 [2]北方民族大学计算机科学与工程学院,宁夏银川750021

出　　处：《模糊系统与数学》2014年第6期88-97,共10页Fuzzy Systems and Mathematics

基　　金：国家自然科学基金资助项目(60873119);北方民族大学项目(2014xb213)

摘　　要：在广义可能性测度下,提出了广义可能性Kripke结构来描述系统的量化行为。在广义可能性Kripke结构下重新定义了线性时序逻辑的语构和语义,研究了线性时间属性的最终可达性、限制可达性、重复可达性等模型检测问题。本文所获得的结果扩大了可能性测度在模型检测中的应用范围。A generalized possibitistic Kripke structure over the generalized possibility measure is proposed to describe the quantitative behaviors of systems. The syntax and semantics of linear temporal logic are redefined in the context of the generalized possibilistic Kripke structure. We then analyzed some properties of the linear time. i.e. the eventual reachability, the constraint reachability and the repeated reachability, since they are common problems in model checking. The results obtained in this paper expand the scope of the application of model checking based on possibility measures.

关 键 词：模型检测 广义可能性测度 KRIPKE结构 可达性 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]