题目：基于广义可能性测度的互模拟及CTL不动点语义

模型检测是对有穷状态系统，包括软硬件系统的形式化自动验证技术，1981年由Clarke和Emerson 以及Quielle和Sifakis 提出。其基本思想是：对状态空间进行穷举搜索来保证其性质的正确性。模型检测的一般步骤是：(1) 抽象出系统的数学模型；(2)给出能够刻画该系统性质的逻辑；(3) 用模型检测算法进行验证，如果所构造的模型满足系统的性质则返回成功，否则返回失败，并给出反例。

经典情况下，模型检测的基本模型是迁移系统，但计算机软硬件系统的复杂性日益增加，模型中状态转移之间常常存在很多不确定的信息。基于此，一些学者提出了状态迁移模型的量化扩展，如在状态中加入时间，或者在模型中引入概率、可能性、多值或统计。1965 年Zadeh 提出了模糊集理论。随后模糊和可能性测度得到了广泛的研究，它们是一种非可加性测度。最近李永明将可能性测度与模型检测结合起来，提出了基于可能性Kripke 结构的模型检测。 虽然可能性计算树逻辑的可表达性强于经典的计算树逻辑，但是它有一定的局限性。一些能被可能性测度理论描述的不确定性仍不能用可能性计算树逻辑来处理，此时需要更强的量化模型检测方法来处理可能性测度中的不确定性问题。鉴于此，李永明提出了广义可能性测度，并将它与模型检测结合，形成了基于广义可能性测度的模型检测理论。本文是此方向工作的延续，我们研究了基于广义可能性测度的互模拟，并给出广义可能性计算树逻辑的不动点语义，丰富和完善了基于广义可能性测度的模型检测理论和方法。

本文的主要工作如下:

1.首先，给出了广义可能性测度下的计算树逻辑的扩张、计算树逻辑的约简以及带回报的计算树逻辑的语构和语义。在经典互模拟和广义可能性测度的基础上讨论了广义可能性互模拟及其相关性质。

2.证明了GPoCTL、GPoCTL* 和GPoCTL-公式与具有互模拟关系的状态之间的等价关系，即给出了广义可能性互模拟的逻辑刻画形式。

3.广义可能性CTL的模型检测问题已有初步研究，为了进一步完善模型检测中的算法，本文给出其不动点语义解释，结论表明广义可能性计算树不动点语义与经典情况下的形式是不同的。