邓楠轶，张兴兴，李永明

(陕西师范大学 计算机科学学院，陕西 西安710119)

广义可能性计算树逻辑的不动点语义

邓楠轶，张兴兴，李永明*

(陕西师范大学 计算机科学学院，陕西 西安710119)

计算树逻辑的不动点语义在其对应的符号模型检测方法中具有重要意义。给出广义可能性计算树逻辑的不动点语义解释，并利用归纳法证明此不动点为最大或最小不动点。结论表明,广义可能性计算树逻辑的不动点语义具有不同于经典情形的形式。

广义可能性测度；计算树逻辑；不动点语义；模型检测

21世纪的信息技术革命愈演愈烈，随着计算机软硬件系统日趋复杂，如何保证其正确性成为系统设计者和应用者不得不关心的问题。为此提出的诸多验证理论和方法中，模型检测[1-4]因其自动化程度高而引人注目。模型检测是一种形式化的自动验证技术，其基本思想是：对状态空间进行穷举搜索从而验证系统是否满足其设计规范。模型检测的一般步骤是：(1)抽象出系统的数学模型；(2)给出能够描述该系统性质的语言；(3)用模型检测算法进行验证。如果构造的模型满足系统的性质则返回“成功”，否则返回“失败”，并给出反例。

经典的模型检测已广泛应用于软硬件系统的正确性验证，但随着系统日益复杂，在验证过程中不可避免会出现一些不确定的信息，而系统中这些不确定的信息有可能会导致非常严重的后果。为了更好地处理这些不确定信息，一些学者提出了状态迁移模型的量化扩展，比如在状态中加入时间[1]，或者在模型中考虑概率[1]、可能性[5]、多值[6-7]或者统计信息[8]。……