武 鹏，吴尽昭，2，3，4*

（1.北京交通大学计算机与信息技术学院，北京 100044；2.中国科学院成都计算机应用研究所，成都 610041；3.广西大学计算机与电子信息学院，南宁 530004；4.广西民族大学人工智能学院，南宁 530006）

0 引言

形式化验证属于形式化方法的范畴，形式化验证主要包含两种方法，模型检验和定理证明。模型检测是由Clarke和Emerson提出的，主要通过搜索系统状态空间来验证系统的正确性的一种方法［1］。而定理证明主要解决如何利用逻辑和数学推理证明的手段验证软件的关键性质。这两种方法优势互补，在学术界［2-3］、工业界［4］得到了广泛应用。定理证明中的推理方法是演绎推理范畴，其中语法、语义、推理规则涉及其中，许多学者在这一领域有广泛的深入研究［5-6］。标签变迁系统或其相似结构广泛应用在模型检验和定理证明相关的验证领域，它是刻画系统的变迁行为的常用技术手段［7］。其中，系统各个状态及变迁条件通过相应逻辑赋值及其满足的条件来刻画。然而，二值或多值逻辑在描述复杂系统的状态并不完全有效［8］。实多项式代数变迁系统将二值逻辑和多值逻辑的状态空间扩展到Rn域，这在描述复杂系统行为和验证复杂系统安全性质上更有效［9］。近年来，在混成系统的验证领域，微分多项式代数和不变量理论［10-11］相继被提出，这进一步地拓宽了基于定理证明的推理方法的应用领域。

另一方面，在复杂系统中，系统参数有时并不是精确确定的，大多数情况下只知道这些参数的取值范围，这增加了这些系统的推理验证工作的难度。……