为了解决复杂计算机系统的验证问题,确保系统的正确性与可靠性,人们提出了模型检测方法.该方法于1981年首次被Clark和Emerson提出,是一种形式化的自动验证技术,其验证能够贯穿系统开发的整个过程,此方法主要分为以下三个过程:首先,抽象出系统的数学模型;其次,形式化描述需要验证的属性;最后,通过模型检测算法验证系统是否满足该属性,若满足将返回是;若不满足将给出一个反例.经典的模型检测只是针对完全确定的系统,但现实中却很少存在这样的系统.于是,人们开始考虑将量化信息引入到状态迁移模型中,比如:概率、多值、时间和可能性等.为了解决具有模糊性系统的验证问题,李永明将可能性测度和模型检测相结合,提出了基于可能性测度的模型检测理论.为了处理更一般的不确定性问题,李永明将可能性测度拓展为广义可能性测度,并结合模型检测,提出了基于广义可能性测度的模型检测理论.由于研究逻辑公式间的表达能力对拓广模型检测的适用范围具有重要意义,但目前对广义可能性计算树逻辑的表达能力还尚未研究全面.本文是在前面工作的基础上,以有限的广义可能性Kripke结构为模型,研究广义可能性计算树逻辑与计算树逻辑表达能力的关系,并以有限的强广义可能性Kripke结构为模型,研究广义可能性计算树逻辑与可能性计算树逻辑表达能力的关系.本文主要工作如下:1.定义了区间广义可能性计算树逻辑的语构和语义.2.以有限的广义可能性Kripke结构为模型,给出区间广义可能性计算树逻辑公式和计算树逻辑公式等价关系的定义,通过归纳法和反证法得出:计算树逻辑是区间广义可能性计算树逻辑的一个真子类,然后得出计算树逻辑公式转化为区间广义可能性计算树逻辑公式的算法.3.定义了强广义可能性Kripke结构,并以有限的强广义可能性Kripke结构为模型,给出区间广义可能性计算树逻辑公式和可能性计算树逻辑公式等价关系的定义,通过归纳法和反证法得出:可能性计算树逻辑是区间广义可能性计算树逻辑的一个真子类,然后得出可能性计算树逻辑公式转化为区间广义可能性计算树逻辑公式的算法.4.对前面等价关系的定义进行拓展,给出相应公式间等价关系的另一种定义.