在广义可能性测度下,提出了广义可能性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.