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

在广义可能性测度下,提出了广义可能性Kripke结构来描述系统的量化行为。在广义可能性Kripke结构下重新定义了线性时序逻辑的语构和语义,研究了线性时间属性的最终可达性、限制可达性、重复可达性等模型检测问题。本文所获得的结果扩大了可能性测度在模型检测中的应用范围。